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