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
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
--- /dev/null
+/******************************************************************************
+ * 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
--- /dev/null
+/******************************************************************************
+ * 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 */
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);
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);
* (>= (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)
* 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)
{
Assert(n.getType().isBag());
d_bags.insert(n);
+ if (!d_ee->hasTerm(n))
+ {
+ d_ee->addTerm(n);
+ }
}
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);
d_bagElements.clear();
d_bags.clear();
d_deq.clear();
+ d_cardTerms.clear();
}
std::vector<Node> SolverState::initialize()
Trace("SolverState::collectBagsAndCountTerms")
<< "registered " << n << endl;
}
+ if (k == BAG_CARD)
+ {
+ Node lemma = registerCardinalityTerm(n);
+ lemmas.push_back(lemma);
+ }
++it;
}
Trace("bags-eqc") << " } " << std::endl;
/**
* @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
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
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;
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
// 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);
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
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;
// 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);
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
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;
}
#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"
/** the main solver for bags */
BagSolver d_solver;
+ /** the main solver for bags */
+ CardSolver d_cardSolver;
+
/** bag reduction */
BagReduction d_bagReduction;
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
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
--- /dev/null
+(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)
--- /dev/null
+(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)