diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-12 18:30:15 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-12 18:30:15 +0000 |
commit | 65798541fa437278cde0c759ab70fd9fa4fe9638 (patch) | |
tree | 27341327b8159e58a5ce6371bede6129bf67beb3 /src/theory/theory_engine.cpp | |
parent | 78d8b3ce56a1fd243acb54d2aaaf6d716e3b9788 (diff) |
merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 149 |
1 files changed, 83 insertions, 66 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 50682f647..872924385 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -35,8 +35,11 @@ #include "util/node_visitor.h" #include "util/ite_removal.h" +#include "theory/model.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/theory_quantifiers.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/first_order_model.h" using namespace std; @@ -53,6 +56,8 @@ TheoryEngine::TheoryEngine(context::Context* context, d_logicInfo(logicInfo), d_sharedTerms(this, context), d_quantEngine(NULL), + d_curr_model(NULL), + d_curr_model_builder(NULL), d_ppCache(), d_possiblePropagations(context), d_hasPropagated(context), @@ -80,6 +85,10 @@ TheoryEngine::TheoryEngine(context::Context* context, // initialize the quantifiers engine d_quantEngine = new QuantifiersEngine(context, this); + //build model information if applicable + d_curr_model = new theory::DefaultModel( context, "DefaultModel" ); + d_curr_model_builder = new theory::TheoryEngineModelBuilder( this ); + Rewriter::init(); StatisticsRegistry::registerStat(&d_combineTheoriesTime); d_true = NodeManager::currentNM()->mkConst<bool>(true); @@ -175,7 +184,7 @@ void TheoryEngine::dumpAssertions(const char* tag) { Dump(tag) << CommentCommand("Completeness check"); Dump(tag) << PushCommand(); - // Dump the shared terms + // Dump the shared terms if (d_logicInfo.isSharingEnabled()) { Dump(tag) << CommentCommand("Shared terms"); context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); @@ -186,14 +195,14 @@ void TheoryEngine::dumpAssertions(const char* tag) { } } - // Dump the assertions + // Dump the assertions Dump(tag) << CommentCommand("Assertions"); context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); for (; it != it_end; ++ it) { // Get the assertion Node assertionNode = (*it).assertion; // Purify all the terms - + BoolExpr assertionExpr(assertionNode.toExpr()); if ((*it).isPreregistered) { Dump(tag) << CommentCommand("Preregistered"); @@ -223,24 +232,24 @@ void TheoryEngine::dumpAssertions(const char* tag) { continue; } - // Check equality + // Check equality Dump(tag) << PushCommand(); BoolExpr eqExpr(equality.toExpr()); Dump(tag) << AssertCommand(eqExpr); - Dump(tag) << CheckSatCommand(); + Dump(tag) << CheckSatCommand(); Dump(tag) << PopCommand(); - // Check disequality + // Check disequality Dump(tag) << PushCommand(); BoolExpr diseqExpr(disequality.toExpr()); Dump(tag) << AssertCommand(diseqExpr); - Dump(tag) << CheckSatCommand(); - Dump(tag) << PopCommand(); + Dump(tag) << CheckSatCommand(); + Dump(tag) << PopCommand(); } } } } - + Dump(tag) << PopCommand(); } } @@ -297,8 +306,8 @@ void TheoryEngine::check(Theory::Effort effort) { // If in full effort, we have a fake new assertion just to jumpstart the checking if (Theory::fullEffort(effort)) { d_factsAsserted = true; - } - + } + // Check until done while (d_factsAsserted && !d_inConflict && !d_lemmasAdded) { @@ -335,17 +344,22 @@ 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_logicInfo.isQuantified() && ! d_inConflict && ! d_lemmasAdded ) { - ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->performCheck(Theory::EFFORT_LAST_CALL); - // if we have given up, then possibly flip decision - if(Options::current()->flipDecision) { - if(d_incomplete && !d_inConflict && !d_lemmasAdded) { - if( ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision() ) { - d_incomplete = false; + if( d_logicInfo.isQuantified() ){ + ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->performCheck(Theory::EFFORT_LAST_CALL); + // if we have given up, then possibly flip decision + if(Options::current()->flipDecision) { + if(d_incomplete && !d_inConflict && !d_lemmasAdded) { + if( ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision() ) { + d_incomplete = false; + } } } + //if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built + }else if( Options::current()->produceModels ){ + //must build model at this point + d_curr_model_builder->buildModel( d_curr_model ); } } @@ -354,8 +368,8 @@ void TheoryEngine::check(Theory::Effort effort) { } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::check() => conflict" << endl; } - - // If fulleffort, check all theories + + // If fulleffort, check all theories if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) { if (!d_inConflict && !d_lemmasAdded) { dumpAssertions("theory::fullcheck"); @@ -415,7 +429,7 @@ void TheoryEngine::combineTheories() { Node literal = value ? equality : equality.notNode(); Node normalizedLiteral = value ? normalizedEquality : normalizedEquality.notNode(); // We're sending the original literal back, backed by the normalized one - if (markPropagation(literal, normalizedLiteral, /* to */ carePair.theory, /* from */ THEORY_SAT_SOLVER)) { + if (markPropagation(literal, normalizedLiteral, /* to */ carePair.theory, /* from */ THEORY_SAT_SOLVER)) { // We assert it, and we know it's preregistereed if it's the same theory bool preregistered = Theory::theoryOf(literal) == carePair.theory; theoryOf(carePair.theory)->assertFact(literal, preregistered); @@ -427,7 +441,7 @@ void TheoryEngine::combineTheories() { } } } - + // We need to split on it Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl; lemma(equality.orNode(equality.notNode()), false, false); @@ -528,23 +542,26 @@ bool TheoryEngine::properExplanation(TNode node, TNode expl) const { return true; } -Node TheoryEngine::getValue(TNode node) { - kind::MetaKind metakind = node.getMetaKind(); - - // special case: prop engine handles boolean vars - if(metakind == kind::metakind::VARIABLE && node.getType().isBoolean()) { - return d_propEngine->getValue(node); +void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){ + //consult each theory to get all relevant information concerning the model + for( int i=0; i<theory::THEORY_LAST; i++ ){ + if( d_theoryTable[i] ){ + d_theoryTable[i]->collectModelInfo( m ); + } } +} - // special case: value of a constant == itself - if(metakind == kind::metakind::CONSTANT) { - return node; +/* get model */ +TheoryModel* TheoryEngine::getModel(){ + Debug("model") << "TheoryEngine::getModel()" << std::endl; + if( d_logicInfo.isQuantified() ){ + Debug("model") << "Get model from quantifiers engine." << std::endl; + return d_quantEngine->getModel(); + }else{ + Debug("model") << "Get default model." << std::endl; + return d_curr_model; } - - // otherwise ask the theory-in-charge - return theoryOf(node)->getValue(node); - -}/* TheoryEngine::getValue(TNode node) */ +} bool TheoryEngine::presolve() { @@ -777,7 +794,7 @@ bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, the // What and where it came from NodeTheoryPair toExplain(originalAssertion, fromTheoryId, d_propagationMapTimestamp); - // See if the theory already got this literal + // See if the theory already got this literal PropagationMap::const_iterator find = d_propagationMap.find(toAssert); if (find != d_propagationMap.end()) { // The theory already knows this @@ -796,11 +813,11 @@ bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, the void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) { - + Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << std::endl; - + Assert(toTheoryId != fromTheoryId); - + if (d_inConflict) { return; } @@ -813,7 +830,7 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, // We assert it, and we know it's preregistereed toTheory->assertFact(assertion, true); // Mark that we have more information - d_factsAsserted = true; + d_factsAsserted = true; } else { Assert(toTheoryId == THEORY_SAT_SOLVER); // Check for propositional conflict @@ -825,18 +842,18 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, } else { return; } - } + } d_propagatedLiterals.push_back(assertion); } return; } - + // Polarity of the assertion bool polarity = assertion.getKind() != kind::NOT; - + // Atom of the assertion TNode atom = polarity ? assertion : assertion[0]; - + // If sending to the shared terms database, it's also simple if (toTheoryId == THEORY_BUILTIN) { Assert(atom.getKind() == kind::EQUAL); @@ -845,11 +862,11 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, } return; } - - // Things from the SAT solver are already normalized, so they go + + // Things from the SAT solver are already normalized, so they go // directly to the apropriate theory if (fromTheoryId == THEORY_SAT_SOLVER) { - // We know that this is normalized, so just send it off to the theory + // We know that this is normalized, so just send it off to the theory if (markPropagation(assertion, assertion, toTheoryId, fromTheoryId)) { // We assert it, and we know it's preregistereed coming from the SAT solver directly theoryOf(toTheoryId)->assertFact(assertion, true); @@ -858,7 +875,7 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, } return; } - + // Propagations to the SAT solver are just enqueued for pickup by // the SAT solver later if (toTheoryId == THEORY_SAT_SOLVER) { @@ -898,14 +915,14 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, // Normalize to lhs < rhs if not a sat literal Assert(atom.getKind() == kind::EQUAL); Assert(atom[0] != atom[1]); - + Node normalizedAtom = atom; if (!d_propEngine->isSatLiteral(normalizedAtom)) { Node reverse = atom[1].eqNode(atom[0]); if (d_propEngine->isSatLiteral(reverse) || atom[0] > atom[1]) { normalizedAtom = reverse; - } - } + } + } Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode(); // Try and assert (note that we assert the non-normalized one) @@ -915,7 +932,7 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, // Assert away theoryOf(toTheoryId)->assertFact(normalizedAssertion, preregistered); d_factsAsserted = true; - } + } return; } @@ -923,7 +940,7 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, void TheoryEngine::assertFact(TNode literal) { Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << std::endl; - + d_propEngine->checkTime(); // If we're in conflict, nothing to do @@ -997,7 +1014,7 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { } if (theory != THEORY_BUILTIN) { // Assert to the shared terms database - assertToTheory(literal, /* to */ THEORY_BUILTIN, /* from */ theory); + assertToTheory(literal, /* to */ THEORY_BUILTIN, /* from */ theory); } } else { // Just send off to the SAT solver @@ -1075,7 +1092,7 @@ Node TheoryEngine::getExplanation(TNode node) { return explanation; } - // Initial thing to explain + // Initial thing to explain NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp); Assert(d_propagationMap.find(toExplain) != d_propagationMap.end()); // Create the workplace for explanations @@ -1084,9 +1101,9 @@ Node TheoryEngine::getExplanation(TNode node) { // Process the explanation getExplanation(explanationVector); Node explanation = mkExplanation(explanationVector); - + Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << std::endl; - + return explanation; } @@ -1131,7 +1148,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable if(!removable) { d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap); } - + // Mark that we added some lemmas d_lemmasAdded = true; @@ -1151,7 +1168,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << CheckSatCommand(conflict.toExpr()); } - + // In the multiple-theories case, we need to reconstruct the conflict if (d_logicInfo.isSharingEnabled()) { // Create the workplace for explanations @@ -1184,9 +1201,9 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector unsigned i = 0; // Index of the current literal we are processing unsigned j = 0; // Index of the last literal we are keeping - + while (i < explanationVector.size()) { - + // Get the current literal to explain NodeTheoryPair toExplain = explanationVector[i]; @@ -1196,7 +1213,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) { ++ i; continue; - } + } if (toExplain.node.getKind() == kind::NOT && toExplain.node[0].isConst() && !toExplain.node[0].getConst<bool>()) { ++ i; continue; @@ -1219,7 +1236,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector continue; } - // See if it was sent to the theory by another theory + // See if it was sent to the theory by another theory PropagationMap::const_iterator find = d_propagationMap.find(toExplain); if (find != d_propagationMap.end()) { // There is some propagation, check if its a timely one @@ -1244,10 +1261,10 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector explanationVector.push_back(newExplain); ++ i; } - + // Keep only the relevant literals explanationVector.resize(j); -} +} void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions) |