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

#include </home/soonhokong/work/dreal4/dreal/solver/context.h>

Classes
class	Impl

Public Member Functions
	Context ()
	Constructs a context with an empty configuration.

	Context (const Context &context)=delete
	Deleted copy constructor.

	Context (Context &&context) noexcept
	Move constructor.

	~Context ()
	Destructor (Defaulted in .cc file. Needed here for compilation).

Context &	operator= (const Context &)=delete
	Deleted copy-assign.

Context &	operator= (Context &&)=delete
	Deleted move-assign.

	Context (const Config &config)
	Constructs a context with `config`.

void	Assert (const Formula &f)
	Asserts a formula `f`.

optional< Box >	CheckSat ()
	Checks the satisfiability of the asserted formulas.

void	DeclareVariable (const Variable &v, bool is_model_variable=true)
	Declare a variable `v`. More...

void	DeclareVariable (const Variable &v, const Expression &lb, const Expression &ub, bool is_model_variable=true)
	Declare a variable `v` which is bounded by an interval `[lb, ub]`. More...

void	Minimize (const Expression &f)
	Asserts a formula minimizing a cost function `f`.

void	Minimize (const std::vector< Expression > &functions)
	Asserts a formula encoding Pareto optimality with a given set of objective functions. More...

void	Maximize (const Expression &f)
	Asserts a formula maximizing a cost function `f`.

void	Pop (int n)
	Pops `n` stacks.

void	Push (int n)
	Pushes `n` stacks.

void	SetInfo (const std::string &key, double val)
	Sets an info `key` with a value `val`.

void	SetInfo (const std::string &key, const std::string &val)
	Sets an info `key` with a value `val`.

void	SetInterval (const Variable &v, double lb, double ub)
	Sets the interval of `v` in the current box (top one in boxes_).

void	SetLogic (const Logic &logic)
	Sets the current logic to be `logic`.

void	SetOption (const std::string &key, double val)
	Sets an option `key` with a value `val`.

void	SetOption (const std::string &key, const std::string &val)
	Sets an option `key` with a value `val`.

optional< std::string >	GetOption (const std::string &key) const
	Gets the associated value for `key`.

const Config &	config () const
	Returns a const reference of configuration.

Config &	mutable_config ()
	Returns a mutable reference of configuration.

const ScopedVector< Formula > &	assertions () const
	Returns the const reference to the asserted formulas. More...

const Box &	box () const
	Returns the const reference to the top box.

const Box &	get_model () const
	Returns a representation of a model computed by the solver in response to an invocation of the check-sat. More...

Static Public Member Functions
static void	Exit ()
	Closes the context.

static std::string	version ()
	Returns the version string.

Detailed Description

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

Note: The implementation details are in context_impl.h file.

Member Function Documentation

◆ assertions()

const ScopedVector< Formula > & assertions ( ) const

Returns the const reference to the asserted formulas.

Note: that the returned vector can be a proper subset of the asserted formulas. For example, when x <= 5 is asserted, box() is updated to have this information (x <= 5) and this formula is thrown away.

◆ DeclareVariable() [1/2]

void DeclareVariable	(	const Variable &	v,
		bool	is_model_variable = `true`
	)

Declare a variable v.

By default v is considered as a model variable. If is_model_variable is false, it is declared as a non-model variable and will not appear in the model.

◆ DeclareVariable() [2/2]

void DeclareVariable	(	const Variable &	v,
		const Expression &	lb,
		const Expression &	ub,
		bool	is_model_variable = `true`
	)

Declare a variable v which is bounded by an interval [lb, ub].

By default v is considered as a model variable. If is_model_variable is false, it is declared as a non-model variable and will not appear in the model.

◆ get_model()

const Box & get_model ( ) const

Returns a representation of a model computed by the solver in response to an invocation of the check-sat.

◆ Minimize()

void Minimize ( const std::vector< Expression > & functions )

Asserts a formula encoding Pareto optimality with a given set of objective functions.

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

/home/soonhokong/work/dreal4/dreal/solver/context.h
/home/soonhokong/work/dreal4/dreal/solver/context.cc

Classes

Public Member Functions