/**
* 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<IndexVarAttributeId, Node> IndexVarAttribute;
+typedef expr::Attribute<FirstIndexVarAttributeId, Node> 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<SecondIndexVarAttributeId, Node>
+ SecondIndexVarAttribute;
Node BagReduction::reduceFoldOperator(Node node, std::vector<Node>& asserts)
{
SkolemFunId::BAGS_FOLD_COMBINE, combineType, {f, t, A});
BoundVarManager* bvm = nm->getBoundVarManager();
- Node i = bvm->mkBoundVar<IndexVarAttribute>(node, "i", nm->integerType());
+ Node i =
+ bvm->mkBoundVar<FirstIndexVarAttribute>(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);
return Node::null();
}
+Node BagReduction::reduceCardOperator(Node node, std::vector<Node>& 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<FirstIndexVarAttribute>(node, "i", nm->integerType());
+ Node j =
+ bvm->mkBoundVar<SecondIndexVarAttribute>(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
* 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)))
* (=>
* (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<Node>& 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<Node>& asserts);
+
private:
};
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<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;
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();
return TrustNode::mkTrustRewrite(node, ret, nullptr);
}
-TrustNode TheoryBags::expandCardOperator(TNode n, std::vector<SkolemLemma>&)
-{
- 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();
projects / cvc5.git / commitdiff