12 #ifndef CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H 13 #define CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H 19 #define MAX_STATE 10000 118 #endif // CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
approximationt & add_approximation(const exprt &expr, bvt &bv)
void freeze_lazy_constraints()
freeze symbols for incremental solving
void set_assumptions(const bvt &_assumptions) override
virtual const std::string solver_text()=0
std::list< approximationt > approximations
void add_under_assumption(literalt l)
void initialize(approximationt &approximation)
void post_process_arrays() override
generate array constraints
bool conflicts_with(approximationt &approximation)
check if an under-approximation is part of the conflict
division (integer and real)
void add_over_assumption(literalt l)
bool refine_arrays
Enable array refinement.
unsigned max_node_refinement
Max number of times we refine a formula node.
std::string decision_procedure_text() const override
bvt convert_mod(const mod_exprt &expr) override
ui_message_handlert::uit ui
approximationt(std::size_t _id_nr)
decision_proceduret::resultt dec_solve() override
void arrays_overapproximated()
check whether counterexample is spurious
bv_refinementt(const infot &info)
bvt convert_floatbv_op(const exprt &expr) override
bvt convert_mult(const exprt &expr) override
void get_values(approximationt &approximation)
Base class for all expressions.
bool refine_arithmetic
Enable arithmetic refinement.
std::string as_string() const
bvt convert_div(const div_exprt &expr) override
std::vector< literalt > bvt