diff options
Diffstat (limited to 'src/theory/bags/inference_generator.cpp')
-rw-r--r-- | src/theory/bags/inference_generator.cpp | 175 |
1 files changed, 164 insertions, 11 deletions
diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 556dc76d6..734572f7c 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -20,6 +20,7 @@ #include "expr/skolem_manager.h" #include "theory/bags/inference_manager.h" #include "theory/bags/solver_state.h" +#include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/uf/equality_engine.h" #include "util/rational.h" @@ -42,7 +43,7 @@ InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e) Assert(n.getType().isBag()); Assert(e.getType() == n.getType().getBagElementType()); - InferInfo inferInfo(d_im, InferenceId::BAG_NON_NEGATIVE_COUNT); + InferInfo inferInfo(d_im, InferenceId::BAGS_NON_NEGATIVE_COUNT); Node count = d_nm->mkNode(kind::BAG_COUNT, e, n); Node gte = d_nm->mkNode(kind::GEQ, count, d_zero); @@ -59,7 +60,7 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e) { // TODO issue #78: refactor this with BagRewriter // (=> true (= (bag.count e (bag e c)) c)) - InferInfo inferInfo(d_im, InferenceId::BAG_MK_BAG_SAME_ELEMENT); + InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG_SAME_ELEMENT); Node skolem = getSkolem(n, inferInfo); Node count = getMultiplicityTerm(e, skolem); inferInfo.d_conclusion = count.eqNode(n[1]); @@ -70,7 +71,7 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e) // (=> // true // (= (bag.count e (bag x c)) (ite (= e x) c 0))) - InferInfo inferInfo(d_im, InferenceId::BAG_MK_BAG); + InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG); Node skolem = getSkolem(n, inferInfo); Node count = getMultiplicityTerm(e, skolem); Node same = d_nm->mkNode(kind::EQUAL, n[0], e); @@ -81,6 +82,27 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e) } } +/** + * A bound variable corresponding to the universally quantified integer + * variable used to range over the distinct elements in a bag, used + * for axiomatizing the behavior of some term. + */ +struct FirstIndexVarAttributeId +{ +}; +typedef expr::Attribute<FirstIndexVarAttributeId, Node> FirstIndexVarAttribute; + +/** + * A bound variable corresponding to the universally quantified integer + * variable used to range over the distinct elements in a bag, used + * for axiomatizing the behavior of some term. + */ +struct SecondIndexVarAttributeId +{ +}; +typedef expr::Attribute<SecondIndexVarAttributeId, Node> + SecondIndexVarAttribute; + struct BagsDeqAttributeId { }; @@ -93,7 +115,7 @@ InferInfo InferenceGenerator::bagDisequality(Node n) Node A = n[0]; Node B = n[1]; - InferInfo inferInfo(d_im, InferenceId::BAG_DISEQUALITY); + InferInfo inferInfo(d_im, InferenceId::BAGS_DISEQUALITY); TypeNode elementType = A.getType().getBagElementType(); BoundVarManager* bvm = d_nm->getBoundVarManager(); @@ -126,7 +148,7 @@ InferInfo InferenceGenerator::empty(Node n, Node e) Assert(n.getKind() == kind::EMPTYBAG); Assert(e.getType() == n.getType().getBagElementType()); - InferInfo inferInfo(d_im, InferenceId::BAG_EMPTY); + InferInfo inferInfo(d_im, InferenceId::BAGS_EMPTY); Node skolem = getSkolem(n, inferInfo); Node count = getMultiplicityTerm(e, skolem); @@ -142,7 +164,7 @@ InferInfo InferenceGenerator::unionDisjoint(Node n, Node e) Node A = n[0]; Node B = n[1]; - InferInfo inferInfo(d_im, InferenceId::BAG_UNION_DISJOINT); + InferInfo inferInfo(d_im, InferenceId::BAGS_UNION_DISJOINT); Node countA = getMultiplicityTerm(e, A); Node countB = getMultiplicityTerm(e, B); @@ -164,7 +186,7 @@ InferInfo InferenceGenerator::unionMax(Node n, Node e) Node A = n[0]; Node B = n[1]; - InferInfo inferInfo(d_im, InferenceId::BAG_UNION_MAX); + InferInfo inferInfo(d_im, InferenceId::BAGS_UNION_MAX); Node countA = getMultiplicityTerm(e, A); Node countB = getMultiplicityTerm(e, B); @@ -187,7 +209,7 @@ InferInfo InferenceGenerator::intersection(Node n, Node e) Node A = n[0]; Node B = n[1]; - InferInfo inferInfo(d_im, InferenceId::BAG_INTERSECTION_MIN); + InferInfo inferInfo(d_im, InferenceId::BAGS_INTERSECTION_MIN); Node countA = getMultiplicityTerm(e, A); Node countB = getMultiplicityTerm(e, B); @@ -208,7 +230,7 @@ InferInfo InferenceGenerator::differenceSubtract(Node n, Node e) Node A = n[0]; Node B = n[1]; - InferInfo inferInfo(d_im, InferenceId::BAG_DIFFERENCE_SUBTRACT); + InferInfo inferInfo(d_im, InferenceId::BAGS_DIFFERENCE_SUBTRACT); Node countA = getMultiplicityTerm(e, A); Node countB = getMultiplicityTerm(e, B); @@ -230,7 +252,7 @@ InferInfo InferenceGenerator::differenceRemove(Node n, Node e) Node A = n[0]; Node B = n[1]; - InferInfo inferInfo(d_im, InferenceId::BAG_DIFFERENCE_REMOVE); + InferInfo inferInfo(d_im, InferenceId::BAGS_DIFFERENCE_REMOVE); Node countA = getMultiplicityTerm(e, A); Node countB = getMultiplicityTerm(e, B); @@ -251,7 +273,7 @@ InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e) Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; - InferInfo inferInfo(d_im, InferenceId::BAG_DUPLICATE_REMOVAL); + InferInfo inferInfo(d_im, InferenceId::BAGS_DUPLICATE_REMOVAL); Node countA = getMultiplicityTerm(e, A); Node skolem = getSkolem(n, inferInfo); @@ -270,6 +292,137 @@ Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag) return count; } +std::tuple<InferInfo, Node, Node> InferenceGenerator::mapDownwards(Node n, + Node e) +{ + Assert(n.getKind() == kind::BAG_MAP && n[1].getType().isBag()); + Assert(n[0].getType().isFunction() + && n[0].getType().getArgTypes().size() == 1); + Assert(e.getType() == n[0].getType().getRangeType()); + + InferInfo inferInfo(d_im, InferenceId::BAGS_MAP); + + Node f = n[0]; + Node A = n[1]; + // declare an uninterpreted function uf: Int -> T + TypeNode domainType = f.getType().getArgTypes()[0]; + TypeNode ufType = d_nm->mkFunctionType(d_nm->integerType(), domainType); + Node uf = + d_sm->mkSkolemFunction(SkolemFunId::BAGS_MAP_PREIMAGE, ufType, {n, e}); + + // declare uninterpreted function sum: Int -> Int + TypeNode sumType = + d_nm->mkFunctionType(d_nm->integerType(), d_nm->integerType()); + Node sum = d_sm->mkSkolemFunction(SkolemFunId::BAGS_MAP_SUM, sumType, {n, e}); + + // (= (sum 0) 0) + Node sum_zero = d_nm->mkNode(kind::APPLY_UF, sum, d_zero); + Node baseCase = d_nm->mkNode(Kind::EQUAL, sum_zero, d_zero); + + // guess the size of the preimage of e + Node preImageSize = d_sm->mkDummySkolem("preImageSize", d_nm->integerType()); + + // (= (sum preImageSize) (bag.count e skolem)) + Node mapSkolem = getSkolem(n, inferInfo); + Node countE = getMultiplicityTerm(e, mapSkolem); + Node totalSum = d_nm->mkNode(kind::APPLY_UF, sum, preImageSize); + Node totalSumEqualCountE = d_nm->mkNode(kind::EQUAL, totalSum, countE); + + // (forall ((i Int)) + // (let ((uf_i (uf i))) + // (let ((count_uf_i (bag.count uf_i A))) + // (=> + // (and (>= i 1) (<= i preImageSize)) + // (and + // (= (f uf_i) e) + // (>= count_uf_i 1) + // (= (sum i) (+ (sum (- i 1)) count_uf_i)) + // (forall ((j Int)) + // (=> + // (and (< i j) (<= j preImageSize)) + // (not (= (uf i) (uf j)))))) + // ))))) + + BoundVarManager* bvm = d_nm->getBoundVarManager(); + Node i = bvm->mkBoundVar<FirstIndexVarAttribute>(n, "i", d_nm->integerType()); + Node j = + bvm->mkBoundVar<SecondIndexVarAttribute>(n, "j", d_nm->integerType()); + Node iList = d_nm->mkNode(kind::BOUND_VAR_LIST, i); + Node jList = d_nm->mkNode(kind::BOUND_VAR_LIST, j); + Node iPlusOne = d_nm->mkNode(kind::PLUS, i, d_one); + Node iMinusOne = d_nm->mkNode(kind::MINUS, i, d_one); + Node uf_i = d_nm->mkNode(kind::APPLY_UF, uf, i); + Node uf_j = d_nm->mkNode(kind::APPLY_UF, uf, j); + Node f_uf_i = d_nm->mkNode(kind::APPLY_UF, f, uf_i); + Node uf_iPlusOne = d_nm->mkNode(kind::APPLY_UF, uf, iPlusOne); + Node uf_iMinusOne = d_nm->mkNode(kind::APPLY_UF, uf, iMinusOne); + Node interval_i = d_nm->mkNode(kind::AND, + d_nm->mkNode(kind::GEQ, i, d_one), + d_nm->mkNode(kind::LEQ, i, preImageSize)); + Node sum_i = d_nm->mkNode(kind::APPLY_UF, sum, i); + Node sum_iPlusOne = d_nm->mkNode(kind::APPLY_UF, sum, iPlusOne); + Node sum_iMinusOne = d_nm->mkNode(kind::APPLY_UF, sum, iMinusOne); + Node count_iMinusOne = d_nm->mkNode(kind::BAG_COUNT, uf_iMinusOne, A); + Node count_uf_i = d_nm->mkNode(kind::BAG_COUNT, uf_i, A); + Node inductiveCase = d_nm->mkNode( + Kind::EQUAL, sum_i, d_nm->mkNode(kind::PLUS, sum_iMinusOne, count_uf_i)); + Node f_iEqualE = d_nm->mkNode(kind::EQUAL, f_uf_i, e); + Node geqOne = d_nm->mkNode(kind::GEQ, count_uf_i, d_one); + + // i < j <= preImageSize + Node interval_j = d_nm->mkNode(kind::AND, + d_nm->mkNode(kind::LT, i, j), + d_nm->mkNode(kind::LEQ, j, preImageSize)); + // uf(i) != uf(j) + Node uf_i_equals_uf_j = d_nm->mkNode(kind::EQUAL, uf_i, uf_j); + Node notEqual = d_nm->mkNode(kind::EQUAL, uf_i, uf_j).negate(); + Node body_j = d_nm->mkNode(kind::OR, interval_j.negate(), notEqual); + Node forAll_j = quantifiers::BoundedIntegers::mkBoundedForall(jList, body_j); + Node andNode = + d_nm->mkNode(kind::AND, {f_iEqualE, geqOne, inductiveCase, forAll_j}); + Node body_i = d_nm->mkNode(kind::OR, interval_i.negate(), andNode); + Node forAll_i = quantifiers::BoundedIntegers::mkBoundedForall(iList, body_i); + Node preImageGTE_zero = d_nm->mkNode(kind::GEQ, preImageSize, d_zero); + Node conclusion = d_nm->mkNode( + kind::AND, {baseCase, totalSumEqualCountE, forAll_i, preImageGTE_zero}); + inferInfo.d_conclusion = conclusion; + + std::map<Node, Node> m; + m[e] = conclusion; + return std::tuple(inferInfo, uf, preImageSize); +} + +InferInfo InferenceGenerator::mapUpwards( + Node n, Node uf, Node preImageSize, Node y, Node x) +{ + Assert(n.getKind() == kind::BAG_MAP && n[1].getType().isBag()); + Assert(n[0].getType().isFunction() + && n[0].getType().getArgTypes().size() == 1); + + InferInfo inferInfo(d_im, InferenceId::BAGS_MAP); + Node f = n[0]; + Node A = n[1]; + + Node countA = getMultiplicityTerm(x, A); + Node xInA = d_nm->mkNode(kind::GEQ, countA, d_one); + Node notEqual = + d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f, x), y).negate(); + + Node k = d_sm->mkDummySkolem("k", d_nm->integerType()); + Node inRange = d_nm->mkNode(kind::AND, + d_nm->mkNode(kind::GEQ, k, d_one), + d_nm->mkNode(kind::LEQ, k, preImageSize)); + Node equal = + d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, uf, k), x); + Node andNode = d_nm->mkNode(kind::AND, inRange, equal); + Node orNode = d_nm->mkNode(kind::OR, notEqual, andNode); + Node implies = d_nm->mkNode(kind::IMPLIES, xInA, orNode); + inferInfo.d_conclusion = implies; + std::cout << "Upwards conclusion: " << inferInfo.d_conclusion << std::endl + << std::endl; + return inferInfo; +} + } // namespace bags } // namespace theory } // namespace cvc5 |