From e6747735d2074fc2651c5edc11fa8170fc13663e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 28 Jul 2021 16:00:49 -0500 Subject: [PATCH] Make extended rewriter methods const (#6948) --- src/theory/quantifiers/extended_rewrite.cpp | 53 +++++++++++--------- src/theory/quantifiers/extended_rewrite.h | 55 ++++++++++++--------- 2 files changed, 61 insertions(+), 47 deletions(-) diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index aa7e183bb..58a78b4aa 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -48,7 +48,7 @@ ExtendedRewriter::ExtendedRewriter(bool aggr) : d_aggr(aggr) d_false = NodeManager::currentNM()->mkConst(false); } -void ExtendedRewriter::setCache(Node n, Node ret) +void ExtendedRewriter::setCache(Node n, Node ret) const { if (d_aggr) { @@ -62,7 +62,7 @@ void ExtendedRewriter::setCache(Node n, Node ret) } } -Node ExtendedRewriter::getCache(Node n) +Node ExtendedRewriter::getCache(Node n) const { if (d_aggr) { @@ -83,7 +83,7 @@ Node ExtendedRewriter::getCache(Node n) bool ExtendedRewriter::addToChildren(Node nc, std::vector& children, - bool dropDup) + bool dropDup) const { // If the operator is non-additive, do not consider duplicates if (dropDup @@ -95,7 +95,7 @@ bool ExtendedRewriter::addToChildren(Node nc, return true; } -Node ExtendedRewriter::extendedRewrite(Node n) +Node ExtendedRewriter::extendedRewrite(Node n) const { n = Rewriter::rewrite(n); @@ -280,7 +280,7 @@ Node ExtendedRewriter::extendedRewrite(Node n) return ret; } -Node ExtendedRewriter::extendedRewriteAggr(Node n) +Node ExtendedRewriter::extendedRewriteAggr(Node n) const { Node new_ret; Trace("q-ext-rewrite-debug2") @@ -341,7 +341,7 @@ Node ExtendedRewriter::extendedRewriteAggr(Node n) return new_ret; } -Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) +Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) const { Assert(n.getKind() == itek); Assert(n[1] != n[2]); @@ -561,7 +561,7 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) return new_ret; } -Node ExtendedRewriter::extendedRewriteAndOr(Node n) +Node ExtendedRewriter::extendedRewriteAndOr(Node n) const { // all the below rewrites are aggressive if (!d_aggr) @@ -592,7 +592,7 @@ Node ExtendedRewriter::extendedRewriteAndOr(Node n) return new_ret; } -Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n) +Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n) const { Assert(n.getKind() != ITE); if (n.isClosure()) @@ -715,7 +715,7 @@ Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n) return Node::null(); } -Node ExtendedRewriter::extendedRewriteNnf(Node ret) +Node ExtendedRewriter::extendedRewriteNnf(Node ret) const { Assert(ret.getKind() == NOT); @@ -761,8 +761,11 @@ Node ExtendedRewriter::extendedRewriteNnf(Node ret) return NodeManager::currentNM()->mkNode(nk, new_children); } -Node ExtendedRewriter::extendedRewriteBcp( - Kind andk, Kind ork, Kind notk, std::map& bcp_kinds, Node ret) +Node ExtendedRewriter::extendedRewriteBcp(Kind andk, + Kind ork, + Kind notk, + std::map& bcp_kinds, + Node ret) const { Kind k = ret.getKind(); Assert(k == andk || k == ork); @@ -926,7 +929,7 @@ Node ExtendedRewriter::extendedRewriteBcp( Node ExtendedRewriter::extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, - Node n) + Node n) const { Trace("ext-rew-factoring") << "Factoring: *** INPUT: " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); @@ -1019,7 +1022,7 @@ Node ExtendedRewriter::extendedRewriteEqRes(Kind andk, Kind notk, std::map& bcp_kinds, Node n, - bool isXor) + bool isXor) const { Assert(n.getKind() == andk || n.getKind() == ork); Trace("ext-rew-eqres") << "Eq res: **** INPUT: " << n << std::endl; @@ -1166,7 +1169,7 @@ class SimpSubsumeTrie }; Node ExtendedRewriter::extendedRewriteEqChain( - Kind eqk, Kind andk, Kind ork, Kind notk, Node ret, bool isXor) + Kind eqk, Kind andk, Kind ork, Kind notk, Node ret, bool isXor) const { Assert(ret.getKind() == eqk); @@ -1527,9 +1530,10 @@ Node ExtendedRewriter::extendedRewriteEqChain( return Node::null(); } -Node ExtendedRewriter::partialSubstitute(Node n, - const std::map& assign, - const std::map& rkinds) +Node ExtendedRewriter::partialSubstitute( + Node n, + const std::map& assign, + const std::map& rkinds) const { std::unordered_map visited; std::unordered_map::iterator it; @@ -1601,10 +1605,11 @@ Node ExtendedRewriter::partialSubstitute(Node n, return visited[n]; } -Node ExtendedRewriter::partialSubstitute(Node n, - const std::vector& vars, - const std::vector& subs, - const std::map& rkinds) +Node ExtendedRewriter::partialSubstitute( + Node n, + const std::vector& vars, + const std::vector& subs, + const std::map& rkinds) const { Assert(vars.size() == subs.size()); std::map assign; @@ -1615,7 +1620,7 @@ Node ExtendedRewriter::partialSubstitute(Node n, return partialSubstitute(n, assign, rkinds); } -Node ExtendedRewriter::solveEquality(Node n) +Node ExtendedRewriter::solveEquality(Node n) const { // TODO (#1706) : implement Assert(n.getKind() == EQUAL); @@ -1626,7 +1631,7 @@ Node ExtendedRewriter::solveEquality(Node n) bool ExtendedRewriter::inferSubstitution(Node n, std::vector& vars, std::vector& subs, - bool usePred) + bool usePred) const { if (n.getKind() == AND) { @@ -1696,7 +1701,7 @@ bool ExtendedRewriter::inferSubstitution(Node n, return false; } -Node ExtendedRewriter::extendedRewriteStrings(Node ret) +Node ExtendedRewriter::extendedRewriteStrings(Node ret) const { Node new_ret; Trace("q-ext-rewrite-debug") diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 047318e86..8996fc441 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -51,7 +51,7 @@ class ExtendedRewriter ExtendedRewriter(bool aggr = true); ~ExtendedRewriter() {} /** return the extended rewritten form of n */ - Node extendedRewrite(Node n); + Node extendedRewrite(Node n) const; private: /** @@ -69,16 +69,16 @@ class ExtendedRewriter Node d_true; Node d_false; /** cache that the extended rewritten form of n is ret */ - void setCache(Node n, Node ret); + void setCache(Node n, Node ret) const; /** get the cache for n */ - Node getCache(Node n); + Node getCache(Node n) const; /** add to children * * Adds nc to the vector of children, if dropDup is true, we do not add * nc if it already occurs in children. This method returns false in this * case, otherwise it returns true. */ - bool addToChildren(Node nc, std::vector& children, bool dropDup); + bool addToChildren(Node nc, std::vector& children, bool dropDup) const; //--------------------------------------generic utilities /** Rewrite ITE, for example: @@ -92,13 +92,13 @@ class ExtendedRewriter * take. If full is false, then we do only perform rewrites that * strictly decrease the term size of n. */ - Node extendedRewriteIte(Kind itek, Node n, bool full = true); + Node extendedRewriteIte(Kind itek, Node n, bool full = true) const; /** Rewrite AND/OR * * This implements BCP, factoring, and equality resolution for the Boolean * term n whose top symbolic is AND/OR. */ - Node extendedRewriteAndOr(Node n); + Node extendedRewriteAndOr(Node n) const; /** Pull ITE, for example: * * D=C2 ---> false @@ -111,7 +111,7 @@ class ExtendedRewriter * * If this function returns a non-null node ret, then n ---> ret. */ - Node extendedRewritePullIte(Kind itek, Node n); + Node extendedRewritePullIte(Kind itek, Node n) const; /** Negation Normal Form (NNF), for example: * * ~( A & B ) ---> ( ~ A | ~B ) @@ -119,7 +119,7 @@ class ExtendedRewriter * * If this function returns a non-null node ret, then n ---> ret. */ - Node extendedRewriteNnf(Node n); + Node extendedRewriteNnf(Node n) const; /** (type-independent) Boolean constraint propagation, for example: * * ~A & ( B V A ) ---> ~A & B @@ -137,8 +137,11 @@ class ExtendedRewriter * * If this function returns a non-null node ret, then n ---> ret. */ - Node extendedRewriteBcp( - Kind andk, Kind ork, Kind notk, std::map& bcp_kinds, Node n); + Node extendedRewriteBcp(Kind andk, + Kind ork, + Kind notk, + std::map& bcp_kinds, + Node n) const; /** (type-independent) factoring, for example: * * ( A V B ) ^ ( A V C ) ----> A V ( B ^ C ) @@ -147,7 +150,7 @@ class ExtendedRewriter * This function takes as arguments the kinds that specify AND, OR, NOT. * We assume that the children of n do not contain duplicates. */ - Node extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, Node n); + Node extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, Node n) const; /** (type-independent) equality resolution, for example: * * ( A V C ) & ( A = B ) ---> ( B V C ) & ( A = B ) @@ -167,7 +170,7 @@ class ExtendedRewriter Kind notk, std::map& bcp_kinds, Node n, - bool isXor = false); + bool isXor = false) const; /** (type-independent) Equality chain rewriting, for example: * * A = ( A = B ) ---> B @@ -178,26 +181,32 @@ class ExtendedRewriter * This function takes as arguments the kinds that specify EQUAL, AND, OR, * and NOT. If the flag isXor is true, the eqk is treated as XOR. */ - Node extendedRewriteEqChain( - Kind eqk, Kind andk, Kind ork, Kind notk, Node n, bool isXor = false); + Node extendedRewriteEqChain(Kind eqk, + Kind andk, + Kind ork, + Kind notk, + Node n, + bool isXor = false) const; /** extended rewrite aggressive * * All aggressive rewriting techniques (those that should be prioritized * at a lower level) go in this function. */ - Node extendedRewriteAggr(Node n); + Node extendedRewriteAggr(Node n) const; /** Decompose right associative chain * * For term f( ... f( f( base, tn ), t{n-1} ) ... t1 ), returns term base, and * appends t1...tn to children. */ - Node decomposeRightAssocChain(Kind k, Node n, std::vector& children); + Node decomposeRightAssocChain(Kind k, + Node n, + std::vector& children) const; /** Make right associative chain * * Sorts children to obtain list { tn...t1 }, and returns the term * f( ... f( f( base, tn ), t{n-1} ) ... t1 ). */ - Node mkRightAssocChain(Kind k, Node base, std::vector& children); + Node mkRightAssocChain(Kind k, Node base, std::vector& children) const; /** Partial substitute * * Applies the substitution specified by assign to n, recursing only beneath @@ -206,18 +215,18 @@ class ExtendedRewriter */ Node partialSubstitute(Node n, const std::map& assign, - const std::map& rkinds); + const std::map& rkinds) const; /** same as above, with vectors */ Node partialSubstitute(Node n, const std::vector& vars, const std::vector& subs, - const std::map& rkinds); + const std::map& rkinds) const; /** solve equality * * If this function returns a non-null node n', then n' is equivalent to n * and is of the form that can be used by inferSubstitution below. */ - Node solveEquality(Node n); + Node solveEquality(Node n) const; /** infer substitution * * If n is an equality of the form x = t, where t is either: @@ -231,12 +240,12 @@ class ExtendedRewriter bool inferSubstitution(Node n, std::vector& vars, std::vector& subs, - bool usePred = false); + bool usePred = false) const; /** extended rewrite * * Prints debug information, indicating the rewrite n ---> ret was found. */ - inline void debugExtendedRewrite(Node n, Node ret, const char* c) const; + void debugExtendedRewrite(Node n, Node ret, const char* c) const; //--------------------------------------end generic utilities //--------------------------------------theory-specific top-level calls @@ -245,7 +254,7 @@ class ExtendedRewriter * If this method returns a non-null node ret', then ret is equivalent to * ret'. */ - Node extendedRewriteStrings(Node ret); + Node extendedRewriteStrings(Node ret) const; //--------------------------------------end theory-specific top-level calls }; -- 2.30.2