27 status() <<
"BV-Refinement: post-processing" <<
eom;
39 status() <<
"BV-Refinement: iteration " << iteration <<
eom;
44 xmlt xml(
"refinement-iteration");
55 status() <<
"BV-Refinement: got SAT, and it simulates => SAT" <<
eom;
56 status() <<
"Total iterations: " << iteration <<
eom;
60 status() <<
"BV-Refinement: got SAT, and it is spurious, refining" 68 status() <<
"BV-Refinement: got UNSAT, and the proof passes => UNSAT" 70 status() <<
"Total iterations: " << iteration <<
eom;
74 status() <<
"BV-Refinement: got UNSAT, and the proof fails, refining" 93 approximation.over_assumptions.begin(),
94 approximation.over_assumptions.end());
97 approximation.under_assumptions.begin(),
98 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::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::list< approximationt > approximations
virtual void set_assumptions(const bvt &)
xmlt xml(const source_locationt &location)
virtual bool has_set_assumptions() const
#define PRECONDITION(CONDITION)
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
virtual resultt prop_solve()=0
Abstraction Refinement Loop.
std::vector< literalt > bvt