dlinear::SmtSolver Class Reference

This class provides an easy interface for using the underling solver. More...

#include <SmtSolver.h>

Public Member Functions
	SmtSolver (Config config=Config{})
	Construct a new SmtSolver object with the given config .
	SmtSolver (const std::string &filename)
	Construct a new SmtSolver object with a default configuration ready to parse the filename .
void	Assert (const Formula &f)
	Assert a formula to the current context.
const SmtSolverOutput &	Parse ()
	Parse the problem from the input indicated in the configuration.
const SmtSolverOutput &	Parse (const std::string &filename)
	Parse the problem from a file or standard input, overriding the configuration.
const SmtSolverOutput &	CheckSat ()
	Check the satisfiability of the current context.
bool	Verify (const Box &model) const
	Check whether the model satisfies all the assertions loaded in the context.

Private Member Functions
bool	ParseInput ()
	Parse the problem from the input indicated in the configuration.

Private Attributes
Config	config_
	Configuration of the solver.
SmtSolverOutput	output_
	Output of the solver.
Context	context_
	Context obtained from the input file and passed to the SAT and SMT solvers.

Detailed Description

This class provides an easy interface for using the underling solver.

Once the correct configuration is set, and the assertions loaded, the user can simply call CheckSat to get the result. It can handle the parsing of the input file or stream

SmtSolver solver;
// Load the problem from the file input.smt2
solver.Parse("input.smt2");
solver.CheckSat();

or the user can assert the constraints manually

SmtSolver solver;
// Declare the variables
Variable x{"x"}, y{"y"};
// Assert the constraint
solver.Assert(x + y == 10);
solver.CheckSat();

See also

Config

Definition at line 41 of file SmtSolver.h.

Constructor & Destructor Documentation

SmtSolver() [1/2]

dlinear::SmtSolver::SmtSolver ( Config config = Config{} )

explicit

Construct a new SmtSolver object with the given config .

Parameters

config

configuration of the solver

Definition at line 42 of file SmtSolver.cpp.

SmtSolver() [2/2]

dlinear::SmtSolver::SmtSolver ( const std::string & filename )

explicit

Construct a new SmtSolver object with a default configuration ready to parse the filename .

Parameters

filename

name of the file to parse

Definition at line 41 of file SmtSolver.cpp.

Member Function Documentation

Assert()

void dlinear::SmtSolver::Assert

(

const Formula &

f

)

Assert a formula to the current context.

The formula will be added to the context and will be checked by the solver in the next call to CheckSat.

Parameters

f	formula to assert

Exceptions

std::runtime_error

if the formula is not in the correct format

Definition at line 94 of file SmtSolver.cpp.

CheckSat()

const SmtSolverOutput & dlinear::SmtSolver::CheckSat

(

)

Check the satisfiability of the current context.

Returns

output of the solver

Definition at line 44 of file SmtSolver.cpp.

Parse() [1/2]

const SmtSolverOutput & dlinear::SmtSolver::Parse

(

)

Parse the problem from the input indicated in the configuration.

All the variables and assertions will be added to the context. If the input contains the (check-sat) command, a satisfiability check will be performed.

Returns

output of the solver, if the input contains the (check-sat) command. Otherwise, the result field will be SmtResult::UNSOLVED.

Exceptions

std::runtime_error	if the input is not in the correct format or the files contains an unsupported command
std::out_of_range	if the file try to access undeclared variables

Definition at line 73 of file SmtSolver.cpp.

Parse() [2/2]

const SmtSolverOutput & dlinear::SmtSolver::Parse

(

const std::string &

filename

)

Parse the problem from a file or standard input, overriding the configuration.

All the variables and assertions will be added to the context. If the input contains the (check-sat) command, a satisfiability check will be performed.

Warning

This overrides the input in the configuration, changing it permanently.

Parameters

filename

name of the file to parse or an empty string for standard input

Returns

output of the solver, if the input contains the (check-sat) command. Otherwise, the result field will be SmtResult::UNSOLVED.

Exceptions

std::runtime_error	if the input is not in the correct format or the files contains an unsupported command
std::out_of_range	if the file try to access undeclared variables

Definition at line 68 of file SmtSolver.cpp.

ParseInput()

bool dlinear::SmtSolver::ParseInput ( )

private

Parse the problem from the input indicated in the configuration.

All the variables and assertions will be added to the context. If the input contains the (check-sat) command, a satisfiability check will be performed.

Returns

true if the input was parsed correctly

false if there was an error parsing the input

Exceptions

std::runtime_error	if the input is not in the correct format or the files contains an unsupported command
std::out_of_range	if the file try to access undeclared variables

Definition at line 101 of file SmtSolver.cpp.

Verify()

bool dlinear::SmtSolver::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 66 of file SmtSolver.cpp.

---

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

• dlinear/solver/SmtSolver.h
• dlinear/solver/SmtSolver.cpp