1 files changed, 14 insertions, 0 deletions
diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h
index ef9a82b17..75b97fda9 100644
--- a/src/smt/env_obj.h
+++ b/src/smt/env_obj.h
@@ -55,6 +55,20 @@ class EnvObj
    * This is a wrapper around theory::Rewriter::extendedRewrite via Env.
    */
   Node extendedRewrite(TNode node, bool aggr = true) const;
+  /**
+   * Evaluate node n under the substitution args -> vals.
+   * This is a wrapper about theory::Rewriter::evaluate via Env.
+   */
+  Node evaluate(TNode n,
+                const std::vector<Node>& args,
+                const std::vector<Node>& vals,
+                bool useRewriter = true) const;
+  /** Same as above, with a visited cache. */
+  Node evaluate(TNode n,
+                const std::vector<Node>& args,
+                const std::vector<Node>& vals,
+                const std::unordered_map<Node, Node>& visited,
+                bool useRewriter = true) const;
 
   /** Get the current logic information. */
   const LogicInfo& logicInfo() const;