cprover
literal_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_PROP_LITERAL_EXPR_H
11 #define CPROVER_SOLVERS_PROP_LITERAL_EXPR_H
12 
13 #include <util/std_expr.h>
14 
15 #include "literal.h"
16 
18 {
19 public:
20  explicit literal_exprt(literalt a):
21  predicate_exprt(ID_literal)
22  {
23  set_literal(a);
24  }
25 
27  {
28  literalt result;
29  result.set(literalt::var_not(get_long_long(ID_literal)));
30  return result;
31  }
32 
34  {
35  set(ID_literal, a.get());
36  }
37 };
38 
44 inline const literal_exprt &to_literal_expr(const exprt &expr)
45 {
46  PRECONDITION(expr.id() == ID_literal);
48  !expr.has_operands(), "literal expression should not have operands");
49  return static_cast<const literal_exprt &>(expr);
50 }
51 
55 {
56  PRECONDITION(expr.id() == ID_literal);
58  !expr.has_operands(), "literal expression should not have operands");
59  return static_cast<literal_exprt &>(expr);
60 }
61 
62 #endif // CPROVER_SOLVERS_PROP_LITERAL_EXPR_H
literalt::var_not
unsigned var_not
Definition: literal.h:31
literal_exprt::get_literal
literalt get_literal() const
Definition: literal_expr.h:26
exprt
Base class for all expressions.
Definition: expr.h:53
irept::get_long_long
long long get_long_long(const irep_namet &name) const
Definition: irep.cpp:79
to_literal_expr
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
Definition: literal_expr.h:44
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:92
predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:535
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
literal_exprt
Definition: literal_expr.h:18
literalt::get
var_not get() const
Definition: literal.h:103
irept::id
const irep_idt & id() const
Definition: irep.h:418
literal.h
literal_exprt::set_literal
void set_literal(literalt a)
Definition: literal_expr.h:33
literalt::set
void set(var_not _l)
Definition: literal.h:93
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
literalt
Definition: literal.h:26
literal_exprt::literal_exprt
literal_exprt(literalt a)
Definition: literal_expr.h:20
std_expr.h
API to expression classes.