maat::solver::Solver class

The generic solver interface. It should be sub-classed for implementations using specific backends (z3, yices, cvc4, ...)

Contents

❱   Public functions

void reset() pure virtual
Remove all current constraints.

void add(const Constraint& constr) pure virtual
Add a constraint to the solver.

void pop() pure virtual
Remove the lastest added constraint.

auto check() -> bool pure virtual
Solve the current constraints. Return true on success and false on failure. If the check was successful, the generated model can be obtained by calling get_model()

auto get_model() -> std::shared_ptr<VarContext> pure virtual

❱   Public variables

unsigned int timeout
Timeout in milliseconds when calling check() (default: 300000ms/5min)

❱   Function documentation

std::shared_ptr<VarContext> maat::solver::Solver::get_model() pure virtual

Get model for the last solved constraints. If the previous call to check() had returned false, the function will return a null pointer