Towards supporting set.map operator in the sets solver.
{SET_COMPREHENSION, cvc5::Kind::SET_COMPREHENSION},
{SET_CHOOSE, cvc5::Kind::SET_CHOOSE},
{SET_IS_SINGLETON, cvc5::Kind::SET_IS_SINGLETON},
+ {SET_MAP, cvc5::Kind::SET_MAP},
/* Relations ----------------------------------------------------------- */
{RELATION_JOIN, cvc5::Kind::RELATION_JOIN},
{RELATION_PRODUCT, cvc5::Kind::RELATION_PRODUCT},
{cvc5::Kind::SET_COMPREHENSION, SET_COMPREHENSION},
{cvc5::Kind::SET_CHOOSE, SET_CHOOSE},
{cvc5::Kind::SET_IS_SINGLETON, SET_IS_SINGLETON},
+ {cvc5::Kind::SET_MAP, SET_MAP},
/* Relations ------------------------------------------------------- */
{cvc5::Kind::RELATION_JOIN, RELATION_JOIN},
{cvc5::Kind::RELATION_PRODUCT, RELATION_PRODUCT},
SET_COMPREHENSION,
/**
* Returns an element from a given set.
- * If a set A = {x}, then the term (choose A) is equivalent to the term x.
- * If the set is empty, then (choose A) is an arbitrary value.
- * If the set has cardinality > 1, then (choose A) will deterministically
+ * If a set A = {x}, then the term (set.choose A) is equivalent to the term x.
+ * If the set is empty, then (set.choose A) is an arbitrary value.
+ * If the set has cardinality > 1, then (set.choose A) will deterministically
* return an element in A.
*
* Parameters:
* - `Solver::mkTerm(Kind kind, const Term& child) const`
*/
SET_IS_SINGLETON,
+ /**
+ * set.map operator applies the first argument, a function of type (-> T1 T2),
+ * to every element of the second argument, a set of type (Set T1),
+ * and returns a set of type (Set T2).
+ *
+ * Parameters:
+ * - 1: a function of type (-> T1 T2)
+ * - 2: a set of type (Set T1)
+ *
+ * Create with:
+ * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2)
+ * const`
+ * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+ */
+ SET_MAP,
/* Relations ------------------------------------------------------------- */
addOperator(api::SET_COMPLEMENT, "set.complement");
addOperator(api::SET_CHOOSE, "set.choose");
addOperator(api::SET_IS_SINGLETON, "set.is_singleton");
+ addOperator(api::SET_MAP, "set.map");
addOperator(api::RELATION_JOIN, "rel.join");
addOperator(api::RELATION_PRODUCT, "rel.product");
addOperator(api::RELATION_TRANSPOSE, "rel.transpose");
case kind::SET_COMPREHENSION: return "set.comprehension";
case kind::SET_CHOOSE: return "set.choose";
case kind::SET_IS_SINGLETON: return "set.is_singleton";
+ case kind::SET_MAP: return "set.map";
case kind::RELATION_JOIN: return "rel.join";
case kind::RELATION_PRODUCT: return "rel.product";
case kind::RELATION_TRANSPOSE: return "rel.transpose";
# The operator is_singleton returns whether the given set is a singleton
operator SET_IS_SINGLETON 1 "return whether the given set is a singleton"
+# The set.map operator applies the first argument, a function of type (-> T1 T2), to every element
+# of the second argument, a set of type (Set T1), and returns a set of type (Set T2).
+operator SET_MAP 2 "set map function"
+
operator RELATION_JOIN 2 "relation join"
operator RELATION_PRODUCT 2 "relation cartesian product"
-operator RELATION_TRANSPOSE 1 "relation transpose"
-operator RELATION_TCLOSURE 1 "relation transitive closure"
-operator RELATION_JOIN_IMAGE 2 "relation join image"
+operator RELATION_TRANSPOSE 1 "relation transpose"
+operator RELATION_TCLOSURE 1 "relation transitive closure"
+operator RELATION_JOIN_IMAGE 2 "relation join image"
operator RELATION_IDEN 1 "relation identity"
typerule SET_UNION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
typerule SET_COMPREHENSION ::cvc5::theory::sets::ComprehensionTypeRule
typerule SET_CHOOSE ::cvc5::theory::sets::ChooseTypeRule
typerule SET_IS_SINGLETON ::cvc5::theory::sets::IsSingletonTypeRule
+typerule SET_MAP ::cvc5::theory::sets::SetMapTypeRule
typerule RELATION_JOIN ::cvc5::theory::sets::RelBinaryOperatorTypeRule
typerule RELATION_PRODUCT ::cvc5::theory::sets::RelBinaryOperatorTypeRule
break;
} // kind::SET_IS_SINGLETON
+ case SET_MAP: return postRewriteMap(node);
+
case kind::RELATION_TRANSPOSE:
{
if (node[0].getKind() == kind::RELATION_TRANSPOSE)
return RewriteResponse(REWRITE_DONE, node);
}
+RewriteResponse TheorySetsRewriter::postRewriteMap(TNode n)
+{
+ Assert(n.getKind() == kind::SET_MAP);
+ NodeManager* nm = NodeManager::currentNM();
+ Kind k = n[1].getKind();
+ TypeNode rangeType = n[0].getType().getRangeType();
+ switch (k)
+ {
+ case SET_EMPTY:
+ {
+ // (set.map f (as set.empty (Set T1)) = (as set.empty (Set T2))
+ Node ret = nm->mkConst(EmptySet(nm->mkSetType(rangeType)));
+ return RewriteResponse(REWRITE_DONE, ret);
+ }
+ case SET_SINGLETON:
+ {
+ // (set.map f (set.singleton x)) = (set.singleton (f x))
+ Node mappedElement = nm->mkNode(APPLY_UF, n[0], n[1][0]);
+ Node ret = nm->mkSingleton(rangeType, mappedElement);
+ return RewriteResponse(REWRITE_AGAIN_FULL, ret);
+ }
+ case SET_UNION:
+ {
+ // (set.map f (set.union A B)) = (set.union (set.map f A) (set.map f B))
+ Node a = nm->mkNode(SET_MAP, n[0], n[1][0]);
+ Node b = nm->mkNode(SET_MAP, n[0], n[1][1]);
+ Node ret = nm->mkNode(SET_UNION, a, b);
+ return RewriteResponse(REWRITE_AGAIN_FULL, ret);
+ }
+
+ default: return RewriteResponse(REWRITE_DONE, n);
+ }
+}
+
} // namespace sets
} // namespace theory
} // namespace cvc5
* Returns true if elementTerm is in setTerm, where both terms are constants.
*/
bool checkConstantMembership(TNode elementTerm, TNode setTerm);
+ /**
+ * rewrites for n include:
+ * - (set.map f (as set.empty (Set T1)) = (as set.empty (Set T2))
+ * - (set.map f (set.singleton x)) = (set.singleton (apply f x))
+ * - (set.map f (set.union A B)) =
+ * (set.union (set.map f A) (set.map f B))
+ * where f: T1 -> T2
+ */
+ RewriteResponse postRewriteMap(TNode n);
}; /* class TheorySetsRewriter */
} // namespace sets
return setType;
}
+TypeNode SetMapTypeRule::computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+{
+ Assert(n.getKind() == kind::SET_MAP);
+ TypeNode functionType = n[0].getType(check);
+ TypeNode setType = n[1].getType(check);
+ if (check)
+ {
+ if (!setType.isSet())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n,
+ "set.map operator expects a set in the second 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 << " *) as a first argument. "
+ << "Found a term of type '" << functionType << "'.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ std::vector<TypeNode> argTypes = functionType.getArgTypes();
+ if (!(argTypes.size() == 1 && argTypes[0] == elementType))
+ {
+ std::stringstream ss;
+ ss << "Operator " << n.getKind() << " expects a function of type (-> "
+ << elementType << " *). "
+ << "Found a function of type '" << functionType << "'.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ }
+ TypeNode rangeType = n[0].getType().getRangeType();
+ TypeNode retType = nodeManager->mkSetType(rangeType);
+ return retType;
+}
+
TypeNode RelBinaryOperatorTypeRule::computeType(NodeManager* nodeManager,
TNode n,
bool check)
static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};
+/**
+ * Type rule for (set.map f S) to make sure f is a unary function of type
+ * (-> T1 T2) where S is a bag of type (Set T1)
+ */
+struct SetMapTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+}; /* struct SetMapTypeRule */
+
struct RelBinaryOperatorTypeRule
{
static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
cvc5_add_unit_test_white(theory_opt_multigoal_white theory)
cvc5_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
cvc5_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
+cvc5_add_unit_test_white(theory_sets_rewriter_white theory)
cvc5_add_unit_test_white(theory_sets_type_enumerator_white theory)
cvc5_add_unit_test_white(theory_sets_type_rules_white theory)
cvc5_add_unit_test_white(theory_strings_skolem_cache_black theory)
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * White box testing of sets rewriter
+ */
+
+#include "expr/dtype.h"
+#include "expr/emptyset.h"
+#include "test_smt.h"
+#include "theory/sets/theory_sets_rewriter.h"
+#include "util/rational.h"
+#include "util/string.h"
+
+namespace cvc5 {
+
+using namespace theory;
+using namespace kind;
+using namespace theory::sets;
+
+namespace test {
+
+typedef expr::Attribute<Node, Node> attribute;
+
+class TestTheoryWhiteSetsRewriter : public TestSmt
+{
+ protected:
+ void SetUp() override
+ {
+ TestSmt::SetUp();
+ d_rewriter.reset(new TheorySetsRewriter());
+ }
+ std::unique_ptr<TheorySetsRewriter> d_rewriter;
+};
+
+TEST_F(TestTheoryWhiteSetsRewriter, map)
+{
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ TypeNode stringType = d_nodeManager->stringType();
+ TypeNode integerType = d_nodeManager->integerType();
+ Node emptysetInteger =
+ d_nodeManager->mkConst(EmptySet(d_nodeManager->mkSetType(integerType)));
+ Node emptysetString =
+ d_nodeManager->mkConst(EmptySet(d_nodeManager->mkSetType(stringType)));
+ Node x = d_nodeManager->mkBoundVar("x", stringType);
+ Node bound = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, x);
+ Node lambda = d_nodeManager->mkNode(LAMBDA, bound, one);
+
+ // (set.map (lambda ((x U)) t) (as set.empty (Set String)) =
+ // (as set.empty (Set Int))
+ Node n1 = d_nodeManager->mkNode(SET_MAP, lambda, emptysetString);
+ RewriteResponse response1 = d_rewriter->postRewrite(n1);
+ ASSERT_TRUE(response1.d_node == emptysetInteger
+ && response1.d_status == REWRITE_DONE);
+
+ Node a = d_nodeManager->mkConst(String("a"));
+ Node b = d_nodeManager->mkConst(String("b"));
+ Node A = d_nodeManager->mkSingleton(d_nodeManager->stringType(), a);
+ Node B = d_nodeManager->mkSingleton(d_nodeManager->stringType(), b);
+ Node unionAB = d_nodeManager->mkNode(SET_UNION, A, B);
+
+ // (set.map
+ // (lambda ((x String)) 1)
+ // (set.union (set.singleton "a") (set.singleton "b"))) = (set.singleton 1))
+ Node n2 = d_nodeManager->mkNode(SET_MAP, lambda, unionAB);
+ Node rewritten2 = Rewriter::rewrite(n2);
+ Node bag = d_nodeManager->mkSingleton(d_nodeManager->integerType(), one);
+ ASSERT_TRUE(rewritten2 == bag);
+
+ // - (set.map f (set.union K1 K2)) =
+ // (set.union (set.map f K1) (set.map f K2))
+ Node k1 = d_skolemManager->mkDummySkolem("K1", A.getType());
+ Node k2 = d_skolemManager->mkDummySkolem("K2", A.getType());
+ Node f = d_skolemManager->mkDummySkolem("f", lambda.getType());
+ Node unionK1K2 = d_nodeManager->mkNode(SET_UNION, k1, k2);
+ Node n3 = d_nodeManager->mkNode(SET_MAP, f, unionK1K2);
+ Node rewritten3 = Rewriter::rewrite(n3);
+ Node mapK1 = d_nodeManager->mkNode(SET_MAP, f, k1);
+ Node mapK2 = d_nodeManager->mkNode(SET_MAP, f, k2);
+ Node unionMapK1K2 = d_nodeManager->mkNode(SET_UNION, mapK1, mapK2);
+ ASSERT_TRUE(rewritten3 == unionMapK1K2);
+}
+
+} // namespace test
+} // namespace cvc5
projects / cvc5.git / commitdiff