Fix cvc5-projects issue 497 (#8331)

Fixes cvc5/cvc5-projects#497

diff --git a/src/theory/bags/card_solver.cpp b/src/theory/bags/card_solver.cpp
index 146149e3bd2549b01df16ddf52fb9b22da90f489..6ec9b7a260da622b44913055631a0619aabce77d 100644 (file)
--- a/src/theory/bags/card_solver.cpp
+++ b/src/theory/bags/card_solver.cpp
@@ -65,7 +65,8 @@ std::set<Node> CardSolver::getChildren(Node bag)
 
 void CardSolver::checkCardinalityGraph()
 {
-  for (const auto& pair : d_state.getCardinalityTerms())
+  const std::map<Node, Node>& cardinalityTerms = d_state.getCardinalityTerms();
+  for (const auto& pair : cardinalityTerms)
   {
     Trace("bags-card") << "CardSolver::checkCardinalityGraph cardTerm: " << pair
                        << std::endl;
@@ -96,14 +97,16 @@ void CardSolver::checkCardinalityGraph()
         case BAG_DIFFERENCE_REMOVE: checkDifferenceRemove(pair, n); break;
         default: break;
       }
+      if (d_im.hasSentLemma())
+      {
+        // exit with each new pending lemma
+        return;
+      }
       it++;
     }
     // if the bag is a leaf in the graph, then we reduce its cardinality
     checkLeafBag(pair, bag);
-  }
-
-  for (const auto& pair : d_state.getCardinalityTerms())
-  {
+    // cardinality term is non-negative
     InferInfo i = d_ig.nonNegativeCardinality(pair.second);
     d_im.lemmaTheoryInference(&i);
   }

diff --git a/src/theory/bags/card_solver.h b/src/theory/bags/card_solver.h
index 5af0bc7013477ac3edeae1081684dcad2f357c64..9e08fcb62cfcfb570f01823744235377be6ff151 100644 (file)
--- a/src/theory/bags/card_solver.h
+++ b/src/theory/bags/card_solver.h
@@ -133,7 +133,6 @@ class CardSolver : protected EnvObj
    * This map needs to cleared before each full effort check.
    */
   std::map<Node, std::set<std::set<Node>>> d_cardGraph;
-
   /** Commonly used constants */
   Node d_true;
   Node d_false;

diff --git a/src/theory/bags/infer_info.cpp b/src/theory/bags/infer_info.cpp
index aa949ebc8678d6764783d37f6fecb20154160e3a..6b222cd3656768285820a979c95165cd7db24fdc 100644 (file)
--- a/src/theory/bags/infer_info.cpp
+++ b/src/theory/bags/infer_info.cpp
@@ -14,8 +14,9 @@
  */
 
 #include "theory/bags/infer_info.h"
-#include "theory/inference_manager_buffered.h"
+
 #include "theory/bags/inference_manager.h"
+#include "theory/inference_manager_buffered.h"
 
 namespace cvc5 {
 namespace theory {
@@ -28,20 +29,31 @@ InferInfo::InferInfo(InferenceManagerBuffered* im, InferenceId id)
 
 TrustNode InferInfo::processLemma(LemmaProperty& p)
 {
-  NodeManager* nm = NodeManager::currentNM();
-  Node pnode = nm->mkAnd(d_premises);
-  Node lemma = nm->mkNode(kind::IMPLIES, pnode, d_conclusion);
+  Node lemma = getLemma();
+
+  Trace("bags::InferInfo::process") << (*this) << std::endl;
+  d_im->addPendingLemma(lemma, getId());
+  return TrustNode::mkTrustLemma(lemma, nullptr);
+}
 
+Node InferInfo::getLemma() const
+{
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> nodes;
+  Node premises = nm->mkAnd(d_premises);
+  Node lemma = nm->mkNode(kind::IMPLIES, premises, d_conclusion);
+  nodes.push_back(lemma);
   // send lemmas corresponding to the skolems introduced
   for (const auto& pair : d_skolems)
   {
     Node n = pair.first.eqNode(pair.second);
-    d_im->addPendingLemma(n, InferenceId::BAGS_SKOLEM);
+    nodes.push_back(n);
   }
-
-  Trace("bags::InferInfo::process") << (*this) << std::endl;
-  d_im->addPendingLemma(lemma, getId());
-  return TrustNode::mkTrustLemma(lemma, nullptr);
+  if (nodes.size() == 1)
+  {
+    return lemma;
+  }
+  return nm->mkNode(kind::AND, nodes);
 }
 
 bool InferInfo::isTrivial() const

diff --git a/src/theory/bags/infer_info.h b/src/theory/bags/infer_info.h
index bebeaa077e920905894370426f20d751deab080d..d896844f6c3cfc910c279d89b4f8afd443fe161c 100644 (file)
--- a/src/theory/bags/infer_info.h
+++ b/src/theory/bags/infer_info.h
@@ -72,6 +72,10 @@ class InferInfo : public TheoryInference
    * engine with no new external premises (d_noExplain).
    */
   bool isFact() const;
+  /**
+   * @return the lemma for this InferInfo.
+   */
+  Node getLemma() const;
 };
 
 /**

diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index 63a90cf185f2281c9cba988a93025de47c1148f4..140b6d0b80bf2cf1d19cf046b5041bbf13853d47 100644 (file)
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -61,7 +61,7 @@ void InferenceGenerator::registerCardinalityTerm(Node n)
   Assert(n.getKind() == BAG_CARD);
   Node bag = d_state->getRepresentative(n[0]);
   Node cardTerm = d_nm->mkNode(BAG_CARD, bag);
-  Node skolem = registerAndAssertSkolemLemma(cardTerm, "bag.card");
+  Node skolem = registerAndAssertSkolemLemma(cardTerm, "bagCard");
   d_state->registerCardinalityTerm(cardTerm, skolem);
   Node premise = n[0].eqNode(bag);
   Node conclusion = skolem.eqNode(n);
@@ -338,7 +338,7 @@ InferInfo InferenceGenerator::cardEmpty(const std::pair<Node, Node>& pair,
   InferInfo inferInfo(d_im, InferenceId::BAGS_CARD_EMPTY);
   Node premise = pair.first[0].eqNode(n);
   Node conclusion = pair.second.eqNode(d_zero);
-  inferInfo.d_conclusion = premise.notNode().orNode(conclusion);
+  inferInfo.d_conclusion = premise.eqNode(conclusion);
   return inferInfo;
 }
 
@@ -373,8 +373,7 @@ InferInfo InferenceGenerator::cardUnionDisjoint(Node premise,
   Node unionDisjoints = child;
   Node card = d_nm->mkNode(BAG_CARD, child);
   std::vector<Node> lemmas;
-  registerCardinalityTerm(card);
-  Node sum = d_state->getCardinalitySkolem(card);
+  Node sum = registerAndAssertSkolemLemma(card, "bagCard");
   ++it;
   while (it != children.end())
   {
@@ -383,14 +382,12 @@ InferInfo InferenceGenerator::cardUnionDisjoint(Node premise,
     unionDisjoints =
         d_nm->mkNode(kind::BAG_UNION_DISJOINT, unionDisjoints, child);
     card = d_nm->mkNode(BAG_CARD, child);
-    registerCardinalityTerm(card);
-    Node skolem = d_state->getCardinalitySkolem(card);
+    Node skolem = registerAndAssertSkolemLemma(card, "bagCard");
     sum = d_nm->mkNode(ADD, sum, skolem);
     ++it;
   }
   Node parentCard = d_nm->mkNode(BAG_CARD, parent);
-  registerCardinalityTerm(parentCard);
-  Node parentSkolem = d_state->getCardinalitySkolem(parentCard);
+  Node parentSkolem = registerAndAssertSkolemLemma(parentCard, "bagCard");
 
   Node bags = parent.eqNode(unionDisjoints);
   lemmas.push_back(bags);

diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h
index ef8939b6431f59ceb57aed15e4fafaf690d51b72..8d67ea4f4db2f22bb98ed92d8eef0ec8458cc4ec 100644 (file)
--- a/src/theory/bags/inference_generator.h
+++ b/src/theory/bags/inference_generator.h
@@ -195,7 +195,7 @@ class InferenceGenerator
    * @param cardTerm a term of the form (bag.card A) where A has type (Bag E)
    * @param n is (as bag.empty (Bag E))
    * @return an inference that represents the following implication
-   * (=> (= A (as bag.empty (Bag E)))
+   * (= (= A (as bag.empty (Bag E)))
    *     (= (bag.card A) 0))
    */
   InferInfo cardEmpty(const std::pair<Node, Node>& pair, Node n);

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 0c2b4e1469fa0c5a8e6e1e985e3faa55688e5fe3..d263fe10ded268106c7cd59eadcea25fe1c1e6c4 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1770,6 +1770,7 @@ set(regress_1_tests
   regress1/bags/product1.smt2
   regress1/bags/product2.smt2
   regress1/bags/product3.smt2
+  regress1/bags/proj-issue497.smt2
   regress1/bags/subbag1.smt2
   regress1/bags/subbag2.smt2
   regress1/bags/union_disjoint.smt2

diff --git a/test/regress/cli/regress1/bags/proj-issue497.smt2 b/test/regress/cli/regress1/bags/proj-issue497.smt2
new file mode 100644 (file)
index 0000000..40950ea
--- /dev/null
+++ b/test/regress/cli/regress1/bags/proj-issue497.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status sat)
+(set-option :fmf-bound true)
+(declare-const x (Bag Bool))
+(declare-const x5 (Bag Bool))
+(check-sat-assuming ((= 0 (bag.card (bag.inter_min x5 (bag.inter_min x5 x))))))