CVC3  2.4.1
theory_array.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_array.cpp
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Thu Feb 27 00:38:55 2003
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_array.h"
23 #include "theory_bitvector.h"
24 #include "array_proof_rules.h"
25 #include "typecheck_exception.h"
26 #include "parser_exception.h"
27 #include "smtlib_exception.h"
28 #include "theory_core.h"
29 #include "command_line_flags.h"
30 #include "translator.h"
31 
32 
33 using namespace std;
34 using namespace CVC3;
35 
36 
37 ///////////////////////////////////////////////////////////////////////////////
38 // TheoryArray Public Methods //
39 ///////////////////////////////////////////////////////////////////////////////
40 
41 
42 TheoryArray::TheoryArray(TheoryCore* core)
43  : Theory(core, "Arrays"), d_reads(core->getCM()->getCurrentContext()),
44  d_applicationsInModel(core->getFlags()["applications"].getBool()),
45  d_liftReadIte(core->getFlags()["liftReadIte"].getBool()),
46  d_sharedSubterms(core->getCM()->getCurrentContext()),
47  d_sharedSubtermsList(core->getCM()->getCurrentContext()),
48  d_index(core->getCM()->getCurrentContext(), 0, 0),
49  d_sharedIdx1(core->getCM()->getCurrentContext(), 0, 0),
50  d_sharedIdx2(core->getCM()->getCurrentContext(), 0, 0),
51  d_inCheckSat(0)
52 {
54 
55  // Register new local kinds with ExprManager
56  getEM()->newKind(ARRAY, "_ARRAY", true);
57  getEM()->newKind(READ, "_READ");
58  getEM()->newKind(WRITE, "_WRITE");
59  getEM()->newKind(ARRAY_LITERAL, "_ARRAY_LITERAL");
60 
61  vector<int> kinds;
62  kinds.push_back(ARRAY);
63  kinds.push_back(READ);
64  kinds.push_back(WRITE);
65 
66  kinds.push_back(ARRAY_LITERAL);
67 
68  registerTheory(this, kinds);
69 }
70 
71 
72 // Destructor: delete the proof rules class if it's present
74  if(d_rules != NULL) delete d_rules;
75 }
76 
77 
79 {
80  if (d_sharedSubterms.count(e) > 0) return;
81 
82  TRACE("arrAddSharedTerm", "TheoryArray::addSharedTerm(", e.toString(), ")");
83 
84  // Cache all shared terms
85  d_sharedSubterms[e]=e;
86 
87  // Make sure we get notified if shared term is assigned to something else
88  // We need this because we only check non-array-normalized (nan) shared terms,
89  // so if a variable gets set to a nan term, we will need to know about it.
90  e.addToNotify(this, Expr());
91 
92  if (isWrite(e) || (isRead(e) && isWrite(e[0]))) {
93 
94  // Children of shared terms better be shared so we can detect any failure of normalization
95  for (int i = 0; i < e.arity(); ++i) addSharedTerm(e[i]);
96 
97  // Only check writes that are not normalized
98  if (!isWrite(e) || e.notArrayNormalized()) {
99  // Put in list to check during checkSat
101  }
102  }
103 }
104 
105 
107 {
108  const Expr& expr = e.getExpr();
109  TRACE("arrAssertFact", "TheoryArray::assertFact(", e.getExpr().toString(), ")");
110 
111  switch (expr.getOpKind()) {
112 
113  case NOT:
114  DebugAssert(expr[0].isEq(), "Unexpected negation");
115 
116  if (isArray(getBaseType(expr[0][0]))) {
117  // For disequalities between arrays, do the polite thing, and introduce witnesses
119  break;
120  }
121 
122  // We can use the shared term mechanism here:
123  // In checksat we will ensure that all shared terms are in a normal form
124  // so if two are known to be equal, we will discover it
125  addSharedTerm(expr[0][0]);
126  addSharedTerm(expr[0][1]);
127 
128  break;
129 
130  case EQ:
131  DebugAssert(theoryCore()->inUpdate() ||
132  (d_inCheckSat > 0) ||
133  !isWrite(expr[0]), "Invariant violated");
134  break;
135 
136  default:
137  FatalAssert(false, "Unexpected case");
138  break;
139  }
140 }
141 
142 
144  DebugAssert(e.arity() != 0, "Invariant Violated");
145  int i;
146  for (i = 0; i < e.arity(); ++i) {
147  if (!e[i].isAtomic()) break;
148  }
149  if (e[i].isAbsAtomicFormula()) return e[i];
150  return findAtom(e[i]);
151 }
152 
153 
154 void TheoryArray::checkSat(bool fullEffort)
155 {
156  if (fullEffort == true) {
157  // Check that all non-array-normalized shared terms are normalized
158  Theorem thm;
159  for (; d_index < d_sharedSubtermsList.size(); d_index = d_index + 1) {
161 
162  if (isRead(e)) {
163  DebugAssert(isWrite(e[0]), "Expected read(write)");
164 
165  // This should be a signature without a find
166  DebugAssert(!e.hasFind(), "Expected no find");
167 
168  // If this is no longer a valid signature, we can skip it
169  if (!e.hasRep()) continue;
170 
171  // Check to see if we know whether indices are equal
172  Expr ieq = e[0][1].eqExpr(e[1]);
173  Theorem ieqSimp = simplify(ieq);
174  if (!ieqSimp.getRHS().isBoolConst()) {
175  // if not, split on equality of indices
176  // TODO: really tricky optimization: maybe we can avoid this split
177  // if both then and else are unknown terms?
178  addSplitter(ieq);
179  return;
180  }
181 
182  // Get the representative for the signature
183  Theorem repEqSig = e.getRep();
184  DebugAssert(!repEqSig.isRefl(), "Expected non-self rep");
185 
186  // Apply the read over write rule
187  thm = d_rules->rewriteReadWrite(e);
188 
189  // Carefully simplify
190  thm = transitivityRule(thm,
191  substitutivityRule(thm.getRHS(), 0, ieqSimp));
192  thm = transitivityRule(thm, rewriteIte(thm.getRHS()));
193 
194  // Derive the new equality and simplify
195  thm = transitivityRule(repEqSig, thm);
196  thm = iffMP(thm, simplify(thm.getExpr()));
197  Expr newExpr = thm.getExpr();
198  if (newExpr.isTrue()) {
199  // Fact is already known, continue
200  continue;
201  }
202  else if (newExpr.isAbsAtomicFormula()) {
203  enqueueFact(thm);
204  }
205  else {
206  // expr is not atomic formula, so pick a splitter that will help make it atomic
207  addSplitter(findAtom(newExpr));
208  }
209  return;
210  }
211 
212  // OK, everything else should be a write
213  DebugAssert(isWrite(e), "Expected Write");
215  "Only non-normalized writes expected");
216 
217  // If write is not its own find, this means that the write
218  // was normalized to something else already, so it's not relevant
219  // any more
220  if (find(e).getRHS() != e) continue;
221 
222  // First check for violation of redundantWrite1
223  Expr store = e[0];
224  while (isWrite(store)) store = store[0];
225  DebugAssert(findExpr(e[2]) == e[2], "Expected own find");
226  thm = simplify(Expr(READ, store, e[1]));
227  if (thm.getRHS() == e[2]) {
228  thm = d_rules->rewriteRedundantWrite1(thm, e);
229  }
230 
231  // Then check for violation of redundantWrite2
232  else if (isWrite(e[0]) && e[0][1] > e[1]) {
233  thm = d_rules->interchangeIndices(e);
234  }
235 
236  else {
237  FatalAssert(false, "Unexpected expr");
238  continue;
239  }
240 
241  // Write needs to be normalized, see what its new normal form is:
242  thm = transitivityRule(thm, simplify(thm.getRHS()));
243  Expr newExpr = thm.getRHS();
244 
245  if (newExpr.isAtomic()) {
246  // If the new normal form is atomic, go ahead and update the normal form directly
247  ++d_inCheckSat;
248  assertEqualities(thm);
249  // To ensure updates are processed and checkSat gets called again
250  enqueueFact(thm);
251  --d_inCheckSat;
252  }
253  else {
254  // normal form is not atomic, so pick a splitter that will help make it atomic
255  addSplitter(findAtom(newExpr));
256  }
257  return;
258  }
259 
260  // All the terms should be normalized now... Ok, lets split on the read
261  // indices.
262  TRACE("sharing", "checking shared terms, size = ", int2string(d_reads.size()), "");
263  // Collect all the arrays and indices of interest
264  ExprMap< hash_set<Expr> > reads_by_array;
265  ExprMap< hash_set<Expr> > const_reads_by_array;
266  for (unsigned i = 0; i < d_reads.size(); ++i) {
267  Expr read = d_reads[i];
268  if (read.getSig().isNull()) continue;
269  if( d_sharedSubterms.find(read[1]) == d_sharedSubterms.end() ) continue;
270  Expr read_array = getBaseArray(read[0]);
271  if (read[1].getKind() != BVCONST) {
272  hash_set<Expr>& reads = reads_by_array[read_array];
273  reads.insert(read);
274  } else {
275  hash_set<Expr>& reads = const_reads_by_array[read_array];
276  reads.insert(read);
277  }
278  }
279 
280  ExprMap< hash_set<Expr> >::iterator it = reads_by_array.begin();
281  ExprMap< hash_set<Expr> >::iterator it_end = reads_by_array.end();
282  for(; it != it_end; ++ it) {
283  Expr array = it->first;
284  hash_set<Expr>& reads_single_array = it->second;
285 
286  hash_set<Expr>::iterator read1_it = reads_single_array.begin();
287  hash_set<Expr>::iterator read1_end = reads_single_array.end();
288  for (; read1_it != read1_end; ++ read1_it) {
289  Expr read1 = (*read1_it);
290  Expr x_k = read1[1];
291  Expr read1_find = find(read1).getRHS();
292  // The non-const reads arrays
293  hash_set<Expr>::iterator read2_it = reads_single_array.begin();
294  for (; read2_it != read1_it; ++ read2_it) {
295  Expr read2 = (*read2_it);
296  Expr read2_find = find(read2).getRHS();
297  if (read1_find != read2_find) {
298  Theorem simpl = simplify(read1.eqExpr(read2));
299  Expr y_k = read2[1];
300  Expr eq = x_k.eqExpr(y_k);
301  if( !simplify(eq).getRHS().isBoolConst() ) {
302  if (simpl.getRHS().isFalse()) {
304  } else {
305  TRACE("sharing", "from " + read2.toString(), "with find = ", find(read2).getRHS());
306  TRACE("sharing", "from " + read1.toString(), "with find = ", find(read1).getRHS());
307  TRACE("sharing", "splitting " + y_k.toString(), " and ", x_k.toString());
308  addSplitter(eq);
309  }
310  }
311  }
312  }
313  // The const reads arrays
314  hash_set<Expr>& const_reads_single_array = const_reads_by_array[array];
315  read2_it = const_reads_single_array.begin();
316  hash_set<Expr>::iterator read2_it_end = const_reads_single_array.end();
317  for (; read2_it != read2_it_end; ++ read2_it) {
318  Expr read2 = (*read2_it);
319  Expr read2_find = find(read2).getRHS();
320  if (read1_find != read2_find) {
321  Theorem simpl = simplify(read1.eqExpr(read2));
322  Expr y_k = read2[1];
323  Expr eq = x_k.eqExpr(y_k);
324  if( !simplify(eq).getRHS().isBoolConst() ) {
325  if (simpl.getRHS().isFalse()) {
327  } else {
328  TRACE("sharing", "from " + read2.toString(), "with find = ", find(read2).getRHS());
329  TRACE("sharing", "from " + read1.toString(), "with find = ", find(read1).getRHS());
330  TRACE("sharing", "splitting " + y_k.toString(), " and ", x_k.toString());
331  addSplitter(eq);
332  }
333  }
334  }
335  }
336  }
337  }
338  TRACE("sharing", "checking shared terms, done", int2string(d_reads.size()), "");
339  }
340 }
341 
342 
343 // w(...,i,v1,...,) => w(......,i,v1')
344 // Returns Null Theorem if index does not appear
345 Theorem TheoryArray::pullIndex(const Expr& e, const Expr& index)
346 {
347  DebugAssert(isWrite(e), "Expected write");
348 
349  if (e[1] == index) return reflexivityRule(e);
350 
351  // Index does not appear
352  if (!isWrite(e[0])) return Theorem();
353 
354  // Index is at next nesting level
355  if (e[0][1] == index) {
356  return d_rules->interchangeIndices(e);
357  }
358 
359  // Index is (possibly) at deeper nesting level
360  Theorem thm = pullIndex(e[0], index);
361  if (thm.isNull()) return thm;
362  thm = substitutivityRule(e, 0, thm);
364  return thm;
365 }
366 
367 
369 {
370  Theorem thm;
371  switch (e.getKind()) {
372  case READ: {
373  switch(e[0].getKind()) {
374  case WRITE:
375  thm = d_rules->rewriteReadWrite(e);
376  return transitivityRule(thm, simplify(thm.getRHS()));
377  case ARRAY_LITERAL: {
378  IF_DEBUG(debugger.counter("Read array literals")++;)
379  thm = d_rules->readArrayLiteral(e);
380  return transitivityRule(thm, simplify(thm.getRHS()));
381  }
382  case ITE: {
383  if (d_liftReadIte) {
384  thm = d_rules->liftReadIte(e);
385  return transitivityRule(thm, simplify(thm.getRHS()));
386  }
387  e.setRewriteNormal();
388  return reflexivityRule(e);
389  }
390  default: {
391  break;
392  }
393  }
394  const Theorem& rep = e.getRep();
395  if (rep.isNull()) return reflexivityRule(e);
396  else return symmetryRule(rep);
397  }
398  case EQ:
399  // if (e[0].isAtomic() && e[1].isAtomic() && isWrite(e[0])) {
400  if (isWrite(e[0])) {
401  Expr left = e[0], right = e[1];
402  int leftWrites = 1, rightWrites = 0;
403 
404  // Count nested writes
405  Expr e1 = left[0];
406  while (isWrite(e1)) { leftWrites++; e1 = e1[0]; }
407 
408  Expr e2 = right;
409  while (isWrite(e2)) { rightWrites++; e2 = e2[0]; }
410 
411  if (rightWrites == 0) {
412  if (e1 == e2) {
413  thm = d_rules->rewriteSameStore(e, leftWrites);
414  return transitivityRule(thm, simplify(thm.getRHS()));
415  }
416  else {
417  e.setRewriteNormal();
418  return reflexivityRule(e);
419  }
420  }
421  if (leftWrites > rightWrites) {
423  thm = transitivityRule(thm, d_rules->rewriteWriteWrite(thm.getRHS()));
424  }
425  else thm = d_rules->rewriteWriteWrite(e);
426  return transitivityRule(thm, simplify(thm.getRHS()));
427  }
428  e.setRewriteNormal();
429  return reflexivityRule(e);
430  case NOT:
431  e.setRewriteNormal();
432  return reflexivityRule(e);
433  case WRITE: {
434 // if (!e.isAtomic()) {
435 // e.setRewriteNormal();
436 // return reflexivityRule(e);
437 // }
438  const Expr& store = e[0];
439  // Enabling this slows stuff down a lot
440  if (!isWrite(store)) {
441  DebugAssert(findExpr(e[2]) == e[2], "Expected own find");
442  if (isRead(e[2]) && e[2][0] == store && e[2][1] == e[1]) {
444  return transitivityRule(thm, simplify(thm.getRHS()));
445  }
446  e.setRewriteNormal();
447  return reflexivityRule(e);
448  }
449  else {
450  // if (isWrite(store)) {
451  thm = pullIndex(store,e[1]);
452  if (!thm.isNull()) {
453  if (thm.isRefl()) {
454  return d_rules->rewriteRedundantWrite2(e);
455  }
456  thm = substitutivityRule(e,0,thm);
457  thm = transitivityRule(thm,
459  return transitivityRule(thm, simplify(thm.getRHS()));
460  }
461  if (store[1] > e[1]) {
462  // Only do this rewrite if the result is atomic
463  // (avoid too many ITEs)
464  thm = d_rules->interchangeIndices(e);
465  thm = transitivityRule(thm, simplify(thm.getRHS()));
466  if (thm.getRHS().isAtomic()) {
467  return thm;
468  }
469  // not normal because might be possible to interchange later
470  return reflexivityRule(e);
471  }
472  }
473  e.setRewriteNormal();
474  return reflexivityRule(e);
475  }
476  case ARRAY_LITERAL:
477  e.setRewriteNormal();
478  return reflexivityRule(e);
479  default:
481  "Unexpected default case");
482  e.setRewriteNormal();
483  return reflexivityRule(e);
484  }
485  FatalAssert(false, "should be unreachable");
486  return reflexivityRule(e);
487 }
488 
489 
490 void TheoryArray::setup(const Expr& e)
491 {
492  if (e.isNot() || e.isEq()) return;
493  DebugAssert(e.isAtomic(), "e should be atomic");
494  for (int k = 0; k < e.arity(); ++k) {
495  e[k].addToNotify(this, e);
496  }
497  if (isRead(e)) {
498  if (e.getType().card() != CARD_INFINITE) {
499  addSharedTerm(e);
500  theoryOf(e.getType())->addSharedTerm(e);
501  }
502  Theorem thm = reflexivityRule(e);
503  e.setSig(thm);
504  e.setRep(thm);
505  e.setUsesCC();
506  DebugAssert(!isWrite(e[0]), "expected no read of writes");
507  // Record the read operator for concrete models
508  TRACE("model", "TheoryArray: add array read ", e, "");
509  d_reads.push_back(e);
510  }
511  else if (isWrite(e)) {
512  Expr store = e[0];
513 
514  if (isWrite(store)) {
515  // check interchangeIndices invariant
516  if (store[1] > e[1]) {
518  if (d_sharedSubterms.count(e) > 0) {
519  // write was identified as a shared term before it was setup: add it to list to check
521  }
522  }
523  // redundantWrite2 invariant should hold
524  DebugAssert(pullIndex(store, e[1]).isNull(),
525  "Unexpected non-array-normalized term in setup");
526  }
527 
528  // check redundantWrite1 invariant
529  // there is a hidden dependency of write(a,i,v) on read(a,i)
530  while (isWrite(store)) store = store[0];
531  // Need to simplify, not just take find: read could be a signature
532  Expr r = simplifyExpr(Expr(READ, store, e[1]));
533  theoryCore()->setupTerm(r, this, theoryCore()->getTheoremForTerm(e));
534  DebugAssert(r.isAtomic(), "Should be atomic");
535  DebugAssert(findExpr(e[2]) == e[2], "Expected own find");
536  if (r == e[2] && !e.notArrayNormalized()) {
538  if (d_sharedSubterms.count(e) > 0) {
539  // write was identified as a shared term before it was setup: add it to list to check
541  }
542  }
543  else {
544  r.addToNotify(this, e);
545  }
546  }
547 }
548 
549 
550 void TheoryArray::update(const Theorem& e, const Expr& d)
551 {
552  if (inconsistent()) return;
553 
554  if (d.isNull()) {
555  // d is a shared term
556  // we want to mark the new find representative as a shared term too
557  Expr lhs = e.getLHS();
558  Expr rhs = e.getRHS();
559  DebugAssert(d_sharedSubterms.find(lhs) != d_sharedSubterms.end(),
560  "Expected lhs to be shared");
562  if (it == d_sharedSubterms.end()) {
563  addSharedTerm(rhs);
564  }
565  return;
566  }
567 
568  int k, ar(d.arity());
569 
570  if (isRead(d)) {
571  const Theorem& dEQdsig = d.getSig();
572  if (!dEQdsig.isNull()) {
573  Expr dsig = dEQdsig.getRHS();
574  Theorem thm = updateHelper(d);
575  Expr sigNew = thm.getRHS();
576  if (sigNew == dsig) return;
577  dsig.setRep(Theorem());
578  if (isWrite(sigNew[0])) {
579  // This is the tricky case.
580  //
581  Theorem thm2 = d_rules->rewriteReadWrite(sigNew);
582  thm2 = transitivityRule(thm2, simplify(thm2.getRHS()));
583  if (thm2.getRHS().isAtomic()) {
584  // If read over write simplifies, go ahead and assert the equality
585  enqueueFact(transitivityRule(thm, thm2));
586  }
587  else {
588  // Otherwise, delay processing until checkSat
589  addSharedTerm(sigNew);
590  }
591  // thm = d_rules->rewriteReadWrite2(sigNew);
592  // Theorem renameTheorem = renameExpr(d);
593  // enqueueFact(transitivityRule(symmetryRule(renameTheorem), thm));
594  // d.setSig(Theorem());
595  // enqueueFact(thm);
596  // enqueueFact(renameTheorem);
597  }
598  // else {
599 
600  // Update the signature in all cases
601  Theorem repEQsigNew = sigNew.getRep();
602  if (!repEQsigNew.isNull()) {
603  d.setSig(Theorem());
604  enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
605  }
606  else {
607  for (k = 0; k < ar; ++k) {
608  if (sigNew[k] != dsig[k]) {
609  sigNew[k].addToNotify(this, d);
610  }
611  }
612  d.setSig(thm);
613  sigNew.setRep(thm);
615  }
616  // }
617  }
618  return;
619  }
620 
621  DebugAssert(isWrite(d), "Expected write: d = "+d.toString());
622  if (find(d).getRHS() != d) return;
623 
624  Theorem thm = updateHelper(d);
625  Expr sigNew = thm.getRHS();
626 
627  // TODO: better normalization in some cases
628  Expr store = sigNew[0];
629  if (!isWrite(store)) {
630  Theorem thm2 = find(Expr(READ, store, sigNew[1]));
631  if (thm2.getRHS() == sigNew[2]) {
632  thm = transitivityRule(thm,
633  d_rules->rewriteRedundantWrite1(thm2, sigNew));
634  sigNew = thm.getRHS();
635  }
636  }
637  else {
638  // TODO: this check is expensive, it seems
639  Theorem thm2 = pullIndex(store,sigNew[1]);
640  if (!thm2.isNull()) {
641  if (thm2.isRefl()) {
642  thm = transitivityRule(thm,
644  }
645  else {
646  thm2 = substitutivityRule(sigNew,0,thm2);
647  thm2 = transitivityRule(thm2,
649  thm = transitivityRule(thm, thm2);
650  }
651  sigNew = thm.getRHS();
652  store = sigNew[0];
653  }
654 
655  if (isWrite(store) && (store[1] > sigNew[1])) {
656  thm2 = d_rules->interchangeIndices(sigNew);
657  thm2 = transitivityRule(thm2, simplify(thm2.getRHS()));
658  // Only update if result is atomic
659  if (thm2.getRHS().isAtomic()) {
660  thm = transitivityRule(thm, thm2);
661  sigNew = thm.getRHS();
662  // no need to update store because d == sigNew
663  // case only happens if sigNew hasn't changed
664  }
665  }
666  }
667 
668  if (d == sigNew) {
669  // Hidden dependency must have changed
670  while (isWrite(store)) store = store[0];
671  Expr r = e.getRHS();
672  if (r == d[2]) {
673  // no need to update notify list as we are already on list of d[2]
674  if (!d.notArrayNormalized()) {
676  if (d_sharedSubterms.count(d) > 0) {
677  // write has become non-normalized: add it to list to check
679  }
680  }
681  }
682  else {
683  // update the notify list
684  r.addToNotify(this, d);
685  }
686  return;
687  }
688 
689  DebugAssert(sigNew.isAtomic(), "Expected atomic formula");
690  // Since we aren't doing a full normalization here, it's possible that sigNew is not normal
691  // and so it might have a different find. In that case, the find should be the new rhs.
692  if (sigNew.hasFind()) {
693  Theorem findThm = findRef(sigNew);
694  if (!findThm.isRefl()) {
695  thm = transitivityRule(thm, findThm);
696  }
697  assertEqualities(thm);
698  return;
699  }
700 
701  // If it doesn't have a find at all, it needs to be simplified
702  Theorem simpThm = simplify(sigNew);
703  thm = transitivityRule(thm, simpThm);
704  sigNew = thm.getRHS();
705  if (sigNew.isAtomic()) {
706  assertEqualities(thm);
707  }
708  else {
709  // Simplify could maybe? introduce case splits in the expression. Handle this by renaminig
710  Theorem renameTheorem = renameExpr(d);
711  enqueueFact(transitivityRule(symmetryRule(renameTheorem), thm));
712  assertEqualities(renameTheorem);
713  }
714 
715 }
716 
717 
719 {
720  const Expr& e = eThm.getExpr();
721  DebugAssert(e.isEq(), "TheoryArray::solve("+e.toString()+")");
722  if (isWrite(e[0])) {
723  DebugAssert(!isWrite(e[1]), "Should have been rewritten: e = "
724  +e.toString());
725  return symmetryRule(eThm);
726  }
727  return eThm;
728 }
729 
730 
732 {
733  switch (e.getKind()) {
734  case ARRAY: {
735  if (e.arity() != 2) throw Exception
736  ("ARRAY type should have two arguments");
737  Type t1(e[0]);
738  if (t1.isBool()) throw Exception
739  ("Array index types must be non-Boolean");
740  if (t1.isFunction()) throw Exception
741  ("Array index types cannot be functions");
742  Type t2(e[1]);
743  if (t2.isBool()) throw Exception
744  ("Array value types must be non-Boolean");
745  if (t2.isFunction()) throw Exception
746  ("Array value types cannot be functions");
747  break;
748  }
749  default:
750  DebugAssert(false, "Unexpected kind in TheoryArray::checkType"
751  +getEM()->getKindName(e.getKind()));
752  }
753 
754 }
755 
756 
758  bool enumerate, bool computeSize)
759 {
760  Cardinality card = CARD_INFINITE;
761  switch (e.getKind()) {
762  case ARRAY: {
763  Type typeIndex = Type(e[0]);
764  Type typeElem = Type(e[1]);
765  if (typeElem.card() == CARD_FINITE &&
766  (typeIndex.card() == CARD_FINITE || typeElem.sizeFinite() == 1)) {
767 
768  card = CARD_FINITE;
769 
770  if (enumerate) {
771  // Right now, we only enumerate the first element for finite arrays
772  if (n == 0) {
773  Expr ind(getEM()->newBoundVarExpr(Type(e[0])));
774  e = arrayLiteral(ind, typeElem.enumerateFinite(0));
775  }
776  else e = Expr();
777  }
778 
779  if (computeSize) {
780  n = 0;
781  Unsigned sizeElem = typeElem.sizeFinite();
782  if (sizeElem == 1) {
783  n = 1;
784  }
785  else if (sizeElem > 1) {
786  Unsigned sizeIndex = typeIndex.sizeFinite();
787  if (sizeIndex > 0) {
788  n = sizeElem;
789  while (--sizeIndex > 0) {
790  n = n * sizeElem;
791  if (n > 1000000) {
792  // if it starts getting too big, just return 0
793  n = 0;
794  break;
795  }
796  }
797  }
798  }
799  }
800  }
801  break;
802  }
803  default:
804  break;
805  }
806  return card;
807 }
808 
809 
811 {
812  switch (e.getKind()) {
813  case READ: {
814  DebugAssert(e.arity() == 2,"");
815  Type arrType = e[0].getType();
816  if (!isArray(arrType)) {
817  arrType = getBaseType(arrType);
818  }
819  if (!isArray(arrType))
820  throw TypecheckException
821  ("Expected an ARRAY type in\n\n "
822  +e[0].toString()+"\n\nBut received this:\n\n "
823  +arrType.toString()+"\n\nIn the expression:\n\n "
824  +e.toString());
825  Type idxType = getBaseType(e[1]);
826  if(getBaseType(arrType[0]) != idxType && idxType != Type::anyType(getEM())) {
827  throw TypecheckException
828  ("The type of index expression:\n\n "
829  +idxType.toString()
830  +"\n\nDoes not match the ARRAY index type:\n\n "
831  +arrType[0].toString()
832  +"\n\nIn the expression: "+e.toString());
833  }
834  e.setType(arrType[1]);
835  break;
836  }
837  case WRITE: {
838  DebugAssert(e.arity() == 3,"");
839  Type arrType = e[0].getType();
840  if (!isArray(arrType)) {
841  arrType = getBaseType(arrType);
842  }
843  Type idxType = getBaseType(e[1]);
844  Type valType = getBaseType(e[2]);
845  if (!isArray(arrType))
846  throw TypecheckException
847  ("Expected an ARRAY type in\n\n "
848  +e[0].toString()+"\n\nBut received this:\n\n "
849  +arrType.toString()+"\n\nIn the expression:\n\n "
850  +e.toString());
851  bool idxCorrect = getBaseType(arrType[0]) == idxType || idxType == Type::anyType(getEM());
852  bool valCorrect = getBaseType(arrType[1]) == valType || valType == Type::anyType(getEM());;
853  if(!idxCorrect) {
854  throw TypecheckException
855  ("The type of index expression:\n\n "
856  +idxType.toString()
857  +"\n\nDoes not match the ARRAY's type index:\n\n "
858  +arrType[0].toString()
859  +"\n\nIn the expression: "+e.toString());
860  }
861  if(!valCorrect) {
862  throw TypecheckException
863  ("The type of value expression:\n\n "
864  +valType.toString()
865  +"\n\nDoes not match the ARRAY's value type:\n\n "
866  +arrType[1].toString()
867  +"\n\nIn the expression: "+e.toString());
868  }
869  e.setType(arrType);
870  break;
871  }
872  case ARRAY_LITERAL: {
873  DebugAssert(e.isClosure(), "TheoryArray::computeType("+e.toString()+")");
874  DebugAssert(e.getVars().size()==1,
875  "TheoryArray::computeType("+e.toString()+")");
876  Type ind(e.getVars()[0].getType());
877  e.setType(arrayType(ind, e.getBody().getType()));
878  break;
879  }
880  default:
881  DebugAssert(false,"Unexpected type");
882  break;
883  }
884 }
885 
886 
888  const Expr& e = t.getExpr();
889  DebugAssert(e.getKind()==ARRAY && e.arity() == 2,
890  "TheoryArray::computeBaseType("+t.toString()+")");
891  vector<Expr> kids;
892  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
893  kids.push_back(getBaseType(Type(*i)).getExpr());
894  }
895  return Type(Expr(e.getOp(), kids));
896 }
897 
898 
899 void TheoryArray::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
900  switch(e.getKind()) {
901  case WRITE:
902  // a WITH [i] := v -- report a, i and v as the model terms.
903 // getModelTerm(e[1], v);
904 // getModelTerm(e[2], v);
905  v.push_back(e[0]);
906  v.push_back(e[1]);
907  v.push_back(e[2]);
908  break;
909  case READ:
910  // For a[i], add the index i
911  // getModelTerm(e[1], v);
912  v.push_back(e[1]);
913  // And continue to collect the reads a[i][j] (remember, e is of
914  // ARRAY type)
915  default:
916  // For array terms, find all their reads
917  if(e.getType().getExpr().getKind() == ARRAY) {
919  i!=iend; ++i) {
920  DebugAssert(isRead(*i) && (*i).arity()==2, "Bad array read: "
921  +(*i).toString());
922  if((*i)[0] == e) {
923  // Add both the read operator a[i]
924  // getModelTerm(*i, v);
925  v.push_back(*i);
926  // and the index 'i' to the model terms. Reason: the index to
927  // the array should better be a concrete value, and it might not
928  // necessarily be in the current list of model terms.
929  // getModelTerm((*i)[1], v);
930  v.push_back((*i)[1]);
931  }
932  }
933  }
934  break;
935  }
936 }
937 
938 
939 void TheoryArray::computeModel(const Expr& e, std::vector<Expr>& v) {
940  static unsigned count(0); // For bound vars
941 
942  switch(e.getKind()) {
943  case WRITE: {
944  // We should already have a value for the original array
945  Expr res(getModelValue(e[0]).getRHS());
946  Expr ind(getEM()->newBoundVarExpr("arr_var", int2string(count++)));
947  Type tp(e.getType());
948  DebugAssert(isArray(tp) && tp.arity()==2,
949  "TheoryArray::computeModel(WRITE)");
950  ind.setType(tp[0]);
951  res = rewrite(Expr(READ, res, ind)).getRHS();
952  Expr indVal(getModelValue(e[1]).getRHS());
953  Expr updVal(getModelValue(e[2]).getRHS());
954  res = (ind.eqExpr(indVal)).iteExpr(updVal, res);
955  res = arrayLiteral(ind, res);
956  assignValue(e, res);
957  v.push_back(e);
958  break;
959  }
960 // case READ: {
961 // // Get the assignment for the index
962 // Expr idx(getModelValue(e[1]).getRHS());
963 // // And the assignment for the
964 // var = read(idxThm.getRHS(), e[0]);
965 // }
966  // And continue to collect the reads a[i][j] (remember, e is of
967  // ARRAY type)
968  default: {
969  // Assign 'e' a value later.
970  v.push_back(e);
971  // Map of e[i] to val for concrete values of i and val
972  ExprHashMap<Expr> reads;
973  // For array terms, find all their reads
974  DebugAssert(getBaseType(e).getExpr().getKind() == ARRAY, "");
975 
977  i!=iend; ++i) {
978  TRACE("model", "TheoryArray::computeModel: read = ", *i, "");
979  DebugAssert(isRead(*i) && (*i).arity()==2, "Bad array read: "
980  +(*i).toString());
981  if((*i)[0] == e) {
982  // Get the value of the index
983  Theorem asst(getModelValue((*i)[1]));
984  Expr var;
985  if(asst.getLHS()!=asst.getRHS()) {
986  vector<Theorem> thms;
987  vector<unsigned> changed;
988  thms.push_back(asst);
989  changed.push_back(1);
990  Theorem subst(substitutivityRule(*i, changed, thms));
992  getModelValue(*i)));
993  var = subst.getRHS();
994  } else
995  var = *i;
996  if(d_applicationsInModel) v.push_back(var);
997  // Record it in the map
998  Expr val(getModelValue(var).getRHS());
999  DebugAssert(!val.isNull(), "TheoryArray::computeModel(): Variable "
1000  +var.toString()+" has a Null value");
1001  reads[var] = val;
1002  }
1003  }
1004  // Create an array literal
1005  if(reads.size()==0) { // Leave the array uninterpreted
1007  } else {
1008  // Bound var for the index
1009  Expr ind(getEM()->newBoundVarExpr("arr_var", int2string(count++)));
1010  Type tp(e.getType());
1011  DebugAssert(isArray(tp) && tp.arity()==2,
1012  "TheoryArray::computeModel(WRITE)");
1013  ind.setType(tp[0]);
1014  ExprHashMap<Expr>::iterator i=reads.begin(), iend=reads.end();
1015  DebugAssert(i!=iend,
1016  "TheoryArray::computeModel(): expected the reads "
1017  "table be non-empty");
1018  // Use one of the concrete values as a default
1019  Expr res((*i).second);
1020  ++i;
1021  DebugAssert(!res.isNull(), "TheoryArray::computeModel()");
1022  for(; i!=iend; ++i) {
1023  // Optimization: if the current value is the same as that of the
1024  // next application, skip this case; i.e. keep 'res' instead of
1025  // building ite(cond, res, res).
1026  if((*i).second == res) continue;
1027  // ITE condition
1028  Expr cond = ind.eqExpr((*i).first[1]);
1029  res = cond.iteExpr((*i).second, res);
1030  }
1031  // Construct the array literal
1032  res = arrayLiteral(ind, res);
1033  assignValue(e, res);
1034  }
1035  break;
1036  }
1037  }
1038 }
1039 
1040 
1042 {
1043  Expr tcc(Theory::computeTCC(e));
1044  switch (e.getKind()) {
1045  case READ:
1046  DebugAssert(e.arity() == 2,"");
1047  return tcc.andExpr(getTypePred(e[0].getType()[0], e[1]));
1048  case WRITE: {
1049  DebugAssert(e.arity() == 3,"");
1050  Type arrType = e[0].getType();
1051  return rewriteAnd(getTypePred(arrType[0], e[1]).andExpr
1052  (getTypePred(arrType[1], e[2])).andExpr(tcc)).getRHS();
1053  }
1054  case ARRAY_LITERAL: {
1055  return tcc;
1056  }
1057  default:
1058  DebugAssert(false,"TheoryArray::computeTCC: Unexpected expression: "
1059  +e.toString());
1060  return tcc;
1061  }
1062 }
1063 
1064 
1065 ///////////////////////////////////////////////////////////////////////////////
1066 // Pretty-printing //
1067 ///////////////////////////////////////////////////////////////////////////////
1068 
1069 
1070 bool debug_write = false;
1071 
1073 {
1074  d_theoryUsed = true;
1075  if (theoryCore()->getTranslator()->printArrayExpr(os, e)) return os;
1076  switch(os.lang()) {
1077  case PRESENTATION_LANG:
1078  switch(e.getKind()) {
1079  case READ:
1080  if(e.arity() == 1)
1081  os << "[" << push << e[0] << push << "]";
1082  else
1083  os << e[0] << "[" << push << e[1] << push << "]";
1084  break;
1085  case WRITE:
1086  IF_DEBUG(
1087  if (debug_write) {
1088  os << "w(" << push << e[0] << space << ", "
1089  << push << e[1] << ", " << push << e[2] << push << ")";
1090  break;
1091  }
1092  )
1093  os << "(" << push << e[0] << space << "WITH ["
1094  << push << e[1] << "] := " << push << e[2] << push << ")";
1095  break;
1096  case ARRAY:
1097  os << "(ARRAY" << space << e[0] << space << "OF" << space << e[1] << ")";
1098  break;
1099  case ARRAY_LITERAL:
1100  if(e.isClosure()) {
1101  const vector<Expr>& vars = e.getVars();
1102  const Expr& body = e.getBody();
1103  os << "(" << push << "ARRAY" << space << "(" << push;
1104  bool first(true);
1105  for(size_t i=0; i<vars.size(); ++i) {
1106  if(first) first=false;
1107  else os << push << "," << pop << space;
1108  os << vars[i];
1109  if(vars[i].isVar())
1110  os << ":" << space << pushdag << vars[i].getType() << popdag;
1111  }
1112  os << push << "):" << pop << pop << space << body << push << ")";
1113  } else
1114  e.printAST(os);
1115  break;
1116  default:
1117  // Print the top node in the default LISP format, continue with
1118  // pretty-printing for children.
1119  e.printAST(os);
1120  }
1121  break; // end of case PRESENTATION_LANGUAGE
1122  case SMTLIB_LANG:
1123  case SMTLIB_V2_LANG:
1124  switch(e.getKind()) {
1125  case READ:
1126  if(e.arity() == 2)
1127  os << "(" << push << "select" << space << e[0]
1128  << space << e[1] << push << ")";
1129  else
1130  e.printAST(os);
1131  break;
1132  case WRITE:
1133  if(e.arity() == 3)
1134  os << "(" << push << "store" << space << e[0]
1135  << space << e[1] << space << e[2] << push << ")";
1136  else
1137  e.printAST(os);
1138  break;
1139  case ARRAY:
1140  throw SmtlibException("ARRAY should be handled by printArrayExpr");
1141  break;
1142  case ARRAY_LITERAL:
1143  throw SmtlibException("SMT-LIB does not support ARRAY literals.\n"
1144  "Suggestion: use command-line flag:\n"
1145  " -output-lang presentation");
1146  e.printAST(os);
1147  default:
1148  throw SmtlibException("TheoryArray::print: default not supported");
1149  // Print the top node in the default LISP format, continue with
1150  // pretty-printing for children.
1151  e.printAST(os);
1152  }
1153  break; // end of case LISP_LANGUAGE
1154  case LISP_LANG:
1155  switch(e.getKind()) {
1156  case READ:
1157  if(e.arity() == 2)
1158  os << "(" << push << "READ" << space << e[0]
1159  << space << e[1] << push << ")";
1160  else
1161  e.printAST(os);
1162  break;
1163  case WRITE:
1164  if(e.arity() == 3)
1165  os << "(" << push << "WRITE" << space << e[0]
1166  << space << e[1] << space << e[2] << push << ")";
1167  else
1168  e.printAST(os);
1169  break;
1170  case ARRAY:
1171  os << "(" << push << "ARRAY" << space << e[0]
1172  << space << e[1] << push << ")";
1173  break;
1174  default:
1175  // Print the top node in the default LISP format, continue with
1176  // pretty-printing for children.
1177  e.printAST(os);
1178  }
1179  break; // end of case LISP_LANGUAGE
1180  default:
1181  // Print the top node in the default LISP format, continue with
1182  // pretty-printing for children.
1183  e.printAST(os);
1184  }
1185  return os;
1186 }
1187 
1188 //////////////////////////////////////////////////////////////////////////////
1189 //parseExprOp:
1190 //translating special Exprs to regular EXPR??
1191 ///////////////////////////////////////////////////////////////////////////////
1192 Expr
1194  // TRACE("parser", "TheoryArray::parseExprOp(", e, ")");
1195  // If the expression is not a list, it must have been already
1196  // parsed, so just return it as is.
1197  if(RAW_LIST != e.getKind()) return e;
1198 
1199  DebugAssert(e.arity() > 0,
1200  "TheoryArray::parseExprOp:\n e = "+e.toString());
1201 
1202  const Expr& c1 = e[0][0];
1203  int kind = getEM()->getKind(c1.getString());
1204  switch(kind) {
1205  case READ:
1206  if(!(e.arity() == 3))
1207  throw ParserException("Bad array access expression: "+e.toString());
1208  return Expr(READ, parseExpr(e[1]), parseExpr(e[2]));
1209  case WRITE:
1210  if(!(e.arity() == 4))
1211  throw ParserException("Bad array update expression: "+e.toString());
1212  return Expr(WRITE, parseExpr(e[1]), parseExpr(e[2]), parseExpr(e[3]));
1213  case ARRAY: {
1214  vector<Expr> k;
1215  Expr::iterator i = e.begin(), iend=e.end();
1216  // Skip first element of the vector of kids in 'e'.
1217  // The first element is the operator.
1218  ++i;
1219  // Parse the kids of e and push them into the vector 'k'
1220  for(; i!=iend; ++i)
1221  k.push_back(parseExpr(*i));
1222  return Expr(kind, k, e.getEM());
1223  break;
1224  }
1225  case ARRAY_LITERAL: { // (ARRAY (v tp1) body)
1226  if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() == 2))
1227  throw ParserException("Bad ARRAY literal expression: "+e.toString());
1228  const Expr& varPair = e[1];
1229  if(varPair.getKind() != RAW_LIST)
1230  throw ParserException("Bad variable declaration block in ARRAY "
1231  "literal expression: "+varPair.toString()+
1232  "\n e = "+e.toString());
1233  if(varPair[0].getKind() != ID)
1234  throw ParserException("Bad variable declaration in ARRAY"
1235  "literal expression: "+varPair.toString()+
1236  "\n e = "+e.toString());
1237  Type varTp(parseExpr(varPair[1]));
1238  vector<Expr> var;
1239  var.push_back(addBoundVar(varPair[0][0].getString(), varTp));
1240  Expr body(parseExpr(e[2]));
1241  // Build the resulting Expr as (LAMBDA (vars) body)
1242  return getEM()->newClosureExpr(ARRAY_LITERAL, var, body);
1243  break;
1244  }
1245  default:
1246  DebugAssert(false,
1247  "TheoryArray::parseExprOp: wrong type: "
1248  + e.toString());
1249  break;
1250  }
1251  return e;
1252 }
1253 
1255  if (e.getKind() == WRITE) return getBaseArray(e[0]);
1256  return e;
1257 }
1258 
1259 namespace CVC3 {
1260 
1261 Expr arrayLiteral(const Expr& ind, const Expr& body) {
1262  vector<Expr> vars;
1263  vars.push_back(ind);
1264  return body.getEM()->newClosureExpr(ARRAY_LITERAL, vars, body);
1265 }
1266 
1267 } // end of namespace CVC3
virtual Theorem simplify(const Expr &e)
Simplify a term e and return a Theorem(e==e')
Definition: theory.cpp:119
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
Definition: theory.cpp:519
int arity() const
Definition: expr.h:1201
virtual Theorem propagateIndexDiseq(const Theorem &read1eqread2isFalse)=0
ExprStream & pop(ExprStream &os)
Restore the indentation.
const bool & d_liftReadIte
Flag to lift ite's over reads.
Definition: theory_array.h:60
bool isNull() const
Definition: expr.h:1223
void setupTerm(const Expr &e, Theory *i, const Theorem &thm)
Setup additional terms within a theory-specific setup().
iterator begin()
Definition: expr_map.h:325
iterator begin() const
Begin iterator.
Definition: expr.h:1211
bool isEq() const
Definition: expr.h:419
bool isAtomic() const
Test if e is atomic.
Definition: expr.cpp:550
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
Definition: expr.cpp:400
TheoryCore * theoryCore()
Get a pointer to theoryCore.
Definition: theory.h:93
bool debug_write
void setRewriteNormal() const
Definition: expr.h:1457
Data structure of expressions in CVC3.
Definition: expr.h:133
Cardinality card() const
Return cardinality of type.
Definition: type.h:64
void addSplitter(const Expr &e, int priority=0)
Suggest a splitter to the SearchEngine.
Definition: theory.cpp:148
ExprManager * getEM() const
Definition: expr.h:1156
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
Definition: expr.h:961
An exception thrown by the parser.
Expr getBaseArray(const Expr &e) const
virtual void assertEqualities(const Theorem &e)
Handle new equalities (usually asserted through addFact)
Definition: theory.cpp:142
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
CDO< unsigned > d_index
Used in checkSat.
Definition: theory_array.h:67
bool isTrue() const
Definition: expr.h:356
Expr arrayLiteral(const Expr &ind, const Expr &body)
bool notArrayNormalized() const
Definition: expr.h:1346
void addToNotify(Theory *i, const Expr &e) const
Add (e,i) to the notify list of this expression.
Definition: expr.cpp:517
An exception to be thrown at typecheck error.
void computeType(const Expr &e)
Compute and store the type of e.
bool isWrite(const Expr &e)
Definition: theory_array.h:111
virtual Theorem rewriteWriteWrite(const Expr &e)=0
Expr findAtom(Expr e)
Type arrayType(const Type &type1, const Type &type2)
Definition: theory_array.h:116
_hash_table::iterator iterator
Definition: hash_set.h:94
bool isFalse() const
Definition: expr.h:355
virtual Theorem liftReadIte(const Expr &e)=0
Lift ite over read.
MS C++ specific settings.
Definition: type.h:42
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
Definition: theory.cpp:128
Base class for theories.
Definition: theory.h:64
SMT-LIB v2 format.
Definition: lang.h:52
iterator begin()
Definition: expr_map.h:190
Lisp-like format for automatically generated specs.
Definition: lang.h:36
Definition: kinds.h:66
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
bool isBool() const
Definition: type.h:60
ExprStream & space(ExprStream &os)
Insert a single white space separator.
bool isAbsAtomicFormula() const
An abstract atomic formua is an atomic formula or a quantified formula.
Definition: expr.h:398
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
Definition: theory.h:719
virtual Theorem rewriteSameStore(const Expr &e, int n)=0
#define DebugAssert(cond, str)
Definition: debug.h:408
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
Definition: expr_manager.h:506
bool hasFind() const
Definition: expr.h:1232
void setRep(const Theorem &e) const
Definition: expr.h:1589
void setSig(const Theorem &e) const
Definition: expr.h:1578
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
T & push_back(const T &data, int scope=-1)
Definition: cdlist.h:66
void setUsesCC() const
Definition: expr.h:1483
Expr andExpr(const Expr &right) const
Definition: expr.h:941
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
Definition: theory.cpp:203
ExprStream & pushdag(ExprStream &os)
virtual Theorem arrayNotEq(const Theorem &e)=0
a /= b |- exists i. a[i] /= b[i]
size_t size() const
Definition: expr_map.h:306
ArrayProofRules * createProofRules()
virtual Theorem rewriteReadWrite(const Expr &e)=0
Theorem renameExpr(const Expr &e)
Derived rule to create a new name for an expression.
Definition: theory.cpp:935
Op getOp() const
Get operator from expression.
Definition: expr.h:1183
const Expr & getExpr() const
Definition: type.h:52
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
e1 AND (e1 IFF e2) ==> e2
Definition: theory.h:714
virtual void assignValue(const Expr &t, const Expr &val)
Assigns t a concrete value val. Used in model generation.
Definition: theory.cpp:162
const_iterator end() const
Definition: cdlist.h:91
bool isNot() const
Definition: expr.h:420
bool isClosure() const
Definition: expr.h:1007
CommonProofRules * getCommonRules()
Get a pointer to common proof rules.
Definition: theory.h:96
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
virtual Theorem rewriteRedundantWrite2(const Expr &e)=0
Theorem solve(const Theorem &e)
An optional solver.
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Definition: kinds.h:44
bool d_theoryUsed
Definition: theory.h:79
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Definition: theory.cpp:81
Identifier is (ID (STRING_EXPR "name"))
Definition: kinds.h:46
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
Expr enumerateFinite(Unsigned n) const
Return nth (starting with 0) element in a finite type.
Definition: type.h:68
virtual Theorem rewriteRedundantWrite1(const Theorem &v_eq_r, const Expr &write)=0
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Definition: expr.h:1196
const Theorem & getSig() const
Definition: expr.h:1560
static int left(int i)
Definition: minisat_heap.h:53
const Theorem & getRep() const
Definition: expr.h:1569
void newKind(int kind, const std::string &name, bool isType=false)
Register a new kind.
bool isBoolConst() const
Definition: expr.h:357
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
const Expr & getBody() const
Get the body of the closure Expr.
Definition: expr.h:1069
std::string int2string(int n)
Definition: cvc_util.h:46
Expr simplifyExpr(const Expr &e)
Simplify a term e w.r.t. the current context.
Definition: theory.h:430
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
const Expr & getRHS() const
Definition: theorem.cpp:246
Expr findExpr(const Expr &e)
Return the find of e, or e if it has no find.
Definition: theory.h:503
const Theorem & findRef(const Expr &e)
Return the find as a reference: expr must have a find.
Definition: theory.cpp:295
Theorem getModelValue(const Expr &e)
Fetch the concrete assignment to the variable during model generation.
Definition: theory.cpp:541
Expr getTypePred(const Type &t, const Expr &e)
Calls the correct theory to compute a type predicate.
Definition: theory.cpp:406
std::string toString() const
Definition: type.h:80
iterator begin()
iterators
Definition: hash_set.h:224
#define IF_DEBUG(code)
Definition: debug.h:406
Expr addBoundVar(const std::string &name, const Type &type)
Create and add a new bound variable to the stack, for parseExprOp().
Definition: theory.cpp:709
unsigned size() const
Definition: cdlist.h:64
Expr getExpr() const
Definition: theorem.cpp:230
bool isNull() const
Definition: theorem.h:164
std::pair< iterator, bool > insert(const value_type &entry)
Definition: hash_set.h:173
static Type anyType(ExprManager *em)
Definition: type.h:74
bool isArray(const Type &t)
Definition: theory_array.h:109
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
CDMap< Expr, Expr > d_sharedSubterms
Backtracking database of subterms of shared terms.
Definition: theory_array.h:63
ExprStream & popdag(ExprStream &os)
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
virtual Theorem readArrayLiteral(const Expr &e)=0
Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg)
Theorem updateHelper(const Expr &e)
Update the children of the term e.
Definition: theory.cpp:417
CDList< Expr > d_sharedSubtermsList
Backtracking database of subterms of shared terms.
Definition: theory_array.h:65
Theorem pullIndex(const Expr &e, const Expr &index)
Derived rule.
void setType(const Type &t) const
Set the cached type.
Definition: expr.h:1427
static int right(int i)
Definition: minisat_heap.h:54
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
Definition: theory.cpp:383
CDList< Expr > d_reads
Backtracking list of array reads, for building concrete models.
Definition: theory_array.h:54
virtual bool inconsistent()
Check if the current context is inconsistent.
Definition: theory.cpp:97
bool isVar() const
Definition: expr.h:1005
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
An exception to be thrown by the smtlib translator.
An exception to be thrown by the smtlib translator.
ArrayProofRules * d_rules
Definition: theory_array.h:51
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Definition: expr.h:1062
SMT-LIB format.
Definition: lang.h:34
Unsigned sizeFinite() const
Return size of a finite type; returns 0 if size cannot be determined.
Definition: type.h:70
iterator end()
Definition: hash_set.h:235
bool isRefl() const
Definition: theorem.h:171
virtual Theorem rewriteUsingSymmetry(const Expr &a1_eq_a2)=0
const Expr & getLHS() const
Definition: theorem.cpp:240
virtual Theorem interchangeIndices(const Expr &e)=0
Definition: kinds.h:81
bool isRead(const Expr &e)
Definition: theory_array.h:110
void checkType(const Expr &e)
Check that e is a valid Type expr.
Theorem rewriteIte(const Expr &e)
Derived rule for rewriting ITE.
Definition: theory.cpp:923
void invalidateSimpCache()
Invalidate the simplifier's cache tag.
Definition: expr_manager.h:341
Definition: kinds.h:61
const_iterator begin() const
Definition: cdlist.h:88
Theorem reflexivityRule(const Expr &a)
==> a == a
Definition: theory.h:673
Theorem substitutivityRule(const Op &op, const std::vector< Theorem > &thms)
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Definition: theory.h:686
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
Definition: kinds.h:99
bool hasRep() const
Definition: expr.h:1554
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Definition: theory.cpp:252
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
InputLanguage lang() const
Get the current output language.
Definition: expr_stream.h:165
bool isFunction() const
Definition: type.h:62
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
void setNotArrayNormalized() const
Definition: expr.h:1488
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
iterator end()
Definition: expr_map.h:191
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
Definition: theory.cpp:310
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
int d_inCheckSat
Flag for use in checkSat.
Definition: theory_array.h:72
const bool & d_applicationsInModel
Flag to include array reads to the concrete model.
Definition: theory_array.h:58
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Definition: theory.h:681
Theorem symmetryRule(const Theorem &a1_eq_a2)
a1 == a2 ==> a2 == a1
Definition: theory.h:677
Nice SAL-like language for manually written specs.
Definition: lang.h:32
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
iterator end()
Definition: expr_map.h:326
iterator end() const
End iterator.
Definition: expr.h:1217