18 max_node_refinement(5),
19 do_array_refinement(true),
20 do_arithmetic_refinement(true)
35 status() <<
"BV-Refinement: post-processing" <<
eom;
47 status() <<
"BV-Refinement: iteration " << iteration <<
eom;
52 xmlt xml(
"refinement-iteration");
53 xml.
data=std::to_string(iteration);
54 std::cout << xml <<
'\n';
63 status() <<
"BV-Refinement: got SAT, and it simulates => SAT" <<
eom;
64 status() <<
"Total iterations: " << iteration <<
eom;
68 status() <<
"BV-Refinement: got SAT, and it is spurious, refining" 76 status() <<
"BV-Refinement: got UNSAT, and the proof passes => UNSAT" 78 status() <<
"Total iterations: " << iteration <<
eom;
82 status() <<
"BV-Refinement: got UNSAT, and the proof fails, refining" 97 for(approximationst::const_iterator
104 a_it->over_assumptions.begin(), a_it->over_assumptions.end());
107 a_it->under_assumptions.begin(), a_it->under_assumptions.end());
128 for(approximationst::iterator
139 for(approximationst::iterator
152 std::cout << n <<
" EEE " << expr.
id() <<
"@" << expr.
type().
id();
154 std::cout <<
" " << it->id() <<
"@" << it->type().id();
155 if(expr.
id()==
"=" && expr.
operands().size()==2)
157 std::cout <<
" " << it->id() <<
"@" << it->type().id();
virtual decision_proceduret::resultt dec_solve()
virtual bool has_is_in_conflict() const
virtual const std::string solver_text()=0
virtual void set_assumptions(const bvt &_assumptions)
virtual void set_to(const exprt &expr, bool value)
approximationst approximations
static mstreamt & eom(mstreamt &m)
xmlt xml(const source_locationt &location)
virtual bool has_set_assumptions() const
const irep_idt & id() const
virtual size_t no_variables() const =0
#define forall_operands(it, expr)
bv_refinementt(const namespacet &_ns, propt &_prop)
virtual void set_assumptions(const bvt &_assumptions)
void arrays_overapproximated()
check whether counterexample is spurious
void post_process() override
Base class for all expressions.
virtual bool has_set_to() const
virtual resultt prop_solve()=0
Abstraction Refinement Loop.
void set_to(const exprt &expr, bool value) override
virtual void check_UNSAT()
std::vector< literalt > bvt