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_MAP_DOWN_ELEMENT: return "SETS_MAP_DOWN_ELEMENT";
case SkolemFunId::HO_TYPE_MATCH_PRED: return "HO_TYPE_MATCH_PRED";
default: return "?";
}
*/
BAGS_CHOOSE,
/** An uninterpreted function for bag.map operator:
- * To compute (bag.count y (map f A)), we need to find the distinct
+ * To compute (bag.count y (bag.map f A)), we need to find the distinct
* elements in A that are mapped to y by function f (i.e., preimage of {y}).
* If n is the cardinality of this preimage, then
* the preimage is the set {uf(1), ..., uf(n)}
BAGS_MAP_PREIMAGE,
/**
* A skolem variable for the size of the preimage of {y} that is unique per
- * terms (map f A), y which might be an element in (map f A). (see the
+ * terms (bag.map f A), y which might be an element in (bag.map f A). (see the
* documentation for BAGS_MAP_PREIMAGE)
*/
BAGS_MAP_PREIMAGE_SIZE,
/**
* A skolem variable for the index that is unique per terms
- * (map f A), y, preImageSize, y, e which might be an element in A.
+ * (bag.map f A), y, preImageSize, y, e which might be an element in A.
* (see the documentation for BAGS_MAP_PREIMAGE)
*/
BAGS_MAP_PREIMAGE_INDEX,
* (choose A) is expanded as
* (witness ((x elementType))
* (ite
- * (= A (as emptyset (Set E)))
+ * (= A (as set.empty (Set E)))
* (= x (uf A))
- * (and (member x A) (= x uf(A)))
+ * (and (set.member x A) (= x uf(A)))
* where uf: (Set E) -> E is a skolem function, and E is the type of elements
* of A
*/
SETS_CHOOSE,
/** set diff to witness (not (= A B)) */
SETS_DEQ_DIFF,
+ /**
+ * 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,
+ * and it is mapped to y by f.
+ */
+ SETS_MAP_DOWN_ELEMENT,
/** Higher-order type match predicate, see HoTermDb */
HO_TYPE_MATCH_PRED
};
case IncompleteId::QUANTIFIERS_SYGUS_SOLVED:
return "QUANTIFIERS_SYGUS_SOLVED";
case IncompleteId::SEP: return "SEP";
+ case IncompleteId::SETS_HO_CARD: return "SETS_HO_CARD";
case IncompleteId::SETS_RELS_CARD: return "SETS_RELS_CARD";
case IncompleteId::STRINGS_LOOP_SKIP: return "STRINGS_LOOP_SKIP";
case IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY:
QUANTIFIERS_SYGUS_SOLVED,
// incomplete due to separation logic
SEP,
+ // Higher order operators like sets.map were used in combination with set
+ // cardinality constraints
+ SETS_HO_CARD,
// relations were used in combination with set cardinality constraints
SETS_RELS_CARD,
// we skipped processing a looping word equation
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_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";
case InferenceId::SETS_MEM_EQ_CONFLICT: return "SETS_MEM_EQ_CONFLICT";
case InferenceId::SETS_PROXY: return "SETS_PROXY";
SETS_EQ_CONFLICT,
SETS_EQ_MEM,
SETS_EQ_MEM_CONFLICT,
+ SETS_MAP_DOWN_POSITIVE,
+ SETS_MAP_UP,
SETS_MEM_EQ,
SETS_MEM_EQ_CONFLICT,
SETS_PROXY,
namespace sets {
SolverState::SolverState(Env& env, Valuation val, SkolemCache& skc)
- : TheoryState(env, val), d_skCache(skc), d_members(env.getContext())
+ : TheoryState(env, val),
+ d_skCache(skc),
+ d_mapTerms(env.getUserContext()),
+ d_mapSkolemElements(env.getUserContext()),
+ d_members(env.getContext())
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
d_nvar_sets[r].push_back(n);
Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
}
+ else if (nk == SET_MAP)
+ {
+ d_mapTerms.insert(n);
+ if (d_mapSkolemElements.find(n) == d_mapSkolemElements.end())
+ {
+ std::shared_ptr<context::CDHashSet<Node>> set =
+ std::make_shared<context::CDHashSet<Node>>(d_env.getUserContext());
+ d_mapSkolemElements[n] = set;
+ }
+ }
else if (nk == SET_COMPREHENSION)
{
d_compSets[r].push_back(n);
const std::map<Node, Node>& SolverState::getMembers(Node r) const
{
+ Assert(r == getRepresentative(r));
return getMembersInternal(r, 0);
}
const std::map<Node, Node>& SolverState::getNegativeMembers(Node r) const
{
+ Assert(r == getRepresentative(r));
return getMembersInternal(r, 1);
}
const std::map<Node, Node>& SolverState::getMembersInternal(Node r,
return d_op_list;
}
+const context::CDHashSet<Node>& SolverState::getMapTerms() const { return d_mapTerms; }
+
+std::shared_ptr<context::CDHashSet<Node>> SolverState::getMapSkolemElements(
+ Node n)
+{
+ return d_mapSkolemElements[n];
+}
+
const std::vector<Node>& SolverState::getComprehensionSets() const
{
return d_allCompSets;
return true;
}
+void SolverState::registerMapSkolemElement(const Node& n, const Node& element)
+{
+ Assert(n.getKind() == kind::SET_MAP);
+ Assert(element.getKind() == SKOLEM
+ && element.getType() == n[1].getType().getSetElementType());
+ d_mapSkolemElements[n].get()->insert(element);
+}
+
} // namespace sets
} // namespace theory
} // namespace cvc5::internal
#include <map>
#include <vector>
+#include "context/cdhashset.h"
#include "theory/sets/skolem_cache.h"
#include "theory/theory_state.h"
#include "theory/uf/equality_engine.h"
* map is a representative of its congruence class.
*/
const std::map<Kind, std::vector<Node> >& getOperatorList() 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
+ * the current user context */
+ std::shared_ptr<context::CDHashSet<Node>> getMapSkolemElements(Node n);
/** Get the list of all comprehension sets in the current context */
const std::vector<Node>& getComprehensionSets() const;
*/
bool merge(TNode t1, TNode t2, std::vector<Node>& facts, TNode cset);
+ /** register the skolem element for the set.map term n */
+ void registerMapSkolemElement(const Node& n, const Node& element);
+
private:
/** constants */
Node d_true;
Node d_false;
/** the empty vector and map */
- std::vector<Node> d_emptyVec;
- std::map<Node, Node> d_emptyMap;
+ const std::vector<Node> d_emptyVec;
+ /** a convenient constant empty map */
+ const std::map<Node, Node> d_emptyMap;
/** Reference to skolem cache */
SkolemCache& d_skCache;
/** The list of all equivalence classes of type set in the current context */
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;
+ /** User context collection of set.map terms */
+ context::CDHashSet<Node> d_mapTerms;
+ /** User context collection of skolem elements generated for set.map terms */
+ context::CDHashMap<Node, std::shared_ptr<context::CDHashSet<Node>>>
+ d_mapSkolemElements;
/** Map from equivalence classes to the list of comprehension sets in it */
std::map<Node, std::vector<Node> > d_compSets;
/** Map from equivalence classes to a variable sets in it */
{
Kind nk = n.getKind();
if (nk != SET_EMPTY && nk != SET_SINGLETON && nk != SET_INTER
- && nk != SET_MINUS && nk != SET_UNION && nk != SET_UNIVERSE)
+ && nk != SET_MINUS && nk != SET_UNION && nk != SET_UNIVERSE
+ && nk != SET_MAP)
{
return n;
}
{
d_rels_enabled = true;
}
+ else if(isHigherOrderKind(nk))
+ {
+ d_higher_order_kinds_enabled = true;
+ }
++eqc_i;
}
Trace("sets-eqc") << std::endl;
}
}
+ if (d_card_enabled && d_higher_order_kinds_enabled)
+ {
+ d_fullCheckIncomplete = true;
+ d_fullCheckIncompleteId = IncompleteId::SETS_HO_CARD;
+ }
+
// We may have sent lemmas while registering the terms in the loop above,
// e.g. the cardinality solver.
if (d_im.hasSent())
{
continue;
}
+ // check map up rules
+ checkMapUp();
+ d_im.doPendingLemmas();
+ if (d_im.hasSent())
+ {
+ continue;
+ }
+ // check map down rules
+ checkMapDown();
+ d_im.doPendingLemmas();
+ if (d_im.hasSent())
+ {
+ continue;
+ }
// check disequalities
checkDisequalities();
d_im.doPendingLemmas();
}
}
+void TheorySetsPrivate::checkMapUp()
+{
+ NodeManager* nm = NodeManager::currentNM();
+ const context::CDHashSet<Node>& mapTerms = d_state.getMapTerms();
+
+ for (const Node& term : mapTerms)
+ {
+ Node f = term[0];
+ Node A = term[1];
+ const std::map<Node, Node>& positiveMembers =
+ d_state.getMembers(d_state.getRepresentative(A));
+ shared_ptr<context::CDHashSet<Node>> skolemElements =
+ d_state.getMapSkolemElements(term);
+ for (const std::pair<const Node, Node>& pair : positiveMembers)
+ {
+ Node x = pair.first;
+ if (skolemElements->contains(x))
+ {
+ // Break this cycle between inferences SETS_MAP_DOWN_POSITIVE
+ // and SETS_MAP_UP:
+ // 1- If (set.member y (set.map f A)) holds, then SETS_MAP_DOWN_POSITIVE
+ // inference would generate a fresh skolem x1 such that (= (f x1) y)
+ // and (set.member x1 A).
+ // 2- Since (set.member x1 A) holds, SETS_MAP_UP would infer
+ // (set.member (f x1) (set.map f A)).
+ // Since (set.member (f x1) (set.map f A)) holds, step 1 would repeat
+ // and generate a new skolem x2 such that (= (f x2) (f x1)) and
+ // (set.member x1 A). The cycle continues with step 2.
+ continue;
+ }
+ // (=>
+ // (and (set.member x B) (= A B))
+ // (set.member (f x) (set.map f A))
+ // )
+ std::vector<Node> exp;
+ exp.push_back(pair.second);
+ Node B = pair.second[1];
+ d_state.addEqualityToExp(A, B, exp);
+ Node f_x = nm->mkNode(APPLY_UF, f, x);
+ Node skolem = d_treg.getProxy(term);
+ Node memberMap = nm->mkNode(kind::SET_MEMBER, f_x, skolem);
+ d_im.assertInference(memberMap, InferenceId::SETS_MAP_UP, exp);
+ if (d_state.isInConflict())
+ {
+ return;
+ }
+ }
+ }
+}
+
+void TheorySetsPrivate::checkMapDown()
+{
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ const context::CDHashSet<Node>& mapTerms = d_state.getMapTerms();
+ for (const Node& term : mapTerms)
+ {
+ Node f = term[0];
+ Node A = term[1];
+ TypeNode elementType = A.getType().getSetElementType();
+ 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 y = pair.first;
+ if (y.getKind() == APPLY_UF && y.getOperator() == f)
+ {
+ // special case
+ // (=>
+ // (set.member (f x) (set.map f A))
+ // (set.member x A))
+ Node x = y[0];
+ Node memberA = nm->mkNode(SET_MEMBER, x, A);
+ d_im.assertInference(memberA, InferenceId::SETS_MAP_DOWN_POSITIVE, exp);
+ }
+ else
+ {
+ // general case
+ // (=>
+ // (and
+ // (set.member y B)
+ // (= B (set.map f A)))
+ // (and
+ // (set.member x A)
+ // (= (f x) y))
+ // )
+ Node x = sm->mkSkolemFunction(
+ SkolemFunId::SETS_MAP_DOWN_ELEMENT, elementType, {term, y});
+
+ d_state.registerMapSkolemElement(term, x);
+ Node memberA = nm->mkNode(kind::SET_MEMBER, x, A);
+ Node f_x = nm->mkNode(APPLY_UF, f, x);
+ Node equal = f_x.eqNode(y);
+ Node fact = memberA.andNode(equal);
+ d_im.assertInference(fact, InferenceId::SETS_MAP_DOWN_POSITIVE, exp);
+ }
+ if (d_state.isInConflict())
+ {
+ return;
+ }
+ }
+ }
+}
+
void TheorySetsPrivate::checkDisequalities()
{
// disequalities
}
}
+/** returns whether the given kind is a higher order kind for sets. */
+bool TheorySetsPrivate::isHigherOrderKind(Kind k) { return k == SET_MAP; }
+
Node TheorySetsPrivate::explain(TNode literal)
{
Trace("sets") << "TheorySetsPrivate::explain(" << literal << ")" << std::endl;
}
}
break;
- case kind::SET_MAP:
- {
- throw LogicException(
- "set.map not currently supported by the sets theory solver");
- }
- break;
default: d_equalityEngine->addTerm(node); break;
}
}
* difference.
*/
void checkUpwardsClosure();
+
+ /**
+ * Apply the following rule for map terms (set.map f A):
+ * Positive member rule:
+ * (=>
+ * (set.member x A)
+ * (set.member (f x) (set.map f A)
+ * )
+ */
+ void checkMapUp();
+ /**
+ * Apply the following rules for map terms (set.map f A) where A has type
+ * (Set T):
+ * - General case:
+ * (=>
+ * (set.member y (set.map f A))
+ * (and
+ * (= (f x) y)
+ * (set.member x A)
+ * )
+ * )
+ * where x is a fresh skolem
+ * - Special case where we can avoid skolems
+ * (=>
+ * (set.member (f x) (set.map f A))
+ * (set.member x A)
+ * )
+ */
+ void checkMapDown();
/**
* This implements a strategy for splitting for set disequalities which
* roughly corresponds the SET DISEQUALITY rule from Bansal et al IJCAR 2016.
//--------------------------------- end standard check
/** Collect model values in m based on the relevant terms given by termSet */
- void addSharedTerm(TNode);
bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet);
void computeCareGraph();
*/
void processCarePairArgs(TNode a, TNode b);
+ /** returns whether the given kind is a higher order kind for sets. */
+ bool isHigherOrderKind(Kind k);
+
private:
TheorySets& d_external;
/** The state of the sets solver at full effort */
*/
bool d_card_enabled;
+ /** are higher order set operators enabled?
+ *
+ * This flag is set to true during a full effort check if any
+ * higher order constraints is asserted to this theory.
+ */
+ bool d_higher_order_kinds_enabled;
+
/** The theory rewriter for this theory. */
TheorySetsRewriter d_rewriter;
}
// we don't merge non-constant intersections
break;
- } // kind::INTERSECION
+ } // kind::INTERSECTION
case kind::SET_UNION:
{
regress1/sets/sets-tuple-poly.cvc.smt2
regress1/sets/sets-uc-wrong.smt2
regress1/sets/set-comp-sat.smt2
+ regress1/sets/set_map_card_incomplete.smt2
+ regress1/sets/set_map_negative_members.smt2
+ regress1/sets/set_map_positive_members.smt2
+ regress1/sets/set_map_unsat1.smt2
regress1/sets/sharingbug.smt2
regress1/sets/univ-set-uf-elim.smt2
regress1/simplification_bug4.smt2
--- /dev/null
+; EXPECT: unknown
+(set-logic HO_ALL)
+; this problem is unsat, but the solver returns unknown for now
+; because set.map and set.card are used together
+;(set-info :status unsat)
+(set-info :status unknown)
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun f (Int) Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(assert (distinct x1 x2))
+(assert (set.member x1 A))
+(assert (set.member x2 A))
+(assert (= (f x1) (f x2)))
+(assert (= B (set.map f A)))
+(assert (= (set.card B) (set.card A)))
+
+(check-sat)
--- /dev/null
+(set-logic HO_ALL)
+
+(set-info :status sat)
+(set-option :finite-model-find true)
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun f (Int) Int)
+
+(declare-const x Int)
+(declare-const y1 Int)
+(declare-const y2 Int)
+(declare-const y3 Int)
+
+(assert (distinct x y1 y2 y3))
+(assert (set.member x A))
+(assert (set.member y1 B))
+(assert (set.member y2 B))
+(assert (not (set.member y3 B)))
+(assert (= B (set.map f A)))
+
+(check-sat)
--- /dev/null
+(set-logic HO_ALL)
+
+(set-info :status sat)
+
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun f (Int) Int)
+
+(declare-const x Int)
+(declare-const y1 Int)
+(declare-const y2 Int)
+(declare-const y3 Int)
+
+(assert (distinct x y1 y2 y3))
+(assert (set.member x A))
+(assert (set.member y1 B))
+(assert (set.member y2 B))
+(assert (set.member y3 B))
+(assert (= B (set.map f A)))
+
+(check-sat)
--- /dev/null
+(set-logic HO_ALL)
+(set-info :status unsat)
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(define-fun f ((x Int)) Int (+ x 1))
+(assert (= B (set.map f A)))
+(assert (set.member (- 2) B))
+(assert (= A (as set.empty (Set Int))))
+(check-sat)
projects / cvc5.git / commitdiff