Go to the documentation of this file.
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
bvt convert_div(const div_exprt &expr) override
unsigned max_node_refinement
Max number of times we refine a formula node.
bool conflicts_with(approximationt &approximation)
check if an under-approximation is part of the conflict
virtual const std::string solver_text()=0
std::vector< literalt > bvt
void arrays_overapproximated()
check whether counterexample is spurious
approximationt & add_approximation(const exprt &expr, bvt &bv)
bool refine_arithmetic
Enable arithmetic refinement.
Base class for all expressions.
std::string decision_procedure_text() const override
bv_refinementt(const infot &info)
approximationt(std::size_t _id_nr)
bvt convert_mult(const mult_exprt &expr) override
std::list< approximationt > approximations
void set_assumptions(const bvt &_assumptions) override
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void initialize(approximationt &approximation)
decision_proceduret::resultt dec_solve() override
void add_under_assumption(literalt l)
void add_over_assumption(literalt l)
Binary multiplication Associativity is not specified.
void post_process_arrays() override
generate array constraints
bvt convert_floatbv_op(const exprt &expr) override
bvt convert_mod(const mod_exprt &expr) override
void get_values(approximationt &approximation)
void freeze_lazy_constraints()
freeze symbols for incremental solving
bool refine_arrays
Enable array refinement.
std::string as_string() const