summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/sep/theory_sep.cpp18
-rw-r--r--src/theory/sep/theory_sep.h4
-rw-r--r--src/theory/theory.h6
-rw-r--r--src/theory/theory_engine.cpp49
-rw-r--r--src/theory/theory_engine.h1
-rw-r--r--test/regress/regress0/sep/Makefile.am3
-rw-r--r--test/regress/regress0/sep/trees-1.smt241
7 files changed, 99 insertions, 23 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
*/
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback