From cbc5adb5d4f131ea6bf9a40b0c27fecf67353b4d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 5 Jul 2016 17:55:25 -0500 Subject: [PATCH] Refactor last call for theories, only create one model when quantifiers are enabled. Fix sep.nil preregistration in TheorySep. --- src/theory/sep/theory_sep.cpp | 18 +++++++++- src/theory/sep/theory_sep.h | 4 +++ src/theory/theory.h | 6 +++- src/theory/theory_engine.cpp | 49 +++++++++++++++----------- src/theory/theory_engine.h | 1 + test/regress/regress0/sep/Makefile.am | 3 +- test/regress/regress0/sep/trees-1.smt2 | 41 +++++++++++++++++++++ 7 files changed, 99 insertions(+), 23 deletions(-) create mode 100644 test/regress/regress0/sep/trees-1.smt2 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 ) { 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 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_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 */ diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index 9d2abaa18..9744cae99 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -53,7 +53,8 @@ TESTS = \ dispose-list-4-init.smt2 \ wand-0526-sat.smt2 \ quant_wand.smt2 \ - fmf-nemp-2.smt2 + fmf-nemp-2.smt2 \ + trees-1.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2 new file mode 100644 index 000000000..88e875f70 --- /dev/null +++ b/test/regress/regress0/sep/trees-1.smt2 @@ -0,0 +1,41 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-sort Loc 0) +(declare-const loc0 Loc) + +(declare-datatypes () ((Node (node (data Int) (left Loc) (right Loc))))) + +(declare-const dv Int) +(declare-const v Loc) + +(declare-const dl Int) +(declare-const l Loc) +(declare-const dr Int) +(declare-const r Loc) + +(define-fun ten-tree0 ((x Loc) (d Int)) Bool +(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (emp loc0) (= l (as sep.nil Loc))) (and (emp loc0) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10))))) + +(declare-const dy Int) +(declare-const y Loc) +(declare-const dz Int) +(declare-const z Loc) + +(define-fun ord-tree0 ((x Loc) (d Int)) Bool +(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (emp loc0) (= y (as sep.nil Loc))) (and (emp loc0) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz)))) + +;------- f ------- +(assert (= y (as sep.nil Loc))) +(assert (= z (as sep.nil Loc))) + +(assert (= dy dv)) +(assert (= dz (+ dv 10))) +;----------------- + +(assert (not (= v (as sep.nil Loc)))) + +(assert (ten-tree0 v dv)) +(assert (not (ord-tree0 v dv))) + +(check-sat) -- 2.30.2