Sum type of symbolic::Expression and symbolic::Formula. More...

Classes
class	AssertCommand
	"assert" command. More...

class	Box
	Represents a n-dimensional interval vector. More...

class	CachedExpression
	Cached expression class. More...

class	CdsInit

class	CdsScopeGuard

class	CheckSatCommand
	"check-sat" command. More...

class	Command
	Command class in smt2lib. More...

class	CommandCell
	CommandCell class. More...

class	Config

class	Context
	Context class that holds a set of constraints and provide Assert/Push/Pop/CheckSat functionalities. More...

class	Contractor

class	ContractorCell
	Abstract base class of contractors. More...

class	ContractorFixpoint
	Fixpoint contractor: apply C₁, ..., Cₙ until it reaches a fixpoint (technically, until it satisfies a given termination condition). More...

class	ContractorForall
	Contractor for forall constraints. More...

class	ContractorForallMt

class	ContractorIbexFwdbwd
	Contractor class wrapping IBEX's forward/backward contractor. More...

class	ContractorIbexFwdbwdMt
	Multi-thread version of ContractorIbexFwdbwd contractor. More...

class	ContractorIbexPolytope

class	ContractorIbexPolytopeMt
	Multi-thread version of ContractorIbexFwdbwd contractor. More...

class	ContractorId

class	ContractorInteger

class	ContractorJoin
	Join contractor. More...

class	ContractorSeq
	Sequential contractor: Sequentially apply C₁, ..., Cₙ. More...

class	ContractorStatus
	Contractor status. More...

class	ContractorWorklistFixpoint
	Fixpoint contractor using the worklist algorithm: apply C₁, ..., Cₙ until it reaches a fixpoint or it satisfies a given termination condition. More...

class	CounterexampleRefiner
	Refines a counterexample using local optimizations. More...

class	DrDriver
	The DrDriver class brings together all components. More...

class	DrScanner
	DrScanner is a derived class to add some extra function to the scanner class. More...

class	EchoCommand
	"echo" command. More...

class	ExitCommand
	"exit" command. More...

struct	ExprCtrDeleter

class	ExpressionEvaluator

class	ForallFormulaEvaluator
	Evaluator for forall formulas. More...

class	FormulaEvaluationResult
	Represents the evaluation result of a constraint given a box. More...

class	FormulaEvaluator
	Class to evaluate a symbolic formula with a box. More...

class	FormulaEvaluatorCell
	Base type for evaluator cell types. More...

class	FunctionDefinition

class	GenericContractorGenerator
	Converts an arbitrary formula into a contractor. More...

class	GetAssertionsCommand
	"get-assertions" command. More...

class	GetAssignmentCommand
	"get-assignments" command. More...

class	GetInfoCommand
	"get-info" command. More...

class	GetModelCommand
	"get-model" command. More...

class	GetOptionCommand
	"get-option" command. More...

class	GetProofCommand
	"get-proof" command. More...

class	GetUnsatAssumptionsCommand
	"get-unsat-assumptions" command. More...

class	GetUnsatCoreCommand
	"get-unsat-core" command. More...

class	IbexConverter
	Visitor class which converts a symbolic Formula into ibex::ExprCtr. More...

class	Icp
	Abstract Class for ICP (Interval Constraint Propagation) algorithm. More...

class	IcpParallel
	Class for Parallel ICP (Interval Constraint Propagation) algorithm. More...

class	IcpSeq
	Class for ICP (Interval Constraint Propagation) algorithm. More...

class	IcpStat
	A class to show statistics information at destruction. More...

class	IfThenElseEliminator
	Eliminates If-Then-Else expressions by introducing new variables. More...

class	MainProgram
	dReal's main program. More...

class	NaiveCnfizer
	Transforms a symbolic formula `f` into a CNF formula by preserving its semantics. More...

class	NloptOptimizer
	Wrapper class for nlopt. More...

class	Nnfizer
	A class implementing NNF (Negation Normal Form) conversion. More...

class	OptionValue
	Represents an optional value in dReal. More...

class	PopCommand
	"pop" command. More...

class	PrecisionGuard
	Sets the decimal precision to be used to format floating-point values on output operations. More...

class	PredicateAbstractor

class	PrefixPrinter
	Class to print expressions and formulas in prefix-form. More...

class	Profiler

class	PushCommand
	"push" command. More...

class	RelationalFormulaEvaluator
	Evaluator for relational formulas. More...

class	ResetAssertionsCommand
	"reset-assertions" command. More...

class	ResetCommand
	"reset" command. More...

class	RoundingModeGuard

class	SatSolver

class	ScopedUnorderedMap
	Backtrackable map. More...

class	ScopedUnorderedSet
	Backtrackable set. More...

class	ScopedVector

class	SetInfoCommand
	"set-info" command. More...

class	SetLogicCommand

class	SetOptionCommand

class	SignalHandlerGuard
	Sets a new signal handler and restores the old one when it goes out of scope. More...

class	Smt2Driver
	The Smt2Driver class brings together all components. More...

class	Smt2Scanner
	Smt2Scanner is a derived class to add some extra function to the scanner class. More...

class	Stat
	Base class for statistics. More...

class	Term

class	TheorySolver
	Theory solver for nonlinear theory over the Reals. More...

class	Timer
	Simple timer class to profile performance. More...

class	TimerGuard
	Pauses the passed timer object when the guard object is destructed (e.g. More...

class	TseitinCnfizer
	Transforms a symbolic formula `f` into an equi-satisfiable CNF formula by introducing extra Boolean variables (Tseitin transformation). More...

Typedefs
using	TerminationCondition = std::function< bool(Box::IntervalVector const &, Box::IntervalVector const &)>

using	gc_type = cds::gc::HP

template<typename T >
using	Stack = cds::container::TreiberStack< gc_type, T >

template<typename T , typename Comparator >
using	PriorityQueue = cds::container::MSPriorityQueue< T, typename cds::container::mspriority_queue::make_traits< cds::opt::buffer< cds::opt::v::initialized_dynamic_buffer< char > >, cds::opt::compare< Comparator > >::type >

using	DynamicBitset = dynamic_bitset< size_t >

template<typename T >
using	optional = tl::optional< T >

Enumerations
enum	Logic { ALL, QF_NRA, QF_NRA_ODE, QF_LRA, QF_RDL }

enum	Sort { Binary, Bool, Int, Real }

enum	FilterAssertionResult { NotFiltered, FilteredWithChange, FilteredWithoutChange }

enum	RelationalOperator { EQ, NEQ, GT, GEQ, LT, LEQ }
	Represents relational operators. More...

Functions
optional< Box >	CheckSatisfiability (const Formula &f, double delta)
	Checks the satisfiability of a given formula `f` with a given precision `delta`. More...

optional< Box >	CheckSatisfiability (const Formula &f, Config config)
	Checks the satisfiability of a given formula `f` with a given configuration `config`. More...

bool	CheckSatisfiability (const Formula &f, double delta, Box *box)
	Checks the satisfiability of a given formula `f` with a given precision `delta`. More...

bool	CheckSatisfiability (const Formula &f, Config config, Box *box)
	Checks the satisfiability of a given formula `f` with a given configuration `config`. More...

optional< Box >	Minimize (const Expression &objective, const Formula &constraint, double delta)
	Finds a solution to minimize `objective` function while satisfying a given `constraint` using `delta`. More...

optional< Box >	Minimize (const Expression &objective, const Formula &constraint, Config config)
	Finds a solution to minimize `objective` function while satisfying a given `constraint` using `delta`. More...

bool	Minimize (const Expression &objective, const Formula &constraint, double delta, Box *box)
	Finds a solution to minimize `objective` function while satisfying a given `constraint` using `delta`. More...

bool	Minimize (const Expression &objective, const Formula &constraint, Config config, Box *box)
	Finds a solution to minimize `objective` function while satisfying a given `constraint` using `delta`. More...

Contractor	make_contractor_id (const Config &config)
	Returns an idempotent contractor. More...

Contractor	make_contractor_integer (const Box &box, const Config &config)
	Returns an integer contractor. More...

Contractor	make_contractor_seq (const std::vector< Contractor > &contractors, const Config &config)
	Returns a sequential contractor `C` from a vector of contractors `vec` = [C₁, ..., Cₙ]. More...

Contractor	make_contractor_ibex_fwdbwd (Formula f, const Box &box, const Config &config)
	Returns a contractor wrapping IBEX's forward/backward contractor. More...

Contractor	make_contractor_ibex_polytope (std::vector< Formula > formulas, const Box &box, const Config &config)
	Returns a contractor wrapping IBEX's polytope contractor. More...

Contractor	make_contractor_fixpoint (TerminationCondition term_cond, const std::vector< Contractor > &contractors, const Config &config)
	Returns a fixed-point contractor. More...

Contractor	make_contractor_worklist_fixpoint (TerminationCondition term_cond, const std::vector< Contractor > &contractors, const Config &config)
	Returns a worklist fixed-point contractor. More...

Contractor	make_contractor_join (std::vector< Contractor > vec, const Config &config)
	Returns a join contractor. More...

ostream &	operator<< (ostream &os, const Contractor &ctc)

bool	is_id (const Contractor &contractor)
	Returns true if `contractor` is idempotent contractor.

bool	is_integer (const Contractor &contractor)
	Returns true if `contractor` is integer contractor.

bool	is_seq (const Contractor &contractor)
	Returns true if `contractor` is sequential contractor.

bool	is_ibex_fwdbwd (const Contractor &contractor)
	Returns true if `contractor` is IBEX fwdbwd contractor.

bool	is_ibex_polytope (const Contractor &contractor)
	Returns true if `contractor` is IBEX polytope contractor.

bool	is_fixpoint (const Contractor &contractor)
	Returns true if `contractor` is fixpoint contractor.

bool	is_worklist_fixpoint (const Contractor &contractor)
	Returns true if `contractor` is worklist-fixpoint contractor.

bool	is_forall (const Contractor &contractor)
	Returns true if `contractor` is forall contractor.

bool	is_join (const Contractor &contractor)
	Returns true if `contractor` is join contractor.

template<typename ContextType >
Contractor	make_contractor_forall (Formula f, const Box &box, double epsilon, double inner_delta, const Config &config)
	Returns a forall contractor. More...

DynamicBitset::size_type	ComputeInputSize (const vector< Contractor > &contractors)

ostream &	operator<< (ostream &os, const ContractorCell &c)

shared_ptr< ContractorId >	to_id (const Contractor &contractor)
	Converts `contractor` to ContractorId.

shared_ptr< ContractorInteger >	to_integer (const Contractor &contractor)
	Converts `contractor` to ContractorInteger.

shared_ptr< ContractorSeq >	to_seq (const Contractor &contractor)
	Converts `contractor` to ContractorSeq.

shared_ptr< ContractorIbexFwdbwd >	to_ibex_fwdbwd (const Contractor &contractor)
	Converts `contractor` to ContractorIbexFwdbwd.

shared_ptr< ContractorIbexPolytope >	to_ibex_polytope (const Contractor &contractor)
	Converts `contractor` to ContractorIbexPolytop.

shared_ptr< ContractorFixpoint >	to_fixpoint (const Contractor &contractor)
	Converts `contractor` to ContractorFixpoint.

shared_ptr< ContractorWorklistFixpoint >	to_worklist_fixpoint (const Contractor &contractor)
	Converts `contractor` to ContractorWorklistFixpoint.

shared_ptr< ContractorJoin >	to_join (const Contractor &contractor)
	Converts `contractor` to ContractorJoin.

template<typename ContextType >
std::shared_ptr< ContractorForall< ContextType > >	to_forall (const Contractor &contractor)
	Converts `contractor` to ContractorForall.

Box	RefineCounterexample (const Formula &query, const Variables &quantified_variables, Box b, double precision)
	Add Doc.

set< Formula >	GenerateExplanation (const Variables &unsat_witness, const set< Formula > &used_constraints)

ContractorStatus	Join (ContractorStatus contractor_status1, const ContractorStatus &contractor_status2)
	Returns a join of `contractor_status1` and `contractor_status2`. More...

void	RunDr (const string &filename, const Config &config, const bool debug_scanning, const bool debug_parsing)

	PYBIND11_MODULE (_dreal_py, m)

optional< Box >	CheckLyapunov (const vector< Variable > &x, const vector< Expression > &f, const Expression &V, const double ball_lb, const double ball_ub, Config config)

optional< Box >	CheckLyapunov (const vector< Variable > &x, const Variable &t, const vector< Expression > &f, const Expression &V, const double ball_lb, const double ball_ub, const double t_lb, const double t_ub, Config config)

optional< Box >	SynthesizeLyapunov (const std::vector< Variable > &x, const std::vector< Expression > &f, const Expression &V, double ball_lb, double ball_ub, double c_lb, double c_ub, Config config)
	Given a partially specified candidate function `V`, synthesizes a Lyapunov function of a dynamic system `xᵢ = fᵢ(x)` within a ball bounded by `ball_lb` and `ball_ub`. More...

optional< Box >	SynthesizeLyapunov (const std::vector< Variable > &x, const Variable &t, const std::vector< Expression > &f, const Expression &V, double ball_lb, double ball_ub, double c_lb, double c_ub, double t_lb, double t_ub, Config config)
	Given a partially specified candidate function `V`, synthesizes a Lyapunov function of a time-varying dynamic system `xᵢ = fᵢ(x, t)` within a ball bounded by `ball_lb` and `ball_ub`. More...

void	synthesize_abs ()

	PYBIND11_MODULE (_odr_test_module_py, m)

ostream &	operator<< (ostream &os, const CachedExpression &expression)

ostream &	operator<< (ostream &os, const Command &c)

Command	assert_command (const Formula &f)

Command	check_sat_command ()

Command	exit_command ()

Command	set_info_command (const string &key, const string &val)

Command	set_logic_command (Logic logic)

Command	set_option_command (const string &key, const string &val)

Command	push_command (int level)

Command	pop_command (int level)

Command	reset_command ()

Logic	parse_logic (const string &s)

ostream &	operator<< (ostream &os, const Logic &logic)

void	RunSmt2 (const string &filename, const Config &config, const bool debug_scanning, const bool debug_parsing)

Sort	ParseSort (const string &s)

ostream &	operator<< (ostream &os, const Sort &sort)

Variable::Type	SortToType (Sort sort)

ostream &	operator<< (ostream &os, const Term &t)

pair< double, int >	FindMaxDiam (const Box &box, const DynamicBitset &active_set)
	Finds the dimension with the maximum diameter in a `box`. More...

int	BranchLargestFirst (const Box &box, const DynamicBitset &active_set, Box left, Box right)
	Finds the largest dimension in `active_set` and partitions `box` into two sub-boxes by branching on the chosen dimension. More...

std::ostream &	operator<< (std::ostream &os, const Config::SatDefaultPhase &sat_default_phase)

ostream &	operator<< (ostream &os, const Config &config)

std::ostream &	operator<< (std::ostream &os, const ExpressionEvaluator &expression_evaluator)

FilterAssertionResult	FilterAssertion (const Formula &assertion, Box *box)
	If the `assertion` can be applied into the `box` update `box` and return true. More...

ostream &	operator<< (ostream &os, FormulaEvaluationResult::Type type)

ostream &	operator<< (ostream &os, const FormulaEvaluationResult &result)

ostream &	operator<< (ostream &os, const FormulaEvaluator &evaluator)

FormulaEvaluator	make_relational_formula_evaluator (const Formula &f)
	Creates FormulaEvaluator for a relational formula `f` using `variables`.

FormulaEvaluator	make_forall_formula_evaluator (const Formula &f, double epsilon, double delta, int number_of_jobs)
	Creates FormulaEvaluator for a universally quantified formula `f` using `variables`, `epsilon`, `delta`, and `number_of_jobs`. More...

optional< DynamicBitset >	EvaluateBox (const std::vector< FormulaEvaluator > &formula_evaluators, const Box &box, double precision, ContractorStatus *cs)
	Evaluates each formula with `box` using interval arithmetic. More...

string	ToPrefix (const Expression &e)
	Returns the prefix-string representation of the expression `e`.

string	ToPrefix (const Formula &f)
	Returns the prefix-string representation of the formula `e`.

Formula	imply (const Formula &f1, const Formula &f2)
	Returns a formula `f1` ⇒ `f2`.

Formula	imply (const Variable &v, const Formula &f)
	Returns a formula `v` ⇒ `f`.

Formula	imply (const Formula &f, const Variable &v)
	Returns a formula `f` ⇒ `v`.

Formula	imply (const Variable &v1, const Variable &v2)
	Returns a formula `v1` ⇒ `v2`.

Formula	iff (const Formula &f1, const Formula &f2)
	Returns a formula `f1` ⇔ `f2`.

Formula	iff (const Variable &v, const Formula &f)
	Returns a formula `v` ⇔ `f`.

Formula	iff (const Formula &f, const Variable &v)
	Returns a formula `f` ⇔ `v`.

Formula	iff (const Variable &v1, const Variable &v2)
	Returns a formula `v1` ⇔ `v2`.

set< Formula >	map (const set< Formula > &formulas, const function< Formula(const Formula &)> &func)

bool	is_atomic (const Formula &f)
	Checks if `f` is atomic.

bool	is_clause (const Formula &f)
	Checks if `f` is a clause.

set< Formula >	get_clauses (const Formula &f)
	Returns the set of clauses in f. More...

bool	is_cnf (const Formula &f)
	Checks if `is` in CNF form.

bool	HaveIntersection (const Variables &variables1, const Variables &variables2)

Formula	DeltaStrengthen (const Formula &f, const double delta)
	Strengthen the input formula $p f by `delta`. More...

Formula	DeltaWeaken (const Formula &f, const double delta)
	Weaken the input formula $p f by `delta`. More...

bool	IsDifferentiable (const Formula &f)
	Returns true if the formula `f` is symbolic-differentiable.

bool	IsDifferentiable (const Expression &e)
	Returns true if the expression f is symbolic-differentiable.

Formula	make_conjunction (const std::vector< Formula > &formulas)
	Make conjunction of `formulas`. More...

Formula	make_disjunction (const vector< Formula > &formulas)

vector< Variable >	CreateVector (const std::string &prefix, int size, Variable::Type type=Variable::Type::CONTINUOUS)
	Creates a vector of variables of `type` whose size is `size`. More...

RelationalOperator	operator! (RelationalOperator op)
	Negates `op`.

ostream &	operator<< (std::ostream &os, RelationalOperator op)
	Outputs `op` to `os`.

std::set< Formula >	map (const std::set< Formula > &formulas, const std::function< Formula(const Formula &)> &func)

template<typename... Args>
void	unused (const Args &...)

ostream &	operator<< (ostream &os, const Box &box)

bool	operator== (const Box &b1, const Box &b2)

bool	operator!= (const Box &b1, const Box &b2)

ostream &	DisplayDiff (ostream &os, const vector< Variable > &variables, const Box::IntervalVector &old_iv, const Box::IntervalVector &new_iv)

bool	file_exists (const std::string &name)
	Returns true if a filename `name` exists.

string	get_extension (const std::string &name)
	Extracts the extension from `name`. More...

Box::Interval	BloatPoint (double c)
	Expands a point value `c` into an interval `[prev_c, next_c]` where `prev_c` is the largest machine-representable floating-point number which is smaller than c and `next_c` is the smallest machine-representable floating-point number which is larger than c. More...

shared_ptr< spdlog::logger >	CreateLogger (const string &logger_name)

spdlog::logger *	log ()
	Provide a global logger. More...

bool	is_integer (double v)
	Returns true if `v` is represented by `int`.

int	convert_int64_to_int (const int64_t v)

double	convert_int64_to_double (const int64_t v)

int	convert_int64_to_int (std::int64_t v)
	Converts `v` of int64_t to int. More...

double	convert_int64_to_double (std::int64_t v)
	Converts `v` of int64_t to double. More...

Box::Interval	StringToInterval (const std::string &s)
	Convert a string `s` into an interval `[lb, ub]` where `lb` is a parsed result of `s` with FE_DOWNWARD round-mode and `ub` is a parsed result of `s` with FE_UPWARD round-mode. More...

ostream &	operator<< (ostream &os, const Timer &timer)

Variables
volatile std::atomic_bool	g_interrupted {false}
	Flag to indicate an interrupt (SIGINT) is received.

constexpr auto	nullopt = tl::nullopt

Detailed Description

Sum type of symbolic::Expression and symbolic::Formula.

Enumeration Type Documentation

◆ RelationalOperator

enum RelationalOperator

strong

Represents relational operators.

Enumerator
EQ	=
NEQ	!=
GT	>
GEQ	>=
LT	<
LEQ	<=

Function Documentation

◆ BloatPoint()

Box::Interval BloatPoint ( double c )

Expands a point value c into an interval [prev_c, next_c] where prev_c is the largest machine-representable floating-point number which is smaller than c and next_c is the smallest machine-representable floating-point number which is larger than c.

Note: When c is +∞ (resp. -∞), this function returns DBL_MAX, +∞.

◆ BranchLargestFirst()

int BranchLargestFirst	(	const Box &	box,
		const DynamicBitset &	active_set,
		Box *	left,
		Box *	right
	)

Finds the largest dimension in active_set and partitions box into two sub-boxes by branching on the chosen dimension.

It traverses only the variables enabled by active_set, to find a branching dimension.

Parameters

[in]	box	The box to branch.
[in]	active_set	A subset of dimensions of the input box that is active in the given constraints.
[out]	left	The left sub-box.
[out]	right	The right sub-box.

Returns: the branching dimension if found, otherwise returns -1.

◆ CheckSatisfiability() [1/4]

optional< Box > CheckSatisfiability	(	const Formula &	f,
		double	delta
	)

Checks the satisfiability of a given formula f with a given precision delta.

Returns: a model, a mapping from a variable to an interval, if f is δ-satisfiable.; a nullopt, if is unsatisfiable.

◆ CheckSatisfiability() [2/4]

optional< Box > CheckSatisfiability	(	const Formula &	f,
		Config	config
	)

Checks the satisfiability of a given formula f with a given configuration config.

◆ CheckSatisfiability() [3/4]

bool CheckSatisfiability	(	const Formula &	f,
		double	delta,
		Box *	box
	)

Checks the satisfiability of a given formula f with a given precision delta.

Returns: true if it finds a model which will be saved in box.; false if it concludes unsat.

Note: We provide this version of API to avoid the use of optional.

◆ CheckSatisfiability() [4/4]

bool CheckSatisfiability	(	const Formula &	f,
		Config	config,
		Box *	box
	)

Checks the satisfiability of a given formula f with a given configuration config.

◆ convert_int64_to_double()

double dreal::convert_int64_to_double ( std::int64_t v )

Converts v of int64_t to double.

Exceptions

std::runtime_error if this conversion result in a loss of precision.

◆ convert_int64_to_int()

int dreal::convert_int64_to_int ( std::int64_t v )

Converts v of int64_t to int.

Exceptions

std::runtime_error if this conversion result in a loss of precision.

◆ CreateVector()

std::vector< Variable > CreateVector	(	const std::string &	prefix,
		int	size,
		Variable::Type	type = `Variable::Type::CONTINUOUS`
	)

Creates a vector of variables of type whose size is size.

The variables are numbered with prefix. For example, CreateVector("x", 5) returns [x0, x1, x2, x3, x4].

Precondition: prefix must not be an empty string.; size >= 1.

◆ DeltaStrengthen()

Formula DeltaStrengthen	(	const Formula &	f,
		double	delta
	)

Strengthen the input formula $p f by delta.

Strengthen the input formula f by delta.

Precondition: delta > 0

◆ DeltaWeaken()

Formula DeltaWeaken	(	const Formula &	f,
		double	delta
	)

Weaken the input formula $p f by delta.

Weaken the input formula f by delta.

Precondition: delta > 0

◆ EvaluateBox()

optional< DynamicBitset > EvaluateBox	(	const std::vector< FormulaEvaluator > &	formula_evaluators,
		const Box &	box,
		double	precision,
		ContractorStatus *	cs
	)

Evaluates each formula with box using interval arithmetic.

There are three possible outcomes:

Returns None if there is fᵢ such that fᵢ(box) is empty. (This indicates the problem is UNSAT)

Returns Some(∅) if for all fᵢ, we have either 1) fᵢ(x) is valid for all x ∈ B or 2) |fᵢ(B)| ≤ δ. (This indicates the problem is delta-SAT)

Returns Some(Vars) if there is fᵢ such that 1) Interval arithmetic can't validate that fᵢ(x) is valid for all x ∈ B and 2) |fᵢ(B)| > δ. Vars = {v | v ∈ fᵢ ∧ |fᵢ(B)| > δ for all fᵢs}.

It cannot conclude if the constraint is satisfied or not completely. It checks the width/diameter of the interval evaluation and adds the free variables in the constraint into the set that it will return.

If it returns an DynamicBitset, it represents the dimensions on which the ICP algorithm needs to consider branching.

It sets cs's box empty if it detects UNSAT. It also calls cs->AddUsedConstraint to store the constraint that is responsible for the UNSAT.

◆ FilterAssertion()

FilterAssertionResult FilterAssertion	(	const Formula &	assertion,
		Box *	box
	)

If the assertion can be applied into the box update box and return true.

Otherwise, return false while keeping box intact.

◆ FindMaxDiam()

std::pair< double, int > FindMaxDiam	(	const Box &	box,
		const DynamicBitset &	active_set
	)

Finds the dimension with the maximum diameter in a box.

It only consider the dimensions enabled in active_set.

Returns: a pair of (max dimension, variable index).

◆ get_clauses()

std::set< Formula > get_clauses ( const Formula & f )

Returns the set of clauses in f.

Precondition: f is in CNF. That is, f is either a single clause or a conjunction of clauses.

◆ get_extension()

std::string get_extension ( const std::string & name )

Extracts the extension from name.

Note: It returns an empty string if there is no extension in name.

◆ HaveIntersection()

bool HaveIntersection	(	const Variables &	variables1,
		const Variables &	variables2
	)

Returns: true if variables1 and variables2 is an non-empty intersection.

◆ Join()

ContractorStatus Join	(	ContractorStatus	contractor_status1,
		const ContractorStatus &	contractor_status2
	)

Returns a join of contractor_status1 and contractor_status2.

Precondition: The boxes of the two ContractorStatus should have the same variables vector.

◆ log()

spdlog::logger * log ( )

Provide a global logger.

See the following usage:

DREAL_LOG_TRACE("message with param {0}, {1}", arg1, arg2);
DREAL_LOG_DEBUG("message with param {0}, {1}", arg1, arg2);
DREAL_LOG_INFO("Support for int: {0:d}; hex: {0:x};", 42, 32);
DREAL_LOG_WARN("Support for floats {:03.2f}", 1.23456);
DREAL_LOG_ERROR("Positional args are {1} {0}..", "too", "supported");
DREAL_LOG_CRITICAL("{:<30}", "left aligned");

Please check https://github.com/gabime/spdlog for more information.

◆ make_conjunction()

Formula make_conjunction ( const std::vector< Formula > & formulas )

Make conjunction of formulas.

Note: This is different from the one in Drake's symbolic library. It takes std::vector<Formula> while Drake's version takes std::set<Formula>.

◆ make_contractor_fixpoint()

Contractor make_contractor_fixpoint	(	TerminationCondition	term_cond,
		const std::vector< Contractor > &	contractors,
		const Config &	config
	)

Returns a fixed-point contractor.

The returned contractor applies the contractors in vec sequentially until term_cond is met.

See also: ContractorFixpoint.

◆ make_contractor_forall()

Contractor make_contractor_forall	(	Formula	f,
		const Box &	box,
		double	epsilon,
		double	inner_delta,
		const Config &	config
	)

Returns a forall contractor.

Note: the implementation is at dreal/contractor/contractor_forall.h file.

See also: ContractorForall.

◆ make_contractor_ibex_fwdbwd()

Contractor make_contractor_ibex_fwdbwd	(	Formula	f,
		const Box &	box,
		const Config &	config
	)

Returns a contractor wrapping IBEX's forward/backward contractor.

If the number of jobs (in config) > 1, it creates a multi-threaded version of the contractor, which is based on ContractorIbexFwdbwdMt. Otherwise, it creates an instance of ContractorIbexFwdbwd.

See also: ContractorIbexFwdbwd.; ContractorIbexFwdbwdMt.

◆ make_contractor_ibex_polytope()

Contractor make_contractor_ibex_polytope	(	std::vector< Formula >	formulas,
		const Box &	box,
		const Config &	config
	)

Returns a contractor wrapping IBEX's polytope contractor.

If then number of jobs (in config) > 1, it creates a multi-threaded version of the contractor, which is based on ContractorIbexPolytopeMt. Otherwise, it creates an instance of ContractorIbexPolytope.

See also: ContractorIbexPolytope.; ContractorIbexPolytopeMt.

◆ make_contractor_id()

Contractor make_contractor_id ( const Config & config )

Returns an idempotent contractor.

See also: ContractorId.

◆ make_contractor_integer()

Contractor make_contractor_integer	(	const Box &	box,
		const Config &	config
	)

Returns an integer contractor.

For an integer variable v, it prunes b[v] = [lb, ub] into [ceil(lb), floor(ub)]. It sets the box empty if it detects an empty interval in pruning.

See also: ContractorInteger.

◆ make_contractor_join()

Contractor make_contractor_join	(	std::vector< Contractor >	vec,
		const Config &	config
	)

Returns a join contractor.

The returned contractor does the following operation:

    (C₁ ∨ ... ∨ Cₙ)(box) = C₁(box) ∨ ... ∨ Cₙ(box).

See also: ContractorJoin.

◆ make_contractor_seq()

Contractor make_contractor_seq	(	const std::vector< Contractor > &	contractors,
		const Config &	config
	)

Returns a sequential contractor C from a vector of contractors vec = [C₁, ..., Cₙ].

It applies Cᵢ sequentially. That is, we have:

    C(box) = (Cₙ∘...∘C₁)(box)

See also: ContractorSeq.

◆ make_contractor_worklist_fixpoint()

Contractor make_contractor_worklist_fixpoint	(	TerminationCondition	term_cond,
		const std::vector< Contractor > &	contractors,
		const Config &	config
	)

Returns a worklist fixed-point contractor.

The returned contractor applies the contractors in vec sequentially until term_cond is met.

See also: ContractorFixpoint.

◆ make_disjunction()

Formula make_disjunction ( const std::vector< Formula > & formulas )

Note: This is different from the one in Drake's symbolic library. It takes std::vector<Formula> while Drake's version takes std::set<Formula>.

◆ make_forall_formula_evaluator()

FormulaEvaluator make_forall_formula_evaluator	(	const Formula &	f,
		double	epsilon,
		double	delta,
		int	number_of_jobs
	)

Creates FormulaEvaluator for a universally quantified formula f using variables, epsilon, delta, and number_of_jobs.

◆ Minimize() [1/4]

optional< Box > Minimize	(	const Expression &	objective,
		const Formula &	constraint,
		double	delta
	)

Finds a solution to minimize objective function while satisfying a given constraint using delta.

Returns: a model, a mapping from a variable to an interval, if a solution exists.; nullopt, if there is no solution.

◆ Minimize() [2/4]

optional< Box > Minimize	(	const Expression &	objective,
		const Formula &	constraint,
		Config	config
	)

Finds a solution to minimize objective function while satisfying a given constraint using delta.

◆ Minimize() [3/4]

bool Minimize	(	const Expression &	objective,
		const Formula &	constraint,
		double	delta,
		Box *	box
	)

Finds a solution to minimize objective function while satisfying a given constraint using delta.

Returns: true if it finds a model which will be saved in box.; false if it concludes unsat.

Note: We provide this version of API to avoid the use of optional.

◆ Minimize() [4/4]

bool Minimize	(	const Expression &	objective,
		const Formula &	constraint,
		Config	config,
		Box *	box
	)

Finds a solution to minimize objective function while satisfying a given constraint using delta.

◆ StringToInterval()

Box::Interval StringToInterval ( const std::string & s )

Convert a string s into an interval [lb, ub] where lb is a parsed result of s with FE_DOWNWARD round-mode and ub is a parsed result of s with FE_UPWARD round-mode.

Exceptions

if	`s` does not represent a double number. (see std::stod)

Note: This function assumes that std::stod implementation honors the current round-mode. There are old versions of Visual C++ and GLIBC where this assumption does not hold. See http://www.exploringbinary.com/visual-c-plus-plus-and-glibc-strtod-ignore-rounding-mode for more information.

◆ SynthesizeLyapunov() [1/2]

optional< Box > SynthesizeLyapunov	(	const std::vector< Variable > &	x,
		const std::vector< Expression > &	f,
		const Expression &	V,
		double	ball_lb,
		double	ball_ub,
		double	c_lb,
		double	c_ub,
		Config	config
	)

Given a partially specified candidate function V, synthesizes a Lyapunov function of a dynamic system xᵢ = fᵢ(x) within a ball bounded by ball_lb and ball_ub.

The candidate function V(c, x) should satisfy the following conditions:

∃c.∀x. x ∈ ball → (V(c, x) ≥ 0 ∧ V̇(c, x) ≤ 0)
∃c. V(c, 0) = 0
∃c. c_lb ≤ c ≤ c_ub

◆ SynthesizeLyapunov() [2/2]

optional< Box > SynthesizeLyapunov	(	const std::vector< Variable > &	x,
		const Variable &	t,
		const std::vector< Expression > &	f,
		const Expression &	V,
		double	ball_lb,
		double	ball_ub,
		double	c_lb,
		double	c_ub,
		double	t_lb,
		double	t_ub,
		Config	config
	)

Given a partially specified candidate function V, synthesizes a Lyapunov function of a time-varying dynamic system xᵢ = fᵢ(x, t) within a ball bounded by ball_lb and ball_ub.

The candidate function V(c, x) should satisfy the following conditions:

∃c. ∀x,t. (x ∈ ball ∧ t ∈ [t_lb, t_ub]) → (V(c, x) ≥ 0 ∧ V̇(c, x) ≤ 0)
∃c. V(c, 0) = 0
∃c. c_lb ≤ c ≤ c_ub

Classes

Typedefs

Enumerations

Functions

Variables

Detailed Description

Enumeration Type Documentation

◆ RelationalOperator

Function Documentation

◆ BloatPoint()

◆ BranchLargestFirst()

◆ CheckSatisfiability() [1/4]

◆ CheckSatisfiability() [2/4]

◆ CheckSatisfiability() [3/4]

◆ CheckSatisfiability() [4/4]

◆ convert_int64_to_double()

◆ convert_int64_to_int()

◆ CreateVector()

◆ DeltaStrengthen()

◆ DeltaWeaken()

◆ EvaluateBox()

◆ FilterAssertion()

◆ FindMaxDiam()

◆ get_clauses()

◆ get_extension()

◆ HaveIntersection()

◆ Join()

◆ log()

◆ make_conjunction()

◆ make_contractor_fixpoint()

◆ make_contractor_forall()

◆ make_contractor_ibex_fwdbwd()

◆ make_contractor_ibex_polytope()

◆ make_contractor_id()

◆ make_contractor_integer()

◆ make_contractor_join()

◆ make_contractor_seq()

◆ make_contractor_worklist_fixpoint()

◆ make_disjunction()

◆ make_forall_formula_evaluator()

◆ Minimize() [1/4]

◆ Minimize() [2/4]

◆ Minimize() [3/4]

◆ Minimize() [4/4]

◆ StringToInterval()

◆ SynthesizeLyapunov() [1/2]

◆ SynthesizeLyapunov() [2/2]