CVC3  2.4.1
circuit.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file circuit.cpp
4  * \brief Circuit class
5  *
6  * <hr>
7  *
8  * License to use, copy, modify, sell and/or distribute this software
9  * and its documentation for any purpose is hereby granted without
10  * royalty, subject to the terms and conditions defined in the \ref
11  * LICENSE file provided with this distribution.
12  *
13  * <hr>
14  *
15  */
16 /*****************************************************************************/
17 
18 
19 #include "circuit.h"
20 #include "search_fast.h"
21 #include "search_rules.h"
22 
23 using namespace std;
24 
25 namespace CVC3
26 {
27 
28 Circuit::Circuit(SearchEngineFast* se, const Theorem& thm)
29  : d_thm(thm)
30 {
31  const Expr& e = d_thm.getExpr();
32  for (int i = 0; i < e.arity(); i++)
33  {
34  d_lits[i] =
35  e[i].isNot() ?
36  Literal(Variable(se->d_vm, e[i][0]), false) :
37  Literal(Variable(se->d_vm, e[i]), true);
38 
39  se->d_circuitsByExpr[e[i]].push_back(this);
40  se->d_circuitsByExpr[e[i].negate()].push_back(this);
41  }
42 }
43 
44 #define vals3(a, b, c) ((a) + 1 + ((b) + 1) * 3 + ((c) + 1) * 9)
45 #define vals4(a, b, c, d) (vals3(a, b, c) + ((d) + 1) * 27)
46 
48 {
49  int v0 = d_lits[0].getValue();
50  int v1 = d_lits[1].getValue();
51  int v2 = d_lits[2].getValue();
52  int v3 = d_lits[3].getValue();
53 
54  const Theorem& t0 = d_lits[0].getTheorem();
55  const Theorem& t1 = d_lits[1].getTheorem();
56  const Theorem& t2 = d_lits[2].getTheorem();
57  const Theorem& t3 = d_lits[3].getTheorem();
58 
59  int values = d_thm.getExpr().arity() == 3 ?
60  vals3(v0, v1, v2) : vals4(v0, v1, v2, v3);
61 
62  Theorem thm;
63  Theorem thm2;
64 
65  switch (d_thm.getExpr().getKind())
66  {
67  case AND_R:
68  switch (values)
69  {
70  case vals3(0,0,0): case vals3(0,0,1): case vals3(0,1,0):
71  case vals3(1,1,1): case vals3(-1,0,0): case vals3(-1,0,-1):
72  case vals3(-1,1,-1): case vals3(-1,-1,0): case vals3(-1,-1,1):
73  case vals3(-1,-1,-1):
74  break;
75 
76  case vals3(0,0,-1): case vals3(0,1,-1): case vals3(0,-1,0):
77  case vals3(0,-1,1): case vals3(0,-1,-1):
78  // simp
79  thm = se->d_rules->propAndrAF(d_thm, v1 == -1, v1 == -1 ? t1 : t2);
80  break;
81 
82  case vals3(0,1,1):
83  // simp
84  thm = se->d_rules->propAndrAT(d_thm, t1, t2);
85  break;
86 
87  case vals3(1,1,0): case vals3(1,0,1): case vals3(1,0,0):
88  // split cases to avoid doing extra work?
89  se->d_rules->propAndrLRT(d_thm, t0, &thm, &thm2);
90  break;
91 
92  case vals3(-1,0,1):
93  thm = se->d_rules->propAndrLF(d_thm, t0, t2);
94  break;
95 
96  case vals3(-1,1,0):
97  thm = se->d_rules->propAndrRF(d_thm, t0, t1);
98  break;
99 
100  case vals3(1,0,-1): case vals3(1,1,-1): case vals3(1,-1,0):
101  case vals3(1,-1,1): case vals3(1,-1,-1):
102  se->d_conflictTheorem =
103  se->d_rules->confAndrAT(d_thm, t0, v1 == -1, v1 == -1 ? t1 : t2);
104  return false;
105 
106  case vals3(-1,1,1):
107  se->d_conflictTheorem =
108  se->d_rules->confAndrAF(d_thm, t0, t1, t2);
109  return false;
110  }
111  break;
112 
113  case IFF_R:
114  switch (values)
115  {
116  case vals3(0,0,0): case vals3(0,0,1): case vals3(0,0,-1):
117  case vals3(0,1,0): case vals3(0,-1,0): case vals3(1,0,0):
118  case vals3(1,1,1): case vals3(1,-1,-1): case vals3(-1,0,0):
119  case vals3(-1,1,-1): case vals3(-1,-1,1):
120  break;
121 
122  case vals3(0,1,1): case vals3(0,-1,-1):
123  case vals3(0,1,-1): case vals3(0,-1,1):
124  // simp
125  thm = se->d_rules->propIffr(d_thm, 0, t1, t2);
126  break;
127 
128  case vals3(1,0,1): case vals3(-1,0,-1):
129  case vals3(1,0,-1): case vals3(-1,0,1):
130  thm = se->d_rules->propIffr(d_thm, 1, t0, t2);
131  break;
132 
133  case vals3(1,1,0): case vals3(-1,-1,0):
134  case vals3(1,-1,0): case vals3(-1,1,0):
135  thm = se->d_rules->propIffr(d_thm, 2, t0, t1);
136  break;
137 
138  case vals3(1,1,-1): case vals3(1,-1,1):
139  case vals3(-1,1,1): case vals3(-1,-1,-1):
140  se->d_conflictTheorem = se->d_rules->confIffr(d_thm, t0, t1, t2);
141  return false;
142  }
143  break;
144 
145  case ITE_R:
146  switch (values)
147  {
148  case vals4(0,0,0,0): case vals4(0,0,0,1): case vals4(0,0,0,-1):
149  case vals4(0,0,1,0): case vals4(0,0,1,1): case vals4(0,0,1,-1):
150  case vals4(0,0,-1,0): case vals4(0,0,-1,1): case vals4(0,0,-1,-1):
151  case vals4(0,1,0,0): case vals4(0,1,0,1): case vals4(0,1,0,-1):
152  case vals4(0,-1,0,0): case vals4(0,-1,1,0): case vals4(0,-1,-1,0):
153  case vals4(1,0,0,0): case vals4(1,0,0,1): case vals4(1,0,1,0):
154  case vals4(1,0,1,1): case vals4(1,1,1,0): case vals4(1,1,1,1):
155  case vals4(1,1,1,-1): case vals4(1,-1,0,1): case vals4(1,-1,1,1):
156  case vals4(1,-1,-1,1): case vals4(-1,0,0,0): case vals4(-1,0,0,-1):
157  case vals4(-1,0,-1,0): case vals4(-1,0,-1,-1): case vals4(-1,1,-1,0):
158  case vals4(-1,1,-1,1): case vals4(-1,1,-1,-1): case vals4(-1,-1,0,-1):
159  case vals4(-1,-1,1,-1): case vals4(-1,-1,-1,-1):
160  break;
161 
162  case vals4(0,1,1,0): case vals4(0,1,1,1): case vals4(0,1,1,-1):
163  case vals4(0,1,-1,0): case vals4(0,1,-1,1): case vals4(0,1,-1,-1):
164  case vals4(0,-1,0,-1): case vals4(0,-1,1,-1): case vals4(0,-1,-1,-1):
165  case vals4(0,-1,0,1): case vals4(0,-1,1,1): case vals4(0,-1,-1,1):
166  // simp
167  thm = se->d_rules->propIterIte(d_thm, v1 == 1, t1, v1 == 1 ? t2 : t3);
168  break;
169 
170  case vals4(1,0,0,-1): case vals4(1,0,1,-1): case vals4(1,0,-1,0):
171  case vals4(1,0,-1,1): case vals4(-1,0,0,1): case vals4(-1,0,1,0):
172  case vals4(-1,0,1,-1): case vals4(-1,0,-1,1):
173  se->d_rules->propIterIfThen(d_thm, v0 == -v2, t0, v0 == -v2 ? t2 : t3,
174  &thm, &thm2);
175  break;
176 
177  case vals4(1,1,0,0): case vals4(1,1,0,1): case vals4(1,1,0,-1):
178  case vals4(1,-1,0,0): case vals4(1,-1,1,0): case vals4(1,-1,-1,0):
179  case vals4(-1,1,0,0): case vals4(-1,1,0,1): case vals4(-1,1,0,-1):
180  case vals4(-1,-1,0,0): case vals4(-1,-1,1,0): case vals4(-1,-1,-1,0):
181  thm = se->d_rules->propIterThen(d_thm, t0, t1);
182  break;
183 
184  case vals4(1,0,-1,-1): case vals4(-1,0,1,1):
185  case vals4(-1,1,1,1): case vals4(1,1,-1,-1):
186  se->d_conflictTheorem =
187  se->d_rules->confIterThenElse(d_thm, t0, t2, t3);
188  return false;
189 
190  case vals4(1,1,-1,0): case vals4(1,1,-1,1): case vals4(1,-1,0,-1):
191  case vals4(1,-1,1,-1): case vals4(1,-1,-1,-1): case vals4(-1,1,1,0):
192  case vals4(-1,1,1,-1): case vals4(-1,-1,0,1): case vals4(-1,-1,1,1):
193  case vals4(-1,-1,-1,1):
194  se->d_conflictTheorem =
195  se->d_rules->confIterIfThen(d_thm, v1 == 1, t0, t1, v1 == 1 ? t2 : t3);
196  return false;
197  }
198  break;
199 
200  default:
201  DebugAssert(false, "unhandled circuit");
202  }
203 
204  if (!thm.isNull() && se->newLiteral(thm.getExpr()).getValue() == 0)
205  {
206  se->d_core->addFact(thm);
207  se->recordFact(thm);
208  se->d_literals.push_back(se->newLiteral(thm.getExpr()));
209  se->d_circuitPropCount++;
210  }
211 
212  if (!thm2.isNull() && se->newLiteral(thm2.getExpr()).getValue() == 0)
213  {
214  se->d_core->addFact(thm2);
215  se->recordFact(thm2);
216  se->d_literals.push_back(se->newLiteral(thm2.getExpr()));
217  se->d_circuitPropCount++;
218  }
219 
220  return true;
221 }
222 
223 
224 } // namespace CVC3
225 
int arity() const
Definition: expr.h:1201
virtual Theorem confAndrAT(const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)=0
Data structure of expressions in CVC3.
Definition: expr.h:133
Definition: kinds.h:75
int getValue() const
Definition: variable.h:144
virtual Theorem confIterThenElse(const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)=0
virtual Theorem propAndrAT(const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)=0
ExprHashMap< std::vector< Circuit * > > d_circuitsByExpr
Definition: search_fast.h:215
virtual void propIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)=0
StatCounter d_circuitPropCount
Total number of circuit propagations.
Definition: search_fast.h:101
void recordFact(const Theorem &thm)
Process a new derived fact (auxiliary function)
Literal newLiteral(const Expr &e)
Construct a Literal out of an Expr or return an existing one.
Theorem d_conflictTheorem
Theorem(FALSE) which generated a conflict.
Definition: search_fast.h:229
#define DebugAssert(cond, str)
Definition: debug.h:408
VariableManager * d_vm
Variable manager for classes Variable and Literal.
virtual Theorem propIterIte(const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)=0
Theorem d_thm
Definition: circuit.h:34
SearchEngineRules * d_rules
Proof rules for the search engine.
Definition: search.h:64
Abstract proof rules interface to the simple search engine.
bool isNot() const
Definition: expr.h:420
std::vector< Literal > d_literals
Set of literals to be processed by bcp.
Definition: search_fast.h:176
virtual void propAndrLRT(const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)=0
virtual Theorem propAndrRF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)=0
Definition: kinds.h:76
const Theorem & getTheorem() const
Definition: variable.h:159
Expr negate() const
Definition: expr.h:937
Implementation of a faster search engine, using newer techniques.
Definition: search_fast.h:86
int getKind() const
Definition: expr.h:1168
Circuit class.
Expr getExpr() const
Definition: theorem.cpp:230
bool isNull() const
Definition: theorem.h:164
virtual Theorem confIffr(const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)=0
virtual Theorem confAndrAF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)=0
Definition: kinds.h:77
#define vals3(a, b, c)
Definition: circuit.cpp:44
#define vals4(a, b, c, d)
Definition: circuit.cpp:45
virtual Theorem propIffr(const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)=0
virtual Theorem confIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)=0
virtual Theorem propAndrLF(const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)=0
void addFact(const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...
bool propagate(SearchEngineFast *se)
Definition: circuit.cpp:47
TheoryCore * d_core
Access to theory reasoning.
Definition: search.h:58
Literal d_lits[4]
Definition: circuit.h:35
virtual Theorem propAndrAF(const Theorem &andr_th, bool left, const Theorem &b_th)=0
virtual Theorem propIterThen(const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)=0