12 #ifndef CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H 13 #define CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H 17 #define MAX_STATE 10000 116 #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
void add_over_assumption(literalt l)
bool refine_arrays
Enable array refinement.
bvt convert_mult(const mult_exprt &expr) override
unsigned max_node_refinement
Max number of times we refine a formula node.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::string decision_procedure_text() const override
bvt convert_mod(const mod_exprt &expr) override
approximationt(std::size_t _id_nr)
decision_proceduret::resultt dec_solve() override
Binary multiplication Associativity is not specified.
void arrays_overapproximated()
check whether counterexample is spurious
bv_refinementt(const infot &info)
bvt convert_floatbv_op(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