From 51d731ec403becd8a46e02933112ff2fc6b310e9 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Wed, 26 Jan 2022 12:41:26 -0600 Subject: [PATCH] Add Card solver to bags (#7986) 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 --- src/CMakeLists.txt | 2 + src/theory/bags/card_solver.cpp | 435 ++++++++++++++++++++ src/theory/bags/card_solver.h | 170 ++++++++ src/theory/bags/inference_generator.cpp | 80 ++++ src/theory/bags/inference_generator.h | 38 ++ src/theory/bags/solver_state.cpp | 46 ++- src/theory/bags/solver_state.h | 27 +- src/theory/bags/strategy.cpp | 4 + src/theory/bags/strategy.h | 4 +- src/theory/bags/theory_bags.cpp | 85 +++- src/theory/bags/theory_bags.h | 4 + test/regress/CMakeLists.txt | 2 + test/regress/regress1/bags/card3.smt2 | 9 + test/regress/regress1/bags/fol_0000119.smt2 | 35 ++ 14 files changed, 921 insertions(+), 20 deletions(-) create mode 100644 src/theory/bags/card_solver.cpp create mode 100644 src/theory/bags/card_solver.h create mode 100644 test/regress/regress1/bags/card3.smt2 create mode 100644 test/regress/regress1/bags/fol_0000119.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 49ea3a500..a1ad056f1 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -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 index 000000000..4ec009c7d --- /dev/null +++ b/src/theory/bags/card_solver.cpp @@ -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 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& 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& 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& 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& 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& 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& 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 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& 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 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& 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& 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& 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& 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>& 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 distinct; + std::vector 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 index 000000000..4bec4ea23 --- /dev/null +++ b/src/theory/bags/card_solver.h @@ -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 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& pair, const Node& n); + /** apply inference rules for bag make */ + void checkBagMake(const std::pair& pair, const Node& n); + /** apply inference rules for union disjoint */ + void checkUnionDisjoint(const std::pair& pair, const Node& n); + /** apply inference rules for union max */ + void checkUnionMax(const std::pair& pair, const Node& n); + /** apply inference rules for intersection_min operator */ + void checkIntersectionMin(const std::pair& pair, const Node& n); + /** apply inference rules for difference subtract */ + void checkDifferenceSubtract(const std::pair& pair, + const Node& n); + /** apply inference rules for difference remove */ + void checkDifferenceRemove(const std::pair& 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& 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& 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>> 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 */ diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index e2b220777..92aa1a0ea 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -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& 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& 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& children) +{ + Assert(premise.getType().isBoolean()); + Assert(!children.empty()); + InferInfo inferInfo(d_im, InferenceId::BAGS_CARD); + + std::set::iterator it = children.begin(); + Node child = *it; + d_state->registerBag(child); + Node unionDisjoints = child; + Node card = d_nm->mkNode(BAG_CARD, child); + std::vector 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); diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index 29da01629..2815058b2 100644 --- a/src/theory/bags/inference_generator.h +++ b/src/theory/bags/inference_generator.h @@ -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& 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& 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& children); + /** * @param n is (bag.map f A) where f is a function (-> E T), A a bag of type * (Bag E) diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp index 52cbb8671..575dcf577 100644 --- a/src/theory/bags/solver_state.cpp +++ b/src/theory/bags/solver_state.cpp @@ -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 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& SolverState::getBags() { return d_bags; } +const std::map& SolverState::getCardinalityTerms() +{ + return d_cardTerms; +} + std::set 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 SolverState::initialize() @@ -127,6 +166,11 @@ std::vector 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; diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h index 64c4b1674..4e3997793 100644 --- a/src/theory/bags/solver_state.h +++ b/src/theory/bags/solver_state.h @@ -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& getBags(); + + /** + * get all cardinality terms + * @return a map from registered card terms to their skolem variables + */ + const std::map& 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>> d_bagElements; /** Disequal bag terms */ std::set d_deq; + /** a map from card terms to their skolem variables */ + std::map d_cardTerms; }; /* class SolverState */ } // namespace bags diff --git a/src/theory/bags/strategy.cpp b/src/theory/bags/strategy.cpp index 541be9ac7..e2517100b 100644 --- a/src/theory/bags/strategy.cpp +++ b/src/theory/bags/strategy.cpp @@ -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 diff --git a/src/theory/bags/strategy.h b/src/theory/bags/strategy.h index 7dc5d693c..19bf2b177 100644 --- a/src/theory/bags/strategy.h +++ b/src/theory/bags/strategy.h @@ -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); diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index cfd6f1178..720e97c25 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -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& lems) switch (atom.getKind()) { case kind::BAG_CHOOSE: return expandChooseOperator(atom, lems); - case kind::BAG_CARD: - { - std::vector 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 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 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(); + const Rational& constructedRational = + constructedBagCard.getConst(); + 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 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; } diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index cc76c5453..18e306e95 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -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; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f521e77ed..b746102b5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -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 index 000000000..4e37eb717 --- /dev/null +++ b/test/regress/regress1/bags/card3.smt2 @@ -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 index 000000000..37003ae02 --- /dev/null +++ b/test/regress/regress1/bags/fol_0000119.smt2 @@ -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) -- 2.30.2