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.
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
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)
{
// 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<Node, Node>::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);
+ proxy = d_treg.getProxy(univ);
d_univProxy[univ] = proxy;
}
else
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());
}
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)
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();
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;
}
}
std::vector<Node>& 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++)
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))
// 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());
{
// 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
#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"
* 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
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
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);
{
if (nk == SINGLETON)
{
- // singleton lemma
- getProxy(n);
Node re = d_ee->getRepresentative(n[0]);
if (d_singleton_index.find(re) == d_singleton_index.end())
{
Node SolverState::getUnivSetEqClass(TypeNode tn) const
{
- std::map<TypeNode, Node>::const_iterator it = d_univset.find(tn);
- if (it != d_univset.end())
+ std::map<TypeNode, Node>::const_iterator it = d_eqc_univset.find(tn);
+ if (it != d_eqc_univset.end())
{
return it->second;
}
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));
{
return d_congruent.find(n) != d_congruent.end();
}
-
-Node SolverState::getEmptySet(TypeNode tn)
-{
- std::map<TypeNode, Node>::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<TypeNode, Node>::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<TypeNode, Node>::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<Node>& SolverState::getNonVariableSets(Node r) const
{
std::map<Node, std::vector<Node> >::const_iterator it = d_nvar_sets.find(r);
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<Node> SolverState::getSetsEqClasses(const TypeNode& t) const
{
vector<Node> representatives;
#include <map>
#include <vector>
-#include "context/cdhashset.h"
#include "theory/sets/skolem_cache.h"
#include "theory/theory_state.h"
#include "theory/uf/equality_engine.h"
/** 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 )*
*/
class SolverState : public TheoryState
{
- typedef context::CDHashMap<Node, Node, NodeHashFunction> 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
/** Get the list of all comprehension sets in the current context */
const std::vector<Node>& 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;
/** the empty vector and map */
std::vector<Node> d_emptyVec;
std::map<Node, Node> 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 */
* to their negative memberships.
*/
std::map<Node, std::map<Node, Node> > 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<Node, std::map<TypeNode, Node> > d_tc_skolem;
- /** Map from types to empty set of that type */
- std::map<TypeNode, Node> d_emptyset;
- /** Map from types to universe set of that type */
- std::map<TypeNode, Node> d_univset;
- // --------------------------------------- end commonly used terms
// -------------------------------- term indices
/** Term index for MEMBER
*
std::vector<Node> d_allCompSets;
// -------------------------------- end term indices
std::map<Kind, std::vector<Node> > 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
--- /dev/null
+/********************* */
+/*! \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<TypeNode, Node>::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<TypeNode, Node>::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<TypeNode, Node>::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
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <vector>
+
+#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<Node, Node, NodeHashFunction> 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<Node, std::map<TypeNode, Node> > d_tc_skolem;
+ /** Map from types to empty set of that type */
+ std::map<TypeNode, Node> d_emptyset;
+ /** Map from types to universe set of that type */
+ std::map<TypeNode, Node> d_univset;
+}; /* class TheorySetsPrivate */
+
+} // namespace sets
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__SETS__TERM_REGISTRY_H */
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
#include <memory>
#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"
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 */
TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
SolverState& state,
- InferenceManager& im)
+ InferenceManager& im,
+ SkolemCache& skc)
: d_members(state.getSatContext()),
d_deq(state.getSatContext()),
d_termProcessed(state.getUserContext()),
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)
{
}
// 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")
// 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;
}
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);
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(
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())
std::vector<Node> 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())
// equivalence class
if (s != ueqc)
{
- u = d_state.getUnivSet(tn);
+ u = d_treg.getUnivSet(tn);
}
univ_set[tn] = u;
}
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]);
#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"
*/
TheorySetsPrivate(TheorySets& external,
SolverState& state,
- InferenceManager& im);
+ InferenceManager& im,
+ SkolemCache& skc);
~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;
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);
}
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;
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();
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);
}
#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"
typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
public:
- TheorySetsRels(SolverState& s, InferenceManager& im);
+ TheorySetsRels(SolverState& s,
+ InferenceManager& im,
+ SkolemCache& skc,
+ TermRegistry& treg);
~TheorySetsRels();
/**
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<Node> d_pending;
NodeSet d_shared_terms;
projects / cvc5.git / commitdiff