31 for(
const auto &bit : bv)
32 if(!bit.is_constant())
57 return result.first->second;
83 else if(expr.
id()==ID_symbol)
85 symbolst::const_iterator
result=
99 if(expr.
type().
id()==ID_bool &&
108 else if(expr.
id()==ID_and || expr.
id()==ID_or)
110 if(expr.
type().
id()==ID_bool &&
113 value=
tvt(expr.
id()==ID_and);
121 if(expr.
id()==ID_and)
149 cachet::const_iterator cache_result=
cache.find(expr);
150 if(cache_result==
cache.end())
160 expr.
id()==ID_symbol ||
161 expr.
id()==ID_constant)
173 return result.first->second;
184 std::cout <<
literal <<
"=" << expr <<
'\n';
204 "constant expression of type bool should be either true or false");
208 else if(expr.
id()==ID_symbol)
212 else if(expr.
id()==ID_literal)
216 else if(expr.
id()==ID_nondet_symbol)
220 else if(expr.
id()==ID_implies)
226 else if(expr.
id()==ID_if)
234 else if(expr.
id()==ID_constraint_select_one)
238 "constraint_select_one should have at least two operands");
240 std::vector<literalt> op_bv;
241 op_bv.resize(op.size());
250 b.reserve(op_bv.size()-1);
252 for(
unsigned i=1; i<op_bv.size(); i++)
259 else if(expr.
id()==ID_or || expr.
id()==ID_and || expr.
id()==ID_xor ||
260 expr.
id()==ID_nor || expr.
id()==ID_nand)
264 "operator `" + expr.
id_string() +
"' takes at least one operand");
275 else if(expr.
id()==ID_nor)
277 else if(expr.
id()==ID_and)
279 else if(expr.
id()==ID_nand)
281 else if(expr.
id()==ID_xor)
285 else if(expr.
id()==ID_not)
287 INVARIANT(op.size() == 1,
"not takes one operand");
290 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
292 INVARIANT(op.size() == 2,
"equality takes two operands");
293 bool equal=(expr.
id()==ID_equal);
295 if(op[0].type().id()==ID_bool &&
296 op[1].type().id()==ID_bool)
304 else if(expr.
id()==ID_let)
345 if(expr.
lhs().
id()==ID_symbol)
352 std::pair<symbolst::iterator, bool>
result=
353 symbols.insert(std::pair<irep_idt, literalt>(identifier, tmp));
368 const bool has_only_boolean_operands = std::all_of(
371 [](
const exprt &expr) {
return expr.
type().
id() == ID_bool; });
373 if(has_only_boolean_operands)
375 if(expr.
id()==ID_not)
389 if(expr.
id()==ID_and)
396 else if(expr.
id()==ID_or)
413 else if(expr.
id()==ID_implies)
423 else if(expr.
id()==ID_equal)
432 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';
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
virtual bool set_equality_to_true(const equal_exprt &expr)
literalt convert(const exprt &expr) override
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)
bool is_false() const
Return whether the expression is a constant representing false.
virtual literalt lor(literalt a, literalt b)=0
The trinary if-then-else operator.
bool is_true() const
Return whether the expression is a constant representing true.
virtual bool is_in_conflict(literalt l) const
determine whether a variable is in the final conflict
virtual literalt convert_bool(const exprt &expr)
typet & type()
Return the type of the expression.
decision_proceduret::resultt dec_solve() override
void set_to(const exprt &expr, bool value) override
virtual void post_process()
virtual literalt limplies(literalt a, literalt b)=0
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
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
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
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
#define PRECONDITION(CONDITION)
virtual void set_variable_name(literalt, const irep_idt &)
virtual void set_frozen(literalt)
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
The Boolean constant false.
bool is_constant() const
Return whether the expression is a constant.
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 an exprt to an equal_exprt.
virtual literalt get_literal(const irep_idt &symbol)
void set_to_false(const exprt &expr)
mstreamt & result() const
bool literal(const symbol_exprt &expr, literalt &literal) 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
#define UNREACHABLE
This should be used to mark dead code.
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
Expression to hold a symbol (variable)
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
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
virtual void ignoring(const exprt &expr)
mstreamt & statistics() const
std::vector< literalt > bvt
virtual void set_assumptions(const bvt &_assumptions)