31 for(
const auto &bit : bv)
32 if(!bit.is_constant())
38 assert(expr.
type().
id()==ID_bool);
40 if(expr.
id()==ID_symbol)
53 throw "found no literal for expression";
62 return result.first->second;
88 else if(expr.
id()==ID_symbol)
90 symbolst::const_iterator
result=
102 if(expr.
id()==ID_not)
104 if(expr.
type().
id()==ID_bool &&
113 else if(expr.
id()==ID_and || expr.
id()==ID_or)
115 if(expr.
type().
id()==ID_bool &&
118 value=
tvt(expr.
id()==ID_and);
126 if(expr.
id()==ID_and)
154 cachet::const_iterator cache_result=
cache.find(expr);
155 if(cache_result==
cache.end())
165 expr.
id()==ID_symbol ||
166 expr.
id()==ID_constant)
178 return result.first->second;
189 std::cout <<
literal <<
"=" << expr <<
'\n';
208 throw "unknown boolean constant: "+expr.
pretty();
210 else if(expr.
id()==ID_symbol)
214 else if(expr.
id()==ID_literal)
218 else if(expr.
id()==ID_nondet_symbol)
222 else if(expr.
id()==ID_implies)
225 throw "implication takes two operands";
229 else if(expr.
id()==ID_if)
232 throw "if takes three operands";
236 else if(expr.
id()==ID_constraint_select_one)
239 throw "constraint_select_one takes at least two operands";
241 std::vector<literalt> op_bv;
242 op_bv.resize(op.size());
251 b.reserve(op_bv.size()-1);
253 for(
unsigned i=1; i<op_bv.size(); i++)
260 else if(expr.
id()==ID_or || expr.
id()==ID_and || expr.
id()==ID_xor ||
261 expr.
id()==ID_nor || expr.
id()==ID_nand)
265 "operator `" + expr.
id_string() +
"' takes at least one operand");
276 else if(expr.
id()==ID_nor)
278 else if(expr.
id()==ID_and)
280 else if(expr.
id()==ID_nand)
282 else if(expr.
id()==ID_xor)
286 else if(expr.
id()==ID_not)
288 INVARIANT(op.size() == 1,
"not takes one operand");
291 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
293 INVARIANT(op.size() == 2,
"equality takes two operands");
294 bool equal=(expr.
id()==ID_equal);
296 if(op[0].type().id()==ID_bool &&
297 op[1].type().id()==ID_bool)
305 else if(expr.
id()==ID_let)
346 if(expr.
lhs().
id()==ID_symbol)
353 std::pair<symbolst::iterator, bool>
result=
354 symbols.insert(std::pair<irep_idt, literalt>(identifier, tmp));
369 const bool has_only_boolean_operands = std::all_of(
372 [](
const exprt &expr) {
return expr.
type().
id() == ID_bool; });
374 if(has_only_boolean_operands)
376 if(expr.
id()==ID_not)
390 if(expr.
id()==ID_and)
397 else if(expr.
id()==ID_or)
414 else if(expr.
id()==ID_implies)
424 else if(expr.
id()==ID_equal)
433 if(expr.
id()==ID_implies)
440 else if(expr.
id()==ID_or)
489 if(expr.
type().
id()==ID_bool &&
503 exprt tmp_op =
get(op);
511 for(
const auto &symbol :
symbols)
512 out << symbol.first <<
" = " <<
prop.
l_get(symbol.second) <<
'\n';
virtual bool set_equality_to_true(const equal_exprt &expr)
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
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
virtual bool is_in_conflict(literalt l) const
determine whether a variable is in the final conflict
virtual literalt convert_bool(const exprt &expr)
decision_proceduret::resultt dec_solve() override
static mstreamt & eom(mstreamt &m)
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
const let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
#define INVARIANT(CONDITION, REASON)
void l_set_to_true(literalt a)
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
mstreamt & warning() const
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
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 literalt lxor(literalt a, literalt b)=0
virtual void set_variable_name(literalt a, const irep_idt &name)
#define PRECONDITION(CONDITION)
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
The boolean constant false.
std::vector< exprt > operandst
virtual literalt lequal(literalt a, literalt b)=0
literalt const_literal(bool value)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
virtual literalt get_literal(const irep_idt &symbol)
void set_to_false(const exprt &expr)
mstreamt & result() const
literalt get_literal() const
Base class for all expressions.
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
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
virtual void ignoring(const exprt &expr)
mstreamt & statistics() const
std::vector< literalt > bvt
virtual void set_assumptions(const bvt &_assumptions)