(define set.filter (# x term (# y term (apply (apply f_set.filter x) y))))
(declare f_set.map term)
(define set.map (# x term (# y term (apply (apply f_set.map x) y))))
+(declare f_set.fold term)
+(define set.fold (# x term (# y term (# z term (apply (apply (apply f_set.fold x) y) z)))))
;; ---- Bags
(declare bag.empty (! s sort term))
theory/sets/normal_form.h
theory/sets/rels_utils.cpp
theory/sets/rels_utils.h
+ theory/sets/set_reduction.cpp
+ theory/sets/set_reduction.h
theory/sets/skolem_cache.cpp
theory/sets/skolem_cache.h
theory/sets/solver_state.cpp
KIND_ENUM(SET_IS_SINGLETON, internal::Kind::SET_IS_SINGLETON),
KIND_ENUM(SET_MAP, internal::Kind::SET_MAP),
KIND_ENUM(SET_FILTER, internal::Kind::SET_FILTER),
+ KIND_ENUM(SET_FOLD, internal::Kind::SET_FOLD),
/* Relations -------------------------------------------------------- */
KIND_ENUM(RELATION_JOIN, internal::Kind::RELATION_JOIN),
KIND_ENUM(RELATION_PRODUCT, internal::Kind::RELATION_PRODUCT),
{internal::Kind::SET_IS_SINGLETON, SET_IS_SINGLETON},
{internal::Kind::SET_MAP, SET_MAP},
{internal::Kind::SET_FILTER, SET_FILTER},
+ {internal::Kind::SET_FOLD, SET_FOLD},
/* Relations ------------------------------------------------------- */
{internal::Kind::RELATION_JOIN, RELATION_JOIN},
{internal::Kind::RELATION_PRODUCT, RELATION_PRODUCT},
* \endrst
*/
SET_FILTER,
+ /**
+ * Set fold.
+ *
+ * \rst
+ * This operator combines elements of a set into a single value.
+ * (set.fold :math:`f \; t \; A`) folds the elements of set :math:`A`
+ * starting with Term :math:`t` and using the combining function :math:`f`.
+ *
+ * - Arity: ``2``
+ *
+ * - ``1:`` Term of function Sort :math:`(\rightarrow S_1 \; S_2 \; S_2)`
+ * - ``2:`` Term of Sort :math:`S_2` (the initial value)
+ * - ``3:`` Term of bag Sort (Set :math:`S_1`)
+ * \endrst
+ *
+ * - Create Term of this Kind with:
+ *
+ * - Solver::mkTerm(Kind, const std::vector<Term>&) const
+ * - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
+ */
+ SET_FOLD,
/* Relations ------------------------------------------------------------- */
/**
* - Solver::mkTerm(Kind, const std::vector<Term>&) const
* - Solver::mkTerm(const Op&, const std::vector<Term>&) const
*
- * - Create Op of this kind with:
- *
- * - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
- *
* \rst
* .. warning:: This kind is experimental and may be changed or removed in
* future versions.
case SkolemFunId::BAGS_DEQ_DIFF: return "BAGS_DEQ_DIFF";
case SkolemFunId::SETS_CHOOSE: return "SETS_CHOOSE";
case SkolemFunId::SETS_DEQ_DIFF: return "SETS_DEQ_DIFF";
+ case SkolemFunId::SETS_FOLD_CARD: return "SETS_FOLD_CARD";
+ case SkolemFunId::SETS_FOLD_COMBINE: return "SETS_FOLD_COMBINE";
+ case SkolemFunId::SETS_FOLD_ELEMENTS: return "SETS_FOLD_ELEMENTS";
+ case SkolemFunId::SETS_FOLD_UNION: return "SETS_FOLD_UNION";
case SkolemFunId::SETS_MAP_DOWN_ELEMENT: return "SETS_MAP_DOWN_ELEMENT";
case SkolemFunId::HO_TYPE_MATCH_PRED: return "HO_TYPE_MATCH_PRED";
default: return "?";
SETS_CHOOSE,
/** set diff to witness (not (= A B)) */
SETS_DEQ_DIFF,
+ SETS_FOLD_CARD,
+ SETS_FOLD_COMBINE,
+ SETS_FOLD_ELEMENTS,
+ SETS_FOLD_UNION,
/**
* A skolem variable that is unique per terms (set.map f A), y which is an
* element in (set.map f A). The skolem is constrained to be an element in A,
addOperator(cvc5::SET_IS_SINGLETON, "set.is_singleton");
addOperator(cvc5::SET_MAP, "set.map");
addOperator(cvc5::SET_FILTER, "set.filter");
+ addOperator(cvc5::SET_FOLD, "set.fold");
addOperator(cvc5::RELATION_JOIN, "rel.join");
addOperator(cvc5::RELATION_PRODUCT, "rel.product");
addOperator(cvc5::RELATION_TRANSPOSE, "rel.transpose");
case kind::SET_IS_SINGLETON: return "set.is_singleton";
case kind::SET_MAP: return "set.map";
case kind::SET_FILTER: return "set.filter";
+ case kind::SET_FOLD: return "set.fold";
case kind::RELATION_JOIN: return "rel.join";
case kind::RELATION_PRODUCT: return "rel.product";
case kind::RELATION_TRANSPOSE: return "rel.transpose";
case InferenceId::SETS_EQ_MEM_CONFLICT: return "SETS_EQ_MEM_CONFLICT";
case InferenceId::SETS_FILTER_DOWN: return "SETS_FILTER_DOWN";
case InferenceId::SETS_FILTER_UP: return "SETS_FILTER_UP";
+ case InferenceId::SETS_FOLD: return "SETS_FOLD";
case InferenceId::SETS_MAP_DOWN_POSITIVE: return "SETS_MAP_DOWN_POSITIVE";
case InferenceId::SETS_MAP_UP: return "SETS_MAP_UP";
case InferenceId::SETS_MEM_EQ: return "SETS_MEM_EQ";
SETS_EQ_MEM_CONFLICT,
SETS_FILTER_DOWN,
SETS_FILTER_UP,
+ SETS_FOLD,
SETS_MAP_DOWN_POSITIVE,
SETS_MAP_UP,
SETS_MEM_EQ,
# and returns the same set excluding those elements that do not satisfy the predicate
operator SET_FILTER 2 "set filter operator"
+# set.fold operator combines elements of a set into a single value.
+# (set.fold f t A) folds the elements of bag A starting with term t and using
+# the combining function f.
+# f: a binary operation of type (-> T1 T2 T2)
+# t: an initial value of type T2
+# A: a bag of type (Set T1)
+operator SET_FOLD 3 "set fold operator"
+
operator RELATION_JOIN 2 "relation join"
operator RELATION_PRODUCT 2 "relation cartesian product"
operator RELATION_TRANSPOSE 1 "relation transpose"
typerule SET_IS_SINGLETON ::cvc5::internal::theory::sets::IsSingletonTypeRule
typerule SET_MAP ::cvc5::internal::theory::sets::SetMapTypeRule
typerule SET_FILTER ::cvc5::internal::theory::sets::SetFilterTypeRule
+typerule SET_FOLD ::cvc5::internal::theory::sets::SetFoldTypeRule
typerule RELATION_JOIN ::cvc5::internal::theory::sets::RelBinaryOperatorTypeRule
typerule RELATION_PRODUCT ::cvc5::internal::theory::sets::RelBinaryOperatorTypeRule
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Mudathir Mohamed, Andrew Reynolds, Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 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.
+ * ****************************************************************************
+ *
+ * set reduction.
+ */
+
+#include "theory/sets/set_reduction.h"
+
+#include "expr/bound_var_manager.h"
+#include "expr/emptyset.h"
+#include "expr/skolem_manager.h"
+#include "theory/datatypes/tuple_utils.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
+#include "util/rational.h"
+
+using namespace cvc5::internal;
+using namespace cvc5::internal::kind;
+
+namespace cvc5::internal {
+namespace theory {
+namespace sets {
+
+SetReduction::SetReduction() {}
+
+SetReduction::~SetReduction() {}
+
+/**
+ * A bound variable corresponding to the universally quantified integer
+ * variable used to range over (may be distinct) elements in a set, used
+ * for axiomatizing the behavior of some term.
+ * If there are multiple quantifiers, this variable should be the first one.
+ */
+struct FirstIndexVarAttributeId
+{
+};
+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 set, 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 SetReduction::reduceFoldOperator(Node node, std::vector<Node>& asserts)
+{
+ Assert(node.getKind() == SET_FOLD);
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ Node f = node[0];
+ Node t = node[1];
+ Node A = node[2];
+ Node zero = nm->mkConstInt(Rational(0));
+ Node one = nm->mkConstInt(Rational(1));
+ // types
+ TypeNode setType = A.getType();
+ TypeNode elementType = A.getType().getSetElementType();
+ TypeNode integerType = nm->integerType();
+ TypeNode ufType = nm->mkFunctionType(integerType, elementType);
+ TypeNode resultType = t.getType();
+ TypeNode combineType = nm->mkFunctionType(integerType, resultType);
+ TypeNode unionType = nm->mkFunctionType(integerType, setType);
+ // skolem functions
+ Node n = sm->mkSkolemFunction(SkolemFunId::SETS_FOLD_CARD, integerType, A);
+ Node uf = sm->mkSkolemFunction(SkolemFunId::SETS_FOLD_ELEMENTS, ufType, A);
+ Node unionNode =
+ sm->mkSkolemFunction(SkolemFunId::SETS_FOLD_UNION, unionType, A);
+ Node combine = sm->mkSkolemFunction(
+ SkolemFunId::SETS_FOLD_COMBINE, combineType, {f, t, A});
+
+ BoundVarManager* bvm = nm->getBoundVarManager();
+ Node i =
+ bvm->mkBoundVar<FirstIndexVarAttribute>(node, "i", nm->integerType());
+ Node iList = nm->mkNode(BOUND_VAR_LIST, i);
+ Node iMinusOne = nm->mkNode(SUB, i, one);
+ Node uf_i = nm->mkNode(APPLY_UF, uf, i);
+ Node combine_0 = nm->mkNode(APPLY_UF, combine, zero);
+ Node combine_iMinusOne = nm->mkNode(APPLY_UF, combine, iMinusOne);
+ Node combine_i = nm->mkNode(APPLY_UF, combine, i);
+ Node combine_n = nm->mkNode(APPLY_UF, combine, n);
+ Node union_0 = nm->mkNode(APPLY_UF, unionNode, zero);
+ Node union_iMinusOne = nm->mkNode(APPLY_UF, unionNode, iMinusOne);
+ Node union_i = nm->mkNode(APPLY_UF, unionNode, i);
+ Node union_n = nm->mkNode(APPLY_UF, unionNode, n);
+ Node combine_0_equal = combine_0.eqNode(t);
+ Node combine_i_equal =
+ combine_i.eqNode(nm->mkNode(APPLY_UF, f, uf_i, combine_iMinusOne));
+ Node union_0_equal = union_0.eqNode(nm->mkConst(EmptySet(setType)));
+ Node singleton = nm->mkNode(SET_SINGLETON, uf_i);
+
+ Node union_i_equal =
+ union_i.eqNode(nm->mkNode(SET_UNION, singleton, union_iMinusOne));
+ Node interval_i =
+ nm->mkNode(AND, nm->mkNode(GEQ, i, one), nm->mkNode(LEQ, i, n));
+
+ Node body_i = nm->mkNode(
+ IMPLIES, interval_i, nm->mkNode(AND, combine_i_equal, union_i_equal));
+ Node forAll_i = quantifiers::BoundedIntegers::mkBoundedForall(iList, body_i);
+ Node nonNegative = nm->mkNode(GEQ, n, zero);
+ Node union_n_equal = A.eqNode(union_n);
+ asserts.push_back(forAll_i);
+ asserts.push_back(combine_0_equal);
+ asserts.push_back(union_0_equal);
+ asserts.push_back(union_n_equal);
+ asserts.push_back(nonNegative);
+ return combine_n;
+}
+
+} // namespace sets
+} // namespace theory
+} // namespace cvc5::internal
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 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.
+ * ****************************************************************************
+ *
+ * set reduction.
+ */
+
+#ifndef CVC5__THEORY__SETS__SET_REDUCTION_H
+#define CVC5__THEORY__SETS__SET_REDUCTION_H
+
+#include <vector>
+
+#include "cvc5_private.h"
+#include "smt/env_obj.h"
+
+namespace cvc5::internal {
+namespace theory {
+namespace sets {
+
+/**
+ * class for set reductions
+ */
+class SetReduction
+{
+ public:
+ SetReduction();
+ ~SetReduction();
+
+ /**
+ * @param node a term of the form (set.fold f t A) where
+ * f: (-> T1 T2 T2) is a binary operation
+ * t: T2 is the initial value
+ * A: (Set T1) is a set
+ * @param asserts a list of assertions generated by this reduction
+ * @return the reduction term (combine n) with asserts:
+ * - (forall ((i Int))
+ * (let ((iMinusOne (- i 1)))
+ * (let ((uf_i (uf i)))
+ * (=>
+ * (and (>= i 1) (<= i n))
+ * (and
+ * (= (combine i) (f uf_i (combine iMinusOne)))
+ * (=
+ * (unionFn i)
+ * (set.union
+ * (set.singleton uf_i)
+ * (unionFn iMinusOne))))))))
+ * - (= (combine 0) t)
+ * - (= (unionFn 0) (as set.empty (Set T1)))
+ * - (= A (unionFn n))
+ * - (>= n 0))
+ * where
+ * n: Int is the cardinality of set A
+ * uf:Int -> T1 is an uninterpreted function that represents elements of A
+ * combine: Int -> T2 is an uninterpreted function
+ * unionFn: Int -> (Set T1) is an uninterpreted function
+ */
+ static Node reduceFoldOperator(Node node, std::vector<Node>& asserts);
+};
+
+} // namespace sets
+} // namespace theory
+} // namespace cvc5::internal
+
+#endif /* CVC5__THEORY__SETS__SET_REDUCTION_H */
#include "theory/sets/theory_sets.h"
#include "options/sets_options.h"
+#include "theory/sets/set_reduction.h"
#include "theory/sets/theory_sets_private.h"
#include "theory/sets/theory_sets_rewriter.h"
#include "theory/theory_model.h"
throw LogicException(ss.str());
}
}
+ if (nk == SET_FOLD)
+ {
+ std::vector<Node> asserts;
+ Node ret = SetReduction::reduceFoldOperator(n, asserts);
+ NodeManager* nm = NodeManager::currentNM();
+ Node andNode = nm->mkNode(AND, asserts);
+ d_im.lemma(andNode, InferenceId::BAGS_FOLD);
+ return TrustNode::mkTrustRewrite(n, ret, nullptr);
+ }
return d_internal->ppRewrite(n, lems);
}
bool TheorySetsPrivate::isHigherOrderKind(Kind k)
{
- return k == SET_MAP || k == SET_FILTER;
+ return k == SET_MAP || k == SET_FILTER || k == SET_FOLD;
}
Node TheorySetsPrivate::explain(TNode literal)
case SET_MAP: return postRewriteMap(node);
case SET_FILTER: return postRewriteFilter(node);
+ case SET_FOLD: return postRewriteFold(node);
case kind::RELATION_TRANSPOSE:
{
}
}
+RewriteResponse TheorySetsRewriter::postRewriteFold(TNode n)
+{
+ Assert(n.getKind() == kind::SET_FOLD);
+ NodeManager* nm = NodeManager::currentNM();
+ Node f = n[0];
+ Node t = n[1];
+ Kind k = n[2].getKind();
+ switch (k)
+ {
+ case SET_EMPTY:
+ {
+ // ((set.fold f t (as set.empty (Set T))) = t
+ return RewriteResponse(REWRITE_DONE, t);
+ }
+ case SET_SINGLETON:
+ {
+ // (set.fold f t (set.singleton x)) = (f x t)
+ Node x = n[2][0];
+ Node f_x_t = nm->mkNode(APPLY_UF, f, x, t);
+ return RewriteResponse(REWRITE_AGAIN_FULL, f_x_t);
+ }
+ case SET_UNION:
+ {
+ // (set.fold f t (set.union B C)) = (set.fold f (set.fold f t A) B))
+ Node A = n[2][0];
+ Node B = n[2][1];
+ Node foldA = nm->mkNode(SET_FOLD, f, t, A);
+ Node fold = nm->mkNode(SET_FOLD, f, foldA, B);
+ return RewriteResponse(REWRITE_AGAIN_FULL, fold);
+ }
+
+ default: return RewriteResponse(REWRITE_DONE, n);
+ }
+}
+
} // namespace sets
} // namespace theory
} // namespace cvc5::internal
* where p: T -> Bool
*/
RewriteResponse postRewriteFilter(TNode n);
+ /**
+ * rewrites for n include:
+ * - (set.fold f t (as set.empty (Set T))) = t
+ * - (set.fold f t (set.singleton x)) = (f t x)
+ * - (set.fold f t (set.union A B)) = (set.fold f (set.fold f t A) B))
+ * where f: T -> S -> S, and t : S
+ */
+ RewriteResponse postRewriteFold(TNode n);
}; /* class TheorySetsRewriter */
} // namespace sets
return setType;
}
+TypeNode SetFoldTypeRule::computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+{
+ Assert(n.getKind() == kind::SET_FOLD);
+ TypeNode functionType = n[0].getType(check);
+ TypeNode initialValueType = n[1].getType(check);
+ TypeNode setType = n[2].getType(check);
+ if (check)
+ {
+ if (!setType.isSet())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n,
+ "set.fold operator expects a set in the third argument, "
+ "a non-set is found");
+ }
+
+ TypeNode elementType = setType.getSetElementType();
+
+ if (!(functionType.isFunction()))
+ {
+ std::stringstream ss;
+ ss << "Operator " << n.getKind() << " expects a function of type (-> "
+ << elementType << " T2 T2) as a first argument. "
+ << "Found a term of type '" << functionType << "'.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ std::vector<TypeNode> argTypes = functionType.getArgTypes();
+ TypeNode rangeType = functionType.getRangeType();
+ if (!(argTypes.size() == 2 && argTypes[0] == elementType
+ && argTypes[1] == rangeType))
+ {
+ std::stringstream ss;
+ ss << "Operator " << n.getKind() << " expects a function of type (-> "
+ << elementType << " T2 T2). "
+ << "Found a function of type '" << functionType << "'.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ if (rangeType != initialValueType)
+ {
+ std::stringstream ss;
+ ss << "Operator " << n.getKind() << " expects an initial value of type "
+ << rangeType << ". Found a term of type '" << initialValueType << "'.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ }
+ TypeNode retType = n[0].getType().getRangeType();
+ return retType;
+}
+
TypeNode RelBinaryOperatorTypeRule::computeType(NodeManager* nodeManager,
TNode n,
bool check)
static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
}; /* struct SetFilterTypeRule */
+/**
+ * Type rule for (set.fold f t A) to make sure f is a binary operation of type
+ * (-> T1 T2 T2), t of type T2, and A is a set of type (Set T1)
+ */
+struct SetFoldTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+}; /* struct SetFoldTypeRule */
+
/**
* Type rule for binary operators (rel.join, rel.product) to check
* if the two arguments are relations (set of tuples).
regress1/sets/set_filter2.smt2
regress1/sets/set_filter3.smt2
regress1/sets/set_filter4.smt2
+ regress1/sets/set_fold1.smt2
+ regress1/sets/set_fold2.smt2
+ regress1/sets/set_fold3.smt2
regress1/sets/set_map_card_incomplete.smt2
regress1/sets/set_map_negative_members.smt2
regress1/sets/set_map_positive_members.smt2
--- /dev/null
+(set-logic HO_ALL)
+(set-info :status sat)
+(define-fun plus ((x Int) (y Int)) Int (+ x y))
+(declare-fun A () (Set Int))
+(declare-fun sumPlus1 () Int)
+(declare-fun sumPlus2 () Int)
+(assert (= A (set.insert 1 2 (set.singleton 3))))
+(assert (= sumPlus1 (set.fold plus 1 A)))
+(assert (= sumPlus2 (set.fold plus 2 (as set.empty (Set Int)))))
+(check-sat)
--- /dev/null
+(set-logic HO_ALL)
+(set-info :status sat)
+(set-option :fmf-bound true)
+(set-option :uf-lazy-ll true)
+(define-fun plus ((x Int) (y Int)) Int (+ x y))
+(declare-fun A () (Set Int))
+(declare-fun sumPlus1 () Int)
+(assert (= sumPlus1 (set.fold plus 1 A)))
+(assert (= sumPlus1 10))
+(check-sat)
--- /dev/null
+(set-logic HO_ALL)
+(set-info :status sat)
+(set-option :fmf-bound true)
+(set-option :uf-lazy-ll true)
+(set-option :strings-exp true)
+(define-fun min ((x String) (y String)) String (ite (str.< x y) x y))
+(declare-fun A () (Set String))
+(declare-fun x () String)
+(declare-fun minimum () String)
+(assert (= minimum (set.fold min "zzz" A)))
+(assert (str.< "aaa" minimum ))
+(assert (str.< minimum "zzz"))
+(assert (distinct x minimum))
+(assert (set.member x A))
+(check-sat)
projects / cvc5.git / commitdiff