cprover
guard.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "guard.h"
13 
14 #include <ostream>
15 
16 #include "expr_util.h"
17 #include "invariant.h"
18 #include "simplify_utils.h"
19 #include "std_expr.h"
20 
21 void guardt::guard_expr(exprt &dest) const
22 {
23  if(is_true())
24  {
25  // do nothing
26  }
27  else
28  {
29  if(dest.is_false())
30  {
31  dest = boolean_negate(as_expr());
32  }
33  else
34  {
35  implies_exprt tmp;
36  tmp.op0()=as_expr();
37  tmp.op1().swap(dest);
38  dest.swap(tmp);
39  }
40  }
41 }
42 
43 void guardt::add(const exprt &expr)
44 {
45  PRECONDITION(expr.type().id() == ID_bool);
46 
47  if(is_false() || expr.is_true())
48  return;
49  else if(is_true() || expr.is_false())
50  {
51  *this=expr;
52 
53  return;
54  }
55  else if(id()!=ID_and)
56  {
57  and_exprt a;
58  a.add_to_operands(*this);
59  *this=a;
60  }
61 
62  operandst &op=operands();
63 
64  if(expr.id()==ID_and)
65  op.insert(op.end(),
66  expr.operands().begin(),
67  expr.operands().end());
68  else
69  op.push_back(expr);
70 }
71 
72 guardt &operator -= (guardt &g1, const guardt &g2)
73 {
74  if(g1.id()!=ID_and || g2.id()!=ID_and)
75  return g1;
76 
77  sort_and_join(g1);
78  guardt g2_sorted=g2;
79  sort_and_join(g2_sorted);
80 
81  exprt::operandst &op1=g1.operands();
82  const exprt::operandst &op2=g2_sorted.operands();
83 
84  exprt::operandst::iterator it1=op1.begin();
85  for(exprt::operandst::const_iterator
86  it2=op2.begin();
87  it2!=op2.end();
88  ++it2)
89  {
90  while(it1!=op1.end() && *it1<*it2)
91  ++it1;
92  if(it1!=op1.end() && *it1==*it2)
93  it1=op1.erase(it1);
94  }
95 
96  g1=conjunction(op1);
97 
98  return g1;
99 }
100 
102 {
103  if(g2.is_false() || g1.is_true())
104  return g1;
105  if(g1.is_false() || g2.is_true())
106  {
107  g1=g2;
108  return g1;
109  }
110 
111  if(g1.id()!=ID_and || g2.id()!=ID_and)
112  {
113  exprt tmp(boolean_negate(g2));
114 
115  if(tmp==g1)
116  g1 = true_exprt();
117  else
118  g1=or_exprt(g1, g2);
119 
120  // TODO: make simplify more capable and apply here
121 
122  return g1;
123  }
124 
125  // find common prefix
126  sort_and_join(g1);
127  guardt g2_sorted=g2;
128  sort_and_join(g2_sorted);
129 
130  exprt::operandst &op1=g1.operands();
131  const exprt::operandst &op2=g2_sorted.operands();
132 
133  exprt::operandst n_op1, n_op2;
134  n_op1.reserve(op1.size());
135  n_op2.reserve(op2.size());
136 
137  exprt::operandst::iterator it1=op1.begin();
138  for(exprt::operandst::const_iterator
139  it2=op2.begin();
140  it2!=op2.end();
141  ++it2)
142  {
143  while(it1!=op1.end() && *it1<*it2)
144  {
145  n_op1.push_back(*it1);
146  it1=op1.erase(it1);
147  }
148  if(it1!=op1.end() && *it1==*it2)
149  ++it1;
150  else
151  n_op2.push_back(*it2);
152  }
153  while(it1!=op1.end())
154  {
155  n_op1.push_back(*it1);
156  it1=op1.erase(it1);
157  }
158 
159  if(n_op2.empty())
160  return g1;
161 
162  // end of common prefix
163  exprt and_expr1=conjunction(n_op1);
164  exprt and_expr2=conjunction(n_op2);
165 
166  g1=conjunction(op1);
167 
168  exprt tmp(boolean_negate(and_expr2));
169 
170  if(tmp!=and_expr1)
171  {
172  if(and_expr1.is_true() || and_expr2.is_true())
173  {
174  }
175  else
176  // TODO: make simplify more capable and apply here
177  g1.add(or_exprt(and_expr1, and_expr2));
178  }
179 
180  return g1;
181 }
exprt as_expr() const
Definition: guard.h:41
void guard_expr(exprt &dest) const
Definition: guard.cpp:21
guardt & operator-=(guardt &g1, const guardt &g2)
Definition: guard.cpp:72
Boolean OR.
Definition: std_expr.h:2531
exprt & op0()
Definition: expr.h:84
Deprecated expression utility functions.
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
guardt & operator|=(guardt &g1, const guardt &g2)
Definition: guard.cpp:101
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
Definition: guard.h:19
typet & type()
Return the type of the expression.
Definition: expr.h:68
Boolean implication.
Definition: std_expr.h:2485
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:50
const irep_idt & id() const
Definition: irep.h:259
The Boolean constant true.
Definition: std_expr.h:4443
Boolean AND.
Definition: std_expr.h:2409
API to expression classes.
exprt & op1()
Definition: expr.h:87
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
Guard Data Structure.
std::vector< exprt > operandst
Definition: expr.h:57
Base class for all expressions.
Definition: expr.h:54
void swap(irept &irep)
Definition: irep.h:303
static bool sort_and_join(const struct saj_tablet &saj_entry, const irep_idt &type_id)
operandst & operands()
Definition: expr.h:78
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
Definition: expr_util.cpp:127
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt&#39;s operands.
Definition: expr.h:130
void add(const exprt &expr)
Definition: guard.cpp:43