00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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
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 & (1 << Unsigned((*c_it).second))) 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
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 = (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 = 1 << Unsigned(position);
00162 if (positive) {
00163 uNew = u & uNew;
00164 if (u == uNew) return;
00165 } else if (u & uNew) 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 & (1 << Unsigned((*c_it).second))) 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 }