dlinear::SmtSolverOutput Struct Reference

Data struct containing the output of the solver, such as the result of the computation as well as some statistics. More...

#include <SmtSolverOutput.h>

Public Member Functions
	SmtSolverOutput (const Config &config)
	Construct a new SmtSolverOutput object.
double	precision_upper_bound () const
	Return the precision upper bound.
bool	is_sat () const
	Return whether the problem is satisfiable or some variant of it.
int	exit_code () const
	Exit code of the solver to return to the user.
bool	matches_expectation (SmtResult expectation) const
	Check if the result of the computation matches the expectation.

Public Attributes
bool	produce_models
	Whether the solver should produce models.
bool	with_timings
	Whether the solver should show timings.
Stats	parser_stats {with_timings, ""}
	Statistics about the solver.
IterationStats	ite_stats {with_timings, ""}
	Statistics about the if-then-else simplifier.
IterationStats	cnfizer_stats {with_timings, ""}
	Statistics about the formula cnfizer.
IterationStats	predicate_abstractor_stats {with_timings, ""}
	Statistics about the predicate abstractor.
IterationStats	sat_stats {with_timings, ""}
	Statistics about the satisfiability check.
IterationStats	theory_stats {with_timings, ""}
	Statistics about the theory check.
IterationStats	preprocessor_stats {with_timings, ""}
	Statistics about the bound preprocessor.
Timer	smt_solver_timer {}
	Timer keeping track of the time spent in the SMT solver.
unsigned int	n_assertions {0}
	Number of assertions in the input.
SmtResult	result {SmtResult::UNSOLVED}
	Result of the computation.
mpq_class	lower_bound {0}
	Lower bound of the result.
mpq_class	upper_bound {0}
	Upper bound of the result.
Box	model
	Model of the result.
Box	complete_model
	Model of the result that include the auxilary variables introduced.
mpq_class	precision
	User-provided precision of the computation.
mpq_class	actual_precision
	Actual precision of the computation. Always <= than precision.

Detailed Description

Data struct containing the output of the solver, such as the result of the computation as well as some statistics.

Definition at line 44 of file SmtSolverOutput.h.

Constructor & Destructor Documentation

SmtSolverOutput()

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

inlineexplicit

Construct a new SmtSolverOutput object.

Parameters

config

configuration of the solver. Used to initialise a few static parameters

Definition at line 50 of file SmtSolverOutput.h.

Member Function Documentation

exit_code()

int dlinear::SmtSolverOutput::exit_code ( ) const

nodiscard

Exit code of the solver to return to the user.

Returns

0 if the problem is satisfiable

1 if the problem is not satisfiable

2 if the solver was unable to determine the satisfiability

3 if an error was detected

4 any other case

Definition at line 56 of file SmtSolverOutput.cpp.

is_sat()

bool dlinear::SmtSolverOutput::is_sat ( ) const

inlinenodiscard

Return whether the problem is satisfiable or some variant of it.

Returns

true if the problem is satisfiable

false if the problem is not satisfiable

Definition at line 68 of file SmtSolverOutput.h.

matches_expectation()

bool dlinear::SmtSolverOutput::matches_expectation ( SmtResult expectation ) const

nodiscard

Check if the result of the computation matches the expectation.

If the solver is running in complete mode, the results are expected to be the same. Otherwise, a relaxation of the result is allowed.

Parameters

expectation

expected result

Returns

true if the result matches the expectation

false if the result does not match the expectation

Definition at line 76 of file SmtSolverOutput.cpp.

precision_upper_bound()

double dlinear::SmtSolverOutput::precision_upper_bound ( ) const

nodiscard

Return the precision upper bound.

Returns

precision upper bound

Definition at line 52 of file SmtSolverOutput.cpp.

---

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

• dlinear/solver/SmtSolverOutput.h
• dlinear/solver/SmtSolverOutput.cpp