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)
63 throw "found no literal for expression";
68 std::pair<symbolst::iterator, bool>
result=
72 return result.first->second;
101 else if(expr.
id()==ID_symbol)
103 symbolst::const_iterator
result=
115 if(expr.
id()==ID_not)
117 if(expr.
type().
id()==ID_bool &&
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);
139 if(expr.
id()==ID_and)
167 cachet::const_iterator cache_result=
cache.find(expr);
168 if(cache_result==
cache.end())
178 expr.
id()==ID_symbol ||
179 expr.
id()==ID_constant)
188 std::pair<cachet::iterator, bool>
result=
192 return result.first->second;
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)
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++)
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)
297 else if(expr.
id()==ID_and)
299 else if(expr.
id()==ID_nand)
301 else if(expr.
id()==ID_xor)
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)
328 else if(expr.
id()==ID_let)
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)
509 if(expr.
type().
id()==ID_bool &&
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
virtual void set_frozen(literalt a)
bool equality_propagation
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
virtual exprt get(const exprt &expr) const override
void lcnf(literalt l0, literalt l1)
virtual const std::string solver_text()=0
const irep_idt & get_identifier() const
#define forall_expr(it, expr)
virtual literalt lor(literalt a, literalt b)=0
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
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
virtual void print_assignment(std::ostream &out) const override
virtual literalt new_variable()=0
The boolean constant true.
virtual void l_set_to(literalt a, bool value)
virtual void set_variable_name(literalt a, const std::string &name)
virtual literalt lxor(literalt a, literalt b)=0
API to expression classes.
#define forall_operands(it, expr)
The boolean constant false.
std::vector< exprt > operandst
virtual literalt lequal(literalt a, literalt b)=0
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 tvt l_get(literalt a) const =0
virtual bool get_bool(const exprt &expr, tvt &value) const
get a boolean value from counter example if not valid
virtual resultt prop_solve()=0
virtual literalt convert_rest(const exprt &expr)
const std::string & id_string() const
#define Forall_operands(it, expr)
bool post_processing_done
tv_enumt get_value() const
virtual void set_frozen(literalt a)
virtual literalt lselect(literalt a, literalt b, literalt c)=0
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)