summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp193
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({
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback