assertTNodeNotExpired();
return getKind() == kind::LAMBDA || getKind() == kind::FORALL
|| getKind() == kind::EXISTS || getKind() == kind::CHOICE
+ || getKind() == kind::COMPREHENSION
|| getKind() == kind::MATCH_BIND_CASE;
}
*/
inline size_t scopeLevel() const { return d_symtab->getLevel(); }
+ /**
+ * Pushes a scope. All subsequent symbol declarations made are only valid in
+ * this scope, i.e. they are deleted on the next call to popScope.
+ *
+ * The argument bindingLevel is true, the assertion level is set to the
+ * current scope level. This determines which scope assertions are declared
+ * at.
+ */
inline void pushScope(bool bindingLevel = false) {
d_symtab->pushScope();
if(!bindingLevel) {
expr = MK_EXPR(kind, args);
}
}
+ | LPAREN_TOK COMPREHENSION_TOK
+ { PARSER_STATE->pushScope(true); }
+ boundVarList[bvl]
+ {
+ args.push_back(bvl);
+ }
+ term[f, f2] { args.push_back(f); }
+ term[f, f2] {
+ args.push_back(f);
+ expr = MK_EXPR(CVC4::kind::COMPREHENSION, args);
+ }
+ RPAREN_TOK
| LPAREN_TOK qualIdentifier[p]
termList[args,expr] RPAREN_TOK
{
DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes';
DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes';
PAR_TOK : { PARSER_STATE->v2_6() }?'par';
+COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }?'comprehension';
TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'is';
MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }?'match';
GET_MODEL_TOK : 'get-model';
parametricTypeChildren = true;
out << smtKindString(k, d_variant) << " ";
break;
+ case kind::COMPREHENSION: out << smtKindString(k, d_variant) << " "; break;
case kind::MEMBER: typeChildren = true; CVC4_FALLTHROUGH;
case kind::INSERT:
case kind::SET_TYPE:
case kind::INSERT: return "insert";
case kind::COMPLEMENT: return "complement";
case kind::CARD: return "card";
+ case kind::COMPREHENSION: return "comprehension";
case kind::JOIN: return "join";
case kind::PRODUCT: return "product";
case kind::TRANSPOSE: return "transpose";
operator COMPLEMENT 1 "set COMPLEMENT (with respect to finite universe)"
nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it."
+# A set comprehension is specified by:
+# (1) a bound variable list x1 ... xn,
+# (2) a predicate P[x1...xn], and
+# (3) a term t[x1...xn].
+# A comprehension C with the above form has members given by the following
+# semantics:
+# forall y. ( exists x1...xn. P[x1...xn] ^ t[x1...xn] = y ) <=> (member y C)
+# where y ranges over the element type of the (set) type of the comprehension.
+# Notice that since all sets must be interpreted as finite, this means that
+# CVC4 will not be able to construct a model for any set comprehension such
+# that there are infinitely many y that satisfy the left hand side of the
+# equivalence above. The same limitation occurs more generally when combining
+# finite sets with quantified formulas.
+operator COMPREHENSION 3 "set comprehension specified by a bound variable list, a predicate, and a term."
+
operator JOIN 2 "set join"
operator PRODUCT 2 "set cartesian product"
operator TRANSPOSE 1 "set transpose"
typerule CARD ::CVC4::theory::sets::CardTypeRule
typerule COMPLEMENT ::CVC4::theory::sets::ComplementTypeRule
typerule UNIVERSE_SET ::CVC4::theory::sets::UniverseSetTypeRule
+typerule COMPREHENSION ::CVC4::theory::sets::ComprehensionTypeRule
typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule
typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule
d_congruent.clear();
d_nvar_sets.clear();
d_var_set.clear();
+ d_compSets.clear();
d_pol_mems[0].clear();
d_pol_mems[1].clear();
d_members_index.clear();
d_singleton_index.clear();
d_bop_index.clear();
d_op_list.clear();
+ d_allCompSets.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 == COMPREHENSION)
+ {
+ d_compSets[r].push_back(n);
+ d_allCompSets.push_back(n);
+ Trace("sets-debug2") << "Comp-set[" << r << "] : " << n << std::endl;
+ }
else if (n.isVar() && !d_skCache.isSkolem(n))
{
// it is important that we check it is a variable, but not an internally
if (d_var_set.find(r) == d_var_set.end())
{
d_var_set[r] = n;
+ Trace("sets-debug2") << "var-set[" << r << "] : " << n << std::endl;
}
}
}
+ else
+ {
+ Trace("sets-debug2") << "Unknown-set[" << r << "] : " << n << std::endl;
+ }
}
bool SolverState::areEqual(Node a, Node b) const
}
return Node::null();
}
+
+const std::vector<Node>& SolverState::getComprehensionSets(Node r) const
+{
+ std::map<Node, std::vector<Node> >::const_iterator it = d_compSets.find(r);
+ if (it == d_compSets.end())
+ {
+ return d_emptyVec;
+ }
+ return it->second;
+}
+
const std::map<Node, Node>& SolverState::getMembers(Node r) const
{
return getMembersInternal(r, 0);
return d_op_list;
}
+const std::vector<Node>& SolverState::getComprehensionSets() const
+{
+ return d_allCompSets;
+}
+
void SolverState::debugPrintSet(Node s, const char* c) const
{
if (s.getNumChildren() == 0)
* if none exist.
*/
Node getVariableSet(Node r) const;
+ /** Get comprehension sets in equivalence class with representative r */
+ const std::vector<Node>& getComprehensionSets(Node r) const;
/** Get (positive) members of the set equivalence class r
*
* The members are return as a map, which maps members to their explanation.
* map is a representative of its congruence class.
*/
const std::map<Kind, std::vector<Node> >& getOperatorList() const;
+ /** Get the list of all comprehension sets in the current context */
+ const std::vector<Node>& getComprehensionSets() const;
// --------------------------------------- commonly used terms
/** Get type constraint skolem
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;
+ /** 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 */
std::map<Node, Node> d_var_set;
/** polarity memberships
std::map<Node, Node> d_singleton_index;
/** Indices for the binary kinds INTERSECT, SETMINUS and UNION. */
std::map<Kind, std::map<Node, std::map<Node, Node> > > d_bop_index;
+ /** A list of comprehension sets */
+ std::vector<Node> d_allCompSets;
// -------------------------------- end term indices
std::map<Kind, std::vector<Node> > d_op_list;
/** the skolem cache */
**/
#include "theory/sets/theory_sets.h"
+#include "options/sets_options.h"
#include "theory/sets/theory_sets_private.h"
+#include "theory/theory_model.h"
+
+using namespace CVC4::kind;
namespace CVC4 {
namespace theory {
// Do not move me to the header. See explanation in the constructor.
}
+void TheorySets::finishInit()
+{
+ TheoryModel* tm = d_valuation.getModel();
+ Assert(tm != nullptr);
+ tm->setUnevaluatedKind(COMPREHENSION);
+}
+
void TheorySets::addSharedTerm(TNode n) {
d_internal->addSharedTerm(n);
}
}
Node TheorySets::expandDefinition(LogicRequest &logicRequest, Node n) {
+ Kind nk = n.getKind();
+ if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
+ || nk == COMPREHENSION)
+ {
+ if (!options::setsExt())
+ {
+ std::stringstream ss;
+ ss << "Extended set operators are not supported in default mode, try "
+ "--sets-ext.";
+ throw LogicException(ss.str());
+ }
+ }
+ if (nk == COMPREHENSION)
+ {
+ // set comprehension is an implicit quantifier, require it in the logic
+ if (!getLogicInfo().isQuantified())
+ {
+ std::stringstream ss;
+ ss << "Set comprehensions require quantifiers in the background logic.";
+ throw LogicException(ss.str());
+ }
+ }
return d_internal->expandDefinition(logicRequest, n);
}
const LogicInfo& logicInfo);
~TheorySets() override;
+ /** finish initialization */
+ void finishInit() override;
void addSharedTerm(TNode) override;
void check(Effort) override;
bool collectModelInfo(TheoryModel* m) override;
context::UserContext* u)
: d_members(c),
d_deq(c),
- d_deq_processed(u),
+ d_termProcessed(u),
d_keep(c),
d_full_check_incomplete(false),
d_external(external),
{
checkDisequalities();
d_im.flushPendingLemmas();
- if (!d_im.hasProcessed() && d_card_enabled)
+ if (!d_im.hasProcessed())
{
- // call the check method of the cardinality solver
- d_cardSolver->check();
+ checkReduceComprehensions();
+ d_im.flushPendingLemmas();
+
+ if (!d_im.hasProcessed() && d_card_enabled)
+ {
+ // call the check method of the cardinality solver
+ d_cardSolver->check();
+ }
}
}
}
// already satisfied
continue;
}
- if (d_deq_processed.find(deq) != d_deq_processed.end())
+ if (d_termProcessed.find(deq) != d_termProcessed.end())
{
// already added lemma
continue;
}
- d_deq_processed.insert(deq);
- d_deq_processed.insert(deq[1].eqNode(deq[0]));
+ d_termProcessed.insert(deq);
+ d_termProcessed.insert(deq[1].eqNode(deq[0]));
Trace("sets") << "Process Disequality : " << deq.negate() << std::endl;
TypeNode elementType = deq[0].getType().getSetElementType();
Node x = d_state.getSkolemCache().mkTypedSkolemCached(
}
}
+void TheorySetsPrivate::checkReduceComprehensions()
+{
+ NodeManager* nm = NodeManager::currentNM();
+ const std::vector<Node>& comps = d_state.getComprehensionSets();
+ for (const Node& n : comps)
+ {
+ if (d_termProcessed.find(n) != d_termProcessed.end())
+ {
+ // already reduced it
+ continue;
+ }
+ d_termProcessed.insert(n);
+ Node v = nm->mkBoundVar(n[2].getType());
+ Node body = nm->mkNode(AND, n[1], v.eqNode(n[2]));
+ // must do substitution
+ std::vector<Node> vars;
+ std::vector<Node> subs;
+ for (const Node& cv : n[0])
+ {
+ vars.push_back(cv);
+ Node cvs = nm->mkBoundVar(cv.getType());
+ subs.push_back(cvs);
+ }
+ body = body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+ Node bvl = nm->mkNode(BOUND_VAR_LIST, subs);
+ body = nm->mkNode(EXISTS, bvl, body);
+ Node mem = nm->mkNode(MEMBER, v, n);
+ Node lem =
+ nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v), body.eqNode(mem));
+ Trace("sets-comprehension")
+ << "Comprehension reduction: " << lem << std::endl;
+ d_im.flushLemma(lem);
+ }
+}
+
/**************************** TheorySetsPrivate *****************************/
/**************************** TheorySetsPrivate *****************************/
/**************************** TheorySetsPrivate *****************************/
<< std::endl;
switch(node.getKind()) {
case kind::EQUAL:
- // TODO: what's the point of this
d_equalityEngine.addTriggerEquality(node);
break;
case kind::MEMBER:
- // TODO: what's the point of this
d_equalityEngine.addTriggerPredicate(node);
break;
case kind::CARD:
d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
break;
default:
- //if( node.getType().isSet() ){
- // d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
- //}else{
d_equalityEngine.addTerm(node);
- //}
break;
}
}
Node TheorySetsPrivate::expandDefinition(LogicRequest &logicRequest, Node n) {
Debug("sets-proc") << "expandDefinition : " << n << std::endl;
- if( n.getKind()==kind::UNIVERSE_SET || n.getKind()==kind::COMPLEMENT || n.getKind()==kind::JOIN_IMAGE ){
- if( !options::setsExt() ){
- std::stringstream ss;
- ss << "Extended set operators are not supported in default mode, try --sets-ext.";
- throw LogicException(ss.str());
- }
- }
return n;
}
* roughly corresponds the SET DISEQUALITY rule from Bansal et al IJCAR 2016.
*/
void checkDisequalities();
+ /**
+ * Check comprehensions. This adds reduction lemmas for all set comprehensions
+ * in the current context.
+ */
+ void checkReduceComprehensions();
void addCarePairs(TNodeTrie* t1,
TNodeTrie* t2,
Node d_false;
Node d_zero;
NodeBoolMap d_deq;
- NodeSet d_deq_processed;
+ /**
+ * The set of terms that we have reduced via a lemma in the current user
+ * context.
+ */
+ NodeSet d_termProcessed;
NodeSet d_keep;
std::vector< Node > d_emp_exp;
namespace theory {
namespace sets {
-class SetsTypeRule {
-public:
-
- /**
- * Compute the type for (and optionally typecheck) a term belonging
- * to the theory of sets.
- *
- * @param check if true, the node's type should be checked as well
- * as computed.
- */
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check)
- {
- // TODO: implement me!
- Unimplemented();
-
- }
-
-};/* class SetsTypeRule */
-
struct SetsBinaryOperatorTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
{
}
};/* struct ComplementTypeRule */
+struct ComprehensionTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ {
+ Assert(n.getKind() == kind::COMPREHENSION);
+ if (check)
+ {
+ if (n[0].getType(check) != nodeManager->boundVarListType())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "first argument of set comprehension is not bound var list");
+ }
+ if (n[1].getType(check) != nodeManager->booleanType())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "body of set comprehension is not boolean");
+ }
+ }
+ return nodeManager->mkSetType(n[2].getType(check));
+ }
+}; /* struct ComprehensionTypeRule */
+
struct InsertTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
{
regress0/sets/complement.cvc
regress0/sets/complement2.cvc
regress0/sets/complement3.cvc
+ regress0/sets/comp-qf-error.smt2
regress0/sets/cvc-sample.cvc
regress0/sets/dt-simp-mem.smt2
regress0/sets/emptyset.smt2
regress1/sets/card-6.smt2
regress1/sets/card-7.smt2
regress1/sets/card-vc6-minimized.smt2
+ regress1/sets/comp-intersect.smt2
+ regress1/sets/comp-odd.smt2
+ regress1/sets/comp-positive.smt2
+ regress1/sets/comp-pos-member.smt2
regress1/sets/copy_check_heap_access_33_4.smt2
regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2
regress1/sets/fuzz14418.smt2
regress1/sets/remove_check_free_31_6.smt2
regress1/sets/sets-disequal.smt2
regress1/sets/sets-tuple-poly.cvc
+ regress1/sets/set-comp-sat.smt2
regress1/sets/sharingbug.smt2
regress1/sets/univ-set-uf-elim.smt2
regress1/simplification_bug4.smt2
--- /dev/null
+; COMMAND-LINE: --sets-ext
+; EXPECT: (error "Set comprehensions require quantifiers in the background logic.")
+; EXIT: 1
+(set-logic QF_UFLIAFS)
+(set-info :status unsat)
+
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun x () (Set U))
+
+
+(assert (subset x (comprehension ((z U)) (not (= z a)) z)))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --sets-ext
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-fun x () (Set Int))
+(declare-fun y () (Set Int))
+
+(assert (= x (comprehension ((z Int)) (> z 4) (* 5 z))))
+(assert (= y (comprehension ((z Int)) (< z 10) (+ (* 5 z) 1))))
+
+(assert (not (= (intersection x y) (as emptyset (Set Int)))))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --sets-ext
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-fun x () (Set Int))
+
+(assert (subset x (comprehension ((z Int)) true (* 2 z))))
+
+(declare-fun a () Int)
+(declare-fun b () Int)
+
+(assert (= a (+ (* 8 b) 1)))
+(assert (member a x))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --sets-ext --full-saturate-quant
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-fun x () (Set Int))
+
+(assert (subset (comprehension ((z Int)) (>= z 0) (* 3 z)) x))
+
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+
+(assert (not (member a x)))
+(assert (not (member b x)))
+(assert (not (member c x)))
+(assert (<= 0 a))
+(assert (<= a b))
+(assert (<= b c))
+(assert (< (- c a) 3))
+(assert (distinct a b c))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --sets-ext
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-fun x () (Set Int))
+
+(assert (subset x (comprehension ((z Int)) (> z 0) z)))
+
+(assert (member 0 x))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --sets-ext --finite-model-find
+; EXPECT: sat
+(set-logic UFFS)
+(set-info :status sat)
+
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun x () (Set U))
+
+
+(assert (subset x (comprehension ((z U)) (not (= z a)) z)))
+
+(assert (not (member b x)))
+(assert (member c x))
+
+(check-sat)
projects / cvc5.git / commitdiff