Merge branch 'master' into issue7504issue7504

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