10 #ifndef CPROVER_SOLVERS_PROP_LITERAL_EXPR_H 11 #define CPROVER_SOLVERS_PROP_LITERAL_EXPR_H 35 set(ID_literal, a.
get());
53 !expr.
has_operands(),
"literal expression should not have operands");
64 !expr.
has_operands(),
"literal expression should not have operands");
68 #endif // CPROVER_SOLVERS_PROP_LITERAL_EXPR_H
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
const irep_idt & id() const
API to expression classes.
#define PRECONDITION(CONDITION)
bool has_operands() const
Return true if there is at least one operand.
literalt get_literal() const
Base class for all expressions.
long long get_long_long(const irep_namet &name) const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
literal_exprt(literalt a)
void set_literal(literalt a)
A base class for expressions that are predicates, i.e., Boolean-typed.