CVC3
|
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 }