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

#include <Context.h>

Classes
class	Impl
	The context juggles between the SAT solver and the theory solver, in order to produce a model. More...

Public Member Functions
	Context (Config &config, SmtSolverOutput *=nullptr)
	Construct a context with `config`.

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

void	AssertPiecewiseLinearFunction (const Variable &var, const Formula &cond, const Expression &active, const Expression &inactive)
	Assert a piecewise linear function with two possible branches.

SatResult	CheckSat (mpq_class *actual_precision)
	Check the satisfiability of the asserted formulas, and sets `actual_precision` to the actual max infeasibility where appropriate.

LpResult	CheckOpt (mpq_class obj_lo, mpq_class obj_up)
	Check the satisfiability of the asserted formulas, and (where possible) optimizes an objective function over them.

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

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] \).

void	Exit ()
	Exit the context.

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

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

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

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

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

std::string	GetInfo (const std::string &key) const
	Get the info `key`.

void	SetInterval (const Variable &v, const mpq_class &lb, const mpq_class &ub)
	Set the interval of `v` to \( [lb, ub] \) in the current box (top one in boxes_).

void	SetLogic (Logic logic)
	Set the current logic to `logic`.

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

std::string	GetOption (const std::string &key) const
	Get the option `key`.

const Config &	config () const
	Get read-only access to the configuration of the context.

const ScopedVector< Formula > &	assertions () const
	Get the the asserted formulas.

const Box &	box () const
	Get the current active box from the top of the stack of boxes.

const Box &	model () const
	Get a representation of a model computed by the solver in response to the last invocation of the check-sat.

bool	have_objective () const
	Check whether or not there is an objective function (which may be zero) to optimize.

const PredicateAbstractor &	predicate_abstractor () const
	Get read-only access to the predicate_abstractor of the context.

bool	is_max () const
	Check whether or not the objective function (if present) is a maximization.

bool	Verify (const Box &model) const
	Check whether the `model` satisfies all the assertions loaded in the context.

Private Attributes
std::unique_ptr< Impl >	impl_
	Pointer to the implementation of the context.

Detailed Description

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

Note: The implementation is hidden in the Context::Impl class.

Definition at line 31 of file Context.h.

Constructor & Destructor Documentation

◆ Context()

dlinear::Context::Context	(	Config &	config,
		SmtSolverOutput *	output = nullptr )

explicit

Construct a context with config.

If smt_solver_output is not null, it will be used to store the output of the SMT solver as well as some statistics.

Parameters

config the configuration of the context

Definition at line 22 of file Context.cpp.

Member Function Documentation

◆ Assert()

void dlinear::Context::Assert ( const Formula & f )

Assert a formula f.

The new formula is added to the box.

Parameters

f	the formula to be asserted

Definition at line 24 of file Context.cpp.

◆ assertions()

const ScopedVector< Formula > & dlinear::Context::assertions ( ) const

nodiscard

Get the 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 and the formula is thrown away.

Definition at line 71 of file Context.cpp.

◆ AssertPiecewiseLinearFunction()

void dlinear::Context::AssertPiecewiseLinearFunction	(	const Variable &	var,
		const Formula &	cond,
		const Expression &	active,
		const Expression &	inactive )

Assert a piecewise linear function with two possible branches.

Consider a piecewise linear function that assigns either active or inactive to var depending on cond

\[ \text{var} =\begin{cases} \text{active} & \text{if } cond \newline \text{inactive} & \text{otherwise} \end{cases} \]

Assigning \( \mathcal{A} = (\text{active} = \text{var}) \) and \( \mathcal{B} = (\text{var} = \text{inactive}) \), we introduce the following assertions:

\[ (\mathcal{A} \lor \neg cond) \land (\mathcal{B} \lor cond) \land (cond \lor \neg cond) \]

Note that the last clause is a tautology, but it forces the sat solver to assign a boolean value to cond and hopefully skip either \( \mathcal{A} \) or \( \mathcal{B} \).

Parameters

var	the variable to be assigned
cond	the condition to be checked
active	the value of the variable if the condition is true
inactive	the value of the variable if the condition is false

Definition at line 25 of file Context.cpp.

◆ box()

const Box & dlinear::Context::box ( ) const

nodiscard

Get the current active box from the top of the stack of boxes.

Returns: the active box of the context

Definition at line 66 of file Context.cpp.

◆ CheckOpt()

LpResult dlinear::Context::CheckOpt	(	mpq_class *	obj_lo,
		mpq_class *	obj_up )

Check the satisfiability of the asserted formulas, and (where possible) optimizes an objective function over them.

If a solution is found, the obj_lo and obj_up store the lower and upper bounds of the objective function.

Parameters

[out]	obj_lo	the lower bound of the objective function
[out]	obj_up	the upper bound of the objective function

Definition at line 30 of file Context.cpp.

◆ CheckSat()

SatResult dlinear::Context::CheckSat ( mpq_class * actual_precision )

Check the satisfiability of the asserted formulas, and sets actual_precision to the actual max infeasibility where appropriate.

Parameters

[out] actual_precision initialized with the desired precision, it will be set to the lowest possible precision below the given one that satisfies the constraints.

Returns: the satisfiability result.

Definition at line 29 of file Context.cpp.

◆ config()

const Config & dlinear::Context::config ( ) const

nodiscard

Get read-only access to the configuration of the context.

Returns: configuration of the context

Definition at line 65 of file Context.cpp.

◆ DeclareVariable() [1/2]

void dlinear::Context::DeclareVariable	(	const Variable &	v,
		bool	is_model_variable = true )

Declare a variable v.

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

Parameters

v	the variable to be declared
is_model_variable	whether or not the variable is a model variable

Definition at line 31 of file Context.cpp.

◆ DeclareVariable() [2/2]

void dlinear::Context::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.

Parameters

v	the variable to be declared
lb	the lower bound of the variable
ub	the upper bound of the variable
is_model_variable	whether or not the variable is a model variable

Definition at line 34 of file Context.cpp.

◆ Exit()

void dlinear::Context::Exit ( )

Exit the context.

Does nothing but prints a debug message.

Definition at line 42 of file Context.cpp.

◆ GetInfo()

std::string dlinear::Context::GetInfo ( const std::string & key ) const

nodiscard

Get the info key.

Parameters

key	the key of the info

Returns: value of the info

Definition at line 58 of file Context.cpp.

◆ GetOption()

std::string dlinear::Context::GetOption ( const std::string & key ) const

nodiscard

Get the option key.

Parameters

key	the key of the option

Returns: value of the option

Definition at line 64 of file Context.cpp.

◆ have_objective()

bool dlinear::Context::have_objective ( ) const

nodiscard

Check whether or not there is an objective function (which may be zero) to optimize.

Returns: true if there is an objective function to optimize. CheckOpt() will be called; false if there is no objective function. CheckSat() will be called

Definition at line 72 of file Context.cpp.

◆ is_max()

bool dlinear::Context::is_max ( ) const

nodiscard

Check whether or not the objective function (if present) is a maximization.

Returns: true if the original objective function is a maximization; false if the original objective function is a minimization

Definition at line 73 of file Context.cpp.

◆ Maximize()

void dlinear::Context::Maximize ( const Expression & f )

Assert a formula maximizing a cost function f.

Parameters

f	the cost function to be maximized

Definition at line 44 of file Context.cpp.

◆ Minimize()

void dlinear::Context::Minimize ( const Expression & f )

Assert a formula minimizing a cost function f.

Parameters

f	the cost function to be minimized

Definition at line 43 of file Context.cpp.

◆ model()

const Box & dlinear::Context::model ( ) const

nodiscard

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

Returns: the model computed by the solver

Definition at line 67 of file Context.cpp.

◆ Pop()

void dlinear::Context::Pop ( int n )

Pop n stacks.

Parameters

n	the number of stacks to be popped

Definition at line 46 of file Context.cpp.

◆ predicate_abstractor()

const PredicateAbstractor & dlinear::Context::predicate_abstractor ( ) const

Get read-only access to the predicate_abstractor of the context.

Returns: predicate_abstractor of the context

Definition at line 70 of file Context.cpp.

◆ Push()

void dlinear::Context::Push ( int n )

Push n stacks.

Parameters

n	number of stacks to be pushed

Definition at line 51 of file Context.cpp.

◆ SetInfo()

void dlinear::Context::SetInfo	(	const std::string &	key,
		const std::string &	val )

Set an info key with a value val.

Parameters

key	the key of the info
val	the value of the info

Definition at line 57 of file Context.cpp.

◆ SetInterval()

void dlinear::Context::SetInterval	(	const Variable &	v,
		const mpq_class &	lb,
		const mpq_class &	ub )

Set the interval of v to \( [lb, ub] \) in the current box (top one in boxes_).

Parameters

v	the variable to be set
lb	the lower bound of the variable
ub	the upper bound of the variable

Definition at line 59 of file Context.cpp.

◆ SetLogic()

void dlinear::Context::SetLogic ( Logic logic )

Set the current logic to logic.

Parameters

logic the logic to be set

Definition at line 62 of file Context.cpp.

◆ SetOption()

void dlinear::Context::SetOption	(	const std::string &	key,
		const std::string &	val )

Set an option key with a value val.

Parameters

key	the key of the option
val	the value of the option

Definition at line 63 of file Context.cpp.

◆ Verify()

bool dlinear::Context::Verify ( const Box & model ) const

nodiscard

Check whether the model satisfies all the assertions loaded in the context.

In other words, verifies if it is a SAT assignment for the input variables.

Parameters

model assignment to check

Returns: true if the model satisfies all assignments; false if there is at leas an assignment not satisfied by the model

Definition at line 74 of file Context.cpp.

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

dlinear/solver/Context.h
dlinear/solver/Context.cpp

Classes

Public Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Context()

Member Function Documentation

◆ Assert()

◆ assertions()

◆ AssertPiecewiseLinearFunction()

◆ box()

◆ CheckOpt()

◆ CheckSat()

◆ config()

◆ DeclareVariable() [1/2]

◆ DeclareVariable() [2/2]

◆ Exit()

◆ GetInfo()

◆ GetOption()

◆ have_objective()

◆ is_max()

◆ Maximize()

◆ Minimize()

◆ model()

◆ Pop()

◆ predicate_abstractor()

◆ Push()

◆ SetInfo()

◆ SetInterval()

◆ SetLogic()

◆ SetOption()

◆ Verify()