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

#include <ContextImpl.h>

Public Member Functions
	Impl (Config &config, SmtSolverOutput *output=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.

void	Pop ()
	Pop the top of the stack of assertions.

void	Push ()
	Push the current set of assertions to the stack.

SatResult	CheckSat (mpq_class *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)
	Declare a variable `v`.

void	SetDomain (const Variable &v, const Expression &lb, const Expression &ub)
	Set a domain for the variable `v`, restricting it to the interval \( [lb, ub] \).

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

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

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 the configuration of the context.

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

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

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

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

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

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

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 Member Functions
std::unique_ptr< TheorySolver >	GetTheorySolver ()
	Get the correct theory solver subclass based on the configuration.

std::unique_ptr< SatSolver >	GetSatSolver ()
	Get the correct sat solver subclass based on the configuration.

void	AddToBox (const Variable &v)
	Add the variable `v` to the current box.

void	LearnExplanation (const LiteralSet &explanation)
	The TheorySolver found a conflict and the explanation is the set of literals that are responsible.

void	LearnExplanations (const TheorySolver::Explanations &explanations)
	The TheorySolver found a number of conflicts and the explanations are the set of literals that are responsible.

SatResult	CheckSatCore (mpq_class *actual_precision)
	Check the satisfiability of the current set of assertions.

LpResult	CheckOptCore (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	MarkModelVariable (const Variable &v)
	Mark the variable `v` as a model variable.

bool	IsModelVariable (const Variable &v) const
	Check if the variable `v` is a model variable.

Box	ExtractModel (const Box &box) const
	Extract a model from the `box`.

void	UpdateAndPrintOutput (SmtResult smt_result) const
	Update the output_ with the last `smt_result` .

Private Attributes
Config &	config_
	Configuration of the context. It could be modified by the problem instance.

SmtSolverOutput *const	output_
	Output of the SMT solver. Stores the result of the checksat and some statistics.

std::optional< Logic >	logic_
	SMT Logic of the context. Must be among the supported logics.

std::unordered_map< std::string, std::string >	info_
	Key-value pairs of information.

std::unordered_map< std::string, std::string >	option_
	Key-value pairs of options.

ScopedVector< Box >	boxes_
	Stack of boxes. The top one is the current box.

ScopedVector< Formula >	stack_
	Stack of asserted formulas.

std::unordered_set< Variable::Id >	model_variables_
	Set of model variables.

Box	model_
	Stores the result of the latest checksat. If the checksat result was UNSAT, the model is empty.

bool	have_objective_
	Keeps track of whether or not there is an objective function.

bool	is_max_
	Keeps track of whether or not the objective function is being maximized.

std::vector< std::unique_ptr< PiecewiseLinearConstraint > >	pl_constraints_
	Special constraints that can be used to guide the SAT solver towards a possible SAT assignment.

PredicateAbstractor	predicate_abstractor_
	Converts the theory literals to boolean variables.

IfThenElseEliminator	ite_eliminator_
	Eliminates if-then-else expressions from the formula.

const std::unique_ptr< SatSolver >	sat_solver_
	SAT solver.

const std::unique_ptr< TheorySolver >	theory_solver_
	Theory solver.

std::set< LiteralSet >	explanations_so_far
	Set of explanations that have been learned so far.

Detailed Description

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

Using a forward declaration of ContextImpl in Context.h, we can avoid including this file in Context.h. This structure is based on the pimpl idiom.

Definition at line 42 of file ContextImpl.h.

Constructor & Destructor Documentation

◆ Impl()

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

explicit

Construct a context with config.

Parameters

config the configuration of the context

Definition at line 57 of file ContextImpl.cpp.

Member Function Documentation

◆ AddToBox()

void dlinear::Context::Impl::AddToBox ( const Variable & v )

private

Add the variable v to the current box.

This is used to introduce a non-model variable to solver. For a model variable, DeclareVariable should be used. But DeclareVariable should be called from outside of this class. Any methods in this class should not call it directly.

Parameters

v	The variable to be added to the current box.

Definition at line 187 of file ContextImpl.cpp.

◆ Assert()

void dlinear::Context::Impl::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 71 of file ContextImpl.cpp.

◆ assertions()

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

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 279 of file ContextImpl.cpp.

◆ AssertPiecewiseLinearFunction()

void dlinear::Context::Impl::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 86 of file ContextImpl.cpp.

◆ box() [1/2]

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

inline

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

Returns: the active box of the context

Definition at line 187 of file ContextImpl.h.

◆ box() [2/2]

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

inline

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

Returns: the active box of the context

Definition at line 192 of file ContextImpl.h.

◆ CheckOpt()

LpResult dlinear::Context::Impl::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 163 of file ContextImpl.cpp.

◆ CheckOptCore()

LpResult dlinear::Context::Impl::CheckOptCore	(	mpq_class *	obj_lo,
		mpq_class *	obj_up )

private

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

This method is called internally by CheckOpt().

Parameters

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

Returns: the result of the check-opt

See also: CheckOpt

Definition at line 442 of file ContextImpl.cpp.

◆ CheckSat()

SatResult dlinear::Context::Impl::CheckSat ( mpq_class * precision )

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

Parameters

[in,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 129 of file ContextImpl.cpp.

◆ CheckSatCore()

SatResult dlinear::Context::Impl::CheckSatCore ( mpq_class * actual_precision )

private

Check the satisfiability of the current set of assertions.

This method is called internally by CheckSat().

Parameters

[out] actual_precision the actual precision of the model

Returns: the result of the check-sat

See also: CheckSat

Definition at line 302 of file ContextImpl.cpp.

◆ config()

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

inline

Get the configuration of the context.

Returns: configuration of the context

Definition at line 176 of file ContextImpl.h.

◆ DeclareVariable()

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

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 192 of file ContextImpl.cpp.

◆ ExtractModel()

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

private

Extract a model from the box.

Note that box might include non-model variables (i.e. variables introduced by if-then-else elimination). This function creates a new box which is free of those non-model variables.

Parameters

box	box to extract a model from.

Returns: box which is free of non-model variables.

Definition at line 259 of file ContextImpl.cpp.

◆ get_model()

const Box & dlinear::Context::Impl::get_model ( )

inline

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 197 of file ContextImpl.h.

◆ GetInfo()

std::string dlinear::Context::Impl::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 220 of file ContextImpl.cpp.

◆ GetOption()

std::string dlinear::Context::Impl::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 251 of file ContextImpl.cpp.

◆ GetSatSolver()

std::unique_ptr< SatSolver > dlinear::Context::Impl::GetSatSolver ( )

private

Get the correct sat solver subclass based on the configuration.

Returns: sat solver subclass

Definition at line 469 of file ContextImpl.cpp.

◆ GetTheorySolver()

std::unique_ptr< TheorySolver > dlinear::Context::Impl::GetTheorySolver ( )

private

Get the correct theory solver subclass based on the configuration.

Returns: theory solver subclass

Definition at line 448 of file ContextImpl.cpp.

◆ have_objective()

bool dlinear::Context::Impl::have_objective ( ) const

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 281 of file ContextImpl.cpp.

◆ is_max()

bool dlinear::Context::Impl::is_max ( ) const

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 283 of file ContextImpl.cpp.

◆ IsModelVariable()

bool dlinear::Context::Impl::IsModelVariable ( const Variable & v ) const

private

Check if the variable v is a model variable.

Parameters

v	the variable to be checked

Returns: true if the variable is a model variable; false if the variable is not a model variable

Definition at line 273 of file ContextImpl.cpp.

◆ LearnExplanation()

void dlinear::Context::Impl::LearnExplanation ( const LiteralSet & explanation )

private

The TheorySolver found a conflict and the explanation is the set of literals that are responsible.

The explanation is returned to the SAT solver so that it can use it to learn a new clause and backtrack, looking for a new, non-conflicting assignment.

Parameters

explanation set of literals that are responsible for the conflict

Definition at line 483 of file ContextImpl.cpp.

◆ LearnExplanations()

void dlinear::Context::Impl::LearnExplanations ( const TheorySolver::Explanations & explanations )

private

The TheorySolver found a number of conflicts and the explanations are the set of literals that are responsible.

The explanations are returned to the SAT solver so that it can use them to learn a new clause and backtrack, looking for a new, non-conflicting assignment.

Parameters

explanations set of sets of literals that are responsible for the conflict

Definition at line 495 of file ContextImpl.cpp.

◆ MarkModelVariable()

void dlinear::Context::Impl::MarkModelVariable ( const Variable & v )

private

Mark the variable v as a model variable.

Parameters

v	the variable to be marked as a model variable

Definition at line 277 of file ContextImpl.cpp.

◆ Maximize()

void dlinear::Context::Impl::Maximize ( const Expression & obj_function )

Assert a formula maximizing a cost function f.

Parameters

f	the cost function to be maximized

Definition at line 210 of file ContextImpl.cpp.

◆ Minimize()

void dlinear::Context::Impl::Minimize ( const Expression & obj_function )

Assert a formula minimizing a cost function f.

Parameters

f	the cost function to be minimized

Definition at line 205 of file ContextImpl.cpp.

◆ predicate_abstractor()

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

inline

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

Returns: predicate_abstractor of the context

Definition at line 200 of file ContextImpl.h.

◆ SetDomain()

void dlinear::Context::Impl::SetDomain	(	const Variable &	v,
		const Expression &	lb,
		const Expression &	ub )

Set a domain for the variable v, restricting it to the interval \( [lb, ub] \).

Parameters

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

Definition at line 198 of file ContextImpl.cpp.

◆ SetInfo()

void dlinear::Context::Impl::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 215 of file ContextImpl.cpp.

◆ SetInterval()

void dlinear::Context::Impl::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 226 of file ContextImpl.cpp.

◆ SetLogic()

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

Set the current logic to logic.

Parameters

logic the logic to be set

Definition at line 232 of file ContextImpl.cpp.

◆ SetOption()

void dlinear::Context::Impl::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 244 of file ContextImpl.cpp.

◆ UpdateAndPrintOutput()

void dlinear::Context::Impl::UpdateAndPrintOutput ( SmtResult smt_result ) const

private

Update the output_ with the last smt_result .

Depending on the configuration, the model could be stored in the output, assertion and statistics could be updated. Finally, the result will be printed to the standard output, if the configuration allows it.

Warning: Precision and bounds are not updated.

Parameters

smt_result smt result to present the user

Definition at line 500 of file ContextImpl.cpp.

◆ Verify()

bool dlinear::Context::Impl::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 285 of file ContextImpl.cpp.

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

dlinear/solver/ContextImpl.h
dlinear/solver/ContextImpl.cpp

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Impl()

Member Function Documentation

◆ AddToBox()

◆ Assert()

◆ assertions()

◆ AssertPiecewiseLinearFunction()

◆ box() [1/2]

◆ box() [2/2]

◆ CheckOpt()

◆ CheckOptCore()

◆ CheckSat()

◆ CheckSatCore()

◆ config()

◆ DeclareVariable()

◆ ExtractModel()

◆ get_model()

◆ GetInfo()

◆ GetOption()

◆ GetSatSolver()

◆ GetTheorySolver()

◆ have_objective()

◆ is_max()

◆ IsModelVariable()

◆ LearnExplanation()

◆ LearnExplanations()

◆ MarkModelVariable()

◆ Maximize()

◆ Minimize()

◆ predicate_abstractor()

◆ SetDomain()

◆ SetInfo()

◆ SetInterval()

◆ SetLogic()

◆ SetOption()

◆ UpdateAndPrintOutput()

◆ Verify()