From c1f794f35cca4be9ad1ca0135806430d06101eb2 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Wed, 12 Mar 2014 13:53:22 -0400 Subject: testlemma regressions --- test/regress/regress0/sets/sets-testlemma-ints.smt2 | 8 ++++++++ test/regress/regress0/sets/sets-testlemma-reals.smt2 | 8 ++++++++ test/regress/regress0/sets/sets-testlemma.smt2 | 2 +- 3 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/sets/sets-testlemma-ints.smt2 create mode 100644 test/regress/regress0/sets/sets-testlemma-reals.smt2 (limited to 'test/regress') diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2 new file mode 100644 index 000000000..23bde47fd --- /dev/null +++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2 @@ -0,0 +1,8 @@ +; EXPECT: sat +(set-logic QF_UFLIA_SETS) +(set-info :status sat) +(declare-fun x () (Set Int)) +(declare-fun y () (Set Int)) +(assert (= x y)) +(check-sat) +(get-model) diff --git a/test/regress/regress0/sets/sets-testlemma-reals.smt2 b/test/regress/regress0/sets/sets-testlemma-reals.smt2 new file mode 100644 index 000000000..97ac5841a --- /dev/null +++ b/test/regress/regress0/sets/sets-testlemma-reals.smt2 @@ -0,0 +1,8 @@ +; EXPECT: sat +(set-logic QF_UFLRA_SETS) +(set-info :status sat) +(declare-fun x () (Set Real)) +(declare-fun y () (Set Real)) +(assert (not (= x y))) +(check-sat) +(get-model) diff --git a/test/regress/regress0/sets/sets-testlemma.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2 index 74ce72747..6f80b7147 100644 --- a/test/regress/regress0/sets/sets-testlemma.smt2 +++ b/test/regress/regress0/sets/sets-testlemma.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFBV_SETS) (set-info :status sat) (declare-fun x () (Set (_ BitVec 2))) (declare-fun y () (Set (_ BitVec 2))) -- cgit v1.2.3 From 705d2851e21fdac11005951f6a47a5446bc8e48b Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Tue, 11 Mar 2014 23:47:33 -0400 Subject: enable check-models for sets/ regressions --- test/regress/regress0/sets/error1.smt2 | 1 - test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 | 1 - test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 | 1 - .../regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 | 1 - .../regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 | 1 - test/regress/regress0/sets/sets-new.smt2 | 1 - test/regress/regress0/sets/sets-testlemma.smt2 | 1 - test/regress/regress0/sets/sets-union.smt2 | 2 +- test/regress/regress0/sets/union-1a-flip.smt2 | 2 +- test/regress/regress0/sets/union-1b-flip.smt2 | 2 +- test/regress/regress0/sets/union-2.smt2 | 1 - 11 files changed, 3 insertions(+), 11 deletions(-) (limited to 'test/regress') diff --git a/test/regress/regress0/sets/error1.smt2 b/test/regress/regress0/sets/error1.smt2 index c4b3dd551..1241b117f 100644 --- a/test/regress/regress0/sets/error1.smt2 +++ b/test/regress/regress0/sets/error1.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_UFLIA_SETS) (set-info :status sat) diff --git a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 index 290ee95d5..7a8661e4d 100644 --- a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 +++ b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 index bcc4c33da..0aa6c88ae 100644 --- a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 +++ b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 index 5a44c0344..35110d831 100644 --- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 index 67d64bd05..d0fda8b86 100644 --- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 index c85ae4837..accb09799 100644 --- a/test/regress/regress0/sets/sets-new.smt2 +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/sets/sets-testlemma.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2 index 6f80b7147..183f54242 100644 --- a/test/regress/regress0/sets/sets-testlemma.smt2 +++ b/test/regress/regress0/sets/sets-testlemma.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_UFBV_SETS) (set-info :status sat) diff --git a/test/regress/regress0/sets/sets-union.smt2 b/test/regress/regress0/sets/sets-union.smt2 index 6f6d3e019..656a0bc88 100644 --- a/test/regress/regress0/sets/sets-union.smt2 +++ b/test/regress/regress0/sets/sets-union.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-check-model +; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: unsat (set-logic ALL_SUPPORTED) diff --git a/test/regress/regress0/sets/union-1a-flip.smt2 b/test/regress/regress0/sets/union-1a-flip.smt2 index 59c2a2024..7bbe442e1 100644 --- a/test/regress/regress0/sets/union-1a-flip.smt2 +++ b/test/regress/regress0/sets/union-1a-flip.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-check-models +; COMMAND-LINE: --incremental ; EXPECT: unsat ; EXPECT: sat diff --git a/test/regress/regress0/sets/union-1b-flip.smt2 b/test/regress/regress0/sets/union-1b-flip.smt2 index 86fed459b..72c544553 100644 --- a/test/regress/regress0/sets/union-1b-flip.smt2 +++ b/test/regress/regress0/sets/union-1b-flip.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-check-models +; COMMAND-LINE: --incremental ; EXPECT: unsat ; EXPECT: sat diff --git a/test/regress/regress0/sets/union-2.smt2 b/test/regress/regress0/sets/union-2.smt2 index 32d949a53..e5e96be5a 100644 --- a/test/regress/regress0/sets/union-2.smt2 +++ b/test/regress/regress0/sets/union-2.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) -- cgit v1.2.3 From ac4a85a1682dd7e59d9ecc23ac7f3cd5e1716e4f Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 13 Mar 2014 19:33:11 -0400 Subject: fix a sharing issues with sets --- src/theory/sets/kinds | 1 + src/theory/sets/theory_sets_private.cpp | 37 ++++++++--------- src/theory/sets/theory_sets_rewriter.cpp | 48 +++++++++++++++++++--- src/theory/theory_model.cpp | 2 +- .../regress/regress0/sets/sets-testlemma-ints.smt2 | 1 - .../regress0/sets/sets-testlemma-reals.smt2 | 1 - 6 files changed, 61 insertions(+), 29 deletions(-) (limited to 'test/regress') diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 68941489f..e46f3a4f8 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -8,6 +8,7 @@ theory THEORY_SETS ::CVC4::theory::sets::TheorySets "theory/sets/theory_sets.h" typechecker "theory/sets/theory_sets_type_rules.h" rewriter ::CVC4::theory::sets::TheorySetsRewriter "theory/sets/theory_sets_rewriter.h" +properties parametric properties check propagate #presolve postsolve # Theory content goes here. diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index bd5324d2c..e5167dd6d 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -435,38 +435,36 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) // Computer terms appearing assertions and shared terms d_external.computeRelevantTerms(terms); + // compute for each setterm elements that it contains + SettermElementsMap settermElementsMap; + TNode true_atom = NodeManager::currentNM()->mkConst(true); + TNode false_atom = NodeManager::currentNM()->mkConst(false); + for(eq::EqClassIterator it_eqclasses(true_atom, &d_equalityEngine); + ! it_eqclasses.isFinished() ; ++it_eqclasses) { + TNode n = (*it_eqclasses); + if(n.getKind() == kind::MEMBER) { + Assert(d_equalityEngine.areEqual(n, true_atom)); + TNode x = d_equalityEngine.getRepresentative(n[0]); + TNode S = d_equalityEngine.getRepresentative(n[1]); + settermElementsMap[S].insert(x); + } + } + // Assert equalities and disequalities to the model m->assertEqualityEngine(&d_equalityEngine, &terms); - // Loop over all collect set-terms for which we generate models + // Loop over terms to collect set-terms for which we generate models set settermsModEq; - SettermElementsMap settermElementsMap; BOOST_FOREACH(TNode term, terms) { TNode n = term.getKind() == kind::NOT ? term[0] : term; Debug("sets-model-details") << "[sets-model-details] > " << n << std::endl; - if(n.getKind() == kind::EQUAL) { - // nothing to do - } else if(n.getKind() == kind::MEMBER) { - - TNode true_atom = NodeManager::currentNM()->mkConst(true); - - if(d_equalityEngine.areEqual(n, true_atom)) { - TNode x = d_equalityEngine.getRepresentative(n[0]); - TNode S = d_equalityEngine.getRepresentative(n[1]); - - settermElementsMap[S].insert(x); - } - - } else if(n.getType().isSet()) { - + if(n.getType().isSet()) { n = d_equalityEngine.getRepresentative(n); - if( !n.isConst() ) { settermsModEq.insert(n); } - } } @@ -477,7 +475,6 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) } } - // settermElementsMap processing BOOST_FOREACH( SettermElementsMap::value_type &it, settermElementsMap ) { BOOST_FOREACH( TNode element, it.second /* elements */ ) { Debug("sets-model-details") << "[sets-model-details] > " << diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index db67576d8..82b79cbd6 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -44,8 +44,9 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm) // static RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { NodeManager* nm = NodeManager::currentNM(); + Kind kind = node.getKind(); - switch(node.getKind()) { + switch(kind) { case kind::MEMBER: { if(!node[0].isConst() || !node[1].isConst()) @@ -54,7 +55,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { // both are constants bool isMember = checkConstantMembership(node[0], node[1]); return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember)); - } + }//kind::MEMBER case kind::SUBSET: { // rewrite (A subset-or-equal B) as (A union B = B) @@ -85,24 +86,59 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { return RewriteResponse(REWRITE_DONE, newNode); } break; - } + }//kind::IFF + + case kind::SETMINUS: { + if(node[0] == node[1]) { + Node newNode = nm->mkConst(EmptySet(nm->toType(node[0].getType()))); + Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; + return RewriteResponse(REWRITE_DONE, newNode); + } else if(node[0].getKind() == kind::EMPTYSET || + node[1].getKind() == kind::EMPTYSET) { + Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; + return RewriteResponse(REWRITE_DONE, node[0]); + } else if (node[0] > node[1]) { + Node newNode = nm->mkNode(node.getKind(), node[1], node[0]); + Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; + return RewriteResponse(REWRITE_DONE, newNode); + } + break; + }//kind::INTERSECION - case kind::UNION: case kind::INTERSECTION: { if(node[0] == node[1]) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; return RewriteResponse(REWRITE_DONE, node[0]); + } else if(node[0].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, node[0]); + } else if(node[1].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, node[1]); } else if (node[0] > node[1]) { Node newNode = nm->mkNode(node.getKind(), node[1], node[0]); Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; return RewriteResponse(REWRITE_DONE, newNode); } break; - } + }//kind::INTERSECION - default: + case kind::UNION: { + if(node[0] == node[1]) { + Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; + return RewriteResponse(REWRITE_DONE, node[0]); + } else if(node[0].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, node[1]); + } else if(node[1].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, node[0]); + } else if (node[0] > node[1]) { + Node newNode = nm->mkNode(node.getKind(), node[1], node[0]); + Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; + return RewriteResponse(REWRITE_DONE, newNode); + } break; + }//kind::UNION + default: + break; }//switch(node.getKind()) // This default implementation diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 4f753187f..8ec25dffd 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -779,7 +779,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) << "n: " << n << endl << "getValue(n): " << tm->getValue(n) << endl << "rep: " << rep << endl; - Assert(tm->getValue(*eqc_i) == rep); + Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details"); } } } diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2 index 23bde47fd..c8277be71 100644 --- a/test/regress/regress0/sets/sets-testlemma-ints.smt2 +++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2 @@ -5,4 +5,3 @@ (declare-fun y () (Set Int)) (assert (= x y)) (check-sat) -(get-model) diff --git a/test/regress/regress0/sets/sets-testlemma-reals.smt2 b/test/regress/regress0/sets/sets-testlemma-reals.smt2 index 97ac5841a..16e7780b4 100644 --- a/test/regress/regress0/sets/sets-testlemma-reals.smt2 +++ b/test/regress/regress0/sets/sets-testlemma-reals.smt2 @@ -5,4 +5,3 @@ (declare-fun y () (Set Real)) (assert (not (= x y))) (check-sat) -(get-model) -- cgit v1.2.3 From c8b948c37364104bf5f9ca5eca83120247b693a4 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Mon, 17 Mar 2014 18:01:10 -0400 Subject: Fix for registration issues of term appearing in a shared lemma (brought to attention by lianah -- fix currently just adapted using arrays -- this is to remind me to raise why do we even have this isPreregistered bussiness) --- src/theory/sets/theory_sets.cpp | 4 ++++ src/theory/sets/theory_sets.h | 2 ++ src/theory/sets/theory_sets_private.cpp | 18 ++++++++++++++++++ src/theory/sets/theory_sets_private.h | 2 ++ test/regress/regress0/sets/sets-testlemma-ints.smt2 | 2 +- 5 files changed, 27 insertions(+), 1 deletion(-) (limited to 'test/regress') diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 73176ff8b..3a5b61390 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -34,6 +34,10 @@ TheorySets::~TheorySets() { delete d_internal; } +void TheorySets::addSharedTerm(TNode n) { + d_internal->addSharedTerm(n); +} + void TheorySets::check(Effort e) { d_internal->check(e); } diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 8900b0e38..f40031514 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -46,6 +46,8 @@ public: ~TheorySets(); + void addSharedTerm(TNode); + void check(Effort); void collectModelInfo(TheoryModel*, bool fullModel); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 17eaf80aa..b45874bf2 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -54,6 +54,19 @@ void TheorySetsPrivate::check(Theory::Effort level) { bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; + if (!assertion.isPreregistered) { + if (atom.getKind() == kind::EQUAL) { + if (!d_equalityEngine.hasTerm(atom[0])) { + Assert(atom[0].isConst()); + d_equalityEngine.addTerm(atom[0]); + } + if (!d_equalityEngine.hasTerm(atom[1])) { + Assert(atom[1].isConst()); + d_equalityEngine.addTerm(atom[1]); + } + } + } + // Solve each switch(atom.getKind()) { case kind::EQUAL: @@ -710,6 +723,11 @@ bool TheorySetsPrivate::propagate(TNode literal) { }/* TheorySetsPropagate::propagate(TNode) */ +void TheorySetsPrivate::addSharedTerm(TNode n) { + Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl; + d_equalityEngine.addTriggerTerm(n, THEORY_SETS); +} + void TheorySetsPrivate::conflict(TNode a, TNode b) { if (a.getKind() == kind::CONST_BOOLEAN) { diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 1f43ede42..58000e435 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -47,6 +47,8 @@ public: ~TheorySetsPrivate(); + void addSharedTerm(TNode); + void check(Theory::Effort); void collectModelInfo(TheoryModel*, bool fullModel); diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2 index c8277be71..9dd257401 100644 --- a/test/regress/regress0/sets/sets-testlemma-ints.smt2 +++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2 @@ -3,5 +3,5 @@ (set-info :status sat) (declare-fun x () (Set Int)) (declare-fun y () (Set Int)) -(assert (= x y)) +(assert (not (= x y))) (check-sat) -- cgit v1.2.3 From 96eccb0d6134ccf4ead0134299b2e3750a890083 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 20 Mar 2014 02:01:24 -0400 Subject: fix for sets/mar2014/..317minimized.. Observed behavior: --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143)) with different set of elements in the model for representative and the node itself. Issue: The trouble with data structure being mainted to ensure that things for which lemmas have been generated are not generated again. This data structure (d_pendingEverInserted) needs to be user context dependent. The bug was in the sequence of steps from requesting that a lemma be generated to when it actually was. Sequence was: addToPending (and also adds to pending ever inserted) -> isComplete (might remove things from pending if requirment met in other ways) -> getLemma (actually generated the lemma, if requirement not already met) Resolution: adding terms to d_pendingEverInserted was moved from addToPending() to getLemma(). --- src/theory/sets/theory_sets_private.cpp | 115 +++++++++++++++++---- src/theory/sets/theory_sets_private.h | 8 ++ src/theory/theory_model.cpp | 14 +++ test/regress/regress0/sets/Makefile.am | 2 + .../mar2014/lemmabug-ListElts317minimized.smt2 | 89 ++++++++++++++++ .../regress0/sets/mar2014/sharing-preregister.smt2 | 12 +++ 6 files changed, 222 insertions(+), 18 deletions(-) create mode 100644 test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 create mode 100644 test/regress/regress0/sets/mar2014/sharing-preregister.smt2 (limited to 'test/regress') diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index b45874bf2..2675b73eb 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -89,9 +89,9 @@ void TheorySetsPrivate::check(Theory::Effort level) { Debug("sets") << "[sets] in conflict = " << d_conflict << std::endl; Assert( d_conflict ^ d_equalityEngine.consistent() ); if(d_conflict) return; + Debug("sets") << "[sets] is complete = " << isComplete() << std::endl; } - Debug("sets") << "[sets] is complete = " << isComplete() << std::endl; if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) { d_external.d_out->lemma(getLemma()); } @@ -377,12 +377,11 @@ void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) { /******************** Model generation ********************/ /******************** Model generation ********************/ -typedef set Elements; -typedef hash_map SettermElementsMap; - -const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap) { +const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements +(TNode setterm, SettermElementsMap& settermElementsMap) { SettermElementsMap::const_iterator it = settermElementsMap.find(setterm); - if(it == settermElementsMap.end() ) { + bool alreadyCalculated = (it != settermElementsMap.end()); + if( !alreadyCalculated ) { Kind k = setterm.getKind(); unsigned numChildren = setterm.getNumChildren(); @@ -419,15 +418,82 @@ const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMa return it->second; } -Node elementsToShape(Elements elements, - TypeNode setType) + +void printSet(std::ostream& out, const std::set& elements) { + out << "{ "; + std::copy(elements.begin(), + elements.end(), + std::ostream_iterator(out, ", ") + ); + out << " }"; +} + + +void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, TNode S) const { + + Debug("sets-model") << "[sets-model] checkModel(..., " << S << "): " + << std::endl; + + Assert(S.getType().isSet()); + + Elements emptySetOfElements; + const Elements& saved = + d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ? + emptySetOfElements : + settermElementsMap.find(d_equalityEngine.getRepresentative(S))->second; + Debug("sets-model") << "[sets-model] saved : "; + printSet(Debug("sets-model"), saved); + Debug("sets-model") << std::endl; + + if(S.getNumChildren() == 2) { + + Elements cur, left, right; + left = settermElementsMap.find(d_equalityEngine.getRepresentative(S[0]))->second; + right = settermElementsMap.find(d_equalityEngine.getRepresentative(S[1]))->second; + switch(S.getKind()) { + case kind::UNION: + if(left.size() >= right.size()) { + cur = left; cur.insert(right.begin(), right.end()); + } else { + cur = right; cur.insert(left.begin(), left.end()); + } + break; + case kind::INTERSECTION: + std::set_intersection(left.begin(), left.end(), right.begin(), right.end(), + std::inserter(cur, cur.begin()) ); + break; + case kind::SETMINUS: + std::set_difference(left.begin(), left.end(), right.begin(), right.end(), + std::inserter(cur, cur.begin()) ); + break; + default: + Unhandled(); + } + + Debug("sets-model") << "[sets-model] cur : "; + printSet(Debug("sets-model"), cur); + Debug("sets-model") << std::endl; + + if(saved != cur) { + Debug("sets-model") << "[sets-model] *** ERRROR *** cur != saved " + << std::endl; + Debug("sets-model") << "[sets-model] FYI: " + << " [" << S << "] = " << d_equalityEngine.getRepresentative(S) << ", " + << " [" << S[0] << "] = " << d_equalityEngine.getRepresentative(S[0]) << ", " + << " [" << S[1] << "] = " << d_equalityEngine.getRepresentative(S[1]) << "\n"; + + } + Assert( saved == cur ); + } +} + +Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) const { NodeManager* nm = NodeManager::currentNM(); if(elements.size() == 0) { return nm->mkConst(EmptySet(nm->toType(setType))); } else { - Elements::iterator it = elements.begin(); Node cur = SET_SINGLETON(*it); while( ++it != elements.end() ) { @@ -444,10 +510,10 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) set terms; - // Computer terms appearing assertions and shared terms + // Compute terms appearing assertions and shared terms d_external.computeRelevantTerms(terms); - // compute for each setterm elements that it contains + // Compute for each setterm elements that it contains SettermElementsMap settermElementsMap; TNode true_atom = NodeManager::currentNM()->mkConst(true); TNode false_atom = NodeManager::currentNM()->mkConst(false); @@ -501,6 +567,14 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) m->assertEquality(shape, setterm, true); m->assertRepresentative(shape); } + +#ifdef CVC4_ASSERTIONS + BOOST_FOREACH(TNode term, terms) { + if( term.getType().isSet() ) { + checkModel(settermElementsMap, term); + } + } +#endif } @@ -550,6 +624,7 @@ Node mkAnd(const std::vector& conjunctions) { TheorySetsPrivate::Statistics::Statistics() : d_checkTime("theory::sets::time") { + StatisticsRegistry::registerStat(&d_checkTime); } @@ -620,20 +695,27 @@ void TheorySetsPrivate::finishPropagation() } void TheorySetsPrivate::addToPending(Node n) { + Debug("sets-pending") << "[sets-pending] addToPending " << n << std::endl; if(d_pendingEverInserted.find(n) == d_pendingEverInserted.end()) { if(n.getKind() == kind::MEMBER) { + Debug("sets-pending") << "[sets-pending] \u2514 added to member queue" + << std::endl; d_pending.push(n); } else { + Debug("sets-pending") << "[sets-pending] \u2514 added to equality queue" + << std::endl; Assert(n.getKind() == kind::EQUAL); d_pendingDisequal.push(n); } - d_pendingEverInserted.insert(n); } } bool TheorySetsPrivate::isComplete() { - while(!d_pending.empty() && present(d_pending.front())) + while(!d_pending.empty() && present(d_pending.front())) { + Debug("sets-pending") << "[sets-pending] removing as already present: " + << d_pending.front() << std::endl; d_pending.pop(); + } return d_pending.empty() && d_pendingDisequal.empty(); } @@ -645,6 +727,7 @@ Node TheorySetsPrivate::getLemma() { if(!d_pending.empty()) { Node n = d_pending.front(); d_pending.pop(); + d_pendingEverInserted.insert(n); Assert(!present(n)); Assert(n.getKind() == kind::MEMBER); @@ -653,16 +736,12 @@ Node TheorySetsPrivate::getLemma() { } else { Node n = d_pendingDisequal.front(); d_pendingDisequal.pop(); + d_pendingEverInserted.insert(n); Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet()); Node x = NodeManager::currentNM()->mkSkolem("sde_$$", n[0].getType().getSetElementType()); Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]); - // d_equalityEngine.addTerm(x); - // d_equalityEngine.addTerm(l1); - // d_equalityEngine.addTerm(l2); - // d_terms.insert(x); - lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2)); } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 58000e435..daf0843e5 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -159,8 +159,16 @@ private: void addToPending(Node n); bool isComplete(); Node getLemma(); + + /** model generation and helper function */ + typedef std::set Elements; + typedef std::hash_map SettermElementsMap; + const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap); + Node elementsToShape(Elements elements, TypeNode setType) const; + void checkModel(const SettermElementsMap& settermElementsMap, TNode S) const; };/* class TheorySetsPrivate */ + }/* CVC4::theory::sets namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 8ec25dffd..6e0a71641 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -56,14 +56,26 @@ void TheoryModel::reset(){ } Node TheoryModel::getValue(TNode n) const { + Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) " + << std::endl; + //apply substitutions Node nn = d_substitutions.apply(n); + Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) post-sub:" + << nn << std::endl; + //get value in model nn = getModelValue(nn); + Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) getmodelvalue: " + << nn << std::endl; + if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) { //normalize nn = Rewriter::rewrite(nn); } + + Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): returning" + << nn << std::endl; return nn; } @@ -228,6 +240,8 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){ /** add substitution */ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ + Debug("model-builder") << "TheoryModel::addSubstitution("<< x << ", " << t + << ", invalidateCache = " << invalidateCache << ")\n"; if( !d_substitutions.hasSubstitution( x ) ){ d_substitutions.addSubstitution( x, t, invalidateCache ); } else { diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index f040a6cd0..04d3433eb 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -51,6 +51,8 @@ TESTS = \ jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \ sets-sample.smt2 \ eqtest.smt2 \ + mar2014/lemmabug-ListElts317minimized.smt2 \ + mar2014/sharing-preregister.smt2 \ emptyset.smt2 \ error2.smt2 diff --git a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 new file mode 100644 index 000000000..a7be520e4 --- /dev/null +++ b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 @@ -0,0 +1,89 @@ +; EXPECT: sat + +; Observed behavior: +; --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143)) +; with different set of elements in the model for representative and the node +; itself. +; +; Issue: +; The trouble with data structure being mainted to ensure that things +; for which lemmas have been generated are not generated again. This +; data structure (d_pendingEverInserted) needs to be user context +; dependent. The bug was in the sequence of steps from requesting that +; a lemma be generated to when it actually was. Sequence was: +; addToPending (and also adds to pending ever inserted) -> +; isComplete (might remove things from pending if requirment met in other ways) -> +; getLemma (actually generated the lemma, if requirement not already met) +; +; Resolution: +; adding terms to d_pendingEverInserted was moved from addToPending() +; to getLemma(). + +(set-logic QF_ALL_SUPPORTED) +(set-info :status sat) +(define-sort Elt () Int) +(define-sort mySet () (Set Elt )) +(define-fun smt_set_emp () mySet (as emptyset mySet)) +(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s)) +(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) +;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) +(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) +;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2)) + +(declare-fun z3v58 () Int) +(declare-fun z3v59 () Int) +(assert (distinct z3v58 z3v59)) + +(declare-fun z3f60 (Int) Bool) +(declare-fun z3v61 () Int) +(declare-fun z3f62 (Int) Int) +(declare-fun z3v63 () Int) +(declare-fun z3v64 () Int) +(declare-fun z3v67 () Int) +(declare-fun z3f68 (Int) Int) +(declare-fun z3f69 (Int) mySet) +(declare-fun z3f70 (Int) mySet) +(declare-fun z3f71 (Int) Bool) +(declare-fun z3v90 () Int) +(declare-fun z3v91 () Int) +(declare-fun z3f92 (Int Int) Int) +(declare-fun z3v140 () Int) +(declare-fun z3v141 () Int) +(declare-fun z3v142 () Int) +(declare-fun z3v143 () Int) +(declare-fun z3v144 () Int) +(declare-fun z3v145 () Int) +(declare-fun z3v147 () Int) +(declare-fun z3v150 () Int) +(declare-fun z3v151 () Int) +(declare-fun z3v152 () Int) + +(assert (not (= (z3f69 z3v152) + (z3f69 z3v140)))) + +(assert (= (z3f69 z3v151) + (smt_set_cup (z3f69 z3v141) + (z3f69 z3v140)))) + +(assert (= (z3f69 z3v152) + (smt_set_cup (setenum z3v143) (z3f69 z3v151)))) + +(assert (= (z3f70 z3v152) + (smt_set_cup (setenum z3v143) (z3f70 z3v151)))) + +(assert (and + (= (z3f69 z3v142) + (smt_set_cup (setenum z3v143) (z3f69 z3v141))) + (= (z3f70 z3v142) + (smt_set_cup (setenum z3v143) (z3f70 z3v141))) + (= z3v142 (z3f92 z3v143 z3v141)) + (= z3v142 z3v144) + (= (z3f62 z3v61) z3v61) + (= (z3f62 z3v63) z3v63) + ) + ) + +(check-sat) diff --git a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 new file mode 100644 index 000000000..dc42abfa2 --- /dev/null +++ b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 @@ -0,0 +1,12 @@ +; EXPECT: unsat +(set-logic QF_UFLIA_SETS) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun x () (Set Int)) +(declare-fun y () (Set Int)) +(assert (= x (setenum a))) +(assert (= y (setenum b))) +(assert (not (= x y))) +(assert (and (< 1 a) (< a 3) (< 1 b) (< b 3))) +(check-sat) -- cgit v1.2.3 From e8021a81993fe5ed201e7fdaf7af007e4d9d012b Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 20 Mar 2014 19:27:21 -0400 Subject: cleanup --- src/smt/smt_engine.h | 3 --- src/theory/sets/kinds | 1 - src/theory/sets/theory_sets_private.cpp | 29 ++++++++-------------- src/theory/sets/theory_sets_private.h | 2 +- src/theory/theory_model.cpp | 12 --------- .../mar2014/lemmabug-ListElts317minimized.smt2 | 2 +- 6 files changed, 12 insertions(+), 37 deletions(-) (limited to 'test/regress') diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8e400468c..c34d3ecba 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -277,9 +277,6 @@ class CVC4_PUBLIC SmtEngine { * as often as you like. Should be called whenever the final options * and logic for the problem are set (at least, those options that are * not permitted to change after assertions and queries are made). - * - * FIXME: Above comment not true. Please don't call this more than - * once. (6/14/2012 -- K) */ void finalOptionsAreSet(); diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index a56601b98..e46f3a4f8 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -41,7 +41,6 @@ operator SUBSET 2 "subset" operator MEMBER 2 "set membership" operator SET_SINGLETON 1 "singleton set" -operator FINITE_SET 1: "finite set" typerule UNION ::CVC4::theory::sets::SetUnionTypeRule typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 2675b73eb..70b757f0c 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -378,7 +378,7 @@ void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) { /******************** Model generation ********************/ const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements -(TNode setterm, SettermElementsMap& settermElementsMap) { +(TNode setterm, SettermElementsMap& settermElementsMap) const { SettermElementsMap::const_iterator it = settermElementsMap.find(setterm); bool alreadyCalculated = (it != settermElementsMap.end()); if( !alreadyCalculated ) { @@ -419,15 +419,6 @@ const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements } -void printSet(std::ostream& out, const std::set& elements) { - out << "{ "; - std::copy(elements.begin(), - elements.end(), - std::ostream_iterator(out, ", ") - ); - out << " }"; -} - void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, TNode S) const { @@ -437,13 +428,13 @@ void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, Assert(S.getType().isSet()); Elements emptySetOfElements; - const Elements& saved = + const Elements& saved = d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ? emptySetOfElements : settermElementsMap.find(d_equalityEngine.getRepresentative(S))->second; - Debug("sets-model") << "[sets-model] saved : "; - printSet(Debug("sets-model"), saved); - Debug("sets-model") << std::endl; + Debug("sets-model") << "[sets-model] saved : { "; + BOOST_FOREACH(TNode element, saved) { Debug("sets-model") << element << ", "; } + Debug("sets-model") << " }" << std::endl; if(S.getNumChildren() == 2) { @@ -470,9 +461,9 @@ void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, Unhandled(); } - Debug("sets-model") << "[sets-model] cur : "; - printSet(Debug("sets-model"), cur); - Debug("sets-model") << std::endl; + Debug("sets-model") << "[sets-model] cur : { "; + BOOST_FOREACH(TNode element, cur) { Debug("sets-model") << element << ", "; } + Debug("sets-model") << " }" << std::endl; if(saved != cur) { Debug("sets-model") << "[sets-model] *** ERRROR *** cur != saved " @@ -880,7 +871,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) { - Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality + Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality << " value = " << value << std::endl; if (value) { return d_theory.propagate(equality); @@ -903,7 +894,7 @@ bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, b bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag + Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag << " t1 = " << t1 << " t2 = " << t2 << " value = " << value << std::endl; if(value) { d_theory.d_termInfoManager->mergeTerms(t1, t2); diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index daf0843e5..62274e1ce 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -163,7 +163,7 @@ private: /** model generation and helper function */ typedef std::set Elements; typedef std::hash_map SettermElementsMap; - const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap); + const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap) const; Node elementsToShape(Elements elements, TypeNode setType) const; void checkModel(const SettermElementsMap& settermElementsMap, TNode S) const; };/* class TheorySetsPrivate */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 6e0a71641..405fceb6f 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -56,24 +56,14 @@ void TheoryModel::reset(){ } Node TheoryModel::getValue(TNode n) const { - Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) " - << std::endl; - //apply substitutions Node nn = d_substitutions.apply(n); - Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) post-sub:" - << nn << std::endl; - //get value in model nn = getModelValue(nn); - Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) getmodelvalue: " - << nn << std::endl; - if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) { //normalize nn = Rewriter::rewrite(nn); } - Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): returning" << nn << std::endl; return nn; @@ -240,8 +230,6 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){ /** add substitution */ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ - Debug("model-builder") << "TheoryModel::addSubstitution("<< x << ", " << t - << ", invalidateCache = " << invalidateCache << ")\n"; if( !d_substitutions.hasSubstitution( x ) ){ d_substitutions.addSubstitution( x, t, invalidateCache ); } else { diff --git a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 index a7be520e4..1ea3ea6b5 100644 --- a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 +++ b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 @@ -17,7 +17,7 @@ ; ; Resolution: ; adding terms to d_pendingEverInserted was moved from addToPending() -; to getLemma(). +; to getLemma(). (set-logic QF_ALL_SUPPORTED) (set-info :status sat) -- cgit v1.2.3