CounterexampleRefiner Class Reference

Refines a counterexample using local optimizations. More...

#include </home/soonhokong/work/dreal4/dreal/contractor/counterexample_refiner.h>

Public Member Functions
	CounterexampleRefiner (const Formula &query, Variables forall_variables, const Config &config)
	Constructs CounterexampleRefiner. More...
Box	Refine (Box box)
	Refines an initial solution and returns an improved one if possible.

Detailed Description

Refines a counterexample using local optimizations.

This is used to refine counterexamples found by the forall contractor (in contractor_forall.h).

Constructor & Destructor Documentation

CounterexampleRefiner()

CounterexampleRefiner	(	const Formula &	query,
		Variables	forall_variables,
		const Config &	config
	)

Constructs CounterexampleRefiner.

Parameters

query	Counterexample query. It should be either a relational formula or a conjunction of relational formulas.
forall_variables	universally quantified variables. They are decision variables that we consider in the local optimization.
config	Configuration to use for finding counterexamples.

Precondition

query is a conjunction.

---

The documentation for this class was generated from the following files:

• /home/soonhokong/work/dreal4/dreal/contractor/counterexample_refiner.h
• /home/soonhokong/work/dreal4/dreal/contractor/counterexample_refiner.cc