diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 18 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.h | 4 | ||||
-rw-r--r-- | src/theory/theory.h | 6 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 49 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 1 |
5 files changed, 56 insertions, 22 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 836a04afa..605537c2d 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -93,6 +93,7 @@ Node TheorySep::ppRewrite(TNode term) { //must process assertions at preprocess so that quantified assertions are processed properly void TheorySep::processAssertions( std::vector< Node >& assertions ) { + d_pp_nils.clear(); std::map< Node, bool > visited; for( unsigned i=0; i<assertions.size(); i++ ){ processAssertion( assertions[i], visited ); @@ -102,7 +103,11 @@ void TheorySep::processAssertions( std::vector< Node >& assertions ) { void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) { if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){ + if( n.getKind()==kind::SEP_NIL ){ + if( std::find( d_pp_nils.begin(), d_pp_nils.end(), n )==d_pp_nils.end() ){ + d_pp_nils.push_back( n ); + } + }else if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){ //get the reference type (will compute d_type_references) int card = 0; TypeNode tn = getReferenceType( n, card ); @@ -307,6 +312,13 @@ void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ) void TheorySep::presolve() { Trace("sep-pp") << "Presolving" << std::endl; //TODO: cleanup if incremental? + + //we must preregister all instances of sep.nil to ensure they are made equal + for( unsigned i=0; i<d_pp_nils.size(); i++ ){ + std::map< TNode, bool > visited; + preRegisterTermRec( d_pp_nils[i], visited ); + } + d_pp_nils.clear(); } @@ -773,6 +785,10 @@ void TheorySep::check(Effort e) { } +bool TheorySep::needsCheckLastEffort() { + return hasFacts(); +} + Node TheorySep::getNextDecisionRequest() { for( unsigned i=0; i<d_neg_guards.size(); i++ ){ Node g = d_neg_guards[i]; diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 852a36721..2c87e79f9 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -50,6 +50,8 @@ class TheorySep : public Theory { /** True node for predicates = false */ Node d_false; + + std::vector< Node > d_pp_nils; Node mkAnd( std::vector< TNode >& assumptions ); @@ -126,6 +128,8 @@ class TheorySep : public Theory { void check(Effort e); + bool needsCheckLastEffort(); + private: // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module diff --git a/src/theory/theory.h b/src/theory/theory.h index e8518b1f6..81062d67a 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -565,7 +565,11 @@ public: * - or call get() until done() is true. */ virtual void check(Effort level = EFFORT_FULL) { } - + + /** + * Needs last effort check? + */ + virtual bool needsCheckLastEffort() { return false; } /** * T-propagate new literal assignments in the current context. */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 881acdddd..f6894e07b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -156,6 +156,14 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf) 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(); @@ -217,6 +225,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 +263,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 +289,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 +528,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")) { @@ -782,14 +798,7 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){ /* 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() { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 53c4aac77..c126e89ad 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -183,6 +183,7 @@ class TheoryEngine { * Default model object */ theory::TheoryModel* d_curr_model; + bool d_aloc_curr_model; /** * Model builder object */ |