12 #ifndef CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H 13 #define CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H 19 #define MAX_STATE 10000 108 virtual void set_to(
const exprt &expr,
bool value);
119 #endif // CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H virtual decision_proceduret::resultt dec_solve()
approximationt & add_approximation(const exprt &expr, bvt &bv)
void freeze_lazy_constraints()
freeze symbols for incremental solving
virtual std::string decision_procedure_text() const
bool is_in_conflict(approximationt &approximation)
check if an under-approximation is part of the conflict
virtual const std::string solver_text()=0
virtual void set_assumptions(const bvt &_assumptions)
virtual void set_to(const exprt &expr, bool value)
approximationst approximations
virtual void post_process_arrays()
generate array constraints
void add_under_assumption(literalt l)
void initialize(approximationt &approximation)
void set_ui(language_uit::uit _ui)
std::list< approximationt > approximationst
virtual bvt convert_floatbv_op(const exprt &expr)
division (integer and real)
void add_over_assumption(literalt l)
bool do_arithmetic_refinement
virtual bvt convert_mult(const exprt &expr)
approximationt(std::size_t _id_nr)
bv_refinementt(const namespacet &_ns, propt &_prop)
virtual bvt convert_mod(const mod_exprt &expr)
void arrays_overapproximated()
check whether counterexample is spurious
unsigned max_node_refinement
void get_values(approximationt &approximation)
virtual bool is_in_conflict(literalt l) const override
determine whether a variable is in the final conflict
Base class for all expressions.
virtual bvt convert_div(const div_exprt &expr)
std::string as_string() const
virtual void check_UNSAT()
std::vector< literalt > bvt