29 status() <<
"BV-Refinement: post-processing" <<
eom;
41 status() <<
"BV-Refinement: iteration " << iteration <<
eom;
46 xmlt xml(
"refinement-iteration");
57 status() <<
"BV-Refinement: got SAT, and it simulates => SAT" <<
eom;
58 status() <<
"Total iterations: " << iteration <<
eom;
62 status() <<
"BV-Refinement: got SAT, and it is spurious, refining" 70 status() <<
"BV-Refinement: got UNSAT, and the proof passes => UNSAT" 72 status() <<
"Total iterations: " << iteration <<
eom;
76 status() <<
"BV-Refinement: got UNSAT, and the proof fails, refining" 95 approximation.over_assumptions.begin(),
96 approximation.over_assumptions.end());
99 approximation.under_assumptions.begin(),
100 approximation.under_assumptions.end());
void set_assumptions(const bvt &_assumptions) override
virtual bool has_is_in_conflict() const
virtual const std::string solver_text()=0
mstreamt & progress() const
std::list< approximationt > approximations
virtual void set_assumptions(const bvt &)
static mstreamt & eom(mstreamt &m)
xmlt xml(const source_locationt &location)
virtual bool has_set_assumptions() const
#define PRECONDITION(CONDITION)
ui_message_handlert::uit ui
decision_proceduret::resultt dec_solve() override
void arrays_overapproximated()
check whether counterexample is spurious
bv_refinementt(const infot &info)
void post_process() override
mstreamt & result() const
mstreamt & status() const
virtual bool has_set_to() const
std::string to_string(const string_constraintt &expr)
Used for debug printing.
virtual resultt prop_solve()=0
Abstraction Refinement Loop.
std::vector< literalt > bvt