From 7ce64c96d655d675778bc70d424fd72f82db589f Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 7 Jan 2020 18:13:07 -0600 Subject: [PATCH] Universe set cardinality for finite types with finite cardinality (#3392) * rewrote set cardinality for finite-types * small changes and format --- src/theory/sets/cardinality_extension.cpp | 190 +++- src/theory/sets/cardinality_extension.h | 63 +- src/theory/sets/solver_state.cpp | 15 +- src/theory/sets/solver_state.h | 7 +- src/theory/sets/theory_sets_private.cpp | 869 +++++++++++------- test/regress/CMakeLists.txt | 17 + .../sets/finite-type/sets-card-arrcolor.smt2 | 11 + .../sets/finite-type/sets-card-arrunit.smt2 | 10 + .../sets/finite-type/sets-card-bool-1.smt2 | 12 + .../sets/finite-type/sets-card-bool-2.smt2 | 10 + .../sets/finite-type/sets-card-bool-3.smt2 | 12 + .../sets/finite-type/sets-card-bool-4.smt2 | 9 + .../sets/finite-type/sets-card-bool-rec.smt2 | 10 + .../sets/finite-type/sets-card-bv-1.smt2 | 10 + .../sets/finite-type/sets-card-bv-2.smt2 | 16 + .../sets/finite-type/sets-card-bv-3.smt2 | 19 + .../sets/finite-type/sets-card-bv-4.smt2 | 18 + .../sets/finite-type/sets-card-color-sat.smt2 | 14 + .../sets/finite-type/sets-card-color.smt2 | 14 + .../finite-type/sets-card-datatype-1.smt2 | 14 + .../finite-type/sets-card-datatype-2.smt2 | 13 + .../sets-card-neg-mem-union-1.smt2 | 30 + .../sets-card-neg-mem-union-2.smt2 | 30 + 23 files changed, 1087 insertions(+), 326 deletions(-) create mode 100644 test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-color.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 create mode 100644 test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 48f5b7b35..a1c91c517 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -19,6 +19,7 @@ #include "expr/node_algorithm.h" #include "options/sets_options.h" #include "theory/sets/normal_form.h" +#include "theory/theory_model.h" #include "theory/valuation.h" using namespace std; @@ -33,8 +34,13 @@ CardinalityExtension::CardinalityExtension(SolverState& s, eq::EqualityEngine& e, context::Context* c, context::UserContext* u) - : d_state(s), d_im(im), d_ee(e), d_card_processed(u) + : d_state(s), + d_im(im), + d_ee(e), + d_card_processed(u), + d_finite_type_constants_processed(false) { + d_true = NodeManager::currentNM()->mkConst(true); d_zero = NodeManager::currentNM()->mkConst(Rational(0)); // we do congruence over cardinality d_ee.addFunctionKind(CARD); @@ -44,6 +50,9 @@ void CardinalityExtension::reset() { d_eqc_to_card_term.clear(); d_t_card_enabled.clear(); + d_finite_type_elements.clear(); + d_finite_type_slack_elements.clear(); + d_univProxy.clear(); } void CardinalityExtension::registerTerm(Node n) { @@ -57,20 +66,112 @@ void CardinalityExtension::registerTerm(Node n) d_eqc_to_card_term[r] = n; registerCardinalityTerm(n[0]); } - if (tnc.isInterpretedFinite()) + Trace("sets-card-debug") << "...finished register term" << std::endl; +} + +void CardinalityExtension::checkFiniteTypes() +{ + for (std::pair& pair : d_t_card_enabled) { - std::stringstream ss; - ss << "ERROR: cannot use cardinality on sets with finite element " - "type (term is " - << n << ")." << std::endl; - throw LogicException(ss.str()); - // TODO (#1123): extend approach for this case + TypeNode type = pair.first; + if (pair.second && type.isInterpretedFinite()) + { + checkFiniteType(type); + } + } +} + +void CardinalityExtension::checkFiniteType(TypeNode& t) +{ + Assert(t.isInterpretedFinite()); + NodeManager* nm = NodeManager::currentNM(); + // get the universe set (as univset (Set t)) + Node univ = d_state.getUnivSet(nm->mkSetType(t)); + std::map::iterator it = d_univProxy.find(univ); + Node proxy; + if (it == d_univProxy.end()) + { + // Force cvc4 to build the cardinality graph for the universe set + proxy = d_state.getProxy(univ); + d_univProxy[univ] = proxy; + } + else + { + proxy = it->second; + } + + // get all equivalent classes of type t + vector representatives = d_state.getSetsEqClasses(t); + // get the cardinality of the finite type t + Cardinality card = t.getCardinality(); + if (!card.isFinite()) + { + // TODO (#1123): support uninterpreted sorts with --finite-model-find + std::stringstream message; + message << "The cardinality " << card << " of the finite type " << t + << " is not supported yet." << endl; + Assert(false) << message.str().c_str(); + } + + Node typeCardinality = nm->mkConst(Rational(card.getFiniteCardinality())); + + Node cardUniv = nm->mkNode(kind::CARD, proxy); + Node leq = nm->mkNode(kind::LEQ, cardUniv, typeCardinality); + + // (=> true (<= (card (as univset t)) cardUniv) + if (!d_state.isEntailed(leq, true)) + { + d_im.assertInference(leq, d_true, "finite type cardinality", 1); + } + + // add subset lemmas for sets, and membership lemmas for negative members + for (Node& representative : representatives) + { + // the universe set is a subset of itself + if (representative != d_ee.getRepresentative(univ)) + { + // here we only add representatives with variables to avoid adding + // infinite equivalent generated terms to the cardinality graph + Node variable = d_state.getVariableSet(representative); + if (variable.isNull()) + { + continue; + } + + // (=> true (subset representative (as univset t)) + Node subset = nm->mkNode(kind::SUBSET, variable, proxy); + // subset terms are rewritten as union terms: (subset A B) implies (= + // (union A B) B) + subset = Rewriter::rewrite(subset); + if (!d_state.isEntailed(subset, true)) + { + d_im.assertInference(subset, d_true, "univset is a super set", 1); + } + + // negative members are members in the universe set + const std::map& negativeMembers = + d_state.getNegativeMembers(representative); + + for (const std::pair& negativeMember : negativeMembers) + { + Node member = nm->mkNode(MEMBER, negativeMember.first, univ); + // negativeMember.second is the reason for the negative membership and + // has kind MEMBER. So we specify the negation as the reason for the + // negative membership lemma + Node notMember = nm->mkNode(NOT, negativeMember.second); + // (=> + // (not (member negativeMember representative))) + // (member negativeMember (as univset t))) + d_im.assertInference( + member, notMember, "negative members are in the universe", 1); + } + } } - Trace("sets-card-debug") << "...finished register term" << std::endl; } void CardinalityExtension::check() { + checkFiniteTypes(); checkRegister(); if (d_im.hasProcessed()) { @@ -858,7 +959,8 @@ void CardinalityExtension::mkModelValueElementsFor( Valuation& val, Node eqc, std::vector& els, - const std::map& mvals) + const std::map& mvals, + TheoryModel* model) { TypeNode elementType = eqc.getType().getSetElementType(); if (isModelValueBasic(eqc)) @@ -875,9 +977,37 @@ void CardinalityExtension::mkModelValueElementsFor( unsigned vu = v.getConst().getNumerator().toUnsignedInt(); Assert(els.size() <= vu); NodeManager* nm = NodeManager::currentNM(); + if (elementType.isInterpretedFinite()) + { + // get all members of this finite type + collectFiniteTypeSetElements(model); + } while (els.size() < vu) { - els.push_back(nm->mkNode(SINGLETON, nm->mkSkolem("msde", elementType))); + if (elementType.isInterpretedFinite()) + { + // At this point we are sure the formula is satisfiable and all + // cardinality constraints are satisfied. Since this type is finite, + // there is only one single cardinality graph for all sets of this + // type because the universe cardinality constraint has been added by + // CardinalityExtension::checkFiniteType. This means we have enough + // slack elements of this finite type for all disjoint leaves in the + // cardinality graph. Therefore we can safely add new distinct slack + // elements for the leaves without worrying about conflicts with the + // current members of this finite type. + + Node slack = nm->mkSkolem("slack", elementType); + Node singleton = nm->mkNode(SINGLETON, slack); + els.push_back(singleton); + d_finite_type_slack_elements[elementType].push_back(slack); + Trace("sets-model") << "Added slack element " << slack << " to set " + << eqc << std::endl; + } + else + { + els.push_back( + nm->mkNode(SINGLETON, nm->mkSkolem("msde", elementType))); + } } } else @@ -906,6 +1036,44 @@ void CardinalityExtension::mkModelValueElementsFor( } } +void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel* model) +{ + if (d_finite_type_constants_processed) + { + return; + } + for (const Node& set : getOrderedSetsEqClasses()) + { + if (!set.getType().isInterpretedFinite()) + { + continue; + } + if (!isModelValueBasic(set)) + { + // only consider leaves in the cardinality graph + continue; + } + for (const std::pair& pair : d_state.getMembers(set)) + { + Node member = pair.first; + Node modelRepresentative = model->getRepresentative(member); + std::vector& elements = d_finite_type_elements[member.getType()]; + if (std::find(elements.begin(), elements.end(), modelRepresentative) + == elements.end()) + { + elements.push_back(modelRepresentative); + } + } + } + d_finite_type_constants_processed = true; +} + +const std::vector& CardinalityExtension::getFiniteTypeMembers( + TypeNode typeNode) +{ + return d_finite_type_elements[typeNode]; +} + } // namespace sets } // namespace theory } // namespace CVC4 diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h index d9c5dd64a..bf9c5eeaa 100644 --- a/src/theory/sets/cardinality_extension.h +++ b/src/theory/sets/cardinality_extension.h @@ -21,6 +21,7 @@ #include "context/context.h" #include "theory/sets/inference_manager.h" #include "theory/sets/solver_state.h" +#include "theory/type_set.h" #include "theory/uf/equality_engine.h" namespace CVC4 { @@ -124,7 +125,8 @@ class CardinalityExtension void mkModelValueElementsFor(Valuation& v, Node eqc, std::vector& els, - const std::map& mvals); + const std::map& mvals, + TheoryModel* model); /** get ordered sets equivalence classes * * Get the ordered set of equivalence classes computed by this class. This @@ -135,8 +137,26 @@ class CardinalityExtension */ const std::vector& getOrderedSetsEqClasses() { return d_oSetEqc; } + /** + * get the slack elements generated for each finite type. This function is + * called by TheorySetsPrivate::collectModelInfo to ask the TheoryModel to + * exclude these slack elements from the members in all sets of that type. + */ + const std::map >& getFiniteTypeSlackElements() + const + { + return d_finite_type_slack_elements; + } + /** + * get non-slack members in all sets of the given finite type. This function + * is called by TheorySetsPrivate::collectModelInfo to specify the exclusion + * sets for TheoryModel + */ + const std::vector& getFiniteTypeMembers(TypeNode typeNode); + private: /** constants */ + Node d_true; Node d_zero; /** the empty vector */ std::vector d_emp_exp; @@ -302,6 +322,21 @@ class CardinalityExtension * function. */ void checkNormalForm(Node eqc, std::vector& intro_sets); + + /** + * add cardinality lemmas for each finite type + */ + void checkFiniteTypes(); + /** + * This function adds the following lemmas for the finite type t for each S + * where S is a (a representative) set term of type t, and for each negative + * member x not in S 1- (=> true (<= (card (as univset t)) n) where n is the + * cardinality of t 2- (=> true (subset S (as univset t)) where S is a set + * term of type t 3- (=> (not (member negativeMember S))) (member + * negativeMember (as univset t))) + */ + void checkFiniteType(TypeNode& t); + /** element types of sets for which cardinality is enabled */ std::map d_t_card_enabled; /** @@ -338,6 +373,32 @@ class CardinalityExtension * ( A ^ B ), and (B \ A). */ std::map d_localBase; + + /** + * a map to store proxy nodes for the universe sets of finite types + */ + std::map d_univProxy; + + /** + * collect the elements in all sets of finite types in model, and + * store them in the field d_finite_type_elements + */ + void collectFiniteTypeSetElements(TheoryModel* model); + /** + * a map to store the non-slack elements encountered so far in all finite + * types + */ + std::map > d_finite_type_elements; + /** + * a map to store slack elements in all finite types + */ + std::map > d_finite_type_slack_elements; + /** This boolean determines whether we already collected finite type constants + * present in the current model. + * Default value is false + */ + bool d_finite_type_constants_processed; + }; /* class CardinalityExtension */ } // namespace sets diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index ca7c0bf2b..9e695bf56 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -404,7 +404,7 @@ Node SolverState::getProxy(Node n) { Kind nk = n.getKind(); if (nk != EMPTYSET && nk != SINGLETON && nk != INTERSECTION && nk != SETMINUS - && nk != UNION) + && nk != UNION && nk != UNIVERSE_SET) { return n; } @@ -605,6 +605,19 @@ void SolverState::debugPrintSet(Node s, const char* c) const } } +const vector SolverState::getSetsEqClasses(const TypeNode& t) const +{ + vector representatives; + for (const Node& eqc : getSetsEqClasses()) + { + if (eqc.getType().getSetElementType() == t) + { + representatives.push_back(eqc); + } + } + return representatives; +} + } // namespace sets } // namespace theory } // namespace CVC4 diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index 7426a701b..5bf20daca 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -121,8 +121,13 @@ class SolverState * class. */ bool isCongruent(Node n) const; - /** Get the list of all equivalence classes of set type */ + + /** Get the list of all equivalence classes of set terms */ const std::vector& getSetsEqClasses() const { return d_set_eqc; } + /** Get the list of all equivalence classes of set terms that have element + * type t */ + const std::vector getSetsEqClasses(const TypeNode& t) const; + /** * Get the list of non-variable sets that exists in the equivalence class * whose representative is r. diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 6a381d471..ad9a8cbdb 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -14,9 +14,10 @@ ** Sets theory implementation. **/ -#include #include "theory/sets/theory_sets_private.h" +#include + #include "expr/emptyset.h" #include "expr/node_algorithm.h" #include "options/sets_options.h" @@ -52,9 +53,9 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_rels_enabled(false), d_card_enabled(false) { - d_true = NodeManager::currentNM()->mkConst( true ); - d_false = NodeManager::currentNM()->mkConst( false ); - d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_equalityEngine.addFunctionKind(kind::SINGLETON); d_equalityEngine.addFunctionKind(kind::UNION); @@ -65,74 +66,92 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_equalityEngine.addFunctionKind(kind::SUBSET); } -TheorySetsPrivate::~TheorySetsPrivate(){ - for (std::pair& current_pair : d_eqc_info) { +TheorySetsPrivate::~TheorySetsPrivate() +{ + for (std::pair& current_pair : d_eqc_info) + { delete current_pair.second; } } -void TheorySetsPrivate::eqNotifyNewClass(TNode t) { - if( t.getKind()==kind::SINGLETON || t.getKind()==kind::EMPTYSET ){ - EqcInfo * e = getOrMakeEqcInfo( t, true ); +void TheorySetsPrivate::eqNotifyNewClass(TNode t) +{ + if (t.getKind() == kind::SINGLETON || t.getKind() == kind::EMPTYSET) + { + EqcInfo* e = getOrMakeEqcInfo(t, true); e->d_singleton = t; } } -void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2){ +void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2) {} -} - -void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){ +void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2) +{ if (!d_state.isInConflict()) { - Trace("sets-prop-debug") << "Merge " << t1 << " and " << t2 << "..." << std::endl; + Trace("sets-prop-debug") + << "Merge " << t1 << " and " << t2 << "..." << std::endl; Node s1, s2; - EqcInfo * e2 = getOrMakeEqcInfo( t2 ); - if( e2 ){ + EqcInfo* e2 = getOrMakeEqcInfo(t2); + if (e2) + { s2 = e2->d_singleton; - EqcInfo * e1 = getOrMakeEqcInfo( t1 ); + EqcInfo* e1 = getOrMakeEqcInfo(t1); Node s1; Trace("sets-prop-debug") << "Merging singletons..." << std::endl; - if( e1 ){ + if (e1) + { s1 = e1->d_singleton; - if( !s1.isNull() && !s2.isNull() ){ - if( s1.getKind()==s2.getKind() ){ - Trace("sets-prop") << "Propagate eq inference : " << s1 << " == " << s2 << std::endl; - //infer equality between elements of singleton - Node exp = s1.eqNode( s2 ); - Node eq = s1[0].eqNode( s2[0] ); - d_keep.insert( exp ); - d_keep.insert( eq ); - assertFact( eq, exp ); - }else{ - //singleton equal to emptyset, conflict - Trace("sets-prop") << "Propagate conflict : " << s1 << " == " << s2 << std::endl; - conflict( s1, s2 ); + if (!s1.isNull() && !s2.isNull()) + { + if (s1.getKind() == s2.getKind()) + { + Trace("sets-prop") << "Propagate eq inference : " << s1 + << " == " << s2 << std::endl; + // infer equality between elements of singleton + Node exp = s1.eqNode(s2); + Node eq = s1[0].eqNode(s2[0]); + d_keep.insert(exp); + d_keep.insert(eq); + assertFact(eq, exp); + } + else + { + // singleton equal to emptyset, conflict + Trace("sets-prop") + << "Propagate conflict : " << s1 << " == " << s2 << std::endl; + conflict(s1, s2); return; } } - }else{ - //copy information - e1 = getOrMakeEqcInfo( t1, true ); - e1->d_singleton.set( e2->d_singleton ); + } + else + { + // copy information + e1 = getOrMakeEqcInfo(t1, true); + e1->d_singleton.set(e2->d_singleton); } } - //merge membership list + // merge membership list Trace("sets-prop-debug") << "Copying membership list..." << std::endl; - NodeIntMap::iterator mem_i2 = d_members.find( t2 ); - if( mem_i2 != d_members.end() ) { - NodeIntMap::iterator mem_i1 = d_members.find( t1 ); + NodeIntMap::iterator mem_i2 = d_members.find(t2); + if (mem_i2 != d_members.end()) + { + NodeIntMap::iterator mem_i1 = d_members.find(t1); int n_members = 0; - if( mem_i1 != d_members.end() ) { + if (mem_i1 != d_members.end()) + { n_members = (*mem_i1).second; } - for( int i=0; i<(*mem_i2).second; i++ ){ + for (int i = 0; i < (*mem_i2).second; i++) + { Assert(i < (int)d_members_data[t2].size() && d_members_data[t2][i].getKind() == kind::MEMBER); Node m2 = d_members_data[t2][i]; - //check if redundant + // check if redundant bool add = true; - for( int j=0; jmkNode( kind::AND, m2[1].eqNode( s1 ), m2 ); - if( s1.getKind()==kind::SINGLETON ){ - if( s1[0]!=m2[0] ){ - Node eq = s1[0].eqNode( m2[0] ); - d_keep.insert( exp ); - d_keep.insert( eq ); - Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp << " => " << eq << std::endl; - assertFact( eq, exp ); + Node exp = NodeManager::currentNM()->mkNode( + kind::AND, m2[1].eqNode(s1), m2); + if (s1.getKind() == kind::SINGLETON) + { + if (s1[0] != m2[0]) + { + Node eq = s1[0].eqNode(m2[0]); + d_keep.insert(exp); + d_keep.insert(eq); + Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp + << " => " << eq << std::endl; + assertFact(eq, exp); } - }else{ - //conflict - Trace("sets-prop") << "Propagate eq-mem conflict : " << exp << std::endl; + } + else + { + // conflict + Trace("sets-prop") + << "Propagate eq-mem conflict : " << exp << std::endl; d_state.setConflict(exp); return; } } - if( n_members<(int)d_members_data[t1].size() ){ + if (n_members < (int)d_members_data[t1].size()) + { d_members_data[t1][n_members] = m2; - }else{ - d_members_data[t1].push_back( m2 ); + } + else + { + d_members_data[t1].push_back(m2); } n_members++; } @@ -174,52 +205,69 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){ } } -void TheorySetsPrivate::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){ - if( t1.getType().isSet() ){ - Node eq = t1.eqNode( t2 ); - if( d_deq.find( eq )==d_deq.end() ){ +void TheorySetsPrivate::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) +{ + if (t1.getType().isSet()) + { + Node eq = t1.eqNode(t2); + if (d_deq.find(eq) == d_deq.end()) + { d_deq[eq] = true; } } } -TheorySetsPrivate::EqcInfo::EqcInfo( context::Context* c ) : d_singleton( c ){ - -} +TheorySetsPrivate::EqcInfo::EqcInfo(context::Context* c) : d_singleton(c) {} -TheorySetsPrivate::EqcInfo* TheorySetsPrivate::getOrMakeEqcInfo( TNode n, bool doMake ){ - std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); - if( eqc_i==d_eqc_info.end() ){ +TheorySetsPrivate::EqcInfo* TheorySetsPrivate::getOrMakeEqcInfo(TNode n, + bool doMake) +{ + std::map::iterator eqc_i = d_eqc_info.find(n); + if (eqc_i == d_eqc_info.end()) + { EqcInfo* ei = NULL; - if( doMake ){ - ei = new EqcInfo( d_external.getSatContext() ); + if (doMake) + { + ei = new EqcInfo(d_external.getSatContext()); d_eqc_info[n] = ei; } return ei; - }else{ + } + else + { return eqc_i->second; } } bool TheorySetsPrivate::areCareDisequal(Node a, Node b) { - if( d_equalityEngine.isTriggerTerm(a, THEORY_SETS) && d_equalityEngine.isTriggerTerm(b, THEORY_SETS) ){ - TNode a_shared = d_equalityEngine.getTriggerTermRepresentative(a, THEORY_SETS); - TNode b_shared = d_equalityEngine.getTriggerTermRepresentative(b, THEORY_SETS); - EqualityStatus eqStatus = d_external.d_valuation.getEqualityStatus(a_shared, b_shared); - if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){ + if (d_equalityEngine.isTriggerTerm(a, THEORY_SETS) + && d_equalityEngine.isTriggerTerm(b, THEORY_SETS)) + { + TNode a_shared = + d_equalityEngine.getTriggerTermRepresentative(a, THEORY_SETS); + TNode b_shared = + d_equalityEngine.getTriggerTermRepresentative(b, THEORY_SETS); + EqualityStatus eqStatus = + d_external.d_valuation.getEqualityStatus(a_shared, b_shared); + if (eqStatus == EQUALITY_FALSE_AND_PROPAGATED || eqStatus == EQUALITY_FALSE + || eqStatus == EQUALITY_FALSE_IN_MODEL) + { return true; } } return false; } -bool TheorySetsPrivate::isMember( Node x, Node s ) { +bool TheorySetsPrivate::isMember(Node x, Node s) +{ Assert(d_equalityEngine.hasTerm(s) && d_equalityEngine.getRepresentative(s) == s); - NodeIntMap::iterator mem_i = d_members.find( s ); - if( mem_i != d_members.end() ) { - for( int i=0; i<(*mem_i).second; i++ ){ + NodeIntMap::iterator mem_i = d_members.find(s); + if (mem_i != d_members.end()) + { + for (int i = 0; i < (*mem_i).second; i++) + { if (d_state.areEqual(d_members_data[s][i][0], x)) { return true; @@ -228,53 +276,71 @@ bool TheorySetsPrivate::isMember( Node x, Node s ) { } return false; } - -bool TheorySetsPrivate::assertFact( Node fact, Node exp ){ - Trace("sets-assert") << "TheorySets::assertFact : " << fact << ", exp = " << exp << std::endl; + +bool TheorySetsPrivate::assertFact(Node fact, Node exp) +{ + Trace("sets-assert") << "TheorySets::assertFact : " << fact + << ", exp = " << exp << std::endl; bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; if (!d_state.isEntailed(atom, polarity)) { - if( atom.getKind()==kind::EQUAL ){ - d_equalityEngine.assertEquality( atom, polarity, exp ); - }else{ - d_equalityEngine.assertPredicate( atom, polarity, exp ); + if (atom.getKind() == kind::EQUAL) + { + d_equalityEngine.assertEquality(atom, polarity, exp); + } + else + { + d_equalityEngine.assertPredicate(atom, polarity, exp); } if (!d_state.isInConflict()) { - if( atom.getKind()==kind::MEMBER && polarity ){ - //check if set has a value, if so, we can propagate - Node r = d_equalityEngine.getRepresentative( atom[1] ); - EqcInfo * e = getOrMakeEqcInfo( r, true ); - if( e ){ + if (atom.getKind() == kind::MEMBER && polarity) + { + // check if set has a value, if so, we can propagate + Node r = d_equalityEngine.getRepresentative(atom[1]); + EqcInfo* e = getOrMakeEqcInfo(r, true); + if (e) + { Node s = e->d_singleton; - if( !s.isNull() ){ - Node exp = NodeManager::currentNM()->mkNode( kind::AND, atom, atom[1].eqNode( s ) ); - d_keep.insert( exp ); - if( s.getKind()==kind::SINGLETON ){ - if( s[0]!=atom[0] ){ + if (!s.isNull()) + { + Node exp = NodeManager::currentNM()->mkNode( + kind::AND, atom, atom[1].eqNode(s)); + d_keep.insert(exp); + if (s.getKind() == kind::SINGLETON) + { + if (s[0] != atom[0]) + { Trace("sets-prop") << "Propagate mem-eq : " << exp << std::endl; - Node eq = s[0].eqNode( atom[0] ); - d_keep.insert( eq ); - assertFact( eq, exp ); + Node eq = s[0].eqNode(atom[0]); + d_keep.insert(eq); + assertFact(eq, exp); } - }else{ - Trace("sets-prop") << "Propagate mem-eq conflict : " << exp << std::endl; + } + else + { + Trace("sets-prop") + << "Propagate mem-eq conflict : " << exp << std::endl; d_state.setConflict(exp); } } } - //add to membership list - NodeIntMap::iterator mem_i = d_members.find( r ); + // add to membership list + NodeIntMap::iterator mem_i = d_members.find(r); int n_members = 0; - if( mem_i != d_members.end() ) { + if (mem_i != d_members.end()) + { n_members = (*mem_i).second; } d_members[r] = n_members + 1; - if( n_members<(int)d_members_data[r].size() ){ + if (n_members < (int)d_members_data[r].size()) + { d_members_data[r][n_members] = atom; - }else{ - d_members_data[r].push_back( atom ); + } + else + { + d_members_data[r].push_back(atom); } } } @@ -302,44 +368,52 @@ void TheorySetsPrivate::fullEffortReset() d_cardSolver->reset(); } -void TheorySetsPrivate::fullEffortCheck(){ +void TheorySetsPrivate::fullEffortCheck() +{ Trace("sets") << "----- Full effort check ------" << std::endl; - do{ + do + { Trace("sets") << "...iterate full effort check..." << std::endl; fullEffortReset(); Trace("sets-eqc") << "Equality Engine:" << std::endl; std::map eqcTypeCount; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ){ + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); + while (!eqcs_i.isFinished()) + { Node eqc = (*eqcs_i); bool isSet = false; TypeNode tn = eqc.getType(); d_state.registerEqc(tn, eqc); eqcTypeCount[tn]++; - //common type node and term + // common type node and term TypeNode tnc; Node tnct; - if( tn.isSet() ){ + if (tn.isSet()) + { isSet = true; tnc = tn.getSetElementType(); tnct = eqc; } Trace("sets-eqc") << "[" << eqc << "] : "; - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ) { + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine); + while (!eqc_i.isFinished()) + { Node n = (*eqc_i); - if( n!=eqc ){ + if (n != eqc) + { Trace("sets-eqc") << n << " "; } TypeNode tnn = n.getType(); - if( isSet ){ + if (isSet) + { Assert(tnn.isSet()); TypeNode tnnel = tnn.getSetElementType(); - tnc = TypeNode::mostCommonTypeNode( tnc, tnnel ); + tnc = TypeNode::mostCommonTypeNode(tnc, tnnel); Assert(!tnc.isNull()); - //update the common type term - if( tnc==tnnel ){ + // update the common type term + if (tnc == tnnel) + { tnct = n; } } @@ -353,23 +427,34 @@ void TheorySetsPrivate::fullEffortCheck(){ // if we do not handle the kind, set incomplete Kind nk = n[0].getKind(); // some kinds of cardinality we cannot handle - if (nk == kind::UNIVERSE_SET || d_rels->isRelationKind(nk)) + if ((nk == kind::UNIVERSE_SET + && !n[0].getType().isInterpretedFinite()) + || d_rels->isRelationKind(nk)) { d_full_check_incomplete = true; Trace("sets-incomplete") << "Sets : incomplete because of " << n << "." << std::endl; - // TODO (#1124) handle this case + // TODO (#1124): The issue can be divided into 4 parts + // 1- Supporting the universe cardinality for finite types with + // finite cardinality (done) 2- Supporting the universe cardinality + // for for uninterpreted sorts with finite-model-find (pending) + // See the implementation of + // CardinalityExtension::checkFiniteType + // 3- Supporting the universe cardinality for non-finite types + // (pending, easy) 4- Supporting cardinality for relations (hard) } } else { - if( d_rels->isRelationKind( n.getKind() ) ){ + if (d_rels->isRelationKind(n.getKind())) + { d_rels_enabled = true; } } ++eqc_i; } - if( isSet ){ + if (isSet) + { Assert(tnct.getType().getSetElementType() == tnc); d_most_common_type[eqc] = tnc; d_most_common_type_term[eqc] = tnct; @@ -394,7 +479,8 @@ void TheorySetsPrivate::fullEffortCheck(){ // e.g. the cardinality solver. if (!d_im.hasProcessed()) { - if( Trace.isOn("sets-mem") ){ + if (Trace.isOn("sets-mem")) + { const std::vector& sec = d_state.getSetsEqClasses(); for (const Node& s : sec) { @@ -421,7 +507,8 @@ void TheorySetsPrivate::fullEffortCheck(){ if (!d_im.hasProcessed()) { checkDownwardsClosure(); - if( options::setsInferAsLemmas() ){ + if (options::setsInferAsLemmas()) + { d_im.flushPendingLemmas(); } if (!d_im.hasProcessed()) @@ -482,7 +569,7 @@ void TheorySetsPrivate::checkSubtypes() Node mctt = d_most_common_type_term[s]; Assert(!mctt.isNull()); Trace("sets") << " most common type term is " << mctt << std::endl; - std::vector< Node > exp; + std::vector exp; exp.push_back(it2.second); Assert(d_state.areEqual(mctt, it2.second[1])); exp.push_back(mctt.eqNode(it2.second[1])); @@ -506,7 +593,7 @@ void TheorySetsPrivate::checkSubtypes() void TheorySetsPrivate::checkDownwardsClosure() { Trace("sets") << "TheorySetsPrivate: check downwards closure..." << std::endl; - //downwards closure + // downwards closure const std::vector& sec = d_state.getSetsEqClasses(); for (const Node& s : sec) { @@ -523,33 +610,42 @@ void TheorySetsPrivate::checkDownwardsClosure() Node mem = it2.second; Node eq_set = nv; Assert(d_equalityEngine.areEqual(mem[1], eq_set)); - if( mem[1]!=eq_set ){ - Trace("sets-debug") << "Downwards closure based on " << mem << ", eq_set = " << eq_set << std::endl; - if( !options::setsProxyLemmas() ){ - Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set ); - nmem = Rewriter::rewrite( nmem ); - std::vector< Node > exp; - exp.push_back( mem ); - exp.push_back( mem[1].eqNode( eq_set ) ); + if (mem[1] != eq_set) + { + Trace("sets-debug") << "Downwards closure based on " << mem + << ", eq_set = " << eq_set << std::endl; + if (!options::setsProxyLemmas()) + { + Node nmem = NodeManager::currentNM()->mkNode( + kind::MEMBER, mem[0], eq_set); + nmem = Rewriter::rewrite(nmem); + std::vector exp; + exp.push_back(mem); + exp.push_back(mem[1].eqNode(eq_set)); d_im.assertInference(nmem, exp, "downc"); if (d_state.isInConflict()) { return; } - }else{ - //use proxy set + } + else + { + // use proxy set Node k = d_state.getProxy(eq_set); - Node pmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], k ); - Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set ); - nmem = Rewriter::rewrite( nmem ); - std::vector< Node > exp; + Node pmem = + NodeManager::currentNM()->mkNode(kind::MEMBER, mem[0], k); + Node nmem = NodeManager::currentNM()->mkNode( + kind::MEMBER, mem[0], eq_set); + nmem = Rewriter::rewrite(nmem); + std::vector exp; if (d_state.areEqual(mem, pmem)) { - exp.push_back( pmem ); + exp.push_back(pmem); } else { - nmem = NodeManager::currentNM()->mkNode( kind::OR, pmem.negate(), nmem ); + nmem = NodeManager::currentNM()->mkNode( + kind::OR, pmem.negate(), nmem); } d_im.assertInference(nmem, exp, "downc"); } @@ -563,7 +659,7 @@ void TheorySetsPrivate::checkDownwardsClosure() void TheorySetsPrivate::checkUpwardsClosure() { - //upwards closure + // upwards closure NodeManager* nm = NodeManager::currentNM(); const std::map > >& boi = d_state.getBinaryOpIndex(); @@ -576,7 +672,7 @@ void TheorySetsPrivate::checkUpwardsClosure() for (const std::pair >& it : itb.second) { Node r1 = it.first; - //see if there are members in first argument r1 + // see if there are members in first argument r1 const std::map& r1mem = d_state.getMembers(r1); if (!r1mem.empty() || k == kind::UNION) { @@ -584,7 +680,7 @@ void TheorySetsPrivate::checkUpwardsClosure() { Node r2 = it2.first; Node term = it2.second; - //see if there are members in second argument + // see if there are members in second argument const std::map& r2mem = d_state.getMembers(r2); const std::map& r2nmem = d_state.getNegativeMembers(r2); if (!r2mem.empty() || k != kind::INTERSECTION) @@ -592,7 +688,7 @@ void TheorySetsPrivate::checkUpwardsClosure() Trace("sets-debug") << "Checking " << term << ", members = " << (!r1mem.empty()) << ", " << (!r2mem.empty()) << std::endl; - //for all members of r1 + // for all members of r1 if (!r1mem.empty()) { for (const std::pair& itm1m : r1mem) @@ -601,14 +697,17 @@ void TheorySetsPrivate::checkUpwardsClosure() Node x = itm1m.second[0]; Trace("sets-debug") << "checking membership " << xr << " " << itm1m.second << std::endl; - std::vector< Node > exp; + std::vector exp; exp.push_back(itm1m.second); d_state.addEqualityToExp(term[0], itm1m.second[1], exp); bool valid = false; int inferType = 0; - if( k==kind::UNION ){ + if (k == kind::UNION) + { valid = true; - }else if( k==kind::INTERSECTION ){ + } + else if (k == kind::INTERSECTION) + { // conclude x is in term // if also existing in members of r2 std::map::const_iterator itm = r2mem.find(xr); @@ -621,7 +720,8 @@ void TheorySetsPrivate::checkUpwardsClosure() } else { - // if not, check whether it is definitely not a member, if unknown, split + // if not, check whether it is definitely not a member, if + // unknown, split if (r2nmem.find(xr) == r2nmem.end()) { exp.push_back(nm->mkNode(kind::MEMBER, x, term[1])); @@ -629,7 +729,9 @@ void TheorySetsPrivate::checkUpwardsClosure() inferType = 1; } } - }else{ + } + else + { Assert(k == kind::SETMINUS); std::map::const_iterator itm = r2mem.find(xr); if (itm == r2mem.end()) @@ -642,9 +744,11 @@ void TheorySetsPrivate::checkUpwardsClosure() inferType = 1; } } - if( valid ){ + if (valid) + { Node rr = d_equalityEngine.getRepresentative(term); - if( !isMember( x, rr ) ){ + if (!isMember(x, rr)) + { Node kk = d_state.getProxy(term); Node fact = nm->mkNode(kind::MEMBER, x, kk); d_im.assertInference(fact, exp, "upc", inferType); @@ -658,16 +762,18 @@ void TheorySetsPrivate::checkUpwardsClosure() << itm1m.second << std::endl; } } - if( k==kind::UNION ){ + if (k == kind::UNION) + { if (!r2mem.empty()) { - //for all members of r2 + // for all members of r2 for (const std::pair& itm2m : r2mem) { Node x = itm2m.second[0]; Node rr = d_equalityEngine.getRepresentative(term); - if( !isMember( x, rr ) ){ - std::vector< Node > exp; + if (!isMember(x, rr)) + { + std::vector exp; exp.push_back(itm2m.second); d_state.addEqualityToExp(term[1], itm2m.second[1], exp); Node k = d_state.getProxy(term); @@ -688,40 +794,46 @@ void TheorySetsPrivate::checkUpwardsClosure() } if (!d_im.hasProcessed()) { - if( options::setsExt() ){ - //universal sets + if (options::setsExt()) + { + // universal sets Trace("sets-debug") << "Check universe sets..." << std::endl; - //all elements must be in universal set + // all elements must be in universal set const std::vector& sec = d_state.getSetsEqClasses(); for (const Node& s : sec) { - //if equivalence class contains a variable + // if equivalence class contains a variable Node v = d_state.getVariableSet(s); if (!v.isNull()) { - //the variable in the equivalence class - std::map< TypeNode, Node > univ_set; + // the variable in the equivalence class + std::map univ_set; const std::map& smems = d_state.getMembers(s); for (const std::pair& it2 : smems) { Node e = it2.second[0]; - TypeNode tn = NodeManager::currentNM()->mkSetType( e.getType() ); + TypeNode tn = NodeManager::currentNM()->mkSetType(e.getType()); Node u; - std::map< TypeNode, Node >::iterator itu = univ_set.find( tn ); - if( itu==univ_set.end() ){ + std::map::iterator itu = univ_set.find(tn); + if (itu == univ_set.end()) + { Node ueqc = d_state.getUnivSetEqClass(tn); - // if the universe does not yet exist, or is not in this equivalence class + // if the universe does not yet exist, or is not in this + // equivalence class if (s != ueqc) { u = d_state.getUnivSet(tn); } univ_set[tn] = u; - }else{ + } + else + { u = itu->second; } - if( !u.isNull() ){ + if (!u.isNull()) + { Assert(it2.second.getKind() == kind::MEMBER); - std::vector< Node > exp; + std::vector exp; exp.push_back(it2.second); if (v != it2.second[1]) { @@ -743,10 +855,11 @@ void TheorySetsPrivate::checkUpwardsClosure() void TheorySetsPrivate::checkDisequalities() { - //disequalities + // disequalities Trace("sets") << "TheorySetsPrivate: check disequalities..." << std::endl; NodeManager* nm = NodeManager::currentNM(); - for(NodeBoolMap::const_iterator it=d_deq.begin(); it !=d_deq.end(); ++it) { + for (NodeBoolMap::const_iterator it = d_deq.begin(); it != d_deq.end(); ++it) + { if (!(*it).second) { // not active @@ -832,9 +945,11 @@ void TheorySetsPrivate::checkReduceComprehensions() /**************************** TheorySetsPrivate *****************************/ /**************************** TheorySetsPrivate *****************************/ -void TheorySetsPrivate::check(Theory::Effort level) { +void TheorySetsPrivate::check(Theory::Effort level) +{ Trace("sets-check") << "Sets check effort " << level << std::endl; - if( level == Theory::EFFORT_LAST_CALL ){ + if (level == Theory::EFFORT_LAST_CALL) + { return; } while (!d_external.done() && !d_state.isInConflict()) @@ -843,15 +958,18 @@ void TheorySetsPrivate::check(Theory::Effort level) { Assertion assertion = d_external.get(); TNode fact = assertion.assertion; Trace("sets-assert") << "Assert from input " << fact << std::endl; - //assert the fact - assertFact( fact, fact ); + // assert the fact + assertFact(fact, fact); } - Trace("sets-check") << "Sets finished assertions effort " << level << std::endl; - //invoke full effort check, relations check + Trace("sets-check") << "Sets finished assertions effort " << level + << std::endl; + // invoke full effort check, relations check if (!d_state.isInConflict()) { - if( level == Theory::EFFORT_FULL ){ - if( !d_external.d_valuation.needCheck() ){ + if (level == Theory::EFFORT_FULL) + { + if (!d_external.d_valuation.needCheck()) + { fullEffortCheck(); if (!d_state.isInConflict() && !d_im.hasSentLemma() && d_full_check_incomplete) @@ -862,13 +980,14 @@ void TheorySetsPrivate::check(Theory::Effort level) { } } Trace("sets-check") << "Sets finish Check effort " << level << std::endl; -}/* TheorySetsPrivate::check() */ +} /* TheorySetsPrivate::check() */ /************************ Sharing ************************/ /************************ Sharing ************************/ /************************ Sharing ************************/ -void TheorySetsPrivate::addSharedTerm(TNode n) { +void TheorySetsPrivate::addSharedTerm(TNode n) +{ Debug("sets") << "[sets] TheorySetsPrivate::addSharedTerm( " << n << ")" << std::endl; d_equalityEngine.addTriggerTerm(n, THEORY_SETS); @@ -880,74 +999,98 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, unsigned depth, unsigned& n_pairs) { - if( depth==arity ){ - if( t2!=NULL ){ + if (depth == arity) + { + if (t2 != NULL) + { Node f1 = t1->getData(); Node f2 = t2->getData(); if (!d_state.areEqual(f1, f2)) { Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl; - vector< pair > currentPairs; - for (unsigned k = 0; k < f1.getNumChildren(); ++ k) { + vector > currentPairs; + for (unsigned k = 0; k < f1.getNumChildren(); ++k) + { TNode x = f1[k]; TNode y = f2[k]; Assert(d_equalityEngine.hasTerm(x)); Assert(d_equalityEngine.hasTerm(y)); Assert(!d_state.areDisequal(x, y)); Assert(!areCareDisequal(x, y)); - if( !d_equalityEngine.areEqual( x, y ) ){ - Trace("sets-cg") << "Arg #" << k << " is " << x << " " << y << std::endl; - if( d_equalityEngine.isTriggerTerm(x, THEORY_SETS) && d_equalityEngine.isTriggerTerm(y, THEORY_SETS) ){ - TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_SETS); - TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_SETS); + if (!d_equalityEngine.areEqual(x, y)) + { + Trace("sets-cg") + << "Arg #" << k << " is " << x << " " << y << std::endl; + if (d_equalityEngine.isTriggerTerm(x, THEORY_SETS) + && d_equalityEngine.isTriggerTerm(y, THEORY_SETS)) + { + TNode x_shared = + d_equalityEngine.getTriggerTermRepresentative(x, THEORY_SETS); + TNode y_shared = + d_equalityEngine.getTriggerTermRepresentative(y, THEORY_SETS); currentPairs.push_back(make_pair(x_shared, y_shared)); - }else if( isCareArg( f1, k ) && isCareArg( f2, k ) ){ - //splitting on sets (necessary for handling set of sets properly) - if( x.getType().isSet() ){ + } + else if (isCareArg(f1, k) && isCareArg(f2, k)) + { + // splitting on sets (necessary for handling set of sets properly) + if (x.getType().isSet()) + { Assert(y.getType().isSet()); if (!d_state.areDisequal(x, y)) { - Trace("sets-cg-lemma") << "Should split on : " << x << "==" << y << std::endl; + Trace("sets-cg-lemma") + << "Should split on : " << x << "==" << y << std::endl; d_im.split(x.eqNode(y)); } } } } } - for (unsigned c = 0; c < currentPairs.size(); ++ c) { - Trace("sets-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl; + for (unsigned c = 0; c < currentPairs.size(); ++c) + { + Trace("sets-cg-pair") << "Pair : " << currentPairs[c].first << " " + << currentPairs[c].second << std::endl; d_external.addCarePair(currentPairs[c].first, currentPairs[c].second); n_pairs++; } } } - }else{ - if( t2==NULL ){ - if( depth<(arity-1) ){ - //add care pairs internal to each child + } + else + { + if (t2 == NULL) + { + if (depth < (arity - 1)) + { + // add care pairs internal to each child for (std::pair& t : t1->d_data) { addCarePairs(&t.second, NULL, arity, depth + 1, n_pairs); } } - //add care pairs based on each pair of non-disequal arguments + // add care pairs based on each pair of non-disequal arguments for (std::map::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it) { std::map::iterator it2 = it; ++it2; - for( ; it2 != t1->d_data.end(); ++it2 ){ - if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ + for (; it2 != t1->d_data.end(); ++it2) + { + if (!d_equalityEngine.areDisequal(it->first, it2->first, false)) + { if (!areCareDisequal(it->first, it2->first)) { - addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs ); + addCarePairs( + &it->second, &it2->second, arity, depth + 1, n_pairs); } } } } - }else{ - //add care pairs based on product of indices, non-disequal arguments + } + else + { + // add care pairs based on product of indices, non-disequal arguments for (std::pair& tt1 : t1->d_data) { for (std::pair& tt2 : t2->d_data) @@ -965,7 +1108,8 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, } } -void TheorySetsPrivate::computeCareGraph() { +void TheorySetsPrivate::computeCareGraph() +{ const std::map >& ol = d_state.getOperatorList(); for (const std::pair >& it : ol) { @@ -978,32 +1122,39 @@ void TheorySetsPrivate::computeCareGraph() { Trace("sets-cg") << "Build index for " << k << "..." << std::endl; std::map index; unsigned arity = 0; - //populate indices + // populate indices for (TNode f1 : it.second) { Assert(d_equalityEngine.hasTerm(f1)); Trace("sets-cg-debug") << "...build for " << f1 << std::endl; Assert(d_equalityEngine.hasTerm(f1)); - //break into index based on operator, and type of first argument (since some operators are parametric) + // break into index based on operator, and type of first argument (since + // some operators are parametric) TypeNode tn = f1[0].getType(); - std::vector< TNode > reps; + std::vector reps; bool hasCareArg = false; - for( unsigned j=0; j0 ){ - //for each index + if (arity > 0) + { + // for each index for (std::pair& tt : index) { Trace("sets-cg") << "Process index " << tt.first << "..." @@ -1016,23 +1167,33 @@ void TheorySetsPrivate::computeCareGraph() { } } -bool TheorySetsPrivate::isCareArg( Node n, unsigned a ) { - if( d_equalityEngine.isTriggerTerm( n[a], THEORY_SETS ) ){ +bool TheorySetsPrivate::isCareArg(Node n, unsigned a) +{ + if (d_equalityEngine.isTriggerTerm(n[a], THEORY_SETS)) + { return true; - }else if( ( n.getKind()==kind::MEMBER || n.getKind()==kind::SINGLETON ) && a==0 && n[0].getType().isSet() ){ + } + else if ((n.getKind() == kind::MEMBER || n.getKind() == kind::SINGLETON) + && a == 0 && n[0].getType().isSet()) + { return true; - }else{ + } + else + { return false; } } -EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) { +EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) +{ Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b)); - if (d_equalityEngine.areEqual(a, b)) { + if (d_equalityEngine.areEqual(a, b)) + { // The terms are implied to be equal return EQUALITY_TRUE; } - if (d_equalityEngine.areDisequal(a, b, false)) { + if (d_equalityEngine.areDisequal(a, b, false)) + { // The terms are implied to be dis-equal return EQUALITY_FALSE; } @@ -1058,13 +1219,43 @@ EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) { /******************** Model generation ********************/ /******************** Model generation ********************/ +namespace { +/** + * This function is a helper function to print sets as + * Set A = { a0, a1, a2, } + * instead of + * (union (singleton a0) (union (singleton a1) (singleton a2))) + */ +void traceSetElementsRecursively(stringstream& stream, const Node& set) +{ + Assert(set.getType().isSet()); + if (set.getKind() == SINGLETON) + { + stream << set[0] << ", "; + } + if (set.getKind() == UNION) + { + traceSetElementsRecursively(stream, set[0]); + traceSetElementsRecursively(stream, set[1]); + } +} + +std::string traceElements(const Node& set) +{ + std::stringstream stream; + traceSetElementsRecursively(stream, set); + return stream.str(); +} + +} // namespace + bool TheorySetsPrivate::collectModelInfo(TheoryModel* m) { Trace("sets-model") << "Set collect model info" << std::endl; set termSet; // Compute terms appearing in assertions and shared terms d_external.computeRelevantTerms(termSet); - + // Assert equalities and disequalities to the model if (!m->assertEqualityEngine(&d_equalityEngine, &termSet)) { @@ -1072,7 +1263,7 @@ bool TheorySetsPrivate::collectModelInfo(TheoryModel* m) } NodeManager* nm = NodeManager::currentNM(); - std::map< Node, Node > mvals; + std::map mvals; // If cardinality is enabled, we need to use the ordered equivalence class // list computed by the cardinality solver, where sets equivalence classes // are assigned model values based on their position in the cardinality @@ -1084,13 +1275,19 @@ bool TheorySetsPrivate::collectModelInfo(TheoryModel* m) for (int i = (int)(sec.size() - 1); i >= 0; i--) { Node eqc = sec[i]; - if( termSet.find( eqc )==termSet.end() ){ - Trace("sets-model") << "* Do not assign value for " << eqc << " since is not relevant." << std::endl; - }else{ - std::vector< Node > els; + if (termSet.find(eqc) == termSet.end()) + { + Trace("sets-model") << "* Do not assign value for " << eqc + << " since is not relevant." << std::endl; + } + else + { + std::vector els; bool is_base = !d_card_enabled || d_cardSolver->isModelValueBasic(eqc); - if( is_base ){ - Trace("sets-model") << "Collect elements of base eqc " << eqc << std::endl; + if (is_base) + { + Trace("sets-model") + << "Collect elements of base eqc " << eqc << std::endl; // members that must be in eqc const std::map& emems = d_state.getMembers(eqc); if (!emems.empty()) @@ -1098,24 +1295,44 @@ bool TheorySetsPrivate::collectModelInfo(TheoryModel* m) for (const std::pair& itmm : emems) { Node t = nm->mkNode(kind::SINGLETON, itmm.first); - els.push_back( t ); + els.push_back(t); } } } - if( d_card_enabled ){ + if (d_card_enabled) + { // make the slack elements for the equivalence class based on set // cardinality - d_cardSolver->mkModelValueElementsFor(val, eqc, els, mvals); + d_cardSolver->mkModelValueElementsFor(val, eqc, els, mvals, m); } - Node rep = NormalForm::mkBop( kind::UNION, els, eqc.getType() ); - rep = Rewriter::rewrite( rep ); - Trace("sets-model") << "* Assign representative of " << eqc << " to " << rep << std::endl; + Node rep = NormalForm::mkBop(kind::UNION, els, eqc.getType()); + rep = Rewriter::rewrite(rep); + Trace("sets-model") << "* Assign representative of " << eqc << " to " + << rep << std::endl; mvals[eqc] = rep; if (!m->assertEquality(eqc, rep, true)) { return false; } m->assertSkeleton(rep); + + Trace("sets-model") << "Set " << eqc << " = { " << traceElements(rep) + << " }" << std::endl; + } + } + + // handle slack elements constraints for finite types + if (d_card_enabled) + { + const std::map >& slackElements = + d_cardSolver->getFiniteTypeSlackElements(); + for (const std::pair >& pair : slackElements) + { + const std::vector& members = + d_cardSolver->getFiniteTypeMembers(pair.first); + m->setAssignmentExclusionSetGroup(pair.second, members); + Trace("sets-model") << "ExclusionSet: Group " << pair.second + << " is excluded from set" << members << std::endl; } } return true; @@ -1125,26 +1342,32 @@ bool TheorySetsPrivate::collectModelInfo(TheoryModel* m) /********************** Helper functions ***************************/ /********************** Helper functions ***************************/ -Node mkAnd(const std::vector& conjunctions) { +Node mkAnd(const std::vector& conjunctions) +{ Assert(conjunctions.size() > 0); std::set all; - for (unsigned i = 0; i < conjunctions.size(); ++i) { + for (unsigned i = 0; i < conjunctions.size(); ++i) + { TNode t = conjunctions[i]; - if (t.getKind() == kind::AND) { - for(TNode::iterator child_it = t.begin(); - child_it != t.end(); ++child_it) { + if (t.getKind() == kind::AND) + { + for (TNode::iterator child_it = t.begin(); child_it != t.end(); + ++child_it) + { Assert((*child_it).getKind() != kind::AND); all.insert(*child_it); } } - else { + else + { all.insert(t); } } Assert(all.size() > 0); - if (all.size() == 1) { + if (all.size() == 1) + { // All the same, or just one return conjunctions[0]; } @@ -1152,35 +1375,37 @@ Node mkAnd(const std::vector& conjunctions) { NodeBuilder<> conjunction(kind::AND); std::set::const_iterator it = all.begin(); std::set::const_iterator it_end = all.end(); - while (it != it_end) { + while (it != it_end) + { conjunction << *it; - ++ it; + ++it; } return conjunction; -}/* mkAnd() */ +} /* mkAnd() */ -void TheorySetsPrivate::propagate(Theory::Effort effort) { +void TheorySetsPrivate::propagate(Theory::Effort effort) {} -} - -bool TheorySetsPrivate::propagate(TNode literal) { - Debug("sets-prop") << " propagate(" << literal << ")" << std::endl; +bool TheorySetsPrivate::propagate(TNode literal) +{ + Debug("sets-prop") << " propagate(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_state.isInConflict()) { - Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl; + Debug("sets-prop") << "TheoryUF::propagate(" << literal + << "): already in conflict" << std::endl; return false; } // Propagate out bool ok = d_external.d_out->propagate(literal); - if (!ok) { + if (!ok) + { d_state.setConflict(); } return ok; -}/* TheorySetsPrivate::propagate(TNode) */ +} /* TheorySetsPrivate::propagate(TNode) */ OutputChannel* TheorySetsPrivate::getOutputChannel() { @@ -1189,11 +1414,11 @@ OutputChannel* TheorySetsPrivate::getOutputChannel() Valuation& TheorySetsPrivate::getValuation() { return d_external.d_valuation; } -void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { +void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) +{ d_equalityEngine.setMasterEqualityEngine(eq); } - void TheorySetsPrivate::conflict(TNode a, TNode b) { Node conf = explain(a.eqNode(b)); @@ -1205,18 +1430,22 @@ void TheorySetsPrivate::conflict(TNode a, TNode b) Node TheorySetsPrivate::explain(TNode literal) { - Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")" - << std::endl; + Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")" << std::endl; bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; std::vector assumptions; - if(atom.getKind() == kind::EQUAL) { + if (atom.getKind() == kind::EQUAL) + { d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); - } else if(atom.getKind() == kind::MEMBER) { + } + else if (atom.getKind() == kind::MEMBER) + { d_equalityEngine.explainPredicate(atom, polarity, assumptions); - } else { + } + else + { Debug("sets") << "unhandled: " << literal << "; (" << atom << ", " << polarity << "); kind" << atom.getKind() << std::endl; Unhandled(); @@ -1229,34 +1458,30 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) { Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")" << std::endl; - switch(node.getKind()) { - case kind::EQUAL: - d_equalityEngine.addTriggerEquality(node); - break; - case kind::MEMBER: - d_equalityEngine.addTriggerPredicate(node); - break; - case kind::CARD: - d_equalityEngine.addTriggerTerm(node, THEORY_SETS); - break; - default: - d_equalityEngine.addTerm(node); - break; + switch (node.getKind()) + { + case kind::EQUAL: d_equalityEngine.addTriggerEquality(node); break; + case kind::MEMBER: d_equalityEngine.addTriggerPredicate(node); break; + case kind::CARD: d_equalityEngine.addTriggerTerm(node, THEORY_SETS); break; + default: d_equalityEngine.addTerm(node); break; } } -Node TheorySetsPrivate::expandDefinition(LogicRequest &logicRequest, Node n) { +Node TheorySetsPrivate::expandDefinition(LogicRequest& logicRequest, Node n) +{ Debug("sets-proc") << "expandDefinition : " << n << std::endl; return n; } -Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { +Theory::PPAssertStatus TheorySetsPrivate::ppAssert( + TNode in, SubstitutionMap& outSubstitutions) +{ Debug("sets-proc") << "ppAssert : " << in << std::endl; Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED; - - //TODO: allow variable elimination for sets when setsExt = true - - //this is based off of Theory::ppAssert + + // TODO: allow variable elimination for sets when setsExt = true + + // this is based off of Theory::ppAssert if (in.getKind() == kind::EQUAL) { if (in[0].isVar() && !expr::hasSubterm(in[1], in[0]) @@ -1294,68 +1519,88 @@ void TheorySetsPrivate::presolve() { d_state.reset(); } /**************************** eq::NotifyClass *****************************/ /**************************** eq::NotifyClass *****************************/ - -bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) +bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, + bool value) { - Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality - << " value = " << value << std::endl; - if (value) { + Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " + << equality << " value = " << value << std::endl; + if (value) + { return d_theory.propagate(equality); - } else { + } + else + { // We use only literal triggers so taking not is safe return d_theory.propagate(equality.notNode()); } } -bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) +bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, + bool value) { - Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate - << " value = " << value << std::endl; - if (value) { + Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " + << predicate << " value = " << value << std::endl; + if (value) + { return d_theory.propagate(predicate); - } else { + } + else + { return d_theory.propagate(predicate.notNode()); } } -bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) +bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) { Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag - << " t1 = " << t1 << " t2 = " << t2 << " value = " << value << std::endl; - d_theory.propagate( value ? t1.eqNode( t2 ) : t1.eqNode( t2 ).negate() ); + << " t1 = " << t1 << " t2 = " << t2 << " value = " << value + << std::endl; + d_theory.propagate(value ? t1.eqNode(t2) : t1.eqNode(t2).negate()); return true; } -void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) +void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, + TNode t2) { - Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl; + Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " + << " t1 = " << t1 << " t2 = " << t2 << std::endl; d_theory.conflict(t1, t2); } void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t) { - Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl; + Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" + << " t = " << t << std::endl; d_theory.eqNotifyNewClass(t); } void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2) { - Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; + Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" + << " t1 = " << t1 << " t2 = " << t2 << std::endl; d_theory.eqNotifyPreMerge(t1, t2); } void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2) { - Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; + Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" + << " t1 = " << t1 << " t2 = " << t2 << std::endl; d_theory.eqNotifyPostMerge(t1, t2); } -void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) +void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, + TNode t2, + TNode reason) { - Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl; + Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" + << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason + << std::endl; d_theory.eqNotifyDisequal(t1, t2, reason); } -}/* CVC4::theory::sets namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace sets +} // namespace theory +} // namespace CVC4 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a53201e3e..22848ff97 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1583,6 +1583,22 @@ set(regress_1_tests 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/finite-type/sets-card-arrcolor.smt2 + regress1/sets/finite-type/sets-card-arrunit.smt2 + regress1/sets/finite-type/sets-card-bool-1.smt2 + regress1/sets/finite-type/sets-card-bool-2.smt2 + regress1/sets/finite-type/sets-card-bool-3.smt2 + regress1/sets/finite-type/sets-card-bool-4.smt2 + regress1/sets/finite-type/sets-card-bool-rec.smt2 + regress1/sets/finite-type/sets-card-bv-1.smt2 + regress1/sets/finite-type/sets-card-bv-2.smt2 + regress1/sets/finite-type/sets-card-bv-3.smt2 + regress1/sets/finite-type/sets-card-bv-4.smt2 + regress1/sets/finite-type/sets-card-color.smt2 + regress1/sets/finite-type/sets-card-color-sat.smt2 + regress1/sets/finite-type/sets-card-datatype-1.smt2 + regress1/sets/finite-type/sets-card-datatype-2.smt2 + regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 regress1/sets/fuzz14418.smt2 regress1/sets/fuzz15201.smt2 regress1/sets/fuzz31811.smt2 @@ -2277,6 +2293,7 @@ set(regression_disabled_tests regress1/rewriterules/test_guards.smt2 regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 regress1/sets/setofsets-disequal.smt2 + regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 regress1/simple-rdl-definefun.smt2 # does not solve after minor modification to search regress1/sygus/car_3.lus.sy diff --git a/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 b/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 new file mode 100644 index 000000000..2c7acf282 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_ALL) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-datatype Color ((Red) (Green) (Blue))) +(declare-fun A () (Set (Array Color Color))) +(declare-fun B () (Set (Array Color Color))) +(assert (> (card A) 25)) +(assert (> (card B) 25)) +(assert (distinct A B)) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 b/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 new file mode 100644 index 000000000..95d363397 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_ALL) +(set-info :status unsat) +(set-option :sets-ext true) +(declare-datatype Unit ((mkUnit))) + +(declare-fun S () (Set (Array Int Unit))) + +(assert (> (card S) 1)) + +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 new file mode 100644 index 000000000..c455caa28 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set Bool)) +(declare-fun B () (Set Bool)) +(declare-fun universe () (Set Bool)) +(assert (= (card A) 2)) +(assert (= (card B) 2)) +(assert (= (intersection A B) (as emptyset (Set Bool)))) +(assert (= universe (as univset (Set Bool)))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 new file mode 100644 index 000000000..977bf3795 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set Bool)) +(declare-fun universe () (Set Bool)) +(assert (= (card A) 2)) +(assert (= universe (as univset (Set Bool)))) +(check-sat) + diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 new file mode 100644 index 000000000..623376e37 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set Bool)) +(declare-fun B () (Set Bool)) +(declare-fun universe () (Set Bool)) +(assert (= (card A) 2)) +(assert (= (card B) 2)) +(assert (= universe (as univset (Set Bool)))) +(check-sat) + diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 new file mode 100644 index 000000000..1e18597dc --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_ALL) +(set-info :status sat) +(set-option :sets-ext true) +(set-option :produce-models true) +(declare-fun A () (Set Bool)) +(declare-fun x () Bool) +(assert (member (member x A) A)) +(assert (> (card A) 1)) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 new file mode 100644 index 000000000..150dd5cff --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_ALL) +(set-info :status sat) +(set-option :sets-ext true) +(declare-fun A () (Set Bool)) +(declare-fun x () Bool) +(assert (member (member x A) A)) +(assert (> (card A) 1)) +(declare-fun U () (Set Bool)) +(assert (= U (as univset (Set Bool)))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 new file mode 100644 index 000000000..1388b9bfa --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set (_ BitVec 3))) +(declare-fun universe () (Set (_ BitVec 3))) +(assert (= (card A) 3)) +(assert (= universe (as univset (Set (_ BitVec 3))))) +(check-sat) + diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 new file mode 100644 index 000000000..26ee05f3c --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 @@ -0,0 +1,16 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set (_ BitVec 3))) +(declare-fun B () (Set (_ BitVec 3))) +(declare-fun universe () (Set (_ BitVec 3))) +(assert (= (card A) 5)) +(assert (= (card B) 5)) +(assert (not (= A B))) +(assert (= (card (intersection A B)) 2)) +(assert (= (card (setminus A B)) 3)) +(assert (= (card (setminus B A)) 3)) +(assert (= universe (as univset (Set (_ BitVec 3))))) +(check-sat) + diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 new file mode 100644 index 000000000..8c92d1c6b --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 @@ -0,0 +1,19 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set (_ BitVec 3))) +(declare-fun B () (Set (_ BitVec 3))) +(declare-fun universe () (Set (_ BitVec 3))) +(declare-fun x () (_ BitVec 3)) +(assert (= (card A) 3)) +(assert (= (card B) 3)) +(assert (not (= A B))) +(assert (= (card (intersection A B)) 1)) +(assert (= (card (setminus A B)) 2)) +(assert (= (card (setminus B A)) 2)) +(assert (not (member x A))) +(assert (not (member x B))) +(assert (= universe (as univset (Set (_ BitVec 3))))) +(check-sat) + diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 new file mode 100644 index 000000000..d2c8a744d --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 @@ -0,0 +1,18 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set (_ BitVec 3))) +(declare-fun B () (Set (_ BitVec 3))) +(declare-fun universe () (Set (_ BitVec 3))) +(declare-fun x () (_ BitVec 3)) +(assert (= (card A) 5)) +(assert (= (card B) 5)) +(assert (not (= A B))) +(assert (= (card (intersection A B)) 2)) +(assert (= (card (setminus A B)) 3)) +(assert (= (card (setminus B A)) 3)) +(assert (= universe (as univset (Set (_ BitVec 3))))) +(assert (not (member x A))) +(assert (not (member x B))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 b/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 new file mode 100644 index 000000000..ca8015622 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_BVDTLIAFS) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-datatype Color ((Red) (Green) (Blue) (Purple))) +(declare-fun A () (Set Color)) +(declare-fun B () (Set Color)) +(assert (> (card A) (card B) )) +(assert (member Red B)) +(declare-fun d () Color) +(assert (not (= d Red))) +(assert (member d B)) +(assert (not (member Green A))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-color.smt2 b/test/regress/regress1/sets/finite-type/sets-card-color.smt2 new file mode 100644 index 000000000..4fe3f0428 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-color.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_BVDTLIAFS) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-datatype Color ((Red) (Green) (Blue))) +(declare-fun A () (Set Color)) +(declare-fun B () (Set Color)) +(assert (> (card A) (card B) )) +(assert (member Red B)) +(declare-fun d () Color) +(assert (not (= d Red))) +(assert (member d B)) +(assert (not (member Green A))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 new file mode 100644 index 000000000..0121479e9 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-datatype Rec ((mkRec (r1 (_ BitVec 2)) (r2 (_ BitVec 2))))) +(declare-fun A () (Set Rec)) +(declare-fun B () (Set Rec)) +(declare-fun universe () (Set Rec)) +(declare-fun x () Rec) +(assert (= (card A) 5)) +(assert (= (card B) 5)) +(assert (= (card (intersection A B)) 1)) +(assert (= universe (as univset (Set Rec)))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 new file mode 100644 index 000000000..708ebb2ca --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-datatype Rec ((mkRec (r1 (_ BitVec 2)) (r2 (_ BitVec 2))))) +(declare-fun A () (Set Rec)) +(declare-fun B () (Set Rec)) +(declare-fun universe () (Set Rec)) +(assert (= (card A) 9)) +(assert (= (card B) 9)) +(assert (= (card (intersection A B)) 1)) +(assert (= universe (as univset (Set Rec)))) +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 new file mode 100644 index 000000000..b4bd97f1d --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 @@ -0,0 +1,30 @@ +(set-logic QF_ALL) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set (_ BitVec 2))) +(declare-fun B () (Set (_ BitVec 2))) +(declare-fun C () (Set (_ BitVec 2))) +(declare-fun D () (Set (_ BitVec 2))) + +(declare-fun x () (_ BitVec 2)) +(assert (not (member x A))) +(assert (not (member x B))) +(assert (not (member x C))) +(assert (not (member x D))) +(declare-fun y () (_ BitVec 2)) +(assert (not (member y A))) +(assert (not (member y B))) +(assert (not (member y C))) +(assert (not (member y D))) +(declare-fun z () (_ BitVec 2)) +(assert (not (member z A))) +(assert (not (member z B))) +(assert (not (member z C))) +(assert (not (member z D))) + +(assert (distinct x y z)) + +(assert (= (card (union A (union B (union C D)))) 2)) + +(check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 new file mode 100644 index 000000000..88825a600 --- /dev/null +++ b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 @@ -0,0 +1,30 @@ +(set-logic QF_ALL) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set (_ BitVec 3))) +(declare-fun B () (Set (_ BitVec 3))) +(declare-fun C () (Set (_ BitVec 3))) +(declare-fun D () (Set (_ BitVec 3))) + +(declare-fun x () (_ BitVec 3)) +(assert (not (member x A))) +(assert (not (member x B))) +(assert (not (member x C))) +(assert (not (member x D))) +(declare-fun y () (_ BitVec 3)) +(assert (not (member y A))) +(assert (not (member y B))) +(assert (not (member y C))) +(assert (not (member y D))) +(declare-fun z () (_ BitVec 3)) +(assert (not (member z A))) +(assert (not (member z B))) +(assert (not (member z C))) +(assert (not (member z D))) + +(assert (distinct x y z)) + +(assert (= (card (union A (union B (union C D)))) 6)) + +(check-sat) -- 2.30.2