1 files changed, 15 insertions, 0 deletions
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 0c60ec5ea..d46b9aab1 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -24,6 +24,7 @@
 #define __CVC4__THEORY__VALUATION_H
 
 #include "expr/node.h"
+#include "theory/substitutions.h"
 
 namespace CVC4 {
 
@@ -50,6 +51,20 @@ public:
    */
   Node getSatValue(TNode n) const;
 
+  /**
+   * Simplify a node.  Intended to be used by a theory's simplify()
+   * function to simplify subterms (TheoryEngine will cache the
+   * results and make sure that the request is directed to the correct
+   * theory).
+   */
+  Node simplify(TNode in, Substitutions& outSubstitutions);
+
+  /**
+   * Rewrite a node.  Intended to be used by a theory to have the
+   * TheoryEngine fully rewrite a node.
+   */
+  Node rewrite(TNode in);
+
 };/* class Valuation */
 
 }/* CVC4::theory namespace */