rewriter: Make rewriteEqualityExt non-static. (#7110)

More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 54d1779ec660563f7635759f38638d9d1f2265a3..bb0f9a413e68ae7038e71eff15e4c35abecefb00 100644 (file)
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -16,6 +16,7 @@
 #include "theory/builtin/proof_checker.h"
 
 #include "expr/skolem_manager.h"
+#include "smt/env.h"
 #include "smt/term_formula_removal.h"
 #include "theory/evaluator.h"
 #include "theory/rewriter.h"
@@ -28,6 +29,8 @@ namespace cvc5 {
 namespace theory {
 namespace builtin {
 
+BuiltinProofRuleChecker::BuiltinProofRuleChecker(Env& env) : d_env(env) {}
+
 void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
 {
   pc->registerChecker(PfRule::ASSUME, this);
@@ -81,7 +84,7 @@ Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
   }
   if (idr == MethodId::RW_REWRITE_EQ_EXT)
   {
-    return Rewriter::rewriteEqualityExt(n);
+    return d_env.getRewriter()->rewriteEqualityExt(n);
   }
   if (idr == MethodId::RW_EVALUATE)
   {

diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 1e671a7b3f86fd876cd4d6da467cf4749aa3f5a5..d7edd2c537b762eca2f0604b040792558a566a56 100644 (file)
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -25,6 +25,9 @@
 #include "theory/quantifiers/extended_rewrite.h"
 
 namespace cvc5 {
+
+class Env;
+
 namespace theory {
 namespace builtin {
 
@@ -32,7 +35,9 @@ namespace builtin {
 class BuiltinProofRuleChecker : public ProofRuleChecker
 {
  public:
-  BuiltinProofRuleChecker() {}
+  /** Constructor. */
+  BuiltinProofRuleChecker(Env& env);
+  /** Destructor. */
   ~BuiltinProofRuleChecker() {}
   /**
    * Apply rewrite on n (in skolem form). This encapsulates the exact behavior
@@ -121,6 +126,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
 
   /** extended rewriter object */
   quantifiers::ExtendedRewriter d_ext_rewriter;
+
+ private:
+  /** Reference to the environment. */
+  Env& d_env;
 };
 
 }  // namespace builtin

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 092bcc9ab5db95e825cd0986980abe10e42f7ec5..ff718bff38d5d4b7ba1139d62ef314812782a683 100644 (file)
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -27,6 +27,7 @@ namespace builtin {
 
 TheoryBuiltin::TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_BUILTIN, env, out, valuation),
+      d_checker(env),
       d_state(env, valuation),
       d_im(*this, d_state, d_pnm, "theory::builtin::")
 {

diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 8996fc44119979a67dd2170260ad24005e4e4905..b1b08657dac0b2c261be8237ed3cee7d6aba2690 100644 (file)
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -54,20 +54,6 @@ class ExtendedRewriter
   Node extendedRewrite(Node n) const;
 
  private:
-  /**
-   * Whether this extended rewriter applies aggressive rewriting techniques,
-   * which are more expensive. Examples of aggressive rewriting include:
-   * - conditional rewriting,
-   * - condition merging,
-   * - sorting childing of commutative operators with more than 5 children.
-   *
-   * Aggressive rewriting is applied for SyGuS, whereas non-aggressive rewriting
-   * may be applied as a preprocessing step.
-   */
-  bool d_aggr;
-  /** true/false nodes */
-  Node d_true;
-  Node d_false;
   /** cache that the extended rewritten form of n is ret */
   void setCache(Node n, Node ret) const;
   /** get the cache for n */
@@ -256,6 +242,21 @@ class ExtendedRewriter
    */
   Node extendedRewriteStrings(Node ret) const;
   //--------------------------------------end theory-specific top-level calls
+
+  /**
+   * Whether this extended rewriter applies aggressive rewriting techniques,
+   * which are more expensive. Examples of aggressive rewriting include:
+   * - conditional rewriting,
+   * - condition merging,
+   * - sorting childing of commutative operators with more than 5 children.
+   *
+   * Aggressive rewriting is applied for SyGuS, whereas non-aggressive rewriting
+   * may be applied as a preprocessing step.
+   */
+  bool d_aggr;
+  /** true/false nodes */
+  Node d_true;
+  Node d_false;
 };
 
 }  // namespace quantifiers

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index d02069fd8fd50264c93f3b4341a898a27e6c5dca..bcd0952652ba140d330e468f0d93f31e4193b5c6 100644 (file)
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -141,8 +141,7 @@ Node Rewriter::rewriteEqualityExt(TNode node)
 {
   Assert(node.getKind() == kind::EQUAL);
   // note we don't force caching of this method currently
-  return getInstance()->d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(
-      node);
+  return d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(node);
 }
 
 void Rewriter::registerTheoryRewriter(theory::TheoryId tid,

diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 9ee13d952054693d36deadc034a2f15a8987fb29..23a9914bd3711776f6070056b9f96508a3f314ec 100644 (file)
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -74,7 +74,7 @@ class Rewriter {
    * combination, which needs to guarantee that equalities between terms
    * can be communicated for all pairs of terms.
    */
-  static Node rewriteEqualityExt(TNode node);
+  Node rewriteEqualityExt(TNode node);
 
   /**
    * Rewrite with proof production, which is managed by the term conversion