Go to the documentation of this file.
12 #ifndef CPROVER_UTIL_DECISION_PROCEDURE_H
13 #define CPROVER_UTIL_DECISION_PROCEDURE_H
38 virtual void set_to(
const exprt &expr,
bool value)=0;
72 #endif // CPROVER_UTIL_DECISION_PROCEDURE_H
Class that provides messages with a built-in verbosity 'level'.
virtual exprt get(const exprt &expr) const =0
Base class for all expressions.
void set_to_true(const exprt &expr)
decision_proceduret(const namespacet &_ns)
void set_to_false(const exprt &expr)
virtual void set_to(const exprt &expr, bool value)=0
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
decision_proceduret & operator<<(decision_proceduret &dest, const exprt &src)
virtual resultt dec_solve()=0
virtual void print_assignment(std::ostream &out) const =0
virtual std::string decision_procedure_text() const =0
virtual ~decision_proceduret()