(define rel.join_image (# x term (# y term (apply (apply f_rel.join_image x) y))))
(declare f_set.insert term)
(define set.insert (# x term (# y term (apply (apply f_set.insert x) y))))
+(declare f_set.filter term)
+(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))))
KIND_ENUM(SET_CHOOSE, internal::Kind::SET_CHOOSE),
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),
/* Relations -------------------------------------------------------- */
KIND_ENUM(RELATION_JOIN, internal::Kind::RELATION_JOIN),
KIND_ENUM(RELATION_PRODUCT, internal::Kind::RELATION_PRODUCT),
{internal::Kind::SET_CHOOSE, SET_CHOOSE},
{internal::Kind::SET_IS_SINGLETON, SET_IS_SINGLETON},
{internal::Kind::SET_MAP, SET_MAP},
+ {internal::Kind::SET_FILTER, SET_FILTER},
/* Relations ------------------------------------------------------- */
{internal::Kind::RELATION_JOIN, RELATION_JOIN},
{internal::Kind::RELATION_PRODUCT, RELATION_PRODUCT},
* \endrst
*/
SET_MAP,
-
+ /**
+ * Set filter.
+ *
+ * \rst
+ * This operator filters the elements of a set.
+ * (set.filter :math:`p \; A`) takes a predicate :math:`p` of Sort
+ * :math:`(\rightarrow T \; Bool)` as a first argument, and a set :math:`A`
+ * of Sort (Set :math:`T`) as a second argument, and returns a subset of Sort
+ * (Set :math:`T`) that includes all elements of :math:`A` that satisfy
+ * :math:`p`.
+ *
+ * - Arity: ``2``
+ *
+ * - ``1:`` Term of function Sort :math:`(\rightarrow T \; Bool)`
+ * - ``2:`` Term of bag Sort (Set :math:`T`)
+ * \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_FILTER,
/* Relations ------------------------------------------------------------- */
/**
* \rst
* This operator filters the elements of a bag.
* (bag.filter :math:`p \; B`) takes a predicate :math:`p` of Sort
- * :math:`(\rightarrow S_1 \; S_2)` as a first argument, and a bag :math:`B`
- * of Sort (Bag :math:`S`) as a second argument, and returns a subbag of Sort
+ * :math:`(\rightarrow T \; Bool)` as a first argument, and a bag :math:`B`
+ * of Sort (Bag :math:`T`) as a second argument, and returns a subbag of Sort
* (Bag :math:`T`) that includes all elements of :math:`B` that satisfy
* :math:`p` with the same multiplicity.
*
* - Arity: ``2``
*
- * - ``1:`` Term of function Sort :math:`(\rightarrow S_1 \; S_2)`
- * - ``2:`` Term of bag Sort (Bag :math:`S_1`)
+ * - ``1:`` Term of function Sort :math:`(\rightarrow T \; Bool)`
+ * - ``2:`` Term of bag Sort (Bag :math:`T`)
* \endrst
*
* - Create Term of this Kind with:
* - 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.
addOperator(cvc5::SET_CHOOSE, "set.choose");
addOperator(cvc5::SET_IS_SINGLETON, "set.is_singleton");
addOperator(cvc5::SET_MAP, "set.map");
+ addOperator(cvc5::SET_FILTER, "set.filter");
addOperator(cvc5::RELATION_JOIN, "rel.join");
addOperator(cvc5::RELATION_PRODUCT, "rel.product");
addOperator(cvc5::RELATION_TRANSPOSE, "rel.transpose");
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::SET_FILTER: return "set.filter";
case kind::RELATION_JOIN: return "rel.join";
case kind::RELATION_PRODUCT: return "rel.product";
case kind::RELATION_TRANSPOSE: return "rel.transpose";
for (const Node& e : elements)
{
- InferInfo i = d_ig.filterDownwards(n, d_state.getRepresentative(e));
+ InferInfo i = d_ig.filterDown(n, d_state.getRepresentative(e));
d_im.lemmaTheoryInference(&i);
}
for (const Node& e : elements)
{
- InferInfo i = d_ig.filterUpwards(n, d_state.getRepresentative(e));
+ InferInfo i = d_ig.filterUp(n, d_state.getRepresentative(e));
d_im.lemmaTheoryInference(&i);
}
}
return inferInfo;
}
-InferInfo InferenceGenerator::filterDownwards(Node n, Node e)
+InferInfo InferenceGenerator::filterDown(Node n, Node e)
{
Assert(n.getKind() == BAG_FILTER && n[1].getType().isBag());
Assert(e.getType() == n[1].getType().getBagElementType());
return inferInfo;
}
-InferInfo InferenceGenerator::filterUpwards(Node n, Node e)
+InferInfo InferenceGenerator::filterUp(Node n, Node e)
{
Assert(n.getKind() == BAG_FILTER && n[1].getType().isBag());
Assert(e.getType() == n[1].getType().getBagElementType());
* (= (bag.count e skolem) (bag.count e A)))
* where skolem is a variable equals (bag.filter p A)
*/
- InferInfo filterDownwards(Node n, Node e);
+ InferInfo filterDown(Node n, Node e);
/**
* @param n is (bag.filter p A) where p is a function (-> E Bool),
* (and (not (p e)) (= (bag.count e skolem) 0)))
* where skolem is a variable equals (bag.filter p A)
*/
- InferInfo filterUpwards(Node n, Node e);
+ InferInfo filterUp(Node n, Node e);
/**
* @param n is a (table.product A B) where A, B are tables
operator BAG_MAP 2 "bag map function"
# The bag.filter operator takes a predicate of type (-> T Bool) and a bag of type (Bag T)
-# and return the same bag excluding those elements that do not satisfy the predicate
+# and returns the same bag excluding those elements that do not satisfy the predicate
operator BAG_FILTER 2 "bag filter operator"
# bag.fold operator combines elements of a bag into a single value.
case InferenceId::SETS_EQ_CONFLICT: return "SETS_EQ_CONFLICT";
case InferenceId::SETS_EQ_MEM: return "SETS_EQ_MEM";
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_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_CONFLICT,
SETS_EQ_MEM,
SETS_EQ_MEM_CONFLICT,
+ SETS_FILTER_DOWN,
+ SETS_FILTER_UP,
SETS_MAP_DOWN_POSITIVE,
SETS_MAP_UP,
SETS_MEM_EQ,
# 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"
+# The set.filter operator takes a predicate of type (-> T Bool) and a set of type (Set T)
+# and returns the same set excluding those elements that do not satisfy the predicate
+operator SET_FILTER 2 "set filter operator"
+
operator RELATION_JOIN 2 "relation join"
operator RELATION_PRODUCT 2 "relation cartesian product"
operator RELATION_TRANSPOSE 1 "relation transpose"
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 RELATION_JOIN ::cvc5::internal::theory::sets::RelBinaryOperatorTypeRule
typerule RELATION_PRODUCT ::cvc5::internal::theory::sets::RelBinaryOperatorTypeRule
d_bop_index.clear();
d_op_list.clear();
d_allCompSets.clear();
+ d_filterTerms.clear();
}
void SolverState::registerEqc(TypeNode tn, Node r)
d_nvar_sets[r].push_back(n);
Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
}
+ else if (nk == SET_FILTER)
+ {
+ d_filterTerms.push_back(n);
+ }
else if (nk == SET_MAP)
{
d_mapTerms.insert(n);
return d_op_list;
}
+const std::vector<Node>& SolverState::getFilterTerms() const { return d_filterTerms; }
+
const context::CDHashSet<Node>& SolverState::getMapTerms() const { return d_mapTerms; }
std::shared_ptr<context::CDHashSet<Node>> SolverState::getMapSkolemElements(
* map is a representative of its congruence class.
*/
const std::map<Kind, std::vector<Node> >& getOperatorList() const;
+ /** Get the list of all set.filter terms */
+ const std::vector<Node>& getFilterTerms() const;
/** Get the list of all set.map terms in the current user context */
const context::CDHashSet<Node>& getMapTerms() const;
/** Get the list of all skolem elements generated for map terms down rules in
std::map<Node, Node> d_congruent;
/** Map from equivalence classes to the list of non-variable sets in it */
std::map<Node, std::vector<Node> > d_nvar_sets;
+ /** A list of filter terms. It is initialized during full effort check */
+ std::vector<Node> d_filterTerms;
/** User context collection of set.map terms */
context::CDHashSet<Node> d_mapTerms;
/** User context collection of skolem elements generated for set.map terms */
{
continue;
}
+ // check filter up rule
+ checkFilterUp();
+ d_im.doPendingLemmas();
+ if (d_im.hasSent())
+ {
+ continue;
+ }
+ // check filter down rules
+ checkFilterDown();
+ d_im.doPendingLemmas();
+ if (d_im.hasSent())
+ {
+ continue;
+ }
// check map up rules
checkMapUp();
d_im.doPendingLemmas();
}
}
+void TheorySetsPrivate::checkFilterUp()
+{
+ NodeManager* nm = NodeManager::currentNM();
+ const std::vector<Node>& filterTerms = d_state.getFilterTerms();
+
+ for (const Node& term : filterTerms)
+ {
+ Node p = term[0];
+ Node A = term[1];
+ const std::map<Node, Node>& positiveMembers =
+ d_state.getMembers(d_state.getRepresentative(A));
+ for (const std::pair<const Node, Node>& pair : positiveMembers)
+ {
+ Node x = pair.first;
+ std::vector<Node> exp;
+ exp.push_back(pair.second);
+ Node B = pair.second[1];
+ d_state.addEqualityToExp(A, B, exp);
+ Node p_x = nm->mkNode(APPLY_UF, p, x);
+ Node skolem = d_treg.getProxy(term);
+ Node memberFilter = nm->mkNode(kind::SET_MEMBER, x, skolem);
+ Node not_p_x = p_x.notNode();
+ Node not_memberFilter = memberFilter.notNode();
+ Node orNode =
+ p_x.andNode(memberFilter).orNode(not_p_x.andNode(not_memberFilter));
+ d_im.assertInference(orNode, InferenceId::SETS_FILTER_UP, exp);
+ if (d_state.isInConflict())
+ {
+ return;
+ }
+ }
+ }
+}
+
+void TheorySetsPrivate::checkFilterDown()
+{
+ NodeManager* nm = NodeManager::currentNM();
+ const std::vector<Node>& filterTerms = d_state.getFilterTerms();
+ for (const Node& term : filterTerms)
+ {
+ Node p = term[0];
+ Node A = term[1];
+
+ const std::map<Node, Node>& positiveMembers =
+ d_state.getMembers(d_state.getRepresentative(term));
+ for (const std::pair<const Node, Node>& pair : positiveMembers)
+ {
+ std::vector<Node> exp;
+ Node B = pair.second[1];
+ exp.push_back(pair.second);
+ d_state.addEqualityToExp(B, term, exp);
+ Node x = pair.first;
+ Node memberA = nm->mkNode(kind::SET_MEMBER, x, A);
+ Node p_x = nm->mkNode(APPLY_UF, p, x);
+ Node fact = memberA.andNode(p_x);
+ d_im.assertInference(fact, InferenceId::SETS_FILTER_DOWN, exp);
+ if (d_state.isInConflict())
+ {
+ return;
+ }
+ }
+ }
+}
+
void TheorySetsPrivate::checkMapUp()
{
NodeManager* nm = NodeManager::currentNM();
}
}
-/** returns whether the given kind is a higher order kind for sets. */
-bool TheorySetsPrivate::isHigherOrderKind(Kind k) { return k == SET_MAP; }
+bool TheorySetsPrivate::isHigherOrderKind(Kind k)
+{
+ return k == SET_MAP || k == SET_FILTER;
+}
Node TheorySetsPrivate::explain(TNode literal)
{
*/
void checkUpwardsClosure();
+ /**
+ * Apply the following rule for filter terms (set.filter p A):
+ * (=>
+ * (and (set.member x B) (= A B))
+ * (or
+ * (and (p x) (set.member x (set.filter p A)))
+ * (and (not (p x)) (not (set.member x (set.filter p A))))
+ * )
+ * )
+ */
+ void checkFilterUp();
+ /**
+ * Apply the following rule for filter terms (set.filter p A):
+ * (=>
+ * (bag.member x (set.filter p A))
+ * (and
+ * (p x)
+ * (set.member x A)
+ * )
+ * )
+ */
+ void checkFilterDown();
+
/**
* Apply the following rule for map terms (set.map f A):
* Positive member rule:
} // kind::SET_IS_SINGLETON
case SET_MAP: return postRewriteMap(node);
+ case SET_FILTER: return postRewriteFilter(node);
case kind::RELATION_TRANSPOSE:
{
}
}
+RewriteResponse TheorySetsRewriter::postRewriteFilter(TNode n)
+{
+ Assert(n.getKind() == kind::SET_FILTER);
+ NodeManager* nm = NodeManager::currentNM();
+ Kind k = n[1].getKind();
+ switch (k)
+ {
+ case SET_EMPTY:
+ {
+ // (set.filter p (as set.empty (Set T)) = (as set.empty (Set T))
+ return RewriteResponse(REWRITE_DONE, n[1]);
+ }
+ case SET_SINGLETON:
+ {
+ // (set.filter p (set.singleton x)) =
+ // (ite (p x) (set.singleton x) (as set.empty (Set T)))
+ Node empty = nm->mkConst(EmptySet(n.getType()));
+ Node condition = nm->mkNode(APPLY_UF, n[0], n[1][0]);
+ Node ret = nm->mkNode(ITE, condition, n[1], empty);
+ return RewriteResponse(REWRITE_AGAIN_FULL, ret);
+ }
+ case SET_UNION:
+ {
+ // (set.filter p (set.union A B)) =
+ // (set.union (set.filter p A) (set.filter p B))
+ Node a = nm->mkNode(SET_FILTER, n[0], n[1][0]);
+ Node b = nm->mkNode(SET_FILTER, 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::internal
* where f: T1 -> T2
*/
RewriteResponse postRewriteMap(TNode n);
+
+ /**
+ * rewrites for n include:
+ * - (set.filter p (as set.empty (Set T)) = (as set.empty (Set T))
+ * - (set.filter p (set.singleton x)) =
+ * (ite (p x) (set.singleton x) (as set.empty (Set T)))
+ * - (set.filter p (set.union A B)) =
+ * (set.union (set.filter p A) (set.filter p B))
+ * where p: T -> Bool
+ */
+ RewriteResponse postRewriteFilter(TNode n);
}; /* class TheorySetsRewriter */
} // namespace sets
return retType;
}
+TypeNode SetFilterTypeRule::computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+{
+ Assert(n.getKind() == kind::SET_FILTER);
+ TypeNode functionType = n[0].getType(check);
+ TypeNode setType = n[1].getType(check);
+ if (check)
+ {
+ if (!setType.isSet())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n,
+ "set.filter 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 << " Bool) as a first argument. "
+ << "Found a term of type '" << functionType << "'.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ std::vector<TypeNode> argTypes = functionType.getArgTypes();
+ NodeManager* nm = NodeManager::currentNM();
+ if (!(argTypes.size() == 1 && argTypes[0] == elementType
+ && functionType.getRangeType() == nm->booleanType()))
+ {
+ std::stringstream ss;
+ ss << "Operator " << n.getKind() << " expects a function of type (-> "
+ << elementType << " Bool). "
+ << "Found a function of type '" << functionType << "'.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ }
+ return setType;
+}
+
TypeNode RelBinaryOperatorTypeRule::computeType(NodeManager* nodeManager,
TNode n,
bool check)
static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
}; /* struct SetMapTypeRule */
+/**
+ * Type rule for (set.filter p A) to make sure p is a unary predicate of type
+ * (-> T Bool) where A is a set of type (Set T)
+ */
+struct SetFilterTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+}; /* struct SetFilterTypeRule */
+
/**
* Type rule for binary operators (rel.join, rel.product) to check
* if the two arguments are relations (set of tuples).
regress1/sets/sets-tuple-poly.cvc.smt2
regress1/sets/sets-uc-wrong.smt2
regress1/sets/set-comp-sat.smt2
+ regress1/sets/set_filter1.smt2
+ regress1/sets/set_filter2.smt2
+ regress1/sets/set_filter3.smt2
+ regress1/sets/set_filter4.smt2
regress1/sets/set_map_card_incomplete.smt2
regress1/sets/set_map_negative_members.smt2
regress1/sets/set_map_positive_members.smt2
(declare-fun B () (Bag Int))
(define-fun p ((x Int)) Bool (> x 1))
(assert (= B (bag.filter p A)))
-(assert (= (bag.count 3 B) 57))
+(assert (= (bag.count 3 A) 57))
(assert (= (bag.count 3 B) 58))
(check-sat)
--- /dev/null
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun p (Int) Bool)
+(assert (= A (set.union (set.singleton x) (set.singleton y))))
+(assert (= B (set.filter p A)))
+(assert (distinct (p x) (p y)))
+(check-sat)
--- /dev/null
+(set-logic HO_ALL)
+(set-info :status sat)
+(set-option :fmf-bound true)
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun p (Int) Bool)
+(assert (= B (set.filter p A)))
+(assert (set.member (- 2) B))
+(check-sat)
--- /dev/null
+(set-logic HO_ALL)
+(set-info :status unsat)
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun element () Int)
+(declare-fun p (Int) Bool)
+(assert (= B (set.filter p A)))
+(assert (p element))
+(assert (not (set.member element B)))
+(assert (set.member element A))
+(check-sat)
--- /dev/null
+(set-logic HO_ALL)
+(set-info :status unsat)
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun element () Int)
+(declare-fun p (Int) Bool)
+(assert (= B (set.filter p A)))
+(assert (p element))
+(assert (not (set.member element A)))
+(assert (set.member element B))
+(check-sat)
projects / cvc5.git / commitdiff