From b7de813c6386a5625c5570c99d8daf0b00e245f8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 27 Jul 2016 15:35:44 -0700
Subject: [PATCH] set solver on simplify command

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.h  |  3 +++
 src/ast/rewriter/th_rewriter.cpp |  9 +++++++++
 src/ast/rewriter/th_rewriter.h   |  5 +++++
 src/cmd_context/simplify_cmd.cpp | 25 ++++++++++++++++++++++++-
 src/solver/solver.h              |  9 +++++++--
 5 files changed, 48 insertions(+), 3 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 82579d53a..2b434f475 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -149,6 +149,9 @@ public:
     void updt_params(params_ref const & p) {}
     static void get_param_descrs(param_descrs & r) {}
 
+    void set_solver(expr_solver* solver) { m_re2aut.set_solver(solver); }
+
+
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
 
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 6f6daf8df..ff6a10274 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -692,6 +692,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         return false;
     }
 
+
 };
 
 template class rewriter_tpl<th_rewriter_cfg>;
@@ -705,6 +706,10 @@ struct th_rewriter::imp : public rewriter_tpl<th_rewriter_cfg> {
     expr_ref mk_app(func_decl* f, unsigned sz, expr* const* args) {
         return m_cfg.mk_app(f, sz, args);
     }
+
+    void set_solver(expr_solver* solver) {
+        m_cfg.m_seq_rw.set_solver(solver);
+    }
 };
 
 th_rewriter::th_rewriter(ast_manager & m, params_ref const & p):
@@ -790,3 +795,7 @@ void th_rewriter::reset_used_dependencies() {
 expr_ref th_rewriter::mk_app(func_decl* f, unsigned num_args, expr* const* args) {
     return m_imp->mk_app(f, num_args, args);
 }
+
+void th_rewriter::set_solver(expr_solver* solver) {
+    m_imp->set_solver(solver);
+}
diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h
index bd5ce9c66..6aa4bb3da 100644
--- a/src/ast/rewriter/th_rewriter.h
+++ b/src/ast/rewriter/th_rewriter.h
@@ -25,6 +25,8 @@ Notes:
 
 class expr_substitution;
 
+class expr_solver;
+
 class th_rewriter {
     struct     imp;
     imp *      m_imp;
@@ -58,6 +60,9 @@ public:
     // Remark: reset_used_dependecies will reset the internal cache if get_used_dependencies() != 0
     expr_dependency * get_used_dependencies();
     void reset_used_dependencies();
+
+    void set_solver(expr_solver* solver);
+
 };
 
 #endif
diff --git a/src/cmd_context/simplify_cmd.cpp b/src/cmd_context/simplify_cmd.cpp
index 1c249ce1f..8b354c8b7 100644
--- a/src/cmd_context/simplify_cmd.cpp
+++ b/src/cmd_context/simplify_cmd.cpp
@@ -24,9 +24,30 @@ Notes:
 #include"scoped_timer.h"
 #include"scoped_ctrl_c.h"
 #include"cancel_eh.h"
+#include"seq_rewriter.h"
 #include<iomanip>
 
 class simplify_cmd : public parametric_cmd {
+
+    class th_solver : public expr_solver {
+        cmd_context& m_ctx;
+        params_ref   m_params;
+        ref<solver> m_solver;
+    public:
+        th_solver(cmd_context& ctx): m_ctx(ctx) {}
+        
+        virtual lbool check_sat(expr* e) {
+            if (!m_solver) {
+                m_solver = m_ctx.get_solver_factory()(m_ctx.m(), m_params, false, true, false, symbol::null);
+            }
+            m_solver->push();
+            m_solver->assert_expr(e);
+            lbool r = m_solver->check_sat(0,0);
+            m_solver->pop(1);
+            return r;
+        }
+    };
+
     expr *                   m_target;
 public:
     simplify_cmd(char const * name = "simplify"):parametric_cmd(name) {}
@@ -70,10 +91,12 @@ public:
         if (m_params.get_bool("som", false))
             m_params.set_bool("flat", true);
         th_rewriter s(ctx.m(), m_params);
+        th_solver solver(ctx);
+        s.set_solver(alloc(th_solver, ctx));
         unsigned cache_sz;
         unsigned num_steps = 0;
         unsigned timeout   = m_params.get_uint("timeout", UINT_MAX);
-        unsigned rlimit    = m_params.get_uint("rlimit", UINT_MAX);
+        unsigned rlimit    = m_params.get_uint("rlimit", UINT_MAX);        
         bool failed = false;
         cancel_eh<reslimit> eh(ctx.m().limit());
         { 
diff --git a/src/solver/solver.h b/src/solver/solver.h
index f320bec7c..e4e4942d3 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -149,8 +149,13 @@ public:
     */
     virtual expr * get_assumption(unsigned idx) const = 0;
 
-
-
+    /**
+    \brief under assumptions, asms, retrieve set of consequences that fix values for expressions that can be 
+      built from fns. For functions that take 0 arguments, we require that the function returns all consequences
+      that mention these functions. The consequences are clauses whose first literal constrain one of the 
+      functions from fns and the other literals are negations of literals from asms.
+     */
+    //virtual lbool get_consequences(expr_ref_vector const& asms, func_ref_vector const& fns, expr_ref_vector& consequences);
 
     /**
        \brief Display the content of this solver.