From: Kshitij Bansal Date: Thu, 13 Mar 2014 23:33:11 +0000 (-0400) Subject: fix a sharing issues with sets X-Git-Tag: cvc5-1.0.0~7002^2~5 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ac4a85a1682dd7e59d9ecc23ac7f3cd5e1716e4f;p=cvc5.git fix a sharing issues with sets --- 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)