From 9acb8b8d0d529c4780191660f8ef2b51e4a92926 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 13 Dec 2019 09:53:02 -0600 Subject: Add support for set comprehension (#3312) --- src/expr/node.h | 1 + src/parser/parser.h | 8 +++ src/parser/smt2/Smt2.g | 13 +++++ src/printer/smt2/smt2_printer.cpp | 2 + src/theory/sets/kinds | 16 ++++++ src/theory/sets/solver_state.cpp | 29 +++++++++++ src/theory/sets/solver_state.h | 8 +++ src/theory/sets/theory_sets.cpp | 33 ++++++++++++ src/theory/sets/theory_sets.h | 2 + src/theory/sets/theory_sets_private.cpp | 68 +++++++++++++++++-------- src/theory/sets/theory_sets_private.h | 11 +++- src/theory/sets/theory_sets_type_rules.h | 42 +++++++-------- test/regress/CMakeLists.txt | 6 +++ test/regress/regress0/sets/comp-qf-error.smt2 | 14 +++++ test/regress/regress1/sets/comp-intersect.smt2 | 14 +++++ test/regress/regress1/sets/comp-odd.smt2 | 16 ++++++ test/regress/regress1/sets/comp-pos-member.smt2 | 23 +++++++++ test/regress/regress1/sets/comp-positive.smt2 | 12 +++++ test/regress/regress1/sets/set-comp-sat.smt2 | 18 +++++++ 19 files changed, 295 insertions(+), 41 deletions(-) create mode 100644 test/regress/regress0/sets/comp-qf-error.smt2 create mode 100644 test/regress/regress1/sets/comp-intersect.smt2 create mode 100644 test/regress/regress1/sets/comp-odd.smt2 create mode 100644 test/regress/regress1/sets/comp-pos-member.smt2 create mode 100644 test/regress/regress1/sets/comp-positive.smt2 create mode 100644 test/regress/regress1/sets/set-comp-sat.smt2 diff --git a/src/expr/node.h b/src/expr/node.h index cd3c99a78..d02cbcefd 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -469,6 +469,7 @@ public: assertTNodeNotExpired(); return getKind() == kind::LAMBDA || getKind() == kind::FORALL || getKind() == kind::EXISTS || getKind() == kind::CHOICE + || getKind() == kind::COMPREHENSION || getKind() == kind::MATCH_BIND_CASE; } diff --git a/src/parser/parser.h b/src/parser/parser.h index 42badf4c5..642b81fb0 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -739,6 +739,14 @@ public: */ 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) { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 96ac7d48e..30239dc2f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1733,6 +1733,18 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] 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 { @@ -2683,6 +2695,7 @@ DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'decla 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'; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 555908ea2..006895df7 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -751,6 +751,7 @@ void Smt2Printer::toStream(std::ostream& out, 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: @@ -1155,6 +1156,7 @@ static string smtKindString(Kind k, Variant v) 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"; diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 34fef7d64..058a20aeb 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -46,6 +46,21 @@ operator CARD 1 "set cardinality operator" 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" @@ -64,6 +79,7 @@ typerule INSERT ::CVC4::theory::sets::InsertTypeRule 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 diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 7756fe081..ca7c0bf2b 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -44,12 +44,14 @@ void SolverState::reset() 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) @@ -137,6 +139,12 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n) 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 @@ -146,9 +154,14 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n) 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 @@ -510,6 +523,17 @@ Node SolverState::getVariableSet(Node r) const } return Node::null(); } + +const std::vector& SolverState::getComprehensionSets(Node r) const +{ + std::map >::const_iterator it = d_compSets.find(r); + if (it == d_compSets.end()) + { + return d_emptyVec; + } + return it->second; +} + const std::map& SolverState::getMembers(Node r) const { return getMembersInternal(r, 0); @@ -550,6 +574,11 @@ const std::map >& SolverState::getOperatorList() const return d_op_list; } +const std::vector& SolverState::getComprehensionSets() const +{ + return d_allCompSets; +} + void SolverState::debugPrintSet(Node s, const char* c) const { if (s.getNumChildren() == 0) diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index 2b4d93ed3..7426a701b 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -133,6 +133,8 @@ class SolverState * if none exist. */ Node getVariableSet(Node r) const; + /** Get comprehension sets in equivalence class with representative r */ + const std::vector& 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. @@ -161,6 +163,8 @@ class SolverState * map is a representative of its congruence class. */ const std::map >& getOperatorList() const; + /** Get the list of all comprehension sets in the current context */ + const std::vector& getComprehensionSets() const; // --------------------------------------- commonly used terms /** Get type constraint skolem @@ -225,6 +229,8 @@ class SolverState std::map d_congruent; /** Map from equivalence classes to the list of non-variable sets in it */ std::map > d_nvar_sets; + /** Map from equivalence classes to the list of comprehension sets in it */ + std::map > d_compSets; /** Map from equivalence classes to a variable sets in it */ std::map d_var_set; /** polarity memberships @@ -262,6 +268,8 @@ class SolverState std::map d_singleton_index; /** Indices for the binary kinds INTERSECT, SETMINUS and UNION. */ std::map > > d_bop_index; + /** A list of comprehension sets */ + std::vector d_allCompSets; // -------------------------------- end term indices std::map > d_op_list; /** the skolem cache */ diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 869cb8926..3b0427ec5 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -15,7 +15,11 @@ **/ #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 { @@ -40,6 +44,13 @@ TheorySets::~TheorySets() // 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); } @@ -78,6 +89,28 @@ void TheorySets::preRegisterTerm(TNode node) { } 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); } diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 4c145aedb..ed2459b32 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -42,6 +42,8 @@ class TheorySets : public Theory const LogicInfo& logicInfo); ~TheorySets() override; + /** finish initialization */ + void finishInit() override; void addSharedTerm(TNode) override; void check(Effort) override; bool collectModelInfo(TheoryModel* m) override; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 94fef85f5..6a381d471 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -38,7 +38,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, 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), @@ -432,10 +432,16 @@ void TheorySetsPrivate::fullEffortCheck(){ { 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(); + } } } } @@ -763,13 +769,13 @@ void TheorySetsPrivate::checkDisequalities() // 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( @@ -787,6 +793,41 @@ void TheorySetsPrivate::checkDisequalities() } } +void TheorySetsPrivate::checkReduceComprehensions() +{ + NodeManager* nm = NodeManager::currentNM(); + const std::vector& 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 vars; + std::vector 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 *****************************/ @@ -1190,35 +1231,22 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) << 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; } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 0468e5fb7..5ef8c4825 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -101,6 +101,11 @@ class TheorySetsPrivate { * 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, @@ -112,7 +117,11 @@ class TheorySetsPrivate { 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; diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 27aa58452..430163121 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -25,26 +25,6 @@ namespace CVC4 { 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) { @@ -216,6 +196,28 @@ struct UniverseSetTypeRule { } };/* 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) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 73393d29a..c4dfd2593 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -803,6 +803,7 @@ set(regress_0_tests 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 @@ -1565,6 +1566,10 @@ set(regress_1_tests 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 @@ -1577,6 +1582,7 @@ set(regress_1_tests 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 diff --git a/test/regress/regress0/sets/comp-qf-error.smt2 b/test/regress/regress0/sets/comp-qf-error.smt2 new file mode 100644 index 000000000..81e4d7411 --- /dev/null +++ b/test/regress/regress0/sets/comp-qf-error.smt2 @@ -0,0 +1,14 @@ +; 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) diff --git a/test/regress/regress1/sets/comp-intersect.smt2 b/test/regress/regress1/sets/comp-intersect.smt2 new file mode 100644 index 000000000..ab3206343 --- /dev/null +++ b/test/regress/regress1/sets/comp-intersect.smt2 @@ -0,0 +1,14 @@ +; 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) diff --git a/test/regress/regress1/sets/comp-odd.smt2 b/test/regress/regress1/sets/comp-odd.smt2 new file mode 100644 index 000000000..1b1a13b34 --- /dev/null +++ b/test/regress/regress1/sets/comp-odd.smt2 @@ -0,0 +1,16 @@ +; 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) diff --git a/test/regress/regress1/sets/comp-pos-member.smt2 b/test/regress/regress1/sets/comp-pos-member.smt2 new file mode 100644 index 000000000..aeba4cadc --- /dev/null +++ b/test/regress/regress1/sets/comp-pos-member.smt2 @@ -0,0 +1,23 @@ +; 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) diff --git a/test/regress/regress1/sets/comp-positive.smt2 b/test/regress/regress1/sets/comp-positive.smt2 new file mode 100644 index 000000000..af75230b3 --- /dev/null +++ b/test/regress/regress1/sets/comp-positive.smt2 @@ -0,0 +1,12 @@ +; 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) diff --git a/test/regress/regress1/sets/set-comp-sat.smt2 b/test/regress/regress1/sets/set-comp-sat.smt2 new file mode 100644 index 000000000..d6a64c36e --- /dev/null +++ b/test/regress/regress1/sets/set-comp-sat.smt2 @@ -0,0 +1,18 @@ +; 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) -- cgit v1.2.3