From 1d3bb6048085342e2d85bf5193367afcd96885fa Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 8 Sep 2020 20:36:08 -0500 Subject: [PATCH] Split term registry from theory state in sets (#5037) Currently, the theory state object SolverState in sets sends lemmas and has a reference to the parent theory. This PR is work towards eliminating these dependencies. This adds a TermRegistry object which is responsible for some of the tasks currently done by SolverState, including all those involving lemmas. Notice this also makes a bug fix in getUnivSetEqClass where the universe set was being returned instead of its representative. A followup PR will make SolverState maintain SAT-context-dependent membership lists which is also required for breaking the dependence on the parent theory. --- src/CMakeLists.txt | 2 + src/theory/sets/cardinality_extension.cpp | 29 ++-- src/theory/sets/cardinality_extension.h | 7 +- src/theory/sets/solver_state.cpp | 127 +----------------- src/theory/sets/solver_state.h | 68 ++-------- src/theory/sets/term_registry.cpp | 154 ++++++++++++++++++++++ src/theory/sets/term_registry.h | 94 +++++++++++++ src/theory/sets/theory_sets.cpp | 5 +- src/theory/sets/theory_sets.h | 3 + src/theory/sets/theory_sets_private.cpp | 40 +++--- src/theory/sets/theory_sets_private.h | 8 +- src/theory/sets/theory_sets_rels.cpp | 36 ++--- src/theory/sets/theory_sets_rels.h | 10 +- 13 files changed, 351 insertions(+), 232 deletions(-) create mode 100644 src/theory/sets/term_registry.cpp create mode 100644 src/theory/sets/term_registry.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6cd2c24d1..5a06df28b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -709,6 +709,8 @@ libcvc4_add_sources( theory/sets/skolem_cache.h theory/sets/solver_state.cpp theory/sets/solver_state.h + theory/sets/term_registry.cpp + theory/sets/term_registry.h theory/sets/theory_sets.cpp theory/sets/theory_sets.h theory/sets/theory_sets_private.cpp diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 321559f5a..447782ba2 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -30,9 +30,12 @@ namespace CVC4 { namespace theory { namespace sets { -CardinalityExtension::CardinalityExtension(SolverState& s, InferenceManager& im) +CardinalityExtension::CardinalityExtension(SolverState& s, + InferenceManager& im, + TermRegistry& treg) : d_state(s), d_im(im), + d_treg(treg), d_card_processed(s.getUserContext()), d_finite_type_constants_processed(false) { @@ -101,7 +104,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) // here we call getUnivSet instead of getUnivSetEqClass to generate // a univset term for finite types even if they are not used in the input - Node univ = d_state.getUnivSet(setType); + Node univ = d_treg.getUnivSet(setType); std::map::iterator it = d_univProxy.find(univ); Node proxy; @@ -109,7 +112,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) if (it == d_univProxy.end()) { // Force cvc4 to build the cardinality graph for the universe set - proxy = d_state.getProxy(univ); + proxy = d_treg.getProxy(univ); d_univProxy[univ] = proxy; } else @@ -208,9 +211,9 @@ void CardinalityExtension::check() Assert(intro_sets.size() == 1); Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl; Trace("sets-intro") << " Actual Intro : "; - d_state.debugPrintSet(intro_sets[0], "sets-nf"); + d_treg.debugPrintSet(intro_sets[0], "sets-nf"); Trace("sets-nf") << std::endl; - Node k = d_state.getProxy(intro_sets[0]); + Node k = d_treg.getProxy(intro_sets[0]); AlwaysAssert(!k.isNull()); } @@ -274,7 +277,7 @@ void CardinalityExtension::registerCardinalityTerm(Node n) for (unsigned k = 0, csize = cterms.size(); k < csize; k++) { Node nn = cterms[k]; - Node nk = d_state.getProxy(nn); + Node nk = d_treg.getProxy(nn); Node pos_lem = nm->mkNode(GEQ, nm->mkNode(CARD, nk), d_zero); d_im.assertInference(pos_lem, d_emp_exp, "pcard", 1); if (nn != nk) @@ -361,7 +364,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, curr.push_back(eqc); TypeNode tn = eqc.getType(); bool is_empty = eqc == d_state.getEmptySetEqClass(tn); - Node emp_set = d_state.getEmptySet(tn); + Node emp_set = d_treg.getEmptySet(tn); for (const Node& n : nvsets) { Kind nk = n.getKind(); @@ -683,7 +686,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, Trace("sets-nf") << " F " << itf.first << " : " << itf.second << std::endl; Trace("sets-nf-debug") << " ..."; - d_state.debugPrintSet(itf.first, "sets-nf-debug"); + d_treg.debugPrintSet(itf.first, "sets-nf-debug"); Trace("sets-nf-debug") << std::endl; } } @@ -696,7 +699,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, std::vector& nfeqc = d_nf[eqc]; NodeManager* nm = NodeManager::currentNM(); bool success = true; - Node emp_set = d_state.getEmptySet(tn); + Node emp_set = d_treg.getEmptySet(tn); if (!base.isNull()) { for (unsigned j = 0, csize = comps.size(); j < csize; j++) @@ -772,7 +775,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, Node r = e == 2 ? common[l] : only[e][l]; Trace("sets-nf-debug") << "Try split empty : " << r << std::endl; Trace("sets-nf-debug") << " actual : "; - d_state.debugPrintSet(r, "sets-nf-debug"); + d_treg.debugPrintSet(r, "sets-nf-debug"); Trace("sets-nf-debug") << std::endl; Assert(!d_state.areEqual(r, emp_set)); if (!d_state.areDisequal(r, emp_set) && !d_state.hasMembers(r)) @@ -780,7 +783,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, // guess that its equal empty if it has no explicit members Trace("sets-nf") << " Split empty : " << r << std::endl; Trace("sets-nf") << "Actual Split : "; - d_state.debugPrintSet(r, "sets-nf"); + d_treg.debugPrintSet(r, "sets-nf"); Trace("sets-nf") << std::endl; d_im.split(r.eqNode(emp_set), 1); Assert(d_im.hasSent()); @@ -820,8 +823,8 @@ void CardinalityExtension::checkNormalForm(Node eqc, { // simply introduce their intersection Assert(o0 != o1); - Node kca = d_state.getProxy(o0); - Node kcb = d_state.getProxy(o1); + Node kca = d_treg.getProxy(o0); + Node kcb = d_treg.getProxy(o1); Node intro = Rewriter::rewrite(nm->mkNode(INTERSECTION, kca, kcb)); Trace("sets-nf") << " Intro split : " << o0 << " against " << o1 diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h index c257f45c5..38f259919 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/sets/term_registry.h" #include "theory/type_set.h" #include "theory/uf/equality_engine.h" @@ -67,7 +68,9 @@ class CardinalityExtension * Constructs a new instance of the cardinality solver w.r.t. the provided * contexts. */ - CardinalityExtension(SolverState& s, InferenceManager& im); + CardinalityExtension(SolverState& s, + InferenceManager& im, + TermRegistry& treg); ~CardinalityExtension() {} /** reset @@ -160,6 +163,8 @@ class CardinalityExtension SolverState& d_state; /** Reference to the inference manager for the theory of sets */ InferenceManager& d_im; + /** Reference to the term registry */ + TermRegistry& d_treg; /** register cardinality term * * This method add lemmas corresponding to the definition of diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 7254bca78..941f59bc6 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -27,8 +27,9 @@ namespace sets { SolverState::SolverState(context::Context* c, context::UserContext* u, - Valuation val) - : TheoryState(c, u, val), d_parent(nullptr), d_proxy(u), d_proxy_to_term(u) + Valuation val, + SkolemCache& skc) + : TheoryState(c, u, val), d_skCache(skc), d_parent(nullptr) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -98,8 +99,6 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n) { if (nk == SINGLETON) { - // singleton lemma - getProxy(n); Node re = d_ee->getRepresentative(n[0]); if (d_singleton_index.find(re) == d_singleton_index.end()) { @@ -186,8 +185,8 @@ Node SolverState::getEmptySetEqClass(TypeNode tn) const Node SolverState::getUnivSetEqClass(TypeNode tn) const { - std::map::const_iterator it = d_univset.find(tn); - if (it != d_univset.end()) + std::map::const_iterator it = d_eqc_univset.find(tn); + if (it != d_eqc_univset.end()) { return it->second; } @@ -368,37 +367,6 @@ bool SolverState::isSetDisequalityEntailedInternal(Node a, return false; } -Node SolverState::getProxy(Node n) -{ - Kind nk = n.getKind(); - if (nk != EMPTYSET && nk != SINGLETON && nk != INTERSECTION && nk != SETMINUS - && nk != UNION && nk != UNIVERSE_SET) - { - return n; - } - NodeMap::const_iterator it = d_proxy.find(n); - if (it != d_proxy.end()) - { - return (*it).second; - } - NodeManager* nm = NodeManager::currentNM(); - Node k = d_skCache.mkTypedSkolemCached( - n.getType(), n, SkolemCache::SK_PURIFY, "sp"); - d_proxy[n] = k; - d_proxy_to_term[k] = n; - Node eq = k.eqNode(n); - Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl; - d_parent->getOutputChannel()->lemma(eq); - if (nk == SINGLETON) - { - Node slem = nm->mkNode(MEMBER, n[0], k); - Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton" - << std::endl; - d_parent->getOutputChannel()->lemma(slem); - } - return k; -} - Node SolverState::getCongruent(Node n) const { Assert(d_ee->hasTerm(n)); @@ -413,65 +381,6 @@ bool SolverState::isCongruent(Node n) const { return d_congruent.find(n) != d_congruent.end(); } - -Node SolverState::getEmptySet(TypeNode tn) -{ - std::map::iterator it = d_emptyset.find(tn); - if (it != d_emptyset.end()) - { - return it->second; - } - Node n = NodeManager::currentNM()->mkConst(EmptySet(tn)); - d_emptyset[tn] = n; - return n; -} -Node SolverState::getUnivSet(TypeNode tn) -{ - std::map::iterator it = d_univset.find(tn); - if (it != d_univset.end()) - { - return it->second; - } - NodeManager* nm = NodeManager::currentNM(); - Node n = nm->mkNullaryOperator(tn, UNIVERSE_SET); - for (it = d_univset.begin(); it != d_univset.end(); ++it) - { - Node n1; - Node n2; - if (tn.isSubtypeOf(it->first)) - { - n1 = n; - n2 = it->second; - } - else if (it->first.isSubtypeOf(tn)) - { - n1 = it->second; - n2 = n; - } - if (!n1.isNull()) - { - Node ulem = nm->mkNode(SUBSET, n1, n2); - Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type" - << std::endl; - d_parent->getOutputChannel()->lemma(ulem); - } - } - d_univset[tn] = n; - return n; -} - -Node SolverState::getTypeConstraintSkolem(Node n, TypeNode tn) -{ - std::map::iterator it = d_tc_skolem[n].find(tn); - if (it == d_tc_skolem[n].end()) - { - Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn); - d_tc_skolem[n][tn] = k; - return k; - } - return it->second; -} - const std::vector& SolverState::getNonVariableSets(Node r) const { std::map >::const_iterator it = d_nvar_sets.find(r); @@ -547,32 +456,6 @@ const std::vector& SolverState::getComprehensionSets() const return d_allCompSets; } -void SolverState::debugPrintSet(Node s, const char* c) const -{ - if (s.getNumChildren() == 0) - { - NodeMap::const_iterator it = d_proxy_to_term.find(s); - if (it != d_proxy_to_term.end()) - { - debugPrintSet((*it).second, c); - } - else - { - Trace(c) << s; - } - } - else - { - Trace(c) << "(" << s.getOperator(); - for (const Node& sc : s) - { - Trace(c) << " "; - debugPrintSet(sc, c); - } - Trace(c) << ")"; - } -} - const vector SolverState::getSetsEqClasses(const TypeNode& t) const { vector representatives; diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index 1786c414b..245ad93f6 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -20,7 +20,6 @@ #include #include -#include "context/cdhashset.h" #include "theory/sets/skolem_cache.h" #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" @@ -33,10 +32,8 @@ class TheorySetsPrivate; /** Sets state * - * The purpose of this class is to: - * (1) Maintain information concerning the current set of assertions during a - * full effort check, - * (2) Maintain a database of commonly used terms. + * The purpose of this class is to maintain information concerning the current + * set of assertions during a full effort check. * * During a full effort check, the solver for theory of sets should call: * reset; ( registerEqc | registerTerm )* @@ -45,10 +42,11 @@ class TheorySetsPrivate; */ class SolverState : public TheoryState { - typedef context::CDHashMap NodeMap; - public: - SolverState(context::Context* c, context::UserContext* u, Valuation val); + SolverState(context::Context* c, + context::UserContext* u, + Valuation val, + SkolemCache& skc); /** Set parent */ void setParent(TheorySetsPrivate* p); //-------------------------------- initialize per check @@ -158,44 +156,6 @@ class SolverState : public TheoryState /** Get the list of all comprehension sets in the current context */ const std::vector& getComprehensionSets() const; - // --------------------------------------- commonly used terms - /** Get type constraint skolem - * - * The sets theory solver outputs equality lemmas of the form: - * n = d_tc_skolem[n][tn] - * where the type of d_tc_skolem[n][tn] is tn, and the type - * of n is not a subtype of tn. This is required to handle benchmarks like - * test/regress/regress0/sets/sets-of-sets-subtypes.smt2 - * where for s : (Set Int) and t : (Set Real), we have that - * ( s = t ^ y in t ) implies ( exists k : Int. y = k ) - * The type constraint Skolem for (y, Int) is the skolemization of k above. - */ - Node getTypeConstraintSkolem(Node n, TypeNode tn); - /** get the proxy variable for set n - * - * Proxy variables are used to communicate information that otherwise would - * not be possible due to rewriting. For example, the literal - * card( singleton( 0 ) ) = 1 - * is rewritten to true. Instead, to communicate this fact (e.g. to other - * theories), we require introducing a proxy variable x for singleton( 0 ). - * Then: - * card( x ) = 1 ^ x = singleton( 0 ) - * communicates the equivalent of the above literal. - */ - Node getProxy(Node n); - /** Get the empty set of type tn */ - Node getEmptySet(TypeNode tn); - /** Get the universe set of type tn if it exists or create a new one */ - Node getUnivSet(TypeNode tn); - /** - * Get the skolem cache of this theory, which manages a database of introduced - * skolem variables used for various inferences. - */ - SkolemCache& getSkolemCache() { return d_skCache; } - // --------------------------------------- end commonly used terms - /** debug print set */ - void debugPrintSet(Node s, const char* c) const; - private: /** constants */ Node d_true; @@ -203,6 +163,8 @@ class SolverState : public TheoryState /** the empty vector and map */ std::vector d_emptyVec; std::map d_emptyMap; + /** Reference to skolem cache */ + SkolemCache& d_skCache; /** Pointer to the parent theory of sets */ TheorySetsPrivate* d_parent; /** The list of all equivalence classes of type set in the current context */ @@ -228,18 +190,6 @@ class SolverState : public TheoryState * to their negative memberships. */ std::map > d_pol_mems[2]; - // --------------------------------------- commonly used terms - /** Map from set terms to their proxy variables */ - NodeMap d_proxy; - /** Backwards map of above */ - NodeMap d_proxy_to_term; - /** Cache of type constraint skolems (see getTypeConstraintSkolem) */ - std::map > d_tc_skolem; - /** Map from types to empty set of that type */ - std::map d_emptyset; - /** Map from types to universe set of that type */ - std::map d_univset; - // --------------------------------------- end commonly used terms // -------------------------------- term indices /** Term index for MEMBER * @@ -260,8 +210,6 @@ class SolverState : public TheoryState std::vector d_allCompSets; // -------------------------------- end term indices std::map > d_op_list; - /** the skolem cache */ - SkolemCache d_skCache; /** is set disequality entailed internal * * This returns true if disequality between sets a and b is entailed in the diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp new file mode 100644 index 000000000..301d5a85b --- /dev/null +++ b/src/theory/sets/term_registry.cpp @@ -0,0 +1,154 @@ +/********************* */ +/*! \file term_registry.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Mudathir Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of sets term registry object + **/ + +#include "theory/sets/term_registry.h" + +#include "expr/emptyset.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace sets { + +TermRegistry::TermRegistry(SolverState& state, + InferenceManager& im, + SkolemCache& skc) + : d_im(im), + d_skCache(skc), + d_proxy(state.getUserContext()), + d_proxy_to_term(state.getUserContext()) +{ +} + +Node TermRegistry::getProxy(Node n) +{ + Kind nk = n.getKind(); + if (nk != EMPTYSET && nk != SINGLETON && nk != INTERSECTION && nk != SETMINUS + && nk != UNION && nk != UNIVERSE_SET) + { + return n; + } + NodeMap::const_iterator it = d_proxy.find(n); + if (it != d_proxy.end()) + { + return (*it).second; + } + NodeManager* nm = NodeManager::currentNM(); + Node k = d_skCache.mkTypedSkolemCached( + n.getType(), n, SkolemCache::SK_PURIFY, "sp"); + d_proxy[n] = k; + d_proxy_to_term[k] = n; + Node eq = k.eqNode(n); + Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl; + d_im.lemma(eq, LemmaProperty::NONE, false); + if (nk == SINGLETON) + { + Node slem = nm->mkNode(MEMBER, n[0], k); + Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton" + << std::endl; + d_im.lemma(slem, LemmaProperty::NONE, false); + } + return k; +} + +Node TermRegistry::getEmptySet(TypeNode tn) +{ + std::map::iterator it = d_emptyset.find(tn); + if (it != d_emptyset.end()) + { + return it->second; + } + Node n = NodeManager::currentNM()->mkConst(EmptySet(tn)); + d_emptyset[tn] = n; + return n; +} + +Node TermRegistry::getUnivSet(TypeNode tn) +{ + std::map::iterator it = d_univset.find(tn); + if (it != d_univset.end()) + { + return it->second; + } + NodeManager* nm = NodeManager::currentNM(); + Node n = nm->mkNullaryOperator(tn, UNIVERSE_SET); + for (it = d_univset.begin(); it != d_univset.end(); ++it) + { + Node n1; + Node n2; + if (tn.isSubtypeOf(it->first)) + { + n1 = n; + n2 = it->second; + } + else if (it->first.isSubtypeOf(tn)) + { + n1 = it->second; + n2 = n; + } + if (!n1.isNull()) + { + Node ulem = nm->mkNode(SUBSET, n1, n2); + Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type" + << std::endl; + d_im.lemma(ulem, LemmaProperty::NONE, false); + } + } + d_univset[tn] = n; + return n; +} + +Node TermRegistry::getTypeConstraintSkolem(Node n, TypeNode tn) +{ + std::map::iterator it = d_tc_skolem[n].find(tn); + if (it == d_tc_skolem[n].end()) + { + Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn); + d_tc_skolem[n][tn] = k; + return k; + } + return it->second; +} + +void TermRegistry::debugPrintSet(Node s, const char* c) const +{ + if (s.getNumChildren() == 0) + { + NodeMap::const_iterator it = d_proxy_to_term.find(s); + if (it != d_proxy_to_term.end()) + { + debugPrintSet((*it).second, c); + } + else + { + Trace(c) << s; + } + } + else + { + Trace(c) << "(" << s.getOperator(); + for (const Node& sc : s) + { + Trace(c) << " "; + debugPrintSet(sc, c); + } + Trace(c) << ")"; + } +} + +} // namespace sets +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h new file mode 100644 index 000000000..8779c7a19 --- /dev/null +++ b/src/theory/sets/term_registry.h @@ -0,0 +1,94 @@ +/********************* */ +/*! \file term_registry.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Mudathir Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Sets state object + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__SETS__TERM_REGISTRY_H +#define CVC4__THEORY__SETS__TERM_REGISTRY_H + +#include +#include + +#include "context/cdhashmap.h" +#include "theory/sets/inference_manager.h" +#include "theory/sets/skolem_cache.h" +#include "theory/sets/solver_state.h" + +namespace CVC4 { +namespace theory { +namespace sets { + +/** + * Term registry, the purpose of this class is to maintain a database of + * commonly used terms, and mappings from sets to their "proxy variables". + */ +class TermRegistry +{ + typedef context::CDHashMap NodeMap; + + public: + TermRegistry(SolverState& state, InferenceManager& im, SkolemCache& skc); + /** Get type constraint skolem + * + * The sets theory solver outputs equality lemmas of the form: + * n = d_tc_skolem[n][tn] + * where the type of d_tc_skolem[n][tn] is tn, and the type + * of n is not a subtype of tn. This is required to handle benchmarks like + * test/regress/regress0/sets/sets-of-sets-subtypes.smt2 + * where for s : (Set Int) and t : (Set Real), we have that + * ( s = t ^ y in t ) implies ( exists k : Int. y = k ) + * The type constraint Skolem for (y, Int) is the skolemization of k above. + */ + Node getTypeConstraintSkolem(Node n, TypeNode tn); + /** get the proxy variable for set n + * + * Proxy variables are used to communicate information that otherwise would + * not be possible due to rewriting. For example, the literal + * card( singleton( 0 ) ) = 1 + * is rewritten to true. Instead, to communicate this fact (e.g. to other + * theories), we require introducing a proxy variable x for singleton( 0 ). + * Then: + * card( x ) = 1 ^ x = singleton( 0 ) + * communicates the equivalent of the above literal. + */ + Node getProxy(Node n); + /** Get the empty set of type tn */ + Node getEmptySet(TypeNode tn); + /** Get the universe set of type tn if it exists or create a new one */ + Node getUnivSet(TypeNode tn); + /** debug print set */ + void debugPrintSet(Node s, const char* c) const; + + private: + /** The inference manager */ + InferenceManager& d_im; + /** Reference to the skolem cache */ + SkolemCache& d_skCache; + /** Map from set terms to their proxy variables */ + NodeMap d_proxy; + /** Backwards map of above */ + NodeMap d_proxy_to_term; + /** Cache of type constraint skolems (see getTypeConstraintSkolem) */ + std::map > d_tc_skolem; + /** Map from types to empty set of that type */ + std::map d_emptyset; + /** Map from types to universe set of that type */ + std::map d_univset; +}; /* class TheorySetsPrivate */ + +} // namespace sets +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__SETS__TERM_REGISTRY_H */ diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 8b969de39..fe5e56aa6 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -34,9 +34,10 @@ TheorySets::TheorySets(context::Context* c, const LogicInfo& logicInfo, ProofNodeManager* pnm) : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm), - d_state(c, u, valuation), + d_skCache(), + d_state(c, u, valuation, d_skCache), d_im(*this, d_state, pnm), - d_internal(new TheorySetsPrivate(*this, d_state, d_im)), + d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache)), d_notify(*d_internal.get()) { // use the official theory state and inference manager objects diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index fed74b1bb..fce57ca6c 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -22,6 +22,7 @@ #include #include "theory/sets/inference_manager.h" +#include "theory/sets/skolem_cache.h" #include "theory/sets/solver_state.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -98,6 +99,8 @@ class TheorySets : public Theory private: TheorySetsPrivate& d_theory; }; + /** The skolem cache */ + SkolemCache d_skCache; /** The state of the sets solver at full effort */ SolverState d_state; /** The inference manager */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 5e78e7ed5..a88374980 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -36,7 +36,8 @@ namespace sets { TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, SolverState& state, - InferenceManager& im) + InferenceManager& im, + SkolemCache& skc) : d_members(state.getSatContext()), d_deq(state.getSatContext()), d_termProcessed(state.getUserContext()), @@ -44,8 +45,10 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_external(external), d_state(state), d_im(im), - d_rels(new TheorySetsRels(d_state, d_im)), - d_cardSolver(new CardinalityExtension(d_state, d_im)), + d_skCache(skc), + d_treg(state, im, skc), + d_rels(new TheorySetsRels(state, im, skc, d_treg)), + d_cardSolver(new CardinalityExtension(state, im, d_treg)), d_rels_enabled(false), d_card_enabled(false) { @@ -334,15 +337,21 @@ void TheorySetsPrivate::fullEffortCheck() } // register it with the state d_state.registerTerm(eqc, tnn, n); - if (n.getKind() == kind::CARD) + Kind nk = n.getKind(); + if (nk == kind::SINGLETON) + { + // ensure the proxy has been introduced + d_treg.getProxy(n); + } + else if (nk == kind::CARD) { d_card_enabled = true; // register it with the cardinality solver d_cardSolver->registerTerm(n); // if we do not handle the kind, set incomplete - Kind nk = n[0].getKind(); + Kind nk0 = n[0].getKind(); // some kinds of cardinality we cannot handle - if (d_rels->isRelationKind(nk)) + if (d_rels->isRelationKind(nk0)) { d_full_check_incomplete = true; Trace("sets-incomplete") @@ -358,12 +367,9 @@ void TheorySetsPrivate::fullEffortCheck() // 4- Supporting cardinality for relations (hard) } } - else + else if (d_rels->isRelationKind(nk)) { - if (d_rels->isRelationKind(n.getKind())) - { - d_rels_enabled = true; - } + d_rels_enabled = true; } ++eqc_i; } @@ -501,7 +507,7 @@ void TheorySetsPrivate::checkSubtypes() exp.push_back(it2.second); Assert(d_state.areEqual(mctt, it2.second[1])); exp.push_back(mctt.eqNode(it2.second[1])); - Node tc_k = d_state.getTypeConstraintSkolem(it2.first, mct); + Node tc_k = d_treg.getTypeConstraintSkolem(it2.first, mct); if (!tc_k.isNull()) { Node etc = tc_k.eqNode(it2.first); @@ -559,7 +565,7 @@ void TheorySetsPrivate::checkDownwardsClosure() else { // use proxy set - Node k = d_state.getProxy(eq_set); + Node k = d_treg.getProxy(eq_set); Node pmem = NodeManager::currentNM()->mkNode(kind::MEMBER, mem[0], k); Node nmem = NodeManager::currentNM()->mkNode( @@ -677,7 +683,7 @@ void TheorySetsPrivate::checkUpwardsClosure() Node rr = d_equalityEngine->getRepresentative(term); if (!isMember(x, rr)) { - Node kk = d_state.getProxy(term); + Node kk = d_treg.getProxy(term); Node fact = nm->mkNode(kind::MEMBER, x, kk); d_im.assertInference(fact, exp, "upc", inferType); if (d_state.isInConflict()) @@ -704,7 +710,7 @@ void TheorySetsPrivate::checkUpwardsClosure() std::vector exp; exp.push_back(itm2m.second); d_state.addEqualityToExp(term[1], itm2m.second[1], exp); - Node r = d_state.getProxy(term); + Node r = d_treg.getProxy(term); Node fact = nm->mkNode(kind::MEMBER, x, r); d_im.assertInference(fact, exp, "upc2"); if (d_state.isInConflict()) @@ -750,7 +756,7 @@ void TheorySetsPrivate::checkUpwardsClosure() // equivalence class if (s != ueqc) { - u = d_state.getUnivSet(tn); + u = d_treg.getUnivSet(tn); } univ_set[tn] = u; } @@ -819,7 +825,7 @@ void TheorySetsPrivate::checkDisequalities() 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( + Node x = d_skCache.mkTypedSkolemCached( elementType, deq[0], deq[1], SkolemCache::SK_DISEQUAL, "sde"); Node mem1 = nm->mkNode(MEMBER, x, deq[0]); Node mem2 = nm->mkNode(MEMBER, x, deq[1]); diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index bd1d5f058..1c038e02f 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -25,6 +25,7 @@ #include "theory/sets/cardinality_extension.h" #include "theory/sets/inference_manager.h" #include "theory/sets/solver_state.h" +#include "theory/sets/term_registry.h" #include "theory/sets/theory_sets_rels.h" #include "theory/sets/theory_sets_rewriter.h" #include "theory/theory.h" @@ -149,7 +150,8 @@ class TheorySetsPrivate { */ TheorySetsPrivate(TheorySets& external, SolverState& state, - InferenceManager& im); + InferenceManager& im, + SkolemCache& skc); ~TheorySetsPrivate(); @@ -231,6 +233,10 @@ class TheorySetsPrivate { SolverState& d_state; /** The inference manager of the sets solver */ InferenceManager& d_im; + /** Reference to the skolem cache */ + SkolemCache& d_skCache; + /** The term registry */ + TermRegistry d_treg; /** Pointer to the equality engine of theory of sets */ eq::EqualityEngine* d_equalityEngine; diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 838d29045..209c3c973 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -31,8 +31,15 @@ typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT; typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator TC_IT; -TheorySetsRels::TheorySetsRels(SolverState& s, InferenceManager& im) - : d_state(s), d_im(im), d_shared_terms(s.getUserContext()) +TheorySetsRels::TheorySetsRels(SolverState& s, + InferenceManager& im, + SkolemCache& skc, + TermRegistry& treg) + : d_state(s), + d_im(im), + d_skCache(skc), + d_treg(treg), + d_shared_terms(s.getUserContext()) { d_trueNode = NodeManager::currentNM()->mkConst(true); d_falseNode = NodeManager::currentNM()->mkConst(false); @@ -542,17 +549,16 @@ void TheorySetsRels::check(Theory::Effort level) } Node fst_element = RelsUtils::nthElementOfTuple( exp[0], 0 ); Node snd_element = RelsUtils::nthElementOfTuple( exp[0], 1 ); - SkolemCache& sc = d_state.getSkolemCache(); - Node sk_1 = sc.mkTypedSkolemCached(fst_element.getType(), - exp[0], - tc_rel[0], - SkolemCache::SK_TCLOSURE_DOWN1, - "stc1"); - Node sk_2 = sc.mkTypedSkolemCached(fst_element.getType(), - exp[0], - tc_rel[0], - SkolemCache::SK_TCLOSURE_DOWN2, - "stc2"); + Node sk_1 = d_skCache.mkTypedSkolemCached(fst_element.getType(), + exp[0], + tc_rel[0], + SkolemCache::SK_TCLOSURE_DOWN1, + "stc1"); + Node sk_2 = d_skCache.mkTypedSkolemCached(fst_element.getType(), + exp[0], + tc_rel[0], + SkolemCache::SK_TCLOSURE_DOWN2, + "stc2"); Node mem_of_r = nm->mkNode(MEMBER, exp[0], tc_rel[0]); Node sk_eq = nm->mkNode(EQUAL, sk_1, sk_2); Node reason = exp; @@ -815,7 +821,7 @@ void TheorySetsRels::check(Theory::Effort level) Node r1_rep = getRepresentative(join_rel[0]); Node r2_rep = getRepresentative(join_rel[1]); TypeNode shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0]; - Node shared_x = d_state.getSkolemCache().mkTypedSkolemCached( + Node shared_x = d_skCache.mkTypedSkolemCached( shared_type, mem, join_rel, SkolemCache::SK_JOIN, "srj"); const DType& dt1 = join_rel[0].getType().getSetElementType().getDType(); unsigned int s1_len = join_rel[0].getType().getSetElementType().getTupleLength(); @@ -1185,7 +1191,7 @@ void TheorySetsRels::check(Theory::Effort level) Trace("rels-share") << " [sets-rels] making shared term " << n << std::endl; // force a proxy lemma to be sent for the singleton containing n Node ss = NodeManager::currentNM()->mkNode(SINGLETON, n); - d_state.getProxy(ss); + d_treg.getProxy(ss); d_shared_terms.insert(n); } diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index f48aaf9c5..2912e5e47 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -24,6 +24,7 @@ #include "theory/sets/inference_manager.h" #include "theory/sets/rels_utils.h" #include "theory/sets/solver_state.h" +#include "theory/sets/term_registry.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -65,7 +66,10 @@ class TheorySetsRels { typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; public: - TheorySetsRels(SolverState& s, InferenceManager& im); + TheorySetsRels(SolverState& s, + InferenceManager& im, + SkolemCache& skc, + TermRegistry& treg); ~TheorySetsRels(); /** @@ -87,6 +91,10 @@ private: SolverState& d_state; /** Reference to the inference manager for the theory of sets */ InferenceManager& d_im; + /** Reference to the skolem cache */ + SkolemCache& d_skCache; + /** Reference to the term registry */ + TermRegistry& d_treg; /** A list of pending inferences to process */ std::vector d_pending; NodeSet d_shared_terms; -- 2.30.2