summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/bags/theory_bags.cpp2
-rw-r--r--src/theory/sets/cardinality_extension.cpp17
-rw-r--r--src/theory/sets/inference_manager.cpp4
-rw-r--r--src/theory/sets/skolem_cache.cpp10
-rw-r--r--src/theory/sets/skolem_cache.h7
-rw-r--r--src/theory/sets/solver_state.cpp2
-rw-r--r--src/theory/sets/theory_sets.cpp8
-rw-r--r--src/theory/sets/theory_sets_private.cpp14
8 files changed, 35 insertions, 29 deletions
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 4823c16e2..9db6149ef 100644
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -185,7 +185,7 @@ bool TheoryBags::collectModelValues(TheoryModel* m,
elementReps[key] = value;
}
Node rep = NormalForm::constructBagFromElements(tn, elementReps);
- rep = Rewriter::rewrite(rep);
+ rep = rewrite(rep);
Trace("bags-model") << "rep of " << n << " is: " << rep << std::endl;
m->assertEquality(rep, n, true);
m->assertSkeleton(rep);
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 4e4ee78a8..d2d7a636a 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -162,7 +162,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& 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);
+ subset = rewrite(subset);
if (!d_state.isEntailed(subset, true))
{
d_im.assertInference(
@@ -242,7 +242,7 @@ void CardinalityExtension::checkRegister()
// if setminus, do for intersection instead
if (n.getKind() == SETMINUS)
{
- n = Rewriter::rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
+ n = rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
}
registerCardinalityTerm(n);
}
@@ -293,7 +293,7 @@ void CardinalityExtension::registerCardinalityTerm(Node n)
if (nn != nk)
{
Node lem = nm->mkNode(EQUAL, nm->mkNode(CARD, nk), nm->mkNode(CARD, nn));
- lem = Rewriter::rewrite(lem);
+ lem = rewrite(lem);
Trace("sets-card") << " " << k << " : " << lem << std::endl;
d_im.assertInference(lem, InferenceId::SETS_CARD_EQUAL, d_emp_exp, 1);
}
@@ -393,21 +393,21 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
d_localBase[n] = n;
for (unsigned e = 0; e < 2; e++)
{
- Node sm = Rewriter::rewrite(nm->mkNode(SETMINUS, n[e], n[1 - e]));
+ Node sm = rewrite(nm->mkNode(SETMINUS, n[e], n[1 - e]));
sib.push_back(sm);
}
true_sib = 2;
}
else
{
- Node si = Rewriter::rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
+ Node si = rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
sib.push_back(si);
d_localBase[n] = si;
- Node osm = Rewriter::rewrite(nm->mkNode(SETMINUS, n[1], n[0]));
+ Node osm = rewrite(nm->mkNode(SETMINUS, n[1], n[0]));
sib.push_back(osm);
true_sib = 1;
}
- Node u = Rewriter::rewrite(nm->mkNode(UNION, n[0], n[1]));
+ Node u = rewrite(nm->mkNode(UNION, n[0], n[1]));
if (!d_state.hasTerm(u))
{
u = Node::null();
@@ -837,8 +837,7 @@ void CardinalityExtension::checkNormalForm(Node eqc,
Assert(o0 != o1);
Node kca = d_treg.getProxy(o0);
Node kcb = d_treg.getProxy(o1);
- Node intro =
- Rewriter::rewrite(nm->mkNode(INTERSECTION, kca, kcb));
+ Node intro = rewrite(nm->mkNode(INTERSECTION, kca, kcb));
Trace("sets-nf") << " Intro split : " << o0 << " against " << o1
<< ", term is " << intro << std::endl;
intro_sets.push_back(intro);
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 15c4fd405..96705c029 100644
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -35,7 +35,7 @@ InferenceManager::InferenceManager(Env& env, Theory& t, SolverState& s)
bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int inferType)
{
// should we send this fact out as a lemma?
- if ((options::setsInferAsLemmas() && inferType != -1) || inferType == 1)
+ if ((options().sets.setsInferAsLemmas && inferType != -1) || inferType == 1)
{
if (d_state.isEntailed(fact, true))
{
@@ -172,7 +172,7 @@ void InferenceManager::assertInference(std::vector<Node>& conc,
void InferenceManager::split(Node n, InferenceId id, int reqPol)
{
- n = Rewriter::rewrite(n);
+ n = rewrite(n);
Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate());
// send the lemma
lemma(lem, id);
diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp
index f759c2a7b..646ae1662 100644
--- a/src/theory/sets/skolem_cache.cpp
+++ b/src/theory/sets/skolem_cache.cpp
@@ -24,14 +24,16 @@ namespace cvc5 {
namespace theory {
namespace sets {
-SkolemCache::SkolemCache() {}
+SkolemCache::SkolemCache(Rewriter* rr) : d_rewriter(rr) {}
Node SkolemCache::mkTypedSkolemCached(
TypeNode tn, Node a, Node b, SkolemId id, const char* c)
{
- a = a.isNull() ? a : Rewriter::rewrite(a);
- b = b.isNull() ? b : Rewriter::rewrite(b);
-
+ if (d_rewriter != nullptr)
+ {
+ a = a.isNull() ? a : d_rewriter->rewrite(a);
+ b = b.isNull() ? b : d_rewriter->rewrite(b);
+ }
std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
if (it == d_skolemCache[a][b].end())
{
diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h
index 62547a66e..a13c48f1e 100644
--- a/src/theory/sets/skolem_cache.h
+++ b/src/theory/sets/skolem_cache.h
@@ -25,6 +25,9 @@
namespace cvc5 {
namespace theory {
+
+class Rewriter;
+
namespace sets {
/**
@@ -35,7 +38,7 @@ namespace sets {
class SkolemCache
{
public:
- SkolemCache();
+ SkolemCache(Rewriter* rr);
/** Identifiers for skolem types
*
* The comments below document the properties of each skolem introduced by
@@ -75,6 +78,8 @@ class SkolemCache
std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
/** the set of all skolems we have generated */
std::unordered_set<Node> d_allSkolems;
+ /** the optional rewriter */
+ Rewriter* d_rewriter;
};
} // namespace sets
diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index 6f8976f4d..d9fb30735 100644
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -113,7 +113,7 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
}
else if (nk == UNIVERSE_SET)
{
- Assert(options::setsExt());
+ Assert(options().sets.setsExt);
d_eqc_univset[tnn] = r;
}
else
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 2901703dd..3cb6c853c 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -29,7 +29,7 @@ namespace sets {
TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation)
: Theory(THEORY_SETS, env, out, valuation),
- d_skCache(),
+ d_skCache(env.getRewriter()),
d_state(env, valuation, d_skCache),
d_im(env, *this, d_state),
d_internal(
@@ -136,7 +136,7 @@ TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
|| nk == COMPREHENSION)
{
- if (!options::setsExt())
+ if (!options().sets.setsExt)
{
std::stringstream ss;
ss << "Extended set operators are not supported in default mode, try "
@@ -173,7 +173,7 @@ Theory::PPAssertStatus TheorySets::ppAssert(
// may appear when this option is enabled, and solving for such a set
// impacts the semantics of universe set, see
// regress0/sets/pre-proc-univ.smt2
- if (!in[0].getType().isSet() || !options::setsExt())
+ if (!in[0].getType().isSet() || !options().sets.setsExt)
{
outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
status = Theory::PP_ASSERT_STATUS_SOLVED;
@@ -181,7 +181,7 @@ Theory::PPAssertStatus TheorySets::ppAssert(
}
else if (in[1].isVar() && isLegalElimination(in[1], in[0]))
{
- if (!in[0].getType().isSet() || !options::setsExt())
+ if (!in[0].getType().isSet() || !options().sets.setsExt)
{
outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
status = Theory::PP_ASSERT_STATUS_SOLVED;
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 2164c26b0..324d6b7dc 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -454,11 +454,11 @@ void TheorySetsPrivate::checkDownwardsClosure()
{
Trace("sets-debug") << "Downwards closure based on " << mem
<< ", eq_set = " << eq_set << std::endl;
- if (!options::setsProxyLemmas())
+ if (!options().sets.setsProxyLemmas)
{
Node nmem = NodeManager::currentNM()->mkNode(
kind::MEMBER, mem[0], eq_set);
- nmem = Rewriter::rewrite(nmem);
+ nmem = rewrite(nmem);
std::vector<Node> exp;
exp.push_back(mem);
exp.push_back(mem[1].eqNode(eq_set));
@@ -476,7 +476,7 @@ void TheorySetsPrivate::checkDownwardsClosure()
NodeManager::currentNM()->mkNode(kind::MEMBER, mem[0], k);
Node nmem = NodeManager::currentNM()->mkNode(
kind::MEMBER, mem[0], eq_set);
- nmem = Rewriter::rewrite(nmem);
+ nmem = rewrite(nmem);
std::vector<Node> exp;
if (d_state.areEqual(mem, pmem))
{
@@ -635,7 +635,7 @@ void TheorySetsPrivate::checkUpwardsClosure()
}
if (!d_im.hasSent())
{
- if (options::setsExt())
+ if (options().sets.setsExt)
{
// universal sets
Trace("sets-debug") << "Check universe sets..." << std::endl;
@@ -737,7 +737,7 @@ void TheorySetsPrivate::checkDisequalities()
Node mem1 = nm->mkNode(MEMBER, x, deq[0]);
Node mem2 = nm->mkNode(MEMBER, x, deq[1]);
Node lem = nm->mkNode(OR, deq, nm->mkNode(EQUAL, mem1, mem2).negate());
- lem = Rewriter::rewrite(lem);
+ lem = rewrite(lem);
d_im.assertInference(lem, InferenceId::SETS_DEQ, d_true, 1);
d_im.doPendingLemmas();
if (d_im.hasSent())
@@ -1152,7 +1152,7 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
}
Node rep = NormalForm::mkBop(kind::UNION, els, eqc.getType());
- rep = Rewriter::rewrite(rep);
+ rep = rewrite(rep);
Trace("sets-model") << "* Assign representative of " << eqc << " to "
<< rep << std::endl;
mvals[eqc] = rep;
@@ -1361,7 +1361,7 @@ TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node)
// we call the rewriter here to handle the pattern
// (is_singleton (singleton x)) because the rewriter is called after expansion
- Node rewritten = Rewriter::rewrite(node);
+ Node rewritten = rewrite(node);
if (rewritten.getKind() != IS_SINGLETON)
{
return TrustNode::mkTrustRewrite(node, rewritten, nullptr);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback