44 xmlt xml(
"refinement-iteration");
45 xml.data=std::to_string(iteration);
46 log.status() <<
xml <<
'\n';
55 log.status() <<
"BV-Refinement: got SAT, and it simulates => SAT"
61 log.progress() <<
"BV-Refinement: got SAT, and it is spurious, refining"
70 <<
"BV-Refinement: got UNSAT, and the proof passes => UNSAT"
77 <<
"BV-Refinement: got UNSAT, and the proof fails, refining"
90 std::vector<exprt> assumptions;
96 approximation.over_assumptions.begin(),
97 approximation.over_assumptions.end());
100 approximation.under_assumptions.begin(),
101 approximation.under_assumptions.end());
Abstraction Refinement Loop.
message_handlert & message_handler
void finish_eager_conversion() override
bv_pointerst(const namespacet &, propt &, message_handlert &, bool get_array_constraints=false)
decision_proceduret::resultt dec_solve(const exprt &) override
Implementation of the decision procedure.
bv_refinementt(const infot &info)
void arrays_overapproximated()
check whether counterexample is spurious
void get_values(approximationt &approximation)
std::list< approximationt > approximations
resultt
Result of running the decision procedure.
Base class for all expressions.
void pop() override
Pop whatever is on top of the stack.
void push() override
Push a new context on the stack This context becomes a child context nested in the current context.
bvt assumption_stack
Assumptions on the stack.
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)