Go to the documentation of this file.
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());
#define PRECONDITION(CONDITION)
virtual bool has_is_in_conflict() const
virtual void set_assumptions(const bvt &)
virtual const std::string solver_text()=0
std::vector< literalt > bvt
mstreamt & status() const
void arrays_overapproximated()
check whether counterexample is spurious
xmlt xml(const source_locationt &location)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bv_refinementt(const infot &info)
virtual bool has_set_assumptions() const
std::list< approximationt > approximations
void set_assumptions(const bvt &_assumptions) override
decision_proceduret::resultt dec_solve() override
mstreamt & result() const
virtual resultt prop_solve()=0
virtual bool has_set_to() const
void post_process() override