Move expand definition from Theory to TheoryRewriter (#6408)

This is work towards eliminating global calls to getCurrentSmtEngine()->expandDefinition.

The next step will be to add Rewriter::expandDefinition.

1 files changed, 24 insertions, 0 deletions

diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h
index 2477de51e..031e32db4 100644
--- a/src/theory/theory_rewriter.h
+++ b/src/theory/theory_rewriter.h
@@ -138,6 +138,30 @@ class TheoryRewriter
    * node if no rewrites are applied.
    */
   virtual TrustNode rewriteEqualityExtWithProof(Node node);
+
+  /**
+   * Expand definitions in the term node. This returns a term that is
+   * equivalent to node. It wraps this term in a TrustNode of kind
+   * TrustNodeKind::REWRITE. If node is unchanged by this method, the
+   * null TrustNode may be returned. This is an optimization to avoid
+   * constructing the trivial equality (= node node) internally within
+   * TrustNode.
+   *
+   * The purpose of this method is typically to eliminate the operators in node
+   * that are syntax sugar that cannot otherwise be eliminated during rewriting.
+   * For example, division relies on the introduction of an uninterpreted
+   * function for the divide-by-zero case, which we do not introduce with
+   * the standard rewrite methods.
+   *
+   * Some theories have kinds that are effectively definitions and should be
+   * expanded before they are handled.  Definitions allow a much wider range of
+   * actions than the normal forms given by the rewriter. However no
+   * assumptions can be made about subterms having been expanded or rewritten.
+   * Where possible rewrite rules should be used, definitions should only be
+   * used when rewrites are not possible, for example in handling
+   * under-specified operations using partially defined functions.
+   */
+  virtual TrustNode expandDefinition(Node node);
 };
 
 }  // namespace theory