46 { d_se->addFact(thm); }
48 {
return d_se->newIntAssumption(assump); }
50 { d_se->addSplitter(e, priority); }
51 virtual bool check(
const Expr& e);
54 bool CoreSatAPI_implBase::check(
const Expr& e)
57 int scope = d_se->theoryCore()->getCM()->scopeLevel();
58 d_se->theoryCore()->getCM()->push();
60 d_se->theoryCore()->getCM()->popto(scope);
75 SearchImplBase::Splitter::Splitter(
const Literal& lit): d_lit(lit) {
84 TRACE(
"Splitter",
"Splitter[copy](",
d_lit,
")");
90 if(
this == &s)
return *
this;
94 TRACE(
"Splitter",
"Splitter[assign](", d_lit,
")");
101 TRACE(
"Splitter",
"~Splitter(", d_lit,
")");
113 d_cnfCache(core->getCM()->getCurrentContext()),
114 d_cnfVars(core->getCM()->getCurrentContext()),
124 core->
getFlags()[
"mm"].getString());
144 IF_DEBUG(
if(debugger.trace(
"search verbose")) {
145 ostream& os(debugger.getOS());
146 os <<
"d_assumptions = [";
149 debugger.getOS() <<
"(" << (*i).first <<
" => " << (*i).second <<
"), ";
154 TRACE(
"search verbose",
"newUserAssumption(", e,
155 "): assumption already exists");
160 TRACE(
"search verbose",
"newUserAssumption(", thm,
161 "): created new assumption");
184 TRACE(
"search verbose",
"newIntAssumption(", thm,
185 "): new assumption");
193 if ((*i).first.isUserAssumption()) assumptions.push_back((*i).first);
201 if ((*i).first.isIntAssumption()) assumptions.push_back((*i).first);
209 assumptions.push_back((*i).first);
219 TRACE(
"addCNFFact",
"addCNFFact(", thm.
getExpr(),
") {");
227 TRACE_MSG(
"addCNFFact",
"addCNFFact => }");
232 TRACE(
"search addFact",
"SearchImplBase::addFact(", thm.
getExpr(),
") {");
237 TRACE_MSG(
"search addFact",
"SearchImplBase::addFact => }");
251 (
"Method getCounterExample() (or command COUNTEREXAMPLE) cannot be used\n"
252 " without assumptions activated");
255 (
"Method getCounterExample() (or command COUNTEREXAMPLE)\n"
256 " must be called only after failed QUERY");
286 (
"DUMP_PROOF cannot be used without proofs activated");
289 (
"DUMP_PROOF must be called only after successful QUERY");
301 (
"DUMP_ASSUMPTIONS cannot be used without assumptions activated");
304 (
"DUMP_ASSUMPTIONS must be called only after successful QUERY");
321 "processResult: bad input"
361 TRACE(
"mycnf",
"enqueueCNF(", beta,
") {");
374 TRACE(
"mycnf",
"enqueueCNFrec(", theta.
getExpr(),
") { ");
375 TRACE(
"cnf-clauses",
"enqueueCNF call", theta.
getExpr(),
"");
385 TRACE_MSG(
"mycnf",
"enqueueCNFrec[cached] => }");
392 while(thetaExpr.isNot() && thetaExpr[0].isNot()) {
400 if(thetaExpr.isPropLiteral()) {
403 "Must be a literal: theta = "
406 TRACE_MSG(
"mycnf",
"enqueueCNFrec[literal] => }");
407 TRACE(
"cnf-clauses",
"literal with proofs(", theta.
getExpr(),
")");
413 switch(thetaExpr.getKind()) {
416 for(
int i=0; i<thetaExpr.arity(); i++)
418 TRACE_MSG(
"mycnf",
"enqueueCNFrec[AND] => }");
426 i!=iend && cnf; i++) {
427 if(!(*i).isPropLiteral())
431 vector<Theorem> thms;
432 vector<unsigned int> changed;
439 changed.push_back(cc);
442 if(changed.size() > 0) {
448 TRACE_MSG(
"mycnf",
"enqueueCNFrec[cnf] => }");
454 const Expr& t0 = thetaExpr[0];
455 const Expr& t1 = thetaExpr[1];
461 }
else if(thetaExpr[0].isPropLiteral()) {
471 if(thetaExpr[0].isPropLiteral() && thetaExpr[1].isPropLiteral()
472 && thetaExpr[2].isPropLiteral()) {
474 vector<Theorem> thms;
475 vector<unsigned int> changed;
476 for(
int c=0, cend=thetaExpr.arity(); c<cend; ++c) {
482 changed.push_back(c);
485 if(changed.size() > 0) {
493 "enqueueCNFrec [ITE over literals]\n thm = "
510 TRACE(
"cnf-clauses",
"enqueueCNFrec call[cache hit]:(",
513 TRACE_MSG(
"mycnf",
"enqueueCNFrec[cached] => }");
522 TRACE(
"mycnf",
"enqueueCNFrec: varIntroSkolem => ", result.
getExpr(),
528 TRACE(
"mycnf",
"enqueueCNFrec: skolemize => ", result.
getExpr(),
532 "SearchImplBase::CNF(): result = "+result.
toString());
535 "SearchImplBase::CNF(): result = "+result.
toString());
537 "SearchImplBase::CNF(): result = "+result.
toString()
544 TRACE(
"mycnf",
"enqueueCNFrec: theta = ", theta.
getExpr(),
547 TRACE(
"mycnf",
"enqueueCNFrec: var = ", var.getExpr(),
550 DebugAssert(var.isAbsLiteral(),
"var = "+var.getExpr().toString());
555 TRACE_MSG(
"mycnf",
"enqueueCNFrec => }");
564 TRACE(
"mycnf",
"applyCNFRules(", thm.
getExpr(),
") { ");
568 "SearchImplBase::applyCNFRules: input must be an iff: " +
569 result.getExpr().toString());
570 Expr lhs = result.getLHS();
571 Expr rhs = result.getRHS();
573 "SearchImplBase::applyCNFRules: rhs of input must be literal: " +
574 result.getExpr().toString());
577 while(result.getLHS().isNot())
580 rhs = result.getRHS();
586 TRACE_MSG(
"mycnf",
"applyCNFRules[temp cache] => }");
591 if(lhs.isPropLiteral()) {
592 if(!lhs.isAbsLiteral()) {
597 "applyCNFRules [literal lhs]\n result = "
603 "applyCNFRules [literal lhs]\n thm = "
611 vector<unsigned> changed;
612 vector<Theorem> substitutions;
614 for(
Expr::iterator j = lhs.begin(), jend = lhs.end(); j!=jend; ++c,++j) {
615 const Expr& phi = *j;
624 "SearchImplBase::applyCNFRules: result = " +
627 "SearchImplBase::applyCNFRules:\n phi = " +
629 +
"\n\n phiIffVar = " + phiIffVar.
toString());
631 "SearchImplBase::applyCNFRules: phiIffVar = " +
633 changed.push_back(c);
634 substitutions.push_back(phiIffVar);
638 if(changed.size() > 0) {
645 switch(result.getLHS().getKind()) {
663 "SearchImplBase::applyCNFRules: "
664 "the input operator must be and|or|iff|imp|ite\n result = " +
665 result.getLHS().toString());
679 for(
int i=0, iend=clauses.
getExpr().
arity(); i<iend; ++i) {
689 if(!e.
isOr())
return false;
693 cnf = (*i).isAbsLiteral();
701 if(!e.
isOr())
return false;
705 cnf = (*i).isPropLiteral();
713 TRACE(
"isGoodSplitter",
"isGoodSplitter(", e,
") {");
717 TRACE(
"isGoodSplitter",
"isGoodSplitter => ", res?
"true" :
"false",
" }");
730 "SearchImplBase::addToCNFCache: input must be an iff: " +
751 TRACE(
"mycnf",
"findInCNFCache(", e,
") { ");
757 phi = phi[0]; numNegs++;
766 "SearchImplBase::findInCNFCache: thm must be an iff: " +
772 if(numNegs % 2 != 0) {
776 for(; numNegs > 0; numNegs-=2) {
782 TRACE(
"mycnf",
"findInCNFCache => ", thm.
getExpr(),
" }");
785 TRACE_MSG(
"mycnf",
"findInCNFCache => null }");
805 TRACE(
"replaceITE",
"replaceITE(", e,
") { ");
811 TRACE(
"replaceITE",
"replaceITE[cached] => ", (*i).second,
" }");
844 TRACE(
"replaceITE",
"replaceITE => ", res,
" }");