diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 193 |
1 files changed, 133 insertions, 60 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 881acdddd..94281156f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -83,33 +83,8 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma, ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - LemmaProofRecipe* proofRecipe = NULL; PROOF({ - // Theory lemmas have one step that proves the empty clause - proofRecipe = new LemmaProofRecipe; - - Node emptyNode; - LemmaProofRecipe::ProofStep proofStep(d_theory, emptyNode); - - Node rewritten; - if (lemma.getKind() == kind::OR) { - for (unsigned i = 0; i < lemma.getNumChildren(); ++i) { - rewritten = theory::Rewriter::rewrite(lemma[i]); - if (rewritten != lemma[i]) { - proofRecipe->addRewriteRule(lemma[i].negate(), rewritten.negate()); - } - proofStep.addAssertion(lemma[i]); - proofRecipe->addBaseAssertion(rewritten); - } - } else { - rewritten = theory::Rewriter::rewrite(lemma); - if (rewritten != lemma) { - proofRecipe->addRewriteRule(lemma.negate(), rewritten.negate()); - } - proofStep.addAssertion(lemma); - proofRecipe->addBaseAssertion(rewritten); - } - proofRecipe->addStep(proofStep); + registerLemmaRecipe(lemma, lemma, preprocess, d_theory); }); theory::LemmaStatus result = d_engine->lemma(lemma, @@ -117,22 +92,101 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma, false, removable, preprocess, - sendAtoms ? d_theory : theory::THEORY_LAST, - proofRecipe); - PROOF(delete proofRecipe;); + sendAtoms ? d_theory : theory::THEORY_LAST); return result; } +void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, theory::TheoryId theoryId) { + // During CNF conversion, conjunctions will be broken down into + // multiple lemmas. In order for the recipes to match, we have to do + // the same here. + NodeManager* nm = NodeManager::currentNM(); + + if (preprocess) + lemma = d_engine->preprocess(lemma); + + bool negated = (lemma.getKind() == kind::NOT); + Node nnLemma = negated ? lemma[0] : lemma; + + switch (nnLemma.getKind()) { + + case kind::AND: + if (!negated) { + for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) + registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId); + } else { + NodeBuilder<> builder(kind::OR); + for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) + builder << nnLemma[i].negate(); + + Node disjunction = (builder.getNumChildren() == 1) ? builder[0] : builder; + registerLemmaRecipe(disjunction, originalLemma, false, theoryId); + } + break; + + case kind::IFF: + if (!negated) { + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId); + } else { + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId); + } + break; + + case kind::ITE: + if (!negated) { + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2]), originalLemma, false, theoryId); + } else { + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2].negate()), originalLemma, false, theoryId); + } + break; + + default: + break; + } + + // Theory lemmas have one step that proves the empty clause + LemmaProofRecipe proofRecipe; + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode); + + // Remember the original lemma, so we can report this later when asked to + proofRecipe.setOriginalLemma(originalLemma); + + // Record the assertions and rewrites + Node rewritten; + if (lemma.getKind() == kind::OR) { + for (unsigned i = 0; i < lemma.getNumChildren(); ++i) { + rewritten = theory::Rewriter::rewrite(lemma[i]); + if (rewritten != lemma[i]) { + proofRecipe.addRewriteRule(lemma[i].negate(), rewritten.negate()); + } + proofStep.addAssertion(lemma[i]); + proofRecipe.addBaseAssertion(rewritten); + } + } else { + rewritten = theory::Rewriter::rewrite(lemma); + if (rewritten != lemma) { + proofRecipe.addRewriteRule(lemma.negate(), rewritten.negate()); + } + proofStep.addAssertion(lemma); + proofRecipe.addBaseAssertion(rewritten); + } + proofRecipe.addStep(proofStep); + ProofManager::getCnfProof()->setProofRecipe(&proofRecipe); +} + theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma(TNode lemma, bool removable) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - - LemmaProofRecipe* proofRecipe = NULL; Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl; - theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, proofRecipe); + theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory); return result; } @@ -157,6 +211,14 @@ void TheoryEngine::finishInit() { // initialize the quantifiers engine d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); + //initialize the model + if( d_logicInfo.isQuantified() ) { + d_curr_model = d_quantEngine->getModel(); + } else { + d_curr_model = new theory::TheoryModel(d_userContext, "DefaultModel", true); + d_aloc_curr_model = true; + } + if (d_logicInfo.isQuantified()) { d_quantEngine->finishInit(); Assert(d_masterEqualityEngine == 0); @@ -217,6 +279,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_masterEENotify(*this), d_quantEngine(NULL), d_curr_model(NULL), + d_aloc_curr_model(false), d_curr_model_builder(NULL), d_ppCache(), d_possiblePropagations(context), @@ -254,7 +317,6 @@ TheoryEngine::TheoryEngine(context::Context* context, } // build model information if applicable - d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true); d_curr_model_builder = new theory::TheoryEngineModelBuilder(this); smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime); @@ -281,7 +343,9 @@ TheoryEngine::~TheoryEngine() { } delete d_curr_model_builder; - delete d_curr_model; + if( d_aloc_curr_model ){ + delete d_curr_model; + } delete d_quantEngine; @@ -518,24 +582,30 @@ void TheoryEngine::check(Theory::Effort effort) { // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) { - //calls to theories requiring the model go here - //FIXME: this should not be theory-specific - if(d_logicInfo.isTheoryEnabled(THEORY_SEP)) { - Assert( d_theoryTable[THEORY_SEP]!=NULL ); - if( d_theoryTable[THEORY_SEP]->hasFacts() ){ - // must build model at this point - d_curr_model_builder->buildModel(getModel(), false); - d_theoryTable[THEORY_SEP]->check(Theory::EFFORT_LAST_CALL); + //checks for theories requiring the model go at last call + bool builtModel = false; + for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { + if( theoryId!=THEORY_QUANTIFIERS ){ + Theory* theory = d_theoryTable[theoryId]; + if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { + if( theory->needsCheckLastEffort() ){ + if( !builtModel ){ + builtModel = true; + d_curr_model_builder->buildModel(d_curr_model, false); + } + theory->check(Theory::EFFORT_LAST_CALL); + } + } } } if( ! d_inConflict && ! needCheck() ){ if(d_logicInfo.isQuantified()) { // quantifiers engine must pass effort last call check d_quantEngine->check(Theory::EFFORT_LAST_CALL); - // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built + // if returning incomplete or SAT, we have ensured that d_curr_model has been built with fullModel=true } else if(options::produceModels()) { // must build model at this point - d_curr_model_builder->buildModel(getModel(), true); + d_curr_model_builder->buildModel(d_curr_model, true); } Trace("theory::assertions-model") << endl; if (Trace.isOn("theory::assertions-model")) { @@ -611,8 +681,7 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; - LemmaProofRecipe* proofRecipe = NULL; - lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, proofRecipe); + lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory); // This code is supposed to force preference to follow what the theory models already have // but it doesn't seem to make a big difference - need to explore more -Clark @@ -780,16 +849,18 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){ } } +void TheoryEngine::postProcessModel( theory::TheoryModel* m ){ + for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) { + if(d_logicInfo.isTheoryEnabled(theoryId)) { + Trace("model-builder-debug") << " PostProcessModel on theory: " << theoryId << endl; + d_theoryTable[theoryId]->postProcessModel( m ); + } + } +} + /* get model */ TheoryModel* TheoryEngine::getModel() { - Debug("model") << "TheoryEngine::getModel()" << endl; - if( d_logicInfo.isQuantified() ) { - Debug("model") << "Get model from quantifiers engine." << endl; - return d_quantEngine->getModel(); - } else { - Debug("model") << "Get default model." << endl; - return d_curr_model; - } + return d_curr_model; } bool TheoryEngine::presolve() { @@ -1596,8 +1667,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, - theory::TheoryId atomsTo, - LemmaProofRecipe* proofRecipe) { + theory::TheoryId atomsTo) { // For resource-limiting (also does a time check). // spendResource(); @@ -1647,10 +1717,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } // assert to prop engine - d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, proofRecipe, node); + d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); - d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, proofRecipe, node); + d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node); } // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. @@ -1709,10 +1779,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { // Process the explanation getExplanation(explanationVector, proofRecipe); + PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); Node fullConflict = mkExplanation(explanationVector); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); - lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe); + lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST); } else { // When only one theory, the conflict should need no processing @@ -1738,9 +1809,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { proofRecipe->getStep(0)->addAssertion(conflict.negate()); proofRecipe->addBaseAssertion(conflict.negate()); } + + ProofManager::getCnfProof()->setProofRecipe(proofRecipe); }); - lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe); + lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST); } PROOF({ |