From 84356320cd9f0127d23d050d0db886cd81363981 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Thu, 23 Jun 2022 09:18:41 -0500 Subject: [PATCH] Add set.fold operator (#8867) --- proofs/lfsc/signatures/theory_def.plf | 2 + src/CMakeLists.txt | 2 + src/api/cpp/cvc5.cpp | 2 + src/api/cpp/cvc5_kind.h | 30 ++++- src/expr/skolem_manager.cpp | 4 + src/expr/skolem_manager.h | 4 + src/parser/smt2/smt2.cpp | 1 + src/printer/smt2/smt2_printer.cpp | 1 + src/theory/inference_id.cpp | 1 + src/theory/inference_id.h | 1 + src/theory/sets/kinds | 9 ++ src/theory/sets/set_reduction.cpp | 125 ++++++++++++++++++ src/theory/sets/set_reduction.h | 73 ++++++++++ src/theory/sets/theory_sets.cpp | 10 ++ src/theory/sets/theory_sets_private.cpp | 2 +- src/theory/sets/theory_sets_rewriter.cpp | 36 +++++ src/theory/sets/theory_sets_rewriter.h | 8 ++ src/theory/sets/theory_sets_type_rules.cpp | 51 +++++++ src/theory/sets/theory_sets_type_rules.h | 9 ++ test/regress/cli/CMakeLists.txt | 3 + test/regress/cli/regress1/sets/set_fold1.smt2 | 10 ++ test/regress/cli/regress1/sets/set_fold2.smt2 | 10 ++ test/regress/cli/regress1/sets/set_fold3.smt2 | 15 +++ 23 files changed, 404 insertions(+), 5 deletions(-) create mode 100644 src/theory/sets/set_reduction.cpp create mode 100644 src/theory/sets/set_reduction.h create mode 100644 test/regress/cli/regress1/sets/set_fold1.smt2 create mode 100644 test/regress/cli/regress1/sets/set_fold2.smt2 create mode 100644 test/regress/cli/regress1/sets/set_fold3.smt2 diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf index 30f00dc29..c5205f734 100644 --- a/proofs/lfsc/signatures/theory_def.plf +++ b/proofs/lfsc/signatures/theory_def.plf @@ -491,6 +491,8 @@ (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)) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 995f15c85..4150c9646 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1012,6 +1012,8 @@ libcvc5_add_sources( 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 diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index ed46fa3ed..52c2045b0 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -301,6 +301,7 @@ const static std::unordered_map> 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), @@ -624,6 +625,7 @@ const static std::unordered_map&) const + * - Solver::mkTerm(const Op&, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst + */ + SET_FOLD, /* Relations ------------------------------------------------------------- */ /** @@ -3693,10 +3719,6 @@ enum Kind : int32_t * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * - * - Create Op of this kind with: - * - * - Solver::mkOp(Kind, const std::vector&) const - * * \rst * .. warning:: This kind is experimental and may be changed or removed in * future versions. diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index d410da650..2171954ba 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -97,6 +97,10 @@ const char* toString(SkolemFunId id) 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 "?"; diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 1d9a74c7a..1b2f3df3b 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -182,6 +182,10 @@ enum class SkolemFunId 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, diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 122f7dbba..8c5be875a 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -606,6 +606,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) 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"); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index f05825324..2f0df00a8 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1152,6 +1152,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) 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"; diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 495971dc9..854070b0c 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -335,6 +335,7 @@ const char* toString(InferenceId i) 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"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 4166560e3..723345a17 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -488,6 +488,7 @@ enum class InferenceId SETS_EQ_MEM_CONFLICT, SETS_FILTER_DOWN, SETS_FILTER_UP, + SETS_FOLD, SETS_MAP_DOWN_POSITIVE, SETS_MAP_UP, SETS_MEM_EQ, diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index d1e22cab1..e3e5e06b6 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -81,6 +81,14 @@ operator SET_MAP 2 "set map function" # 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" @@ -104,6 +112,7 @@ typerule SET_CHOOSE ::cvc5::internal::theory::sets::ChooseTypeRule 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 diff --git a/src/theory/sets/set_reduction.cpp b/src/theory/sets/set_reduction.cpp new file mode 100644 index 000000000..78b5b8036 --- /dev/null +++ b/src/theory/sets/set_reduction.cpp @@ -0,0 +1,125 @@ +/****************************************************************************** + * 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 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 + SecondIndexVarAttribute; + +Node SetReduction::reduceFoldOperator(Node node, std::vector& 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(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 diff --git a/src/theory/sets/set_reduction.h b/src/theory/sets/set_reduction.h new file mode 100644 index 000000000..43172012b --- /dev/null +++ b/src/theory/sets/set_reduction.h @@ -0,0 +1,73 @@ +/****************************************************************************** + * 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 + +#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& asserts); +}; + +} // namespace sets +} // namespace theory +} // namespace cvc5::internal + +#endif /* CVC5__THEORY__SETS__SET_REDUCTION_H */ diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 454a86a73..820f33e3b 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -16,6 +16,7 @@ #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" @@ -158,6 +159,15 @@ TrustNode TheorySets::ppRewrite(TNode n, std::vector& lems) throw LogicException(ss.str()); } } + if (nk == SET_FOLD) + { + std::vector 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); } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 8c2665eb8..bf1022048 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1244,7 +1244,7 @@ void TheorySetsPrivate::processCarePairArgs(TNode a, TNode b) 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) diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 9a0b5a875..8ee9a33d1 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -334,6 +334,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { case SET_MAP: return postRewriteMap(node); case SET_FILTER: return postRewriteFilter(node); + case SET_FOLD: return postRewriteFold(node); case kind::RELATION_TRANSPOSE: { @@ -705,6 +706,41 @@ RewriteResponse TheorySetsRewriter::postRewriteFilter(TNode n) } } +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 diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h index 74735a878..ba48e4030 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -94,6 +94,14 @@ private: * 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 diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp index 49bd24e17..b2eb7987a 100644 --- a/src/theory/sets/theory_sets_type_rules.cpp +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -356,6 +356,57 @@ TypeNode SetFilterTypeRule::computeType(NodeManager* nodeManager, 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 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) diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 7461ec4cc..59ea66158 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -149,6 +149,15 @@ struct SetFilterTypeRule 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). diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 945f31ea8..eeeae8692 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2510,6 +2510,9 @@ set(regress_1_tests 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 diff --git a/test/regress/cli/regress1/sets/set_fold1.smt2 b/test/regress/cli/regress1/sets/set_fold1.smt2 new file mode 100644 index 000000000..285e64569 --- /dev/null +++ b/test/regress/cli/regress1/sets/set_fold1.smt2 @@ -0,0 +1,10 @@ +(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) diff --git a/test/regress/cli/regress1/sets/set_fold2.smt2 b/test/regress/cli/regress1/sets/set_fold2.smt2 new file mode 100644 index 000000000..0d86665d0 --- /dev/null +++ b/test/regress/cli/regress1/sets/set_fold2.smt2 @@ -0,0 +1,10 @@ +(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) diff --git a/test/regress/cli/regress1/sets/set_fold3.smt2 b/test/regress/cli/regress1/sets/set_fold3.smt2 new file mode 100644 index 000000000..a5d80f980 --- /dev/null +++ b/test/regress/cli/regress1/sets/set_fold3.smt2 @@ -0,0 +1,15 @@ +(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) -- 2.30.2