From: mudathirmahgoub Date: Mon, 13 Dec 2021 14:51:20 +0000 (-0600) Subject: Fix cvc5-projects issues #358 and #375 (#7743) X-Git-Tag: cvc5-1.0.0~680 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=05f2d5f39a2e1021bbaf8fc5ba3c9a0d053759a1;p=cvc5.git Fix cvc5-projects issues #358 and #375 (#7743) --- diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index 444878574..4428d0350 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -89,7 +89,7 @@ void BagSolver::postCheck() { for (const Node& e : d_state.getElements(n)) { - checkNonNegativeCountTerms(n, e); + checkNonNegativeCountTerms(n, d_state.getRepresentative(e)); } } } @@ -115,7 +115,7 @@ void BagSolver::checkEmpty(const Node& n) Assert(n.getKind() == BAG_EMPTY); for (const Node& e : d_state.getElements(n)) { - InferInfo i = d_ig.empty(n, e); + InferInfo i = d_ig.empty(n, d_state.getRepresentative(e)); d_im.lemmaTheoryInference(&i); } } @@ -126,7 +126,7 @@ void BagSolver::checkUnionDisjoint(const Node& n) std::set elements = getElementsForBinaryOperator(n); for (const Node& e : elements) { - InferInfo i = d_ig.unionDisjoint(n, e); + InferInfo i = d_ig.unionDisjoint(n, d_state.getRepresentative(e)); d_im.lemmaTheoryInference(&i); } } @@ -137,7 +137,7 @@ void BagSolver::checkUnionMax(const Node& n) std::set elements = getElementsForBinaryOperator(n); for (const Node& e : elements) { - InferInfo i = d_ig.unionMax(n, e); + InferInfo i = d_ig.unionMax(n, d_state.getRepresentative(e)); d_im.lemmaTheoryInference(&i); } } @@ -148,7 +148,7 @@ void BagSolver::checkIntersectionMin(const Node& n) std::set elements = getElementsForBinaryOperator(n); for (const Node& e : elements) { - InferInfo i = d_ig.intersection(n, e); + InferInfo i = d_ig.intersection(n, d_state.getRepresentative(e)); d_im.lemmaTheoryInference(&i); } } @@ -159,7 +159,7 @@ void BagSolver::checkDifferenceSubtract(const Node& n) std::set elements = getElementsForBinaryOperator(n); for (const Node& e : elements) { - InferInfo i = d_ig.differenceSubtract(n, e); + InferInfo i = d_ig.differenceSubtract(n, d_state.getRepresentative(e)); d_im.lemmaTheoryInference(&i); } } @@ -172,7 +172,7 @@ void BagSolver::checkBagMake(const Node& n) << " are: " << d_state.getElements(n) << std::endl; for (const Node& e : d_state.getElements(n)) { - InferInfo i = d_ig.bagMake(n, e); + InferInfo i = d_ig.bagMake(n, d_state.getRepresentative(e)); d_im.lemmaTheoryInference(&i); } } @@ -188,7 +188,7 @@ void BagSolver::checkDifferenceRemove(const Node& n) std::set elements = getElementsForBinaryOperator(n); for (const Node& e : elements) { - InferInfo i = d_ig.differenceRemove(n, e); + InferInfo i = d_ig.differenceRemove(n, d_state.getRepresentative(e)); d_im.lemmaTheoryInference(&i); } } @@ -205,7 +205,7 @@ void BagSolver::checkDuplicateRemoval(Node n) for (const Node& e : elements) { - InferInfo i = d_ig.duplicateRemoval(n, e); + InferInfo i = d_ig.duplicateRemoval(n, d_state.getRepresentative(e)); d_im.lemmaTheoryInference(&i); } } @@ -224,8 +224,9 @@ void BagSolver::checkMap(Node n) Assert(n.getKind() == BAG_MAP); const set& downwards = d_state.getElements(n); const set& upwards = d_state.getElements(n[1]); - for (const Node& y : downwards) + for (const Node& z : downwards) { + Node y = d_state.getRepresentative(z); if (d_mapCache.count(n) && d_mapCache[n].get()->contains(y)) { continue; diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp index 5c7c1dd73..ad817062f 100644 --- a/src/theory/bags/solver_state.cpp +++ b/src/theory/bags/solver_state.cpp @@ -43,7 +43,7 @@ void SolverState::registerBag(TNode n) void SolverState::registerCountTerm(TNode n) { Assert(n.getKind() == BAG_COUNT); - Node element = getRepresentative(n[0]); + Node element = n[0]; Node bag = getRepresentative(n[1]); d_bagElements[bag].insert(element); } diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 68bdb7b1b..61b4ebcbf 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -270,7 +270,18 @@ bool TheoryBags::collectModelValues(TheoryModel* m, { Node key = d_state.getRepresentative(e); Node countTerm = NodeManager::currentNM()->mkNode(BAG_COUNT, e, r); - Node value = d_state.getRepresentative(countTerm); + context::CDList::const_iterator shared_it = + std::find(d_sharedTerms.begin(), d_sharedTerms.end(), countTerm); + eq::EqClassIterator it = + eq::EqClassIterator(r, d_state.getEqualityEngine()); + while (!it.isFinished() && shared_it == d_sharedTerms.end()) + { + Node bag = *(++it); + countTerm = NodeManager::currentNM()->mkNode(BAG_COUNT, e, bag); + shared_it = + std::find(d_sharedTerms.begin(), d_sharedTerms.end(), countTerm); + } + Node value = d_valuation.getModelValue(countTerm); elementReps[key] = value; } Node rep = NormalForm::constructBagFromElements(tn, elementReps); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index dd1d96767..ae71ac484 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1108,7 +1108,8 @@ Node TheoryEngine::getModelValue(TNode var) { // the model value of a constant must be itself return var; } - Assert(d_sharedSolver->isShared(var)); + Assert(d_sharedSolver->isShared(var)) + << "node " << var << " is not shared" << std::endl; return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); } diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 1e56bd6ba..a83527004 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -1034,7 +1034,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) if (!repSet.empty()) { Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() - << ", first = " << *(repSet.begin()) << endl; + << ", repSet = " << repSet << endl; Assert(false); } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fda388832..6b8debc88 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1622,10 +1622,12 @@ set(regress_1_tests regress1/bags/intersection_min1.smt2 regress1/bags/intersection_min2.smt2 regress1/bags/issue5759.smt2 - regress1/bags/map-lazy-lam.smt2 regress1/bags/map1.smt2 regress1/bags/map2.smt2 regress1/bags/map3.smt2 + regress1/bags/map-lazy-lam.smt2 + regress1/bags/murxla1.smt2 + regress1/bags/murxla2.smt2 regress1/bags/subbag1.smt2 regress1/bags/subbag2.smt2 regress1/bags/union_disjoint.smt2 diff --git a/test/regress/regress1/bags/murxla1.smt2 b/test/regress/regress1/bags/murxla1.smt2 new file mode 100644 index 000000000..248f566f0 --- /dev/null +++ b/test/regress/regress1/bags/murxla1.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-option :produce-models true) +(set-info :status sat) +(declare-const A (Bag Bool)) +(declare-const B (Bag Bool)) +(check-sat-assuming ((distinct A B))) diff --git a/test/regress/regress1/bags/murxla2.smt2 b/test/regress/regress1/bags/murxla2.smt2 new file mode 100644 index 000000000..82ca2e90c --- /dev/null +++ b/test/regress/regress1/bags/murxla2.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :strings-exp true) +(declare-const x Int) +(assert (seq.contains (seq.at (seq.unit (bag false x)) x) (seq.unit (bag false x)))) +(check-sat)