From 9b81d04da42615642c2fd4ec6b4637862848ae0a Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Mon, 13 Dec 2021 16:16:30 -0600 Subject: [PATCH] A more efficient implementation for bag.card operator (#7797) This PR provides a fold like implementation for bag.card operator that does not depends on higher order logic, although it still requires finite model finding. --- src/expr/skolem_manager.cpp | 5 ++ src/expr/skolem_manager.h | 4 ++ src/theory/bags/bag_reduction.cpp | 100 ++++++++++++++++++++++++-- src/theory/bags/bag_reduction.h | 54 ++++++++++---- src/theory/bags/theory_bags.cpp | 36 ++++------ src/theory/bags/theory_bags.h | 2 - src/theory/inference_id.cpp | 1 + src/theory/inference_id.h | 1 + test/regress/CMakeLists.txt | 1 + test/regress/regress1/bags/card1.smt2 | 11 +-- test/regress/regress1/bags/card2.smt2 | 11 +++ 11 files changed, 180 insertions(+), 46 deletions(-) create mode 100644 test/regress/regress1/bags/card2.smt2 diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 476517820..206ebb9ce 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -67,6 +67,11 @@ const char* toString(SkolemFunId id) case SkolemFunId::SK_FIRST_MATCH: return "SK_FIRST_MATCH"; case SkolemFunId::SK_FIRST_MATCH_POST: return "SK_FIRST_MATCH_POST"; case SkolemFunId::RE_UNFOLD_POS_COMPONENT: return "RE_UNFOLD_POS_COMPONENT"; + case SkolemFunId::BAGS_CARD_CARDINALITY: return "BAGS_CARD_CARDINALITY"; + case SkolemFunId::BAGS_CARD_ELEMENTS: return "BAGS_CARD_ELEMENTS"; + case SkolemFunId::BAGS_CARD_N: return "BAGS_CARD_N"; + case SkolemFunId::BAGS_CARD_UNION_DISJOINT: + return "BAGS_CARD_UNION_DISJOINT"; case SkolemFunId::BAGS_CHOOSE: return "BAGS_CHOOSE"; case SkolemFunId::BAGS_FOLD_CARD: return "BAGS_FOLD_CARD"; case SkolemFunId::BAGS_FOLD_COMBINE: return "BAGS_FOLD_COMBINE"; diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 780413d17..93b26b6cb 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -112,6 +112,10 @@ enum class SkolemFunId * i = 0, ..., n. */ RE_UNFOLD_POS_COMPONENT, + BAGS_CARD_CARDINALITY, + BAGS_CARD_ELEMENTS, + BAGS_CARD_N, + BAGS_CARD_UNION_DISJOINT, BAGS_FOLD_CARD, BAGS_FOLD_COMBINE, BAGS_FOLD_ELEMENTS, diff --git a/src/theory/bags/bag_reduction.cpp b/src/theory/bags/bag_reduction.cpp index 9203a1c45..6e1b4c1a5 100644 --- a/src/theory/bags/bag_reduction.cpp +++ b/src/theory/bags/bag_reduction.cpp @@ -34,13 +34,26 @@ BagReduction::~BagReduction() {} /** * A bound variable corresponding to the universally quantified integer - * variable used to range over the distinct elements in a bag, used + * variable used to range over (may be distinct) elements in a bag, used * for axiomatizing the behavior of some term. + * If there are multiple quantifiers, this variable should be the first one. */ -struct IndexVarAttributeId +struct FirstIndexVarAttributeId { }; -typedef expr::Attribute IndexVarAttribute; +typedef expr::Attribute FirstIndexVarAttribute; + +/** + * A bound variable corresponding to the universally quantified integer + * variable used to range over (may be distinct) elements in a bag, used + * for axiomatizing the behavior of some term. + * This variable should be the second of multiple quantifiers. + */ +struct SecondIndexVarAttributeId +{ +}; +typedef expr::Attribute + SecondIndexVarAttribute; Node BagReduction::reduceFoldOperator(Node node, std::vector& asserts) { @@ -71,7 +84,8 @@ Node BagReduction::reduceFoldOperator(Node node, std::vector& asserts) SkolemFunId::BAGS_FOLD_COMBINE, combineType, {f, t, A}); BoundVarManager* bvm = nm->getBoundVarManager(); - Node i = bvm->mkBoundVar(node, "i", nm->integerType()); + Node i = + bvm->mkBoundVar(node, "i", nm->integerType()); Node iList = nm->mkNode(BOUND_VAR_LIST, i); Node iMinusOne = nm->mkNode(MINUS, i, one); Node uf_i = nm->mkNode(APPLY_UF, uf, i); @@ -114,6 +128,84 @@ Node BagReduction::reduceFoldOperator(Node node, std::vector& asserts) return Node::null(); } +Node BagReduction::reduceCardOperator(Node node, std::vector& asserts) +{ + Assert(node.getKind() == BAG_CARD); + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + Node A = node[0]; + Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + // types + TypeNode bagType = A.getType(); + TypeNode elementType = A.getType().getBagElementType(); + TypeNode integerType = nm->integerType(); + TypeNode ufType = nm->mkFunctionType(integerType, elementType); + TypeNode cardinalityType = nm->mkFunctionType(integerType, integerType); + TypeNode unionDisjointType = nm->mkFunctionType(integerType, bagType); + // skolem functions + Node n = sm->mkSkolemFunction(SkolemFunId::BAGS_CARD_N, integerType, A); + Node uf = sm->mkSkolemFunction(SkolemFunId::BAGS_CARD_ELEMENTS, ufType, A); + Node unionDisjoint = sm->mkSkolemFunction( + SkolemFunId::BAGS_CARD_UNION_DISJOINT, unionDisjointType, A); + Node cardinality = sm->mkSkolemFunction( + SkolemFunId::BAGS_CARD_CARDINALITY, cardinalityType, A); + + BoundVarManager* bvm = nm->getBoundVarManager(); + Node i = + bvm->mkBoundVar(node, "i", nm->integerType()); + Node j = + bvm->mkBoundVar(node, "j", nm->integerType()); + Node iList = nm->mkNode(BOUND_VAR_LIST, i); + Node jList = nm->mkNode(BOUND_VAR_LIST, j); + Node iMinusOne = nm->mkNode(MINUS, i, one); + Node uf_i = nm->mkNode(APPLY_UF, uf, i); + Node uf_j = nm->mkNode(APPLY_UF, uf, j); + Node cardinality_0 = nm->mkNode(APPLY_UF, cardinality, zero); + Node cardinality_iMinusOne = nm->mkNode(APPLY_UF, cardinality, iMinusOne); + Node cardinality_i = nm->mkNode(APPLY_UF, cardinality, i); + Node cardinality_n = nm->mkNode(APPLY_UF, cardinality, n); + Node unionDisjoint_0 = nm->mkNode(APPLY_UF, unionDisjoint, zero); + Node unionDisjoint_iMinusOne = nm->mkNode(APPLY_UF, unionDisjoint, iMinusOne); + Node unionDisjoint_i = nm->mkNode(APPLY_UF, unionDisjoint, i); + Node unionDisjoint_n = nm->mkNode(APPLY_UF, unionDisjoint, n); + Node cardinality_0_equal = cardinality_0.eqNode(zero); + Node uf_i_multiplicity = nm->mkNode(BAG_COUNT, uf_i, A); + Node cardinality_i_equal = cardinality_i.eqNode( + nm->mkNode(PLUS, uf_i_multiplicity, cardinality_iMinusOne)); + Node unionDisjoint_0_equal = + unionDisjoint_0.eqNode(nm->mkConst(EmptyBag(bagType))); + Node bag = nm->mkBag(elementType, uf_i, uf_i_multiplicity); + + Node unionDisjoint_i_equal = unionDisjoint_i.eqNode( + nm->mkNode(BAG_UNION_DISJOINT, bag, unionDisjoint_iMinusOne)); + // 1 <= i <= n + Node interval_i = + nm->mkNode(AND, nm->mkNode(GEQ, i, one), nm->mkNode(LEQ, i, n)); + + // i < j <= n + Node interval_j = + nm->mkNode(AND, nm->mkNode(LT, i, j), nm->mkNode(LEQ, j, n)); + // uf(i) != uf(j) + Node uf_i_equals_uf_j = nm->mkNode(EQUAL, uf_i, uf_j); + Node notEqual = nm->mkNode(EQUAL, uf_i, uf_j).negate(); + Node body_j = nm->mkNode(OR, interval_j.negate(), notEqual); + Node forAll_j = quantifiers::BoundedIntegers::mkBoundedForall(jList, body_j); + Node body_i = nm->mkNode( + IMPLIES, + interval_i, + nm->mkNode(AND, cardinality_i_equal, unionDisjoint_i_equal, forAll_j)); + Node forAll_i = quantifiers::BoundedIntegers::mkBoundedForall(iList, body_i); + Node nonNegative = nm->mkNode(GEQ, n, zero); + Node unionDisjoint_n_equal = A.eqNode(unionDisjoint_n); + asserts.push_back(forAll_i); + asserts.push_back(cardinality_0_equal); + asserts.push_back(unionDisjoint_0_equal); + asserts.push_back(unionDisjoint_n_equal); + asserts.push_back(nonNegative); + return cardinality_n; +} + } // namespace bags } // namespace theory } // namespace cvc5 diff --git a/src/theory/bags/bag_reduction.h b/src/theory/bags/bag_reduction.h index 11f091f94..694379dfc 100644 --- a/src/theory/bags/bag_reduction.h +++ b/src/theory/bags/bag_reduction.h @@ -41,9 +41,8 @@ class BagReduction : EnvObj * t: T2 is the initial value * A: (Bag T1) is a bag * @param asserts a list of assertions generated by this reduction - * @return the reduction term (combine n) such that - * (and - * (forall ((i Int)) + * @return the reduction term (combine n) with asserts: + * - (forall ((i Int)) * (let ((iMinusOne (- i 1))) * (let ((uf_i (uf i))) * (=> @@ -55,18 +54,49 @@ class BagReduction : EnvObj * (bag.union_disjoint * (bag uf_i 1) * (unionDisjoint iMinusOne)))))))) - * (= (combine 0) t) - * (= (unionDisjoint 0) (as bag.empty (Bag T1))) - * (= A (unionDisjoint n)) - * (>= n 0)) - * where - * n: Int is the cardinality of bag A - * uf:Int -> T1 is an uninterpreted function that represents elements of A - * combine: Int -> T2 is an uninterpreted function - * unionDisjoint: Int -> (Bag T1) is an uninterpreted function + * - (= (combine 0) t) + * - (= (unionDisjoint 0) (as bag.empty (Bag T1))) + * - (= A (unionDisjoint n)) + * - (>= n 0)) + * where + * n: Int is the cardinality of bag A + * uf:Int -> T1 is an uninterpreted function that represents elements of A + * combine: Int -> T2 is an uninterpreted function + * unionDisjoint: Int -> (Bag T1) is an uninterpreted function */ Node reduceFoldOperator(Node node, std::vector& asserts); + /** + * @param node a term of the form (bag.card A) where A: (Bag T) is a bag + * @param asserts a list of assertions generated by this reduction + * @return the reduction term (cardinality n) with asserts: + * - (forall ((i Int)) + * (let ((uf_i (uf i))) + * (let ((count_uf_i (bag.count uf_i A))) + * (=> + * (and (>= i 1) (<= i n)) + * (and + * (= (cardinality i) (+ count_uf_i (cardinality (- i 1)))) + * (= + * (unionDisjoint i) + * (bag.union_disjoint (bag uf_i count_uf_i) (unionDisjoint (- i 1)))) + * (forall ((j Int)) + * (or (not (and (< i j) (<= j n))) + * (not (= (uf i) (uf j)))))))))) + * - (= (cardinality 0) 0) + * - (= (unionDisjoint 0) (as bag.empty (Bag String))) + * - (= A (unionDisjoint n)) + * - (>= n 0) + * + * where + * n: number of distinct elements in A + * uf:Int -> T is an uninterpreted function that represents distinct + * elements of A + * cardinality: Int -> Int is an uninterpreted function + * unionDisjoint: Int -> (Bag T1) is an uninterpreted function + */ + Node reduceCardOperator(Node node, std::vector& asserts); + private: }; diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 522f6749c..0694c179b 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -88,7 +88,18 @@ TrustNode TheoryBags::ppRewrite(TNode atom, std::vector& lems) switch (atom.getKind()) { case kind::BAG_CHOOSE: return expandChooseOperator(atom, lems); - case kind::BAG_CARD: return expandCardOperator(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; @@ -98,7 +109,7 @@ TrustNode TheoryBags::ppRewrite(TNode atom, std::vector& lems) d_im.lemma(andNode, InferenceId::BAGS_FOLD); Trace("bags::ppr") << "reduce(" << atom << ") = " << ret << " such that:" << std::endl - << asserts << std::endl; + << andNode << std::endl; return TrustNode::mkTrustRewrite(atom, ret, nullptr); } default: return TrustNode::null(); @@ -145,27 +156,6 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node, return TrustNode::mkTrustRewrite(node, ret, nullptr); } -TrustNode TheoryBags::expandCardOperator(TNode n, std::vector&) -{ - Assert(n.getKind() == BAG_CARD); - if (d_env.getLogicInfo().isHigherOrder()) - { - // (bag.card A) = (bag.count 1 (bag.map (lambda ((x E)) 1) A)), - // where E is the type of elements of A - NodeManager* nm = NodeManager::currentNM(); - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); - TypeNode type = n[0].getType().getBagElementType(); - Node x = nm->mkBoundVar("x", type); - Node lambda = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, x), one); - Node map = nm->mkNode(kind::BAG_MAP, lambda, n[0]); - Node countOne = nm->mkNode(kind::BAG_COUNT, one, map); - Trace("TheoryBags::ppRewrite") - << "ppRewrite(" << n << ") = " << countOne << std::endl; - return TrustNode::mkTrustRewrite(n, countOne, nullptr); - } - return TrustNode::null(); -} - void TheoryBags::postCheck(Effort effort) { d_im.doPendingFacts(); diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index 1a8af780e..8d15947ef 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -93,8 +93,6 @@ class TheoryBags : public Theory /** expand the definition of the bag.choose operator */ TrustNode expandChooseOperator(const Node& node, std::vector& lems); - /** expand the definition of bag.card operator */ - TrustNode expandCardOperator(TNode n, std::vector& lems); /** The state of the bags solver at full effort */ SolverState d_state; diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index d4fc32197..ced885abb 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -119,6 +119,7 @@ const char* toString(InferenceId i) case InferenceId::BAGS_DUPLICATE_REMOVAL: return "BAGS_DUPLICATE_REMOVAL"; case InferenceId::BAGS_MAP: return "BAGS_MAP"; case InferenceId::BAGS_FOLD: return "BAGS_FOLD"; + case InferenceId::BAGS_CARD: return "BAGS_CARD"; case InferenceId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT"; case InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA: diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index d5a3e1b2c..f0c726f78 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -181,6 +181,7 @@ enum class InferenceId BAGS_DUPLICATE_REMOVAL, BAGS_MAP, BAGS_FOLD, + BAGS_CARD, // ---------------------------------- end bags theory // ---------------------------------- bitvector theory diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3be63c46d..20722a1da 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1605,6 +1605,7 @@ set(regress_1_tests regress1/bug694-Unapply1.scala-0.smt2 regress1/bug800.smt2 regress1/bags/card1.smt2 + regress1/bags/card2.smt2 regress1/bags/choose1.smt2 regress1/bags/choose2.smt2 regress1/bags/choose3.smt2 diff --git a/test/regress/regress1/bags/card1.smt2 b/test/regress/regress1/bags/card1.smt2 index 4ea5488d2..3b19fb2cf 100644 --- a/test/regress/regress1/bags/card1.smt2 +++ b/test/regress/regress1/bags/card1.smt2 @@ -1,7 +1,8 @@ -; COMMAND-LINE: --fmf-bound --uf-lazy-ll -; EXPECT: sat -(set-logic HO_ALL) -(define-fun f ((x String)) Int 1) +(set-logic ALL) +(set-option :fmf-bound true) +(set-option :produce-models true) +(set-info :status sat) (declare-fun A () (Bag String)) -(assert (= (bag.card A) 20)) +(assert (= (bag.card A) 10000000)) (check-sat) + diff --git a/test/regress/regress1/bags/card2.smt2 b/test/regress/regress1/bags/card2.smt2 new file mode 100644 index 000000000..260c6927f --- /dev/null +++ b/test/regress/regress1/bags/card2.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-option :fmf-bound true) +(set-option :produce-models true) +(set-info :status sat) +(declare-fun A () (Bag String)) +(declare-fun B () (Bag String)) +(declare-fun C () (Bag String)) +(assert (distinct A B C (as bag.empty (Bag String)))) +(assert (= C (bag.union_disjoint A B))) +(assert (= (bag.card C) 10000000)) +(check-sat) -- 2.30.2