Add Card solver to bags (#7986)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Wed, 26 Jan 2022 18:41:26 +0000 (12:41 -0600)
committerGitHub <noreply@github.com>
Wed, 26 Jan 2022 18:41:26 +0000 (18:41 +0000)
This PR avoids reducing bag.card terms with quantifiers unless it is needed.
It does so by building a cardinality graph for bags and adds appropriate constraints on internal nodes in the graph and min size constraints for the leaves.
This works for many of the benchmarks where each internal node has a single set of children.
Reduction lemmas are only generated when there are multiple sets of children.
Cardinality for bag.difference_remove and bag.duplicate_removal is not supported and would handled in future PR

14 files changed:
src/CMakeLists.txt
src/theory/bags/card_solver.cpp [new file with mode: 0644]
src/theory/bags/card_solver.h [new file with mode: 0644]
src/theory/bags/inference_generator.cpp
src/theory/bags/inference_generator.h
src/theory/bags/solver_state.cpp
src/theory/bags/solver_state.h
src/theory/bags/strategy.cpp
src/theory/bags/strategy.h
src/theory/bags/theory_bags.cpp
src/theory/bags/theory_bags.h
test/regress/CMakeLists.txt
test/regress/regress1/bags/card3.smt2 [new file with mode: 0644]
test/regress/regress1/bags/fol_0000119.smt2 [new file with mode: 0644]

index 49ea3a5005e6d2aed6adc51bdccde87177578dec..a1ad056f1eced3878641972f5c7807a36c28dca0 100644 (file)
@@ -549,6 +549,8 @@ libcvc5_add_sources(
   theory/bags/bag_reduction.h
   theory/bags/bags_statistics.cpp
   theory/bags/bags_statistics.h
+  theory/bags/card_solver.cpp
+  theory/bags/card_solver.h
   theory/bags/infer_info.cpp
   theory/bags/infer_info.h
   theory/bags/inference_generator.cpp
diff --git a/src/theory/bags/card_solver.cpp b/src/theory/bags/card_solver.cpp
new file mode 100644 (file)
index 0000000..4ec009c
--- /dev/null
@@ -0,0 +1,435 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Cardinality solver for theory of bags.
+ */
+
+#include "theory/bags/card_solver.h"
+
+#include "expr/emptybag.h"
+#include "smt/logic_exception.h"
+#include "theory/bags/inference_generator.h"
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/normal_form.h"
+#include "theory/bags/solver_state.h"
+#include "theory/bags/term_registry.h"
+#include "theory/uf/equality_engine_iterator.h"
+#include "util/rational.h"
+
+using namespace std;
+using namespace cvc5::context;
+using namespace cvc5::kind;
+
+namespace cvc5 {
+namespace theory {
+namespace bags {
+
+CardSolver::CardSolver(Env& env, SolverState& s, InferenceManager& im)
+    : EnvObj(env), d_state(s), d_ig(&s, &im), d_im(im), d_bagReduction(env)
+{
+  d_nm = NodeManager::currentNM();
+  d_zero = d_nm->mkConstInt(Rational(0));
+  d_one = d_nm->mkConstInt(Rational(1));
+  d_true = d_nm->mkConst(true);
+  d_false = d_nm->mkConst(false);
+}
+
+CardSolver::~CardSolver() {}
+
+void CardSolver::reset() { d_cardGraph.clear(); }
+
+bool CardSolver::isLeaf(const Node& bag)
+{
+  Node rep = d_state.getRepresentative(bag);
+  return (d_cardGraph.count(rep) == 0 || d_cardGraph[rep].empty());
+}
+
+std::set<Node> CardSolver::getChildren(Node bag)
+{
+  Node rep = d_state.getRepresentative(bag);
+  if (d_cardGraph[rep].empty())
+  {
+    return {};
+  }
+  return *d_cardGraph[rep].begin();
+}
+
+void CardSolver::checkCardinalityGraph()
+{
+  generateRelatedCardinalityTerms();
+
+  for (const auto& pair : d_state.getCardinalityTerms())
+  {
+    Trace("bags-card") << "CardSolver::checkCardinalityGraph cardTerm: " << pair
+                       << std::endl;
+    Assert(pair.first.getKind() == BAG_CARD);
+    Assert(d_state.hasTerm(pair.first[0]));
+    Node bag = d_state.getRepresentative(pair.first[0]);
+    Trace("bags-card") << "CardSolver::checkCardinalityGraph bag rep: " << bag
+                       << std::endl;
+    // enumerate all bag terms with bag operators
+    eq::EqClassIterator it =
+        eq::EqClassIterator(bag, d_state.getEqualityEngine());
+    while (!it.isFinished())
+    {
+      Node n = (*it);
+      Kind k = n.getKind();
+      switch (k)
+      {
+        case BAG_EMPTY: checkEmpty(pair, n); break;
+        case BAG_MAKE: checkBagMake(pair, n); break;
+        case BAG_UNION_DISJOINT:
+        {
+          checkUnionDisjoint(pair, n);
+          break;
+        }
+        case BAG_UNION_MAX: checkUnionMax(pair, n); break;
+        case BAG_INTER_MIN: checkIntersectionMin(pair, n); break;
+        case BAG_DIFFERENCE_SUBTRACT: checkDifferenceSubtract(pair, n); break;
+        case BAG_DIFFERENCE_REMOVE: checkDifferenceRemove(pair, n); break;
+        default: break;
+      }
+      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())
+  {
+    InferInfo i = d_ig.nonNegativeCardinality(pair.second);
+    d_im.lemmaTheoryInference(&i);
+  }
+}
+
+void CardSolver::generateRelatedCardinalityTerms()
+{
+  const set<Node>& bags = d_state.getBags();
+  for (const auto& pair : d_state.getCardinalityTerms())
+  {
+    Assert(pair.first.getKind() == BAG_CARD);
+    // get the representative of the bag in the card term
+    Node rep = d_state.getRepresentative(pair.first[0]);
+    // enumerate all bag terms that are related to the current bag
+    for (const auto& bag : bags)
+    {
+      if (rep == bag)
+      {
+        continue;
+      }
+
+      eq::EqClassIterator it = eq::EqClassIterator(
+          d_state.getRepresentative(bag), d_state.getEqualityEngine());
+      while (!it.isFinished())
+      {
+        Node n = (*it);
+        Kind k = n.getKind();
+        switch (k)
+        {
+          case BAG_EMPTY: break;
+          case BAG_MAKE: break;
+          case BAG_UNION_DISJOINT:
+          {
+            Node A = d_state.getRepresentative(n[0]);
+            Node B = d_state.getRepresentative(n[1]);
+            if (A == rep || B == rep)
+            {
+              d_state.registerCardinalityTerm(d_nm->mkNode(BAG_CARD, A));
+              d_state.registerCardinalityTerm(d_nm->mkNode(BAG_CARD, B));
+              d_state.registerCardinalityTerm(d_nm->mkNode(BAG_CARD, n));
+            }
+            break;
+          }
+          case BAG_UNION_MAX:
+          {
+            Node A = d_state.getRepresentative(n[0]);
+            Node B = d_state.getRepresentative(n[1]);
+            if (A == rep || B == rep)
+            {
+              d_state.registerCardinalityTerm(d_nm->mkNode(BAG_CARD, A));
+              d_state.registerCardinalityTerm(d_nm->mkNode(BAG_CARD, B));
+              d_state.registerCardinalityTerm(d_nm->mkNode(BAG_CARD, n));
+              // break the intersection symmetry using the node id
+              Node inter = A <= B ? d_nm->mkNode(BAG_INTER_MIN, A, B)
+                                  : d_nm->mkNode(BAG_INTER_MIN, B, A);
+              Node subtractAB =
+                  d_nm->mkNode(kind::BAG_DIFFERENCE_SUBTRACT, A, B);
+              Node subtractBA =
+                  d_nm->mkNode(kind::BAG_DIFFERENCE_SUBTRACT, B, A);
+              d_state.registerBag(inter);
+              d_state.registerBag(subtractAB);
+              d_state.registerBag(subtractBA);
+              d_state.registerCardinalityTerm(d_nm->mkNode(BAG_CARD, inter));
+              d_state.registerCardinalityTerm(
+                  d_nm->mkNode(BAG_CARD, subtractAB));
+              d_state.registerCardinalityTerm(
+                  d_nm->mkNode(BAG_CARD, subtractBA));
+            }
+            break;
+          }
+          case BAG_INTER_MIN: break;
+          case BAG_DIFFERENCE_SUBTRACT:
+          {
+            Node A = d_state.getRepresentative(n[0]);
+            Node B = d_state.getRepresentative(n[1]);
+            if (A == rep || B == rep)
+            {
+              d_state.registerCardinalityTerm(d_nm->mkNode(BAG_CARD, A));
+              d_state.registerCardinalityTerm(d_nm->mkNode(BAG_CARD, B));
+              d_state.registerCardinalityTerm(d_nm->mkNode(BAG_CARD, n));
+              // break the intersection symmetry using the node id
+              Node inter = A <= B ? d_nm->mkNode(BAG_INTER_MIN, A, B)
+                                  : d_nm->mkNode(BAG_INTER_MIN, B, A);
+              d_state.registerBag(inter);
+              d_state.registerCardinalityTerm(d_nm->mkNode(BAG_CARD, inter));
+            }
+            break;
+          }
+          case BAG_DIFFERENCE_REMOVE: break;
+          default: break;
+        }
+        it++;
+      }
+    }
+  }
+}
+
+void CardSolver::checkEmpty(const std::pair<Node, Node>& pair, const Node& n)
+{
+  Assert(n.getKind() == BAG_EMPTY);
+  InferInfo i = d_ig.cardEmpty(pair, n);
+  d_im.lemmaTheoryInference(&i);
+}
+
+void CardSolver::checkBagMake(const std::pair<Node, Node>& pair, const Node& n)
+{
+  Assert(n.getKind() == BAG_MAKE);
+  InferInfo i = d_ig.cardBagMake(pair, n);
+  d_im.lemmaTheoryInference(&i);
+}
+
+void CardSolver::checkUnionDisjoint(const std::pair<Node, Node>& pair,
+                                    const Node& n)
+{
+  Assert(n.getKind() == BAG_UNION_DISJOINT);
+  Node bag = d_state.getRepresentative(pair.first[0]);
+  Node A = d_state.getRepresentative(n[0]);
+  Node B = d_state.getRepresentative(n[1]);
+  addChildren(bag.eqNode(n), bag, {A, B});
+}
+
+void CardSolver::checkUnionMax(const std::pair<Node, Node>& pair, const Node& n)
+{
+  Assert(n.getKind() == BAG_UNION_MAX);
+  Node bag = d_state.getRepresentative(pair.first[0]);
+  Node A = d_state.getRepresentative(n[0]);
+  Node B = d_state.getRepresentative(n[1]);
+  Node subtractAB = d_nm->mkNode(BAG_DIFFERENCE_SUBTRACT, A, B);
+  Node subtractBA = d_nm->mkNode(BAG_DIFFERENCE_SUBTRACT, B, A);
+  // break the intersection symmetry using the node id
+  Node interAB = A <= B ? d_nm->mkNode(BAG_INTER_MIN, A, B)
+                        : d_nm->mkNode(BAG_INTER_MIN, B, A);
+  d_state.registerBag(subtractAB);
+  d_state.registerBag(subtractBA);
+  d_state.registerBag(interAB);
+  Node subtractABRep = d_state.getRepresentative(subtractAB);
+  Node subtractBARep = d_state.getRepresentative(subtractBA);
+  Node interABRep = d_state.getRepresentative(interAB);
+  addChildren(bag.eqNode(n), bag, {subtractABRep, interABRep, subtractBARep});
+}
+
+void CardSolver::addChildren(const Node& premise,
+                             const Node& parent,
+                             const set<Node>& children)
+{
+  if (children.count(parent) > 0 && children.size() > 1)
+  {
+    // handle the case when the parent is among the children, which implies
+    // other children are empty.
+    // This case is needed to avoid adding cycles in the cardinality graph
+    std::vector<Node> emptyBags;
+    Node empty = d_nm->mkConst(EmptyBag(parent.getType()));
+    Trace("bags-card") << "CardSolver::addChildren parent: " << parent
+                       << " is one of its children " << std::endl;
+    for (Node child : children)
+    {
+      Trace("bags-card") << "CardSolver::addChildren child: " << child
+                         << std::endl;
+      if (child != parent)
+      {
+        // this child should be empty
+        emptyBags.push_back(child.eqNode(empty));
+      }
+    }
+    Trace("bags-card") << "CardSolver::addChildren empty bags: " << emptyBags
+                       << std::endl;
+    InferInfo i(&d_im, InferenceId::BAGS_CARD);
+    i.d_premises.push_back(premise);
+    if (emptyBags.size() == 1)
+    {
+      i.d_conclusion = *emptyBags.begin();
+    }
+    else
+    {
+      i.d_conclusion = d_nm->mkNode(AND, emptyBags);
+    }
+    Trace("bags-card") << "CardSolver::addChildren info: " << i << std::endl;
+    d_im.lemmaTheoryInference(&i);
+    return;
+  }
+  // add inferences
+  InferInfo i = d_ig.cardUnionDisjoint(premise, parent, children);
+  d_im.lemmaTheoryInference(&i);
+
+  // make sure parent is in the graph
+  if (d_cardGraph.count(parent) == 0)
+  {
+    d_cardGraph[parent] = {};
+  }
+  // make sure children are in the graph
+  for (Node child : children)
+  {
+    if (d_cardGraph.count(child) == 0)
+    {
+      d_cardGraph[child] = {};
+    }
+  }
+
+  // only add children if not in the graph
+  if (d_cardGraph[parent].count(children) == 0)
+  {
+    if (d_cardGraph[parent].empty())
+    {
+      // The simple case is when the parent is a leaf in the cardinality graph.
+      // This means we can just add the current set of children without
+      // merging with a different set of children
+      d_cardGraph[parent].insert(children);
+    }
+    else
+    {
+      // The hard case is when the parent is an internal node in the
+      // cardinality graph, and has a different set of children.
+      // In this case we reduce the cardinality of the parent bag using
+      // quantifiers. This is faster than reducing the cardinality of each
+      // child.
+      const std::set<Node>& oldChildren = *d_cardGraph[parent].begin();
+      d_cardGraph[parent].insert(children);
+      Trace("bags-card") << "CardSolver::addChildren set1: " << oldChildren
+                         << std::endl;
+      Trace("bags-card") << "CardSolver::addChildren set2: " << children
+                         << std::endl;
+
+      Node card = d_nm->mkNode(BAG_CARD, parent);
+      std::vector<Node> asserts;
+      Node reduced = d_bagReduction.reduceCardOperator(card, asserts);
+      asserts.push_back(card.eqNode(reduced));
+      InferInfo inferInfo(&d_im, InferenceId::BAGS_CARD);
+      inferInfo.d_premises.push_back(premise);
+      inferInfo.d_conclusion = d_nm->mkNode(AND, asserts);
+      d_im.lemmaTheoryInference(&inferInfo);
+    }
+  }
+}
+
+void CardSolver::checkIntersectionMin(const std::pair<Node, Node>& pair,
+                                      const Node& n)
+{
+  Assert(n.getKind() == BAG_INTER_MIN);
+  Node bag = d_state.getRepresentative(pair.first[0]);
+  Node A = d_state.getRepresentative(n[0]);
+  Node B = d_state.getRepresentative(n[1]);
+  Node subtractAB = d_nm->mkNode(BAG_DIFFERENCE_SUBTRACT, A, B);
+  Node subtractBA = d_nm->mkNode(BAG_DIFFERENCE_SUBTRACT, B, A);
+  // break the intersection symmetry using the node id
+  Node interAB = A <= B ? d_nm->mkNode(BAG_INTER_MIN, A, B)
+                        : d_nm->mkNode(BAG_INTER_MIN, B, A);
+  d_state.registerBag(subtractAB);
+  d_state.registerBag(subtractBA);
+  d_state.registerBag(interAB);
+  Node subtractABRep = d_state.getRepresentative(subtractAB);
+  Node subtractBARep = d_state.getRepresentative(subtractBA);
+  Node interABRep = d_state.getRepresentative(interAB);
+  addChildren(bag.eqNode(n), A, {subtractABRep, interABRep});
+  addChildren(bag.eqNode(n), B, {interABRep, subtractBARep});
+}
+
+void CardSolver::checkDifferenceSubtract(const std::pair<Node, Node>& pair,
+                                         const Node& n)
+{
+  Assert(n.getKind() == BAG_DIFFERENCE_SUBTRACT);
+  Node bag = d_state.getRepresentative(pair.first[0]);
+  Node A = d_state.getRepresentative(n[0]);
+  Node B = d_state.getRepresentative(n[1]);
+  // break the intersection symmetry using the node id
+  Node interAB = A <= B ? d_nm->mkNode(BAG_INTER_MIN, A, B)
+                        : d_nm->mkNode(BAG_INTER_MIN, B, A);
+  d_state.registerBag(interAB);
+  Node interABRep = d_state.getRepresentative(interAB);
+  addChildren(bag.eqNode(n), A, {bag, interABRep});
+}
+
+void CardSolver::checkDifferenceRemove(const std::pair<Node, Node>& pair,
+                                       const Node& n)
+{
+  Assert(n.getKind() == BAG_DIFFERENCE_REMOVE);
+  throw LogicException(
+      "Cardinality for BAG_DIFFERENCE_REMOVE is not implemented yet");
+}
+
+void CardSolver::checkLeafBag(const std::pair<Node, Node>& pair,
+                              const Node& bag)
+{
+  if (d_cardGraph[bag].size() == 0)
+  {
+    Trace("bags-card") << "Leaf: " << bag << std::endl;
+    Trace("bags-card") << "cardTerm: " << pair << std::endl;
+    const std::vector<std::pair<Node, Node>>& pairs =
+        d_state.getElementCountPairs(bag);
+    for (size_t i = 0; i < pairs.size(); i++)
+    {
+      Trace("bags-card") << "pair: " << pairs[i] << std::endl;
+      bags::InferInfo inferInfo(&d_im, InferenceId::BAGS_CARD);
+      Node leq = d_nm->mkNode(LEQ, pairs[i].second, pair.second);
+      inferInfo.d_conclusion = leq;
+      d_im.lemmaTheoryInference(&inferInfo);
+      for (size_t j = i + 1; j < pairs.size(); j++)
+      {
+        std::vector<Node> distinct;
+        std::vector<Node> counts;
+        for (size_t k = 0; k < j; k++)
+        {
+          distinct.push_back(pairs[k].first.eqNode(pairs[j].first).notNode());
+          counts.push_back(pairs[k].second);
+        }
+        counts.push_back(pairs[j].second);
+        Node sum = d_nm->mkNode(PLUS, counts);
+        Node premise;
+        if (distinct.size() == 1)
+        {
+          premise = distinct[0];
+        }
+        else
+        {
+          premise = d_nm->mkNode(AND, distinct);
+        }
+        bags::InferInfo sumInfo(&d_im, InferenceId::BAGS_CARD);
+        Node sumLEQ = d_nm->mkNode(LEQ, sum, pair.second);
+        sumInfo.d_conclusion = premise.negate().orNode(sumLEQ);
+        d_im.lemmaTheoryInference(&sumInfo);
+      }
+    }
+  }
+}
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/bags/card_solver.h b/src/theory/bags/card_solver.h
new file mode 100644 (file)
index 0000000..4bec4ea
--- /dev/null
@@ -0,0 +1,170 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Cardinality solver for theory of bags.
+ */
+
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "cvc5_private.h"
+#include "smt/env_obj.h"
+#include "theory/bags/bag_reduction.h"
+
+#ifndef CVC5__THEORY__CARD__SOLVER_H
+#define CVC5__THEORY__CARD__SOLVER_H
+
+#include "theory/bags/inference_generator.h"
+
+namespace cvc5 {
+namespace theory {
+namespace bags {
+
+class InferenceManager;
+class SolverState;
+class TermRegistry;
+
+/** The cardinality solver for the theory of bags
+ *
+ */
+class CardSolver : protected EnvObj
+{
+ public:
+  CardSolver(Env& env, SolverState& s, InferenceManager& im);
+  ~CardSolver();
+
+  /** clear all data structures */
+  void reset();
+
+  /**
+   * add lemmas related to cardinality constraints
+   */
+  void checkCardinalityGraph();
+  /**
+   * @param bag a node of a bag type
+   * @return whether the given node is a leaf in the cardinality graph
+   */
+  bool isLeaf(const Node& bag);
+
+  /**
+   * @param bag a node of a bag type
+   * @return a set of children for that bag in the cardinality graph
+   */
+  std::set<Node> getChildren(Node bag);
+
+ private:
+  /**
+   * Generate all cardinality terms needed in the cardinality graph.
+   * suppose (bag.card bag) is a term, and r is the representative of bag.
+   * Suppose A, B are bag terms and r in {A, B}.
+   * - If (bag.union_disjoint A B) is a term, add the following terms:
+   *   (bag.card A)
+   *   (bag.card B)
+   *   (bag.card (bag.union_disjoint A B))
+   * - If (bag.union_max A B) is a term, add the following terms:
+   *   (bag.card A)
+   *   (bag.card B)
+   *   (bag.card (bag.difference_subtract A B))
+   *   (bag.card (bag.inter_min A B))
+   *   (bag.card (bag.difference_subtract B A))
+   * - If (bag.difference_subtract A B) is a term, add the following terms:
+   *   (bag.card A)
+   *   (bag.card B)
+   *   (bag.card (bag.inter_min A B))
+   *   (bag.card (bag.difference_subtract A B))
+   */
+  void generateRelatedCardinalityTerms();
+
+  /** apply inference rules for empty bags */
+  void checkEmpty(const std::pair<Node, Node>& pair, const Node& n);
+  /** apply inference rules for bag make */
+  void checkBagMake(const std::pair<Node, Node>& pair, const Node& n);
+  /** apply inference rules for union disjoint */
+  void checkUnionDisjoint(const std::pair<Node, Node>& pair, const Node& n);
+  /** apply inference rules for union max */
+  void checkUnionMax(const std::pair<Node, Node>& pair, const Node& n);
+  /** apply inference rules for intersection_min operator */
+  void checkIntersectionMin(const std::pair<Node, Node>& pair, const Node& n);
+  /** apply inference rules for difference subtract */
+  void checkDifferenceSubtract(const std::pair<Node, Node>& pair,
+                               const Node& n);
+  /** apply inference rules for difference remove */
+  void checkDifferenceRemove(const std::pair<Node, Node>& pair, const Node& n);
+  /**
+   * This function propagates minsize constraints for a leaf bag and related
+   * elements.
+   * Example If bag A is a leaf and {e1, ... , en} are elements, then this
+   * function adds the following lemmas:
+   * - (<= (bag.count e1 A) (bag.card A))
+   * - (<= (bag.count e2 A) (bag.card A))
+   *   ...
+   * - (<= (bag.count en A) (bag.card A))
+   *   (=> (distinct e1 e2)
+   *       (<= (+ (bag.count e1 A) (bag.count e2 A))
+   *           (bag.card A)))
+   *
+   * - (=> (distinct e1 e2 e3)
+   *      (<= (+ (bag.count e1 A) (bag.count e2 A) (bag.count e3 A))
+   *          (bag.card A)))
+   *   ...
+   * - (=> (distinct e1 ... en)
+   *     (<= (+ (bag.count e1 A) ... (bag.count en A))
+   *         (bag.card A)))
+   */
+  void checkLeafBag(const std::pair<Node, Node>& pair, const Node& bag);
+  /**
+   * This function updates cardinality graph by adding parent and its children
+   * to the cardinality graph. It also adds necessary lemmas when the premise
+   * holds.
+   * @param premise a node of boolean type
+   * @param parent a representative bag term
+   * @param children a set of bag representatives whose disjoint union equals to
+   * parent when the premise holds
+   */
+  void addChildren(const Node& premise,
+                   const Node& parent,
+                   const std::set<Node>& children);
+
+  /** The solver state object */
+  SolverState& d_state;
+  /** The inference generator object*/
+  InferenceGenerator d_ig;
+  /** Reference to the inference manager for the theory of bags */
+  InferenceManager& d_im;
+  NodeManager* d_nm;
+
+  /** bag reduction */
+  BagReduction d_bagReduction;
+
+  /**
+   * A map from bag representatives to sets of bag representatives with the
+   * invariant that each key is the disjoint union of each set in the value.
+   * Example:
+   * C -> {{A, B}, {X,Y, Z}}
+   * implies we have the following constraints in the current context.
+   * (= C (bag.union_disjoint A B))
+   * (= C (bag.union_disjoint X Y Z))
+   * 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;
+  Node d_zero;
+  Node d_one;
+}; /* class CardSolver */
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace cvc5
+
+#endif /* CVC5__THEORY__CARD__SOLVER_H */
index e2b2207771fba552e7e53ade5fde0e58414e1ca7..92aa1a0ea7f801da89b8cd8e10ab85c8b90f7c6a 100644 (file)
@@ -53,6 +53,14 @@ InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
   return inferInfo;
 }
 
+InferInfo InferenceGenerator::nonNegativeCardinality(Node n)
+{
+  InferInfo inferInfo(d_im, InferenceId::BAGS_NON_NEGATIVE_COUNT);
+  Node gte = d_nm->mkNode(GEQ, n, d_zero);
+  inferInfo.d_conclusion = gte;
+  return inferInfo;
+}
+
 InferInfo InferenceGenerator::bagMake(Node n)
 {
   Assert(n.getKind() == BAG_MAKE);
@@ -303,6 +311,78 @@ InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e)
   return inferInfo;
 }
 
+InferInfo InferenceGenerator::cardEmpty(const std::pair<Node, Node>& pair,
+                                        Node n)
+{
+  Assert(pair.first.getKind() == BAG_CARD);
+  Assert(n.getKind() == BAG_EMPTY && n.getType() == pair.first[0].getType());
+  InferInfo inferInfo(d_im, InferenceId::BAGS_CARD);
+  Node premise = pair.first[0].eqNode(n);
+  Node conclusion = pair.second.eqNode(d_zero);
+  inferInfo.d_conclusion = premise.notNode().orNode(conclusion);
+  return inferInfo;
+}
+
+InferInfo InferenceGenerator::cardBagMake(const std::pair<Node, Node>& pair,
+                                          Node n)
+{
+  Assert(pair.first.getKind() == BAG_CARD);
+  Assert(n.getKind() == BAG_MAKE && n.getType() == pair.first[0].getType());
+  //(=>
+  //  (and (= A (bag x c)) (>= 0 c))
+  //  (= (bag.card A) c))
+  Node c = n[1];
+  InferInfo inferInfo(d_im, InferenceId::BAGS_CARD);
+  Node nonNegative = d_nm->mkNode(GEQ, c, d_zero);
+  Node premise = pair.first[0].eqNode(n).andNode(nonNegative);
+  Node conclusion = pair.second.eqNode(c);
+  inferInfo.d_conclusion = premise.notNode().orNode(conclusion);
+  return inferInfo;
+}
+
+InferInfo InferenceGenerator::cardUnionDisjoint(Node premise,
+                                                Node parent,
+                                                const std::set<Node>& children)
+{
+  Assert(premise.getType().isBoolean());
+  Assert(!children.empty());
+  InferInfo inferInfo(d_im, InferenceId::BAGS_CARD);
+
+  std::set<Node>::iterator it = children.begin();
+  Node child = *it;
+  d_state->registerBag(child);
+  Node unionDisjoints = child;
+  Node card = d_nm->mkNode(BAG_CARD, child);
+  std::vector<Node> lemmas;
+  lemmas.push_back(d_state->registerCardinalityTerm(card));
+  Node sum = d_state->getCardinalitySkolem(card);
+  ++it;
+  while (it != children.end())
+  {
+    child = *it;
+    d_state->registerBag(child);
+    unionDisjoints =
+        d_nm->mkNode(kind::BAG_UNION_DISJOINT, unionDisjoints, child);
+    card = d_nm->mkNode(BAG_CARD, child);
+    lemmas.push_back(d_state->registerCardinalityTerm(card));
+    d_state->getCardinalitySkolem(card);
+    Node skolem = d_state->getCardinalitySkolem(card);
+    sum = d_nm->mkNode(PLUS, sum, skolem);
+    ++it;
+  }
+  Node parentCard = d_nm->mkNode(BAG_CARD, parent);
+  lemmas.push_back(d_state->registerCardinalityTerm(parentCard));
+  Node parentSkolem = d_state->getCardinalitySkolem(parentCard);
+
+  Node bags = parent.eqNode(unionDisjoints);
+  lemmas.push_back(bags);
+  Node cards = parentSkolem.eqNode(sum);
+  lemmas.push_back(cards);
+  Node conclusion = d_nm->mkNode(AND, lemmas);
+  inferInfo.d_conclusion = premise.notNode().orNode(conclusion);
+  return inferInfo;
+}
+
 Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag)
 {
   Node count = d_nm->mkNode(BAG_COUNT, element, bag);
index 29da0162959f359792d7e85a2dd7b6672b2de18d..2815058b263ea68eab9a9a4df65487482f994321 100644 (file)
@@ -46,6 +46,12 @@ class InferenceGenerator
    *   (>= (bag.count e A) 0)
    */
   InferInfo nonNegativeCount(Node n, Node e);
+  /**
+   * @param n a node of integer type that equals to a card term
+   * @return an inference that represents the following implication
+   * (>= n 0)
+   */
+  InferInfo nonNegativeCardinality(Node n);
 
   /**
    * @param n is (bag x c) of type (Bag E)
@@ -170,6 +176,38 @@ class InferenceGenerator
    * where skolem is a fresh variable equals (bag.duplicate_removal A)
    */
   InferInfo duplicateRemoval(Node n, Node e);
+  /**
+   * @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)))
+   *     (= (bag.card A) 0))
+   */
+  InferInfo cardEmpty(const std::pair<Node, Node>& pair, Node n);
+  /**
+   * @param cardTerm a term of the form (bag.card A) where A has type (Bag E)
+   * @param n is a node of the form (bag x c) of type (Bag E)
+   * @return an inference that represents the following implication
+   * (=>
+   *     (and (= A (bag x c)) (>= 0 c))
+   *     (= (bag.card A) c))
+   */
+  InferInfo cardBagMake(const std::pair<Node, Node>& pair, Node n);
+  /**
+   * @param premise a boolean node explains why parent equals the disjoint union
+   * of its children
+   * @param parent a bag term
+   * @param children (child_1, ... child_n) nonempty set of bag terms
+   * @return an inference that represents the following implication
+   * (=> premise
+   *     (and
+   *       (= parent (bag.union_disjoint child_1 ... child_n))
+   *       (= (bag.card parent) (+ (bag.card child_1) ... (bag.card child_n)))))
+   */
+  InferInfo cardUnionDisjoint(Node premise,
+                              Node parent,
+                              const std::set<Node>& children);
+
   /**
    * @param n is (bag.map f A) where f is a function (-> E T), A a bag of type
    * (Bag E)
index 52cbb86717d5020977f81b4115102b536076d8d3..575dcf577bceee39eecb4108d93f190f098d3480 100644 (file)
@@ -38,6 +38,10 @@ void SolverState::registerBag(TNode n)
 {
   Assert(n.getType().isBag());
   d_bags.insert(n);
+  if (!d_ee->hasTerm(n))
+  {
+    d_ee->addTerm(n);
+  }
 }
 
 Node SolverState::registerCountTerm(TNode n)
@@ -47,12 +51,46 @@ Node SolverState::registerCountTerm(TNode n)
   Node bag = getRepresentative(n[1]);
   Node count = d_nm->mkNode(BAG_COUNT, element, bag);
   Node skolem = d_nm->getSkolemManager()->mkPurifySkolem(count, "bag.count");
-  d_bagElements[bag].push_back(std::make_pair(element, skolem));
+  std::pair<Node, Node> pair = std::make_pair(element, skolem);
+  if (std::find(d_bagElements[bag].begin(), d_bagElements[bag].end(), pair)
+      == d_bagElements[bag].end())
+  {
+    d_bagElements[bag].push_back(pair);
+  }
   return count.eqNode(skolem);
 }
 
+Node SolverState::registerCardinalityTerm(TNode n)
+{
+  Assert(n.getKind() == BAG_CARD);
+  if (!d_ee->hasTerm(n))
+  {
+    d_ee->addTerm(n);
+  }
+  Node bag = getRepresentative(n[0]);
+  Node cardTerm = d_nm->mkNode(BAG_CARD, bag);
+  Node skolem = d_nm->getSkolemManager()->mkPurifySkolem(cardTerm, "bag.card");
+  d_cardTerms[cardTerm] = skolem;
+  return cardTerm.eqNode(skolem).andNode(skolem.eqNode(n));
+}
+
+Node SolverState::getCardinalitySkolem(TNode n)
+{
+  Assert(n.getKind() == BAG_CARD);
+  Node bag = getRepresentative(n[0]);
+  Node cardTerm = d_nm->mkNode(BAG_CARD, bag);
+  return d_cardTerms[cardTerm];
+}
+
+bool SolverState::hasCardinalityTerms() const { return !d_cardTerms.empty(); }
+
 const std::set<Node>& SolverState::getBags() { return d_bags; }
 
+const std::map<Node, Node>& SolverState::getCardinalityTerms()
+{
+  return d_cardTerms;
+}
+
 std::set<Node> SolverState::getElements(Node B)
 {
   Node bag = getRepresentative(B);
@@ -79,6 +117,7 @@ void SolverState::reset()
   d_bagElements.clear();
   d_bags.clear();
   d_deq.clear();
+  d_cardTerms.clear();
 }
 
 std::vector<Node> SolverState::initialize()
@@ -127,6 +166,11 @@ std::vector<Node> SolverState::collectBagsAndCountTerms()
         Trace("SolverState::collectBagsAndCountTerms")
             << "registered " << n << endl;
       }
+      if (k == BAG_CARD)
+      {
+        Node lemma = registerCardinalityTerm(n);
+        lemmas.push_back(lemma);
+      }
       ++it;
     }
     Trace("bags-eqc") << " } " << std::endl;
index 64c4b16741d0649c786c44f601854faee55a7e12..4e3997793f1b16553c3ee2b2e4901e3844126eac 100644 (file)
@@ -41,16 +41,39 @@ class SolverState : public TheoryState
 
   /**
    * @param n has the form (bag.count e A)
-   * @pre bag A needs is already registered using registerBag(A)
+   * @pre bag A is already registered using registerBag(A)
    * @return a lemma (= skolem (bag.count eRep ARep)) where
    * eRep, ARep are representatives of e, A respectively
    */
   Node registerCountTerm(TNode n);
+
+  /**
+   * This function generates a skolem variable for the given card term and
+   * stores both of them in a cache.
+   * @param n has the form (bag.card A)
+   * @return a lemma that the card term equals the skolem variable
+   */
+  Node registerCardinalityTerm(TNode n);
+
+  /**
+   * @param n has the form (bag.card A)
+   */
+  Node getCardinalitySkolem(TNode n);
+
+  bool hasCardinalityTerms() const;
+
   /** get all bag terms that are representatives in the equality engine.
    * This function is valid after the current solver is initialized during
    * postCheck. See SolverState::initialize and BagSolver::postCheck
    */
   const std::set<Node>& getBags();
+
+  /**
+   * get all cardinality terms
+   * @return a map from registered card terms to their skolem variables
+   */
+  const std::map<Node, Node>& getCardinalityTerms();
+
   /**
    * @pre B is a registered bag
    * @return all elements associated with bag B so far
@@ -100,6 +123,8 @@ class SolverState : public TheoryState
   std::map<Node, std::vector<std::pair<Node, Node>>> d_bagElements;
   /** Disequal bag terms */
   std::set<Node> d_deq;
+  /** a map from card terms to their skolem variables */
+  std::map<Node, Node> d_cardTerms;
 }; /* class SolverState */
 
 }  // namespace bags
index 541be9ac7391518254d3bd3232f7f95a71b85f9f..e2517100ba32b2856830eec73affb8d40aa4fbca 100644 (file)
@@ -27,6 +27,9 @@ std::ostream& operator<<(std::ostream& out, InferStep s)
     case CHECK_INIT: out << "check_init"; break;
     case CHECK_BAG_MAKE: out << "check_bag_make"; break;
     case CHECK_BASIC_OPERATIONS: out << "CHECK_BASIC_OPERATIONS"; break;
+    case CHECK_CARDINALITY_CONSTRAINTS:
+      out << "CHECK_CARDINALITY_CONSTRAINTS";
+      break;
     default: out << "?"; break;
   }
   return out;
@@ -86,6 +89,7 @@ void Strategy::initializeStrategy()
     addStrategyStep(CHECK_INIT);
     addStrategyStep(CHECK_BAG_MAKE);
     addStrategyStep(CHECK_BASIC_OPERATIONS);
+    addStrategyStep(CHECK_CARDINALITY_CONSTRAINTS);
     step_end[Theory::EFFORT_FULL] = d_infer_steps.size() - 1;
 
     // set the beginning/ending ranges
index 7dc5d693cc149b777fe4a4716f9afdb5593c9d20..19bf2b1776b00a441d79825ce1cb59b729d7e377 100644 (file)
@@ -42,7 +42,9 @@ enum InferStep
   // check bag operator
   CHECK_BAG_MAKE,
   // check basic operations
-  CHECK_BASIC_OPERATIONS
+  CHECK_BASIC_OPERATIONS,
+  // check cardinality constraints
+  CHECK_CARDINALITY_CONSTRAINTS
 };
 std::ostream& operator<<(std::ostream& out, InferStep i);
 
index cfd6f117862122ddf5df14f80e9a6dfd7ac3f0ab..720e97c25dfff90573a36b5444908991e288bbde 100644 (file)
@@ -41,6 +41,7 @@ TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation)
       d_rewriter(&d_statistics.d_rewrites),
       d_termReg(env, d_state, d_im),
       d_solver(env, d_state, d_im, d_termReg),
+      d_cardSolver(env, d_state, d_im),
       d_bagReduction(env)
 {
   // use the official theory state and inference manager objects
@@ -88,18 +89,6 @@ TrustNode TheoryBags::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
   switch (atom.getKind())
   {
     case kind::BAG_CHOOSE: return expandChooseOperator(atom, lems);
-    case kind::BAG_CARD:
-    {
-      std::vector<Node> asserts;
-      Node ret = d_bagReduction.reduceCardOperator(atom, asserts);
-      NodeManager* nm = NodeManager::currentNM();
-      Node andNode = nm->mkNode(AND, asserts);
-      Trace("bags::ppr") << "reduce(" << atom << ") = " << ret
-                         << " such that:" << std::endl
-                         << andNode << std::endl;
-      d_im.lemma(andNode, InferenceId::BAGS_CARD);
-      return TrustNode::mkTrustRewrite(atom, ret, nullptr);
-    }
     case kind::BAG_FOLD:
     {
       std::vector<Node> asserts;
@@ -175,6 +164,7 @@ void TheoryBags::postCheck(Effort effort)
       // TODO issue #78: add ++(d_statistics.d_strategyRuns);
       Trace("bags-check") << "  * Run strategy..." << std::endl;
       std::vector<Node> lemmas = d_state.initialize();
+      d_cardSolver.reset();
       for (Node lemma : lemmas)
       {
         d_im.lemma(lemma, InferenceId::BAGS_COUNT_SKOLEM);
@@ -264,6 +254,9 @@ bool TheoryBags::runInferStep(InferStep s, int effort)
       break;
     }
     case CHECK_BASIC_OPERATIONS: d_solver.checkBasicOperations(); break;
+    case CHECK_CARDINALITY_CONSTRAINTS:
+      d_cardSolver.checkCardinalityGraph();
+      break;
     default: Unreachable(); break;
   }
   Trace("bags-process") << "Done " << s
@@ -328,11 +321,69 @@ bool TheoryBags::collectModelValues(TheoryModel* m,
       Node value = m->getRepresentative(countSkolem);
       elementReps[key] = value;
     }
-    Node rep = NormalForm::constructBagFromElements(tn, elementReps);
-    rep = rewrite(rep);
-    Trace("bags-model") << "rep of " << n << " is: " << rep << std::endl;
-    m->assertEquality(rep, n, true);
-    m->assertSkeleton(rep);
+    Node constructedBag = NormalForm::constructBagFromElements(tn, elementReps);
+    constructedBag = rewrite(constructedBag);
+    Trace("bags-model") << "constructed bag for " << n
+                        << " is: " << constructedBag << std::endl;
+    NodeManager* nm = NodeManager::currentNM();
+    if (d_state.hasCardinalityTerms())
+    {
+      if (d_cardSolver.isLeaf(n))
+      {
+        Node constructedBagCard = rewrite(nm->mkNode(BAG_CARD, constructedBag));
+        Trace("bags-model")
+            << "constructed bag cardinality: " << constructedBagCard
+            << std::endl;
+        Node rCard = nm->mkNode(BAG_CARD, r);
+        Node rCardSkolem = d_state.getCardinalitySkolem(rCard);
+        Trace("bags-model") << "rCardSkolem : " << rCardSkolem << std::endl;
+        if (!rCardSkolem.isNull())
+        {
+          Node rCardModelValue = m->getRepresentative(rCardSkolem);
+          const Rational& rCardRational = rCardModelValue.getConst<Rational>();
+          const Rational& constructedRational =
+              constructedBagCard.getConst<Rational>();
+          Trace("bags-model")
+              << "constructedRational : " << constructedRational << std::endl;
+          Trace("bags-model")
+              << "rCardRational : " << rCardRational << std::endl;
+          Assert(constructedRational <= rCardRational);
+          TypeNode elementType = r.getType().getBagElementType();
+          if (constructedRational < rCardRational
+              && !d_env.isFiniteType(elementType))
+          {
+            Node newElement = nm->getSkolemManager()->mkDummySkolem("slack", elementType);
+            Trace("bags-model") << "newElement is " << newElement << std::endl;
+            Rational difference = rCardRational - constructedRational;
+            Node multiplicity = nm->mkConst(CONST_RATIONAL, difference);
+            Node slackBag = nm->mkBag(elementType, newElement, multiplicity);
+            constructedBag =
+                nm->mkNode(kind::BAG_UNION_DISJOINT, constructedBag, slackBag);
+            constructedBag = rewrite(constructedBag);
+            Trace("bags-model") << "constructed bag for " << n
+                                << " is: " << constructedBag << std::endl;
+          }
+        }
+      }
+      else
+      {
+        std::set<Node> children = d_cardSolver.getChildren(n);
+        Assert(!children.empty());
+        constructedBag = nm->mkConst(EmptyBag(r.getType()));
+        for (Node child : children)
+        {
+          Trace("bags-model")
+              << "child bag for " << n << " is: " << child << std::endl;
+          constructedBag =
+              nm->mkNode(BAG_UNION_DISJOINT, child, constructedBag);
+        }
+        constructedBag = rewrite(constructedBag);
+        Trace("bags-model") << "constructed bag for " << n
+                            << " is: " << constructedBag << std::endl;
+      }
+    }
+    m->assertEquality(constructedBag, n, true);
+    m->assertSkeleton(constructedBag);
   }
   return true;
 }
index cc76c5453d6a3905518656ae3934cf3dc56d58c0..18e306e9593b22abb6bff75fa3305b56311cf06b 100644 (file)
@@ -22,6 +22,7 @@
 #include "theory/bags/bag_solver.h"
 #include "theory/bags/bags_rewriter.h"
 #include "theory/bags/bags_statistics.h"
+#include "theory/bags/card_solver.h"
 #include "theory/bags/inference_generator.h"
 #include "theory/bags/inference_manager.h"
 #include "theory/bags/solver_state.h"
@@ -117,6 +118,9 @@ class TheoryBags : public Theory
   /** the main solver for bags */
   BagSolver d_solver;
 
+  /** the main solver for bags */
+  CardSolver d_cardSolver;
+
   /** bag reduction */
   BagReduction d_bagReduction;
 
index f521e77eda65794758b56d178e471f876a914fdf..b746102b5ff8b54f6598a46b3edcae26330f55b2 100644 (file)
@@ -1642,6 +1642,7 @@ set(regress_1_tests
   regress1/bags/bags-of-bags-subtypes.smt2
   regress1/bags/card1.smt2
   regress1/bags/card2.smt2
+  regress1/bags/card3.smt2
   regress1/bags/choose1.smt2
   regress1/bags/choose2.smt2
   regress1/bags/choose3.smt2
@@ -1651,6 +1652,7 @@ set(regress_1_tests
   regress1/bags/duplicate_removal1.smt2
   regress1/bags/duplicate_removal2.smt2
   regress1/bags/emptybag1.smt2
+  regress1/bags/fol_0000119.smt2
   regress1/bags/fold1.smt2
   regress1/bags/fuzzy1.smt2
   regress1/bags/fuzzy2.smt2
diff --git a/test/regress/regress1/bags/card3.smt2 b/test/regress/regress1/bags/card3.smt2
new file mode 100644 (file)
index 0000000..4e37eb7
--- /dev/null
@@ -0,0 +1,9 @@
+(set-logic ALL)
+(set-info :status unsat)
+(set-option :fmf-bound true)
+(declare-fun B () (Bag (Tuple Int Int)))
+(declare-fun x () (Tuple Int Int))
+(assert
+ (and (= (as bag.empty (Bag (Tuple Int Int))) (bag x (bag.card B)))
+      (not (= (as bag.empty (Bag (Tuple Int Int))) B))))
+(check-sat)
diff --git a/test/regress/regress1/bags/fol_0000119.smt2 b/test/regress/regress1/bags/fol_0000119.smt2
new file mode 100644 (file)
index 0000000..37003ae
--- /dev/null
@@ -0,0 +1,35 @@
+(set-logic ALL)
+
+(set-option :fmf-bound true)
+
+
+(set-info :status unsat)
+
+; forall a_fh:A. 2a_fh + |~f| - 2n >= 1 or 1 <= 0
+
+(declare-fun n () Int)
+(declare-fun t () Int)
+
+(declare-fun f () (Bag Int))
+(declare-fun UNIVERALSET () (Bag Int))
+
+(assert (bag.subbag f UNIVERALSET))
+(assert (= (bag.card UNIVERALSET) n))
+
+(assert (> n 0))
+(assert (> n (* 3 t)))
+(assert (<= (bag.card f) t))
+
+(declare-fun a_fh () Int)
+
+(assert (<= a_fh n))
+(assert (>= a_fh 0))
+(assert (>= a_fh (- n t)))
+
+
+(assert
+ (and
+  (< (- (+ (* 2 a_fh) (bag.card (bag.difference_subtract UNIVERALSET f))) (* 2 n)) 1)
+  (> 1 0)))
+
+(check-sat)