41 for(
unsigned i=0; i<bv.size(); i++)
42 if(!bv[i].is_constant())
48 assert(expr.
type().
id()==ID_bool);
50 if(expr.
id()==ID_symbol)
55 symbolst::const_iterator
result=symbols.find(identifier);
57 if(result==symbols.end())
63 throw "found no literal for expression";
68 std::pair<symbolst::iterator, bool>
result=
69 symbols.insert(std::pair<irep_idt, literalt>(identifier,
literalt()));
72 return result.first->second;
75 literalt literal=prop.new_variable();
78 prop.set_variable_name(literal,
id2string(identifier));
81 result.first->second=literal;
101 else if(expr.
id()==ID_symbol)
103 symbolst::const_iterator
result=
106 if(result==symbols.end())
109 value=prop.l_get(result->second);
115 if(expr.
id()==ID_not)
117 if(expr.
type().
id()==ID_bool &&
120 if(get_bool(expr.
op0(), value))
126 else if(expr.
id()==ID_and || expr.
id()==ID_or)
128 if(expr.
type().
id()==ID_bool &&
131 value=
tvt(expr.
id()==ID_and);
136 if(get_bool(*it, tmp))
139 if(expr.
id()==ID_and)
167 cachet::const_iterator cache_result=cache.find(expr);
168 if(cache_result==cache.end())
171 value=prop.l_get(cache_result->second);
178 expr.
id()==ID_symbol ||
179 expr.
id()==ID_constant)
181 literalt literal=convert_bool(expr);
183 prop.set_frozen(literal);
188 std::pair<cachet::iterator, bool>
result=
189 cache.insert(std::pair<exprt, literalt>(expr,
literalt()));
192 return result.first->second;
194 literalt literal=convert_bool(expr);
198 result.first->second=literal;
200 prop.set_frozen(literal);
203 std::cout << literal <<
"=" << expr <<
'\n';
211 if(expr.
type().
id()!=ID_bool)
213 std::string msg=
"prop_convt::convert_bool got " 214 "non-boolean expression: ";
228 throw "unknown boolean constant: "+expr.
pretty();
230 else if(expr.
id()==ID_symbol)
234 else if(expr.
id()==ID_literal)
238 else if(expr.
id()==ID_nondet_symbol)
240 return prop.new_variable();
242 else if(expr.
id()==ID_implies)
245 throw "implication takes two operands";
249 else if(expr.
id()==ID_if)
252 throw "if takes three operands";
256 else if(expr.
id()==ID_constraint_select_one)
259 throw "constraint_select_one takes at least two operands";
261 std::vector<literalt> op_bv;
262 op_bv.resize(op.size());
271 b.reserve(op_bv.size()-1);
273 for(
unsigned i=1; i<op_bv.size(); i++)
274 b.push_back(prop.lequal(op_bv[0], op_bv[i]));
276 prop.l_set_to_true(prop.lor(b));
280 else if(expr.
id()==ID_or || expr.
id()==ID_and || expr.
id()==ID_xor ||
281 expr.
id()==ID_nor || expr.
id()==ID_nand)
284 throw "operator `"+expr.
id_string()+
"' takes at least one operand";
295 else if(expr.
id()==ID_nor)
296 return !prop.lor(bv);
297 else if(expr.
id()==ID_and)
298 return prop.land(bv);
299 else if(expr.
id()==ID_nand)
300 return !prop.land(bv);
301 else if(expr.
id()==ID_xor)
302 return prop.lxor(bv);
305 else if(expr.
id()==ID_not)
308 throw "not takes one operand";
312 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
315 throw "equality takes two operands";
317 bool equal=(expr.
id()==ID_equal);
319 if(op[0].type().id()==ID_bool &&
320 op[1].type().id()==ID_bool)
325 equal?prop.lequal(tmp1, tmp2):prop.lxor(tmp1, tmp2);
328 else if(expr.
id()==ID_let)
334 return convert_rest(expr);
341 return prop.new_variable();
346 if(!equality_propagation)
352 if(expr.
lhs().
id()==ID_symbol)
359 std::pair<symbolst::iterator, bool>
result=
360 symbols.insert(std::pair<irep_idt, literalt>(identifier, tmp));
373 if(expr.
type().
id()!=ID_bool)
375 std::string msg=
"prop_convt::set_to got " 376 "non-boolean expression: ";
384 if(it->type().id()!=ID_bool)
392 if(expr.
id()==ID_not)
406 if(expr.
id()==ID_and)
413 else if(expr.
id()==ID_or)
430 else if(expr.
id()==ID_implies)
440 else if(expr.
id()==ID_equal)
449 if(expr.
id()==ID_implies)
456 else if(expr.
id()==ID_or)
467 prop.l_set_to(
convert(expr), value);
484 if(!post_processing_done)
488 post_processing_done=
true;
491 statistics() <<
"Solving with " << prop.solver_text() <<
eom;
509 if(expr.
type().
id()==ID_bool &&
510 !get_bool(expr, value))
524 exprt tmp_op=
get(*it);
533 for(symbolst::const_iterator it=symbols.begin();
536 out << it->first <<
" = " << prop.l_get(it->second) <<
"\n";
const std::string & id2string(const irep_idt &d)
virtual bool set_equality_to_true(const equal_exprt &expr)
virtual literalt convert(const exprt &expr) override
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
virtual exprt get(const exprt &expr) const override
const irep_idt & get_identifier() const
#define forall_expr(it, expr)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
virtual bool is_in_conflict(literalt l) const
determine whether a variable is in the final conflict
virtual literalt convert_bool(const exprt &expr)
virtual decision_proceduret::resultt dec_solve() override
static mstreamt & eom(mstreamt &m)
virtual void set_to(const exprt &expr, bool value) override
virtual void post_process()
virtual bool literal(const exprt &expr, literalt &literal) const
const irep_idt & id() const
virtual void print_assignment(std::ostream &out) const override
The boolean constant true.
API to expression classes.
virtual literalt convert(const exprt &expr)=0
#define forall_operands(it, expr)
virtual void set_to(const exprt &expr, bool value)=0
The boolean constant false.
std::vector< exprt > operandst
literalt const_literal(bool value)
virtual literalt get_literal(const irep_idt &symbol)
void set_to_false(const exprt &expr)
literalt get_literal() const
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void set_to_true(const exprt &expr)
virtual bool get_bool(const exprt &expr, tvt &value) const
get a boolean value from counter example if not valid
virtual literalt convert_rest(const exprt &expr)
const std::string & id_string() const
#define Forall_operands(it, expr)
tv_enumt get_value() const
virtual void set_frozen(literalt a)
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
virtual void ignoring(const exprt &expr)
std::vector< literalt > bvt
virtual void set_assumptions(const bvt &_assumptions)