CVC3  2.4.1
theory_datatype_lazy.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file theory_datatype_lazy.cpp
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Wed Dec 1 22:32:26 2004
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 
22 #include "theory_datatype_lazy.h"
23 #include "datatype_proof_rules.h"
24 #include "typecheck_exception.h"
25 #include "parser_exception.h"
26 #include "smtlib_exception.h"
27 #include "theory_core.h"
28 #include "theory_uf.h"
29 #include "command_line_flags.h"
30 
31 
32 using namespace std;
33 using namespace CVC3;
34 
35 
36 ///////////////////////////////////////////////////////////////////////////////
37 // TheoryDatatypeLazy Public Methods //
38 ///////////////////////////////////////////////////////////////////////////////
39 
40 
41 TheoryDatatypeLazy::TheoryDatatypeLazy(TheoryCore* core)
42  : TheoryDatatype(core),
43  d_processQueue(core->getCM()->getCurrentContext()),
44  d_processQueueKind(core->getCM()->getCurrentContext()),
45  d_processIndex(core->getCM()->getCurrentContext(), 0),
46  d_typeComplete(core->getCM()->getCurrentContext(), false)
47 { }
48 
49 
51 {
52  DebugAssert(e.hasFind() && findExpr(e) == e,
53  "datatype: instantiate: Expected find(e)=e");
54  if (isConstructor(e) || e.isTranslated()) return;
55  DebugAssert(u != 0 && (u & (u-1)) == 0,
56  "datatype: instantiate: Expected single label in u");
57  DebugAssert(d_datatypes.find(e.getType().getExpr()) != d_datatypes.end(),
58  "datatype: instantiate: Unexpected type: "+e.getType().toString()
59  +"\n\n for expression: "+e.toString());
61  ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end();
62  for (; c_it != c_end; ++c_it) {
63  if ((u & ((Unsigned)1 << unsigned((*c_it).second))) != 0) break;
64  }
65  DebugAssert(c_it != c_end,
66  "datatype: instantiate: couldn't find constructor");
67  Expr cons = (*c_it).first;
68 
69  if (!cons.isFinite() && !e.isSelected()) return;
70 
71  Type consType = cons.getType();
72  if (consType.arity() == 1) {
73  d_processQueue.push_back(d_rules->dummyTheorem(d_facts, e.eqExpr(cons)));
75  return;
76  }
77  // create vars
78  vector<Expr> vars;
79  for (int i = 0; i < consType.arity()-1; ++i) {
80  vars.push_back(getEM()->newBoundVarExpr(consType[i]));
81  }
82  Expr e2 = getEM()->newClosureExpr(EXISTS, vars,
83  e.eqExpr(Expr(cons.mkOp(), vars)));
84  d_processQueue.push_back(d_rules->dummyTheorem(d_facts, e2));
86  e.setTranslated();
87 }
88 
89 
91 {
92  DebugAssert(findExpr(e) == e,
93  "datatype: initializeLabels: Expected find(e)=e");
94  DebugAssert(d_datatypes.find(t.getExpr()) != d_datatypes.end(),
95  "Unknown datatype: "+t.getExpr().toString());
97  DebugAssert(d_labels.find(e) == d_labels.end(),
98  "datatype: initializeLabels: expected unlabeled expr");
99  if (isConstructor(e)) {
100  Expr cons = getConstructor(e);
101  DebugAssert(c.find(cons) != c.end(),
102  "datatype: initializeLabels: Couldn't find constructor "
103  +cons.toString());
104  unsigned position = c[cons];
105  d_labels.insert(e,
106  SmartCDO<Unsigned>(theoryCore()->getCM()->getCurrentContext(),
107  1 << position, 0));
108  }
109  else {
110  DebugAssert(c.size() > 0, "No constructors?");
111  Unsigned value = ((Unsigned)1 << unsigned(c.size())) - 1;
112  d_labels.insert(e,
113  SmartCDO<Unsigned>(theoryCore()->getCM()->getCurrentContext(),
114  value, 0));
115  if (value == 1) instantiate(e, 1);
116  else if (!d_typeComplete) {
118  }
119  }
120 }
121 
122 
124  const Expr& e1, const Expr& e2)
125 {
126  DebugAssert(e2.hasFind(),
127  "datatype: mergeLabels: Expected hasFind(e2)");
128  Theorem fthm = find(e2);
129  const Expr& f = fthm.getRHS();
130  DebugAssert(d_labels.find(e1) != d_labels.end() &&
131  d_labels.find(f) != d_labels.end(),
132  "mergeLabels: expr is not labeled");
133  DebugAssert(e1.getType() == f.getType(), "Expected same type");
134  Unsigned u = d_labels[f].get().get();
135  Unsigned uNew = u & d_labels[e1].get().get();
136  if (u != uNew) {
137  if (e2 != f) d_facts.push_back(fthm);
138  if (!thm.isNull()) d_facts.push_back(thm);
139  d_labels[f].get().set(uNew);
140  if (uNew == 0) {
142  return;
143  }
144  }
145  if (uNew != 0 && ((uNew - 1) & uNew) == 0) {
146  instantiate(f, uNew);
147  }
148 }
149 
150 
151 void TheoryDatatypeLazy::mergeLabels(const Theorem& thm, const Expr& e,
152  unsigned position, bool positive)
153 {
154  DebugAssert(e.hasFind(),
155  "datatype: mergeLabels2: Expected hasFind(e)");
156  Theorem fthm = find(e);
157  const Expr& f = fthm.getRHS();
158  DebugAssert(d_labels.find(f) != d_labels.end(),
159  "mergeLabels2: expr is not labeled");
160  Unsigned u = d_labels[f].get().get();
161  Unsigned uNew = (Unsigned)1 << position;
162  if (positive) {
163  uNew = u & uNew;
164  if (u == uNew) return;
165  } else if ((u & uNew) != 0) uNew = u - uNew;
166  else return;
167  if (e != f) d_facts.push_back(fthm);
168  d_facts.push_back(thm);
169  d_labels[f].get().set(uNew);
170  if (uNew == 0)
172  else if (((uNew - 1) & uNew) == 0) {
173  instantiate(f, uNew);
174  }
175 }
176 
177 
178 void TheoryDatatypeLazy::checkSat(bool fullEffort)
179 {
180  bool done = false;
181  while (!done && d_splittersIndex < d_splitters.size()) {
183  if (findExpr(e) == e) {
184  DebugAssert(d_labels.find(e) != d_labels.end(),
185  "checkSat: expr is not labeled");
186  Unsigned u = d_labels[e].get().get();
187  if ((u & (u-1)) != 0) {
188  done = true;
189  DebugAssert(!d_splitterAsserted || !fullEffort,
190  "splitter should have been resolved");
191  if (!d_splitterAsserted) {
193  (d_datatypes.find(e.getType().getExpr()) != d_datatypes.end(),
194  "datatype: checkSat: Unexpected type: "+e.getType().toString()
195  +"\n\n for expression: "+e.toString());
197  ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end();
198  for (; c_it != c_end; ++c_it) {
199  if ((u & ((Unsigned)1 << unsigned((*c_it).second))) != 0) break;
200  }
201  DebugAssert(c_it != c_end,
202  "datatype: checkSat: couldn't find constructor");
203  addSplitter(datatypeTestExpr((*c_it).first.getName(), e));
204  d_splitterAsserted = true;
205  }
206  }
207  }
208  if (!done) {
209  d_splitterAsserted = false;
211  }
212  }
213  while (!done && d_processIndex < d_processQueue.size()) {
214  d_typeComplete = true;
217  switch (kind) {
218  case MERGE1: {
219  break;
220  }
221  case ENQUEUE:
222  done = true;
223  enqueueFact(e);
224  break;
225  case MERGE2: {
226  const Expr& lhs = e.getLHS();
227  const Expr& rhs = e.getRHS();
228  Theorem thm(e);
229  if (lhs.isSelected() && !rhs.isSelected()) {
230  d_facts.push_back(e);
231  rhs.setSelected();
232  thm = Theorem();
233  }
234  mergeLabels(thm, lhs, rhs);
235  break;
236  }
237  default:
238  DebugAssert(false, "Unknown case");
239  }
241  }
242 }
243 
244 
245 
247 {
248  if (e.getType().getExpr().getKind() == DATATYPE &&
249  d_labels.find(e) == d_labels.end()) {
250  initializeLabels(e, e.getType());
251  e.addToNotify(this, Expr());
252  }
253  if (e.getKind() != APPLY) return;
254  if (isConstructor(e) && e.arity() > 0) {
255  d_processQueue.push_back(d_rules->noCycle(e));
257  }
258  if (isSelector(e)) {
259  e[0].setSelected();
260  d_processQueue.push_back(reflexivityRule(e[0]));
262  }
263  setupCC(e);
264 }
265 
266 
267 void TheoryDatatypeLazy::update(const Theorem& e, const Expr& d)
268 {
269  if (d.isNull()) {
270  const Expr& lhs = e.getLHS();
271  const Expr& rhs = e.getRHS();
272  if (isConstructor(lhs) && isConstructor(rhs) &&
273  lhs.isApply() && rhs.isApply() &&
274  lhs.getOpExpr() == rhs.getOpExpr()) {
275  d_processQueue.push_back(d_rules->decompose(e));
277  }
278  else {
279  d_processQueue.push_back(e);
281  }
282  }
283  else {
284  const Theorem& dEQdsig = d.getSig();
285  if (!dEQdsig.isNull()) {
286  const Expr& dsig = dEQdsig.getRHS();
287  Theorem thm = updateHelper(d);
288  const Expr& sigNew = thm.getRHS();
289  if (sigNew == dsig) return;
290  dsig.setRep(Theorem());
291  if (isSelector(sigNew) && canCollapse(sigNew)) {
292  d.setSig(Theorem());
293  d_processQueue.push_back(transitivityRule(thm, d_rules->rewriteSelCons(d_facts, sigNew)));
295  }
296  else if (isTester(sigNew) && isConstructor(sigNew[0])) {
297  d.setSig(Theorem());
298  d_processQueue.push_back(transitivityRule(thm, d_rules->rewriteTestCons(sigNew)));
300  }
301  else {
302  const Theorem& repEQsigNew = sigNew.getRep();
303  if (!repEQsigNew.isNull()) {
304  d.setSig(Theorem());
305  d_processQueue.push_back(transitivityRule(repEQsigNew, symmetryRule(thm)));
307  }
308  else {
309  int k, ar(d.arity());
310  for (k = 0; k < ar; ++k) {
311  if (sigNew[k] != dsig[k]) {
312  sigNew[k].addToNotify(this, d);
313  }
314  }
315  d.setSig(thm);
316  sigNew.setRep(thm);
318  }
319  }
320  }
321  }
322 }