CVC3

theory_datatype_lazy.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file theory_datatype_lazy.cpp
00004  *
00005  * Author: Clark Barrett
00006  *
00007  * Created: Wed Dec  1 22:32:26 2004
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 
00022 #include "theory_datatype_lazy.h"
00023 #include "datatype_proof_rules.h"
00024 #include "typecheck_exception.h"
00025 #include "parser_exception.h"
00026 #include "smtlib_exception.h"
00027 #include "theory_core.h"
00028 #include "theory_uf.h"
00029 #include "command_line_flags.h"
00030 
00031 
00032 using namespace std;
00033 using namespace CVC3;
00034 
00035 
00036 ///////////////////////////////////////////////////////////////////////////////
00037 // TheoryDatatypeLazy Public Methods                                             //
00038 ///////////////////////////////////////////////////////////////////////////////
00039 
00040 
00041 TheoryDatatypeLazy::TheoryDatatypeLazy(TheoryCore* core)
00042   : TheoryDatatype(core),
00043     d_processQueue(core->getCM()->getCurrentContext()),
00044     d_processQueueKind(core->getCM()->getCurrentContext()),
00045     d_processIndex(core->getCM()->getCurrentContext(), 0),
00046     d_typeComplete(core->getCM()->getCurrentContext(), false)
00047 { }
00048 
00049 
00050 void TheoryDatatypeLazy::instantiate(const Expr& e, const Unsigned& u)
00051 {
00052   DebugAssert(e.hasFind() && findExpr(e) == e,
00053               "datatype: instantiate: Expected find(e)=e");
00054   if (isConstructor(e) || e.isTranslated()) return;
00055   DebugAssert(u != 0 && (u & (u-1)) == 0,
00056               "datatype: instantiate: Expected single label in u");
00057   DebugAssert(d_datatypes.find(e.getType().getExpr()) != d_datatypes.end(),
00058               "datatype: instantiate: Unexpected type: "+e.getType().toString()
00059               +"\n\n for expression: "+e.toString());
00060   ExprMap<unsigned>& c = d_datatypes[e.getType().getExpr()];
00061   ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end();
00062   for (; c_it != c_end; ++c_it) {
00063     if ((u & ((Unsigned)1 << unsigned((*c_it).second))) != 0) break;
00064   }
00065   DebugAssert(c_it != c_end,
00066               "datatype: instantiate: couldn't find constructor");
00067   Expr cons = (*c_it).first;
00068 
00069   if (!cons.isFinite() && !e.isSelected()) return;
00070 
00071   Type consType = cons.getType();
00072   if (consType.arity() == 1) {
00073     d_processQueue.push_back(d_rules->dummyTheorem(d_facts, e.eqExpr(cons)));
00074     d_processQueueKind.push_back(ENQUEUE);
00075     return;
00076   }
00077   // create vars
00078   vector<Expr> vars;
00079   for (int i = 0; i < consType.arity()-1; ++i) {
00080     vars.push_back(getEM()->newBoundVarExpr(consType[i]));
00081   }
00082   Expr e2 = getEM()->newClosureExpr(EXISTS, vars,
00083                                     e.eqExpr(Expr(cons.mkOp(), vars)));
00084   d_processQueue.push_back(d_rules->dummyTheorem(d_facts, e2));
00085   d_processQueueKind.push_back(ENQUEUE);
00086   e.setTranslated();
00087 }
00088 
00089 
00090 void TheoryDatatypeLazy::initializeLabels(const Expr& e, const Type& t)
00091 {
00092   DebugAssert(findExpr(e) == e,
00093               "datatype: initializeLabels: Expected find(e)=e");
00094   DebugAssert(d_datatypes.find(t.getExpr()) != d_datatypes.end(),
00095               "Unknown datatype: "+t.getExpr().toString());
00096   ExprMap<unsigned>& c = d_datatypes[t.getExpr()];
00097   DebugAssert(d_labels.find(e) == d_labels.end(),
00098               "datatype: initializeLabels: expected unlabeled expr");
00099   if (isConstructor(e)) {
00100     Expr cons = getConstructor(e);
00101     DebugAssert(c.find(cons) != c.end(),
00102                 "datatype: initializeLabels: Couldn't find constructor "
00103                 +cons.toString());
00104     unsigned position = c[cons];
00105     d_labels.insert(e,
00106       SmartCDO<Unsigned>(theoryCore()->getCM()->getCurrentContext(),
00107                             1 << position, 0));
00108   }
00109   else {
00110     DebugAssert(c.size() > 0, "No constructors?");
00111     Unsigned value = ((Unsigned)1 << unsigned(c.size())) - 1;
00112     d_labels.insert(e,
00113       SmartCDO<Unsigned>(theoryCore()->getCM()->getCurrentContext(),
00114                             value, 0));
00115     if (value == 1) instantiate(e, 1);
00116     else if (!d_typeComplete) {
00117       d_splitters.push_back(e);
00118     }
00119   }
00120 }
00121 
00122 
00123 void TheoryDatatypeLazy::mergeLabels(const Theorem& thm,
00124                                  const Expr& e1, const Expr& e2)
00125 {
00126   DebugAssert(e2.hasFind(),
00127               "datatype: mergeLabels: Expected hasFind(e2)");
00128   Theorem fthm = find(e2);
00129   const Expr& f = fthm.getRHS();
00130   DebugAssert(d_labels.find(e1) != d_labels.end() &&
00131               d_labels.find(f) != d_labels.end(),
00132               "mergeLabels: expr is not labeled");
00133   DebugAssert(e1.getType() == f.getType(), "Expected same type");
00134   Unsigned u = d_labels[f].get().get();
00135   Unsigned uNew = u & d_labels[e1].get().get();
00136   if (u != uNew) {
00137     if (e2 != f) d_facts.push_back(fthm);
00138     if (!thm.isNull()) d_facts.push_back(thm);
00139     d_labels[f].get().set(uNew);
00140     if (uNew == 0) {
00141       setInconsistent(d_rules->dummyTheorem(d_facts, falseExpr()));
00142       return;
00143     }
00144   }
00145   if (uNew != 0 && ((uNew - 1) & uNew) == 0) {
00146     instantiate(f, uNew);
00147   }
00148 }
00149 
00150 
00151 void TheoryDatatypeLazy::mergeLabels(const Theorem& thm, const Expr& e,
00152                                  unsigned position, bool positive)
00153 {
00154   DebugAssert(e.hasFind(),
00155               "datatype: mergeLabels2: Expected hasFind(e)");
00156   Theorem fthm = find(e);
00157   const Expr& f = fthm.getRHS();
00158   DebugAssert(d_labels.find(f) != d_labels.end(),
00159               "mergeLabels2: expr is not labeled");
00160   Unsigned u = d_labels[f].get().get();
00161   Unsigned uNew = (Unsigned)1 << position;
00162   if (positive) {
00163     uNew = u & uNew;
00164     if (u == uNew) return;
00165   } else if ((u & uNew) != 0) uNew = u - uNew;
00166   else return;
00167   if (e != f) d_facts.push_back(fthm);
00168   d_facts.push_back(thm);
00169   d_labels[f].get().set(uNew);
00170   if (uNew == 0)
00171     setInconsistent(d_rules->dummyTheorem(d_facts, falseExpr()));
00172   else if (((uNew - 1) & uNew) == 0) {
00173     instantiate(f, uNew);
00174   }
00175 }
00176 
00177 
00178 void TheoryDatatypeLazy::checkSat(bool fullEffort)
00179 {
00180   bool done = false;
00181   while (!done && d_splittersIndex < d_splitters.size()) {
00182     Expr e = d_splitters[d_splittersIndex];
00183     if (findExpr(e) == e) {
00184       DebugAssert(d_labels.find(e) != d_labels.end(),
00185                   "checkSat: expr is not labeled");
00186       Unsigned u = d_labels[e].get().get();
00187       if ((u & (u-1)) != 0) {
00188         done = true;
00189         DebugAssert(!d_splitterAsserted || !fullEffort,
00190                     "splitter should have been resolved");
00191         if (!d_splitterAsserted) {
00192           DebugAssert
00193             (d_datatypes.find(e.getType().getExpr()) != d_datatypes.end(),
00194              "datatype: checkSat: Unexpected type: "+e.getType().toString()
00195              +"\n\n for expression: "+e.toString());
00196           ExprMap<unsigned>& c = d_datatypes[e.getType().getExpr()];
00197           ExprMap<unsigned>::iterator c_it = c.begin(), c_end = c.end();
00198           for (; c_it != c_end; ++c_it) {
00199             if ((u & ((Unsigned)1 << unsigned((*c_it).second))) != 0) break;
00200           }
00201           DebugAssert(c_it != c_end,
00202               "datatype: checkSat: couldn't find constructor");
00203           addSplitter(datatypeTestExpr((*c_it).first.getName(), e));
00204           d_splitterAsserted = true;
00205         }
00206       }
00207     }
00208     if (!done) {
00209       d_splitterAsserted = false;
00210       d_splittersIndex = d_splittersIndex + 1;
00211     }
00212   }
00213   while (!done && d_processIndex < d_processQueue.size()) {
00214     d_typeComplete = true;
00215     Theorem e = d_processQueue[d_processIndex];
00216     int kind = d_processQueueKind[d_processIndex];
00217     switch (kind) {
00218       case MERGE1: {
00219         break;
00220       }
00221       case ENQUEUE:
00222         done = true;
00223         enqueueFact(e);
00224         break;
00225       case MERGE2: {
00226         const Expr& lhs = e.getLHS();
00227         const Expr& rhs = e.getRHS();
00228         Theorem thm(e);
00229         if (lhs.isSelected() && !rhs.isSelected()) {
00230           d_facts.push_back(e);
00231           rhs.setSelected();
00232           thm = Theorem();
00233         }
00234         mergeLabels(thm, lhs, rhs);
00235         break;
00236       }
00237       default:
00238         DebugAssert(false, "Unknown case");
00239     }
00240     d_processIndex = d_processIndex + 1;
00241   }
00242 }
00243 
00244 
00245 
00246 void TheoryDatatypeLazy::setup(const Expr& e)
00247 {
00248   if (e.getType().getExpr().getKind() == DATATYPE &&
00249       d_labels.find(e) == d_labels.end()) {
00250     initializeLabels(e, e.getType());
00251     e.addToNotify(this, Expr());
00252   }
00253   if (e.getKind() != APPLY) return;
00254   if (isConstructor(e) && e.arity() > 0) {
00255     d_processQueue.push_back(d_rules->noCycle(e));
00256     d_processQueueKind.push_back(ENQUEUE);
00257   }
00258   if (isSelector(e)) {
00259     e[0].setSelected();
00260     d_processQueue.push_back(reflexivityRule(e[0]));
00261     d_processQueueKind.push_back(MERGE2);
00262   }
00263   setupCC(e);
00264 }
00265 
00266 
00267 void TheoryDatatypeLazy::update(const Theorem& e, const Expr& d)
00268 {
00269   if (d.isNull()) {
00270     const Expr& lhs = e.getLHS();
00271     const Expr& rhs = e.getRHS();
00272     if (isConstructor(lhs) && isConstructor(rhs) &&
00273         lhs.isApply() && rhs.isApply() &&
00274         lhs.getOpExpr() == rhs.getOpExpr()) {
00275       d_processQueue.push_back(d_rules->decompose(e));
00276       d_processQueueKind.push_back(ENQUEUE);
00277     }
00278     else {
00279       d_processQueue.push_back(e);
00280       d_processQueueKind.push_back(MERGE2);
00281     }
00282   }
00283   else {
00284     const Theorem& dEQdsig = d.getSig();
00285     if (!dEQdsig.isNull()) {
00286       const Expr& dsig = dEQdsig.getRHS();
00287       Theorem thm = updateHelper(d);
00288       const Expr& sigNew = thm.getRHS();
00289       if (sigNew == dsig) return;
00290       dsig.setRep(Theorem());
00291       if (isSelector(sigNew) && canCollapse(sigNew)) {
00292         d.setSig(Theorem());
00293         d_processQueue.push_back(transitivityRule(thm, d_rules->rewriteSelCons(d_facts, sigNew)));
00294         d_processQueueKind.push_back(ENQUEUE);
00295       }
00296       else if (isTester(sigNew) && isConstructor(sigNew[0])) {
00297         d.setSig(Theorem());
00298         d_processQueue.push_back(transitivityRule(thm, d_rules->rewriteTestCons(sigNew)));
00299         d_processQueueKind.push_back(ENQUEUE);
00300       }
00301       else {
00302         const Theorem& repEQsigNew = sigNew.getRep();
00303         if (!repEQsigNew.isNull()) {
00304           d.setSig(Theorem());
00305           d_processQueue.push_back(transitivityRule(repEQsigNew, symmetryRule(thm)));
00306           d_processQueueKind.push_back(ENQUEUE);
00307         }
00308         else {
00309           int k, ar(d.arity());
00310           for (k = 0; k < ar; ++k) {
00311             if (sigNew[k] != dsig[k]) {
00312               sigNew[k].addToNotify(this, d);
00313             }
00314           }
00315           d.setSig(thm);
00316           sigNew.setRep(thm);
00317           getEM()->invalidateSimpCache();
00318         }
00319       }
00320     }
00321   }
00322 }