From: Andrew Reynolds Date: Mon, 1 Nov 2021 23:34:41 +0000 (-0500) Subject: Eliminate calls to Rewriter::rewrite and options:: in sets and bags (#7550) X-Git-Tag: cvc5-1.0.0~912 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8fee12bf84b4d056056baf90fd8a54c06a19637b;p=cvc5.git Eliminate calls to Rewriter::rewrite and options:: in sets and bags (#7550) There is 1 remaining call to Rewriter::rewrite in the bags type enumerator which is not straightforward to eliminate; it should perhaps call an intermediate call to a normal form utility instead of the full rewriter. --- 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& 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::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 > > d_skolemCache; /** the set of all skolems we have generated */ std::unordered_set 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& 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 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 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);