(proof-new) Make static methods in re-elim (#4623)

In preparation for coarse-grained rule for re-elim to be used by the solver and proof checker.

1 files changed, 4 insertions, 10 deletions

diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h
index a2e300993..e5f2fa854 100644
--- a/src/theory/strings/regexp_elim.h
+++ b/src/theory/strings/regexp_elim.h
@@ -40,25 +40,19 @@ class RegExpElimination
    * form (str.in.re x R). If this method returns a non-null node ret, then ret
    * is equivalent to atom.
    */
-  Node eliminate(Node atom);
+  static Node eliminate(Node atom);
 
  private:
-  /** common terms */
-  Node d_zero;
-  Node d_one;
-  Node d_neg_one;
-  /** The type of regular expressions */
-  TypeNode d_regExpType;
   /** return elimination
    *
    * This method is called when atom is rewritten to atomElim, and returns
    * atomElim. id is an identifier indicating the reason for the elimination.
    */
-  Node returnElim(Node atom, Node atomElim, const char* id);
+  static Node returnElim(Node atom, Node atomElim, const char* id);
   /** elimination for regular expression concatenation */
-  Node eliminateConcat(Node atom);
+  static Node eliminateConcat(Node atom);
   /** elimination for regular expression star */
-  Node eliminateStar(Node atom);
+  static Node eliminateStar(Node atom);
 }; /* class RegExpElimination */
 
 }  // namespace strings