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 444878574a8a078fb941aaf484bd416cf39907f3..4428d03508fa8fc99c9821be498889834d22ba4f 100644 (file)
--- 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node>& downwards = d_state.getElements(n);
   const set<Node>& 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 5c7c1dd7380e71820efc8e6bf46b92c832439e4f..ad817062fb512a6999d3c8a354e20f4e54ed3175 100644 (file)
--- 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 68bdb7b1bbc5109fab8e4bde929147f2a9f7b9ac..61b4ebcbf18280905ff39849d15467380d5fd85a 100644 (file)
--- 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<TNode>::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 dd1d9676743084b7e4415275c08540806afdbebc..ae71ac4842715e1436edb1140671ac7a0918e144 100644 (file)
--- 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 1e56bd6ba031c6892d2717f09f617e80a4232c01..a835270043591f21b0068139e00ce970f766fdb3 100644 (file)
--- 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 fda3888322bd5e0d06bae38379ec671bfdcf8c17..6b8debc880cd3abf576899f4d424f3a3c266596c 100644 (file)
--- 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 (file)
index 0000000..248f566
--- /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 (file)
index 0000000..82ca2e9
--- /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)