From 491b3b34aa25ee5c48fdf86db4f4256e39600de3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 3 Aug 2016 11:14:29 -0700
Subject: [PATCH] tune consequence finding. Factor solver pretty-printing as
 SMT-LIB into top-level

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.h                 |  4 +-
 src/opt/opt_solver.h                  |  2 +-
 src/sat/sat_solver/inc_sat_solver.cpp |  2 +-
 src/smt/smt_conflict_resolution.cpp   | 15 +++++
 src/smt/smt_conflict_resolution.h     |  3 +
 src/smt/smt_consequences.cpp          | 91 ++++++++++++++++++++++++---
 src/smt/smt_context.cpp               |  1 -
 src/smt/smt_context.h                 |  6 +-
 src/smt/smt_kernel.cpp                | 32 +++++-----
 src/smt/smt_kernel.h                  |  3 +-
 src/smt/smt_solver.cpp                | 16 ++---
 src/solver/check_sat_result.h         |  4 +-
 src/solver/combined_solver.cpp        |  2 +-
 src/solver/solver.cpp                 | 15 ++++-
 src/solver/tactic2solver.cpp          | 22 +------
 15 files changed, 149 insertions(+), 69 deletions(-)

diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 07fe53268..ac1fe8e7a 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -48,7 +48,7 @@ namespace opt {
         virtual filter_model_converter& fm() = 0;   // converter that removes fresh names introduced by simplification.
         virtual bool sat_enabled() const = 0;       // is using th SAT solver core enabled?
         virtual solver& get_solver() = 0;           // retrieve solver object (SAT or SMT solver)
-        virtual ast_manager& get_manager() = 0;      
+        virtual ast_manager& get_manager() const = 0;      
         virtual params_ref& params() = 0;
         virtual void enable_sls(bool force) = 0;              // stochastic local search 
         virtual symbol const& maxsat_engine() const = 0; // retrieve maxsat engine configuration parameter.
@@ -217,7 +217,7 @@ namespace opt {
         virtual filter_model_converter& fm() { return m_fm; }
         virtual bool sat_enabled() const { return 0 != m_sat_solver.get(); }
         virtual solver& get_solver();
-        virtual ast_manager& get_manager() { return this->m; }
+        virtual ast_manager& get_manager() const { return this->m; }
         virtual params_ref& params() { return m_params; }
         virtual void enable_sls(bool force);
         virtual symbol const& maxsat_engine() const { return m_maxsat_engine; }
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index e5ee5afcf..b2fa18ad8 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -105,7 +105,7 @@ namespace opt {
         virtual unsigned get_num_assertions() const;
         virtual expr * get_assertion(unsigned idx) const;
         virtual std::ostream& display(std::ostream & out) const;
-        virtual ast_manager& get_manager() { return m; } 
+        virtual ast_manager& get_manager() const { return m; } 
         void set_logic(symbol const& logic);
 
         smt::theory_var add_objective(app* term);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index badb0a67a..ce6b199d6 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -196,7 +196,7 @@ public:
             assert_expr(t);
         }
     }
-    virtual ast_manager& get_manager() { return m; }
+    virtual ast_manager& get_manager() const { return m; }
     virtual void assert_expr(expr * t) {
         TRACE("sat", tout << mk_pp(t, m) << "\n";);
         m_fmls.push_back(t);
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 6c7c71602..6907d6f37 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -187,6 +187,10 @@ namespace smt {
         SASSERT(m_todo_js_qhead <= m_todo_js.size());
         m_antecedents = &result;
         mark_justification(js);
+        process_justifications();
+    }
+
+    void conflict_resolution::process_justifications() {
         while (true) {
             unsigned sz = m_todo_js.size();
             while (m_todo_js_qhead < sz) {
@@ -234,6 +238,17 @@ namespace smt {
         SASSERT(m_todo_eqs.empty());
     }
 
+    void conflict_resolution::eq2literals(enode* n1, enode* n2, literal_vector & result) {
+        SASSERT(m_todo_js.empty());
+        SASSERT(m_todo_js_qhead == 0);
+        SASSERT(m_todo_eqs.empty());
+        m_antecedents = &result;
+        m_todo_eqs.push_back(enode_pair(n1, n2));
+        process_justifications();
+        unmark_justifications(0);
+        SASSERT(m_todo_eqs.empty());
+    }
+
     /**
        \brief Return maximum scope level of an antecedent literal of js.
     */
diff --git a/src/smt/smt_conflict_resolution.h b/src/smt/smt_conflict_resolution.h
index daccadbb7..fad3ab50d 100644
--- a/src/smt/smt_conflict_resolution.h
+++ b/src/smt/smt_conflict_resolution.h
@@ -168,6 +168,7 @@ namespace smt {
         void eq_branch2literals(enode * n1, enode * n2);
         void eq2literals(enode * n1, enode * n2);
         void justification2literals_core(justification * js, literal_vector & result) ;
+        void process_justifications();
         void unmark_justifications(unsigned old_js_qhead);
 
         literal_vector m_tmp_literal_vector;
@@ -257,6 +258,8 @@ namespace smt {
 
         void justification2literals(justification * js, literal_vector & result);
 
+        void eq2literals(enode * n1, enode * n2, literal_vector & result);
+
     };
 
     inline void mark_literals(conflict_resolution & cr, unsigned sz, literal const * ls) {
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index 49236be1b..1ae9f28e7 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -102,7 +102,7 @@ namespace smt {
         }
     }
 
-    void context::delete_unfixed(obj_map<expr, expr*>& var2val) {
+    unsigned context::delete_unfixed(obj_map<expr, expr*>& var2val, expr_ref_vector& unfixed) {
         ast_manager& m = m_manager;
         ptr_vector<expr> to_delete;
         obj_map<expr,expr*>::iterator it = var2val.begin(), end = var2val.end();
@@ -137,14 +137,59 @@ namespace smt {
                 to_delete.push_back(k);
             }
         }
-        IF_VERBOSE(1, verbose_stream() << "(get-consequences deleting: " << to_delete.size() << " num-values: " << var2val.size() << ")\n";);
+        for (unsigned i = 0; i < to_delete.size(); ++i) {
+            var2val.remove(to_delete[i]);
+            unfixed.push_back(to_delete[i]);
+        }
+        return to_delete.size();
+    }
+
+    //
+    // Extract equalities that are congruent at the search level.
+    // 
+    unsigned context::extract_fixed_eqs(obj_map<expr, expr*>& var2val, expr_ref_vector& conseq) {
+        ast_manager& m = m_manager;
+        ptr_vector<expr> to_delete;
+        expr_ref fml(m), eq(m);
+        obj_map<expr,expr*>::iterator it = var2val.begin(), end = var2val.end();
+        for (; it != end; ++it) {
+            expr* k = it->m_key;
+            expr* v = it->m_value;
+            if (!m.is_bool(k) && e_internalized(k) && e_internalized(v) && 
+                get_enode(k)->get_root() == get_enode(v)->get_root()) {
+                literal_vector literals;
+                m_conflict_resolution->eq2literals(get_enode(v), get_enode(k), literals);
+                uint_set s;
+                for (unsigned i = 0; i < literals.size(); ++i) {
+                    SASSERT(get_assign_level(literals[i]) <= get_search_level());
+                    s |= m_antecedents.find(literals[i].var());
+                }
+                
+                fml = m.mk_eq(k, v);
+                fml = m.mk_implies(antecedent2fml(s), fml);
+                conseq.push_back(fml);
+                to_delete.push_back(k);
+
+                for (unsigned i = 0; i < literals.size(); ++i) {
+                    literals[i].neg();
+                }
+                eq = mk_eq_atom(k, v);
+                internalize_formula(eq, false);
+                literal lit(get_bool_var(eq), true);
+                literals.push_back(lit);
+                mk_clause(literals.size(), literals.c_ptr(), 0);
+            }
+        }    
         for (unsigned i = 0; i < to_delete.size(); ++i) {
             var2val.remove(to_delete[i]);
         }
+        return to_delete.size();
     }
 
     lbool context::get_consequences(expr_ref_vector const& assumptions, 
-                                    expr_ref_vector const& vars, expr_ref_vector& conseq) {
+                                    expr_ref_vector const& vars, 
+                                    expr_ref_vector& conseq, 
+                                    expr_ref_vector& unfixed) {
 
         m_antecedents.reset();
         lbool is_sat = check(assumptions.size(), assumptions.c_ptr());
@@ -168,6 +213,9 @@ namespace smt {
                 trail.push_back(val);
                 var2val.insert(vars[i], val);
             } 
+            else {
+                unfixed.push_back(vars[i]);
+            }
         }
         extract_fixed_consequences(0, var2val, _assumptions, conseq);
         unsigned num_units = assigned_literals().size();
@@ -178,8 +226,10 @@ namespace smt {
         m_case_split_queue->init_search_eh();
         unsigned num_iterations = 0;
         unsigned model_threshold = 2;
+        unsigned num_unfixed = 0;
+        unsigned num_fixed_eqs = 0;
+        unsigned num_reiterations = 0;
         while (!var2val.empty()) {
-            ++num_iterations;
             obj_map<expr,expr*>::iterator it = var2val.begin();
             expr* e = it->m_key;
             expr* val = it->m_value;
@@ -212,28 +262,50 @@ namespace smt {
             }
             if (get_assignment(lit) == l_true) {
                 var2val.erase(e);
+                unfixed.push_back(e);
             }
             else if (get_assign_level(lit) > get_search_level()) {
                 TRACE("context", tout << "Retry fixing: " << mk_pp(e, m) << "\n";);
                 pop_to_search_lvl();
+                ++num_reiterations;
                 continue;
             }
             else {
                 TRACE("context", tout << "Fixed: " << mk_pp(e, m) << "\n";);
             }
+            ++num_iterations;
 
-            TRACE("context", tout << "Unfixed variables: " << var2val.size() << "\n";);
-            if (model_threshold <= num_iterations) {
-                delete_unfixed(var2val);
+            bool apply_slow_pass = model_threshold <= num_iterations || num_iterations <= 2;
+            if (apply_slow_pass) {
+                num_unfixed += delete_unfixed(var2val, unfixed);
                 // The next time we check the model is after 1.5 additional iterations.
                 model_threshold *= 3;
-                model_threshold /= 2;                
+                model_threshold /= 2;                                
             }
             // repeat until we either have a model with negated literal or 
             // the literal is implied at base.
 
             extract_fixed_consequences(num_units, var2val, _assumptions, conseq);
             num_units = assigned_literals().size();
+            if (apply_slow_pass) {
+                num_fixed_eqs += extract_fixed_eqs(var2val, conseq);
+                IF_VERBOSE(1, verbose_stream() << "(get-consequences"
+                           << " iterations: " << num_iterations 
+                           << " variables: " << var2val.size() 
+                           << " fixed: " << conseq.size() 
+                           << " unfixed: " << unfixed.size() 
+                           << " fixed-eqs: " << num_fixed_eqs
+                           << " unfixed-deleted: " << num_unfixed
+                           << ")\n";);        
+                TRACE("context", tout << "(get-consequences"
+                      << " iterations: " << num_iterations 
+                      << " variables: " << var2val.size() 
+                      << " fixed: " << conseq.size() 
+                      << " unfixed: " << unfixed.size() 
+                      << " fixed-eqs: " << num_fixed_eqs
+                      << " unfixed-deleted: " << num_unfixed
+                      << ")\n";);        
+            }
             if (var2val.contains(e)) {
                 TRACE("context", tout << "Fixed value to " << mk_pp(e, m) << " was not processed\n";);
                 expr_ref fml(m);
@@ -242,8 +314,7 @@ namespace smt {
                 conseq.push_back(fml);
                 var2val.erase(e);
                 SASSERT(get_assignment(lit) == l_false);
-            }
-        
+            }        
         }
         end_search();
         return l_true;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 88d0c8aff..c692173e6 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3422,7 +3422,6 @@ namespace smt {
     }
 
     lbool context::bounded_search() {
-        SASSERT(!inconsistent());
         unsigned counter = 0;
         
         TRACE("bounded_search", tout << "starting bounded search...\n";);
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 30a262285..48f6004e9 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1347,7 +1347,9 @@ namespace smt {
         u_map<uint_set> m_antecedents;
         void extract_fixed_consequences(unsigned idx, obj_map<expr, expr*>& var2val, uint_set const& assumptions, expr_ref_vector& conseq);
         
-        void delete_unfixed(obj_map<expr, expr*>& var2val);
+        unsigned delete_unfixed(obj_map<expr, expr*>& var2val, expr_ref_vector& unfixed);
+
+        unsigned extract_fixed_eqs(obj_map<expr, expr*>& var2val, expr_ref_vector& conseq);
 
         expr_ref antecedent2fml(uint_set const& ante);
 
@@ -1391,7 +1393,7 @@ namespace smt {
 
         lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true);        
 
-        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq);
+        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed);
         
         lbool setup_and_check(bool reset_cancel = true);
         
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index 8f18b7311..6b65d0426 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -55,6 +55,18 @@ namespace smt {
         void set_progress_callback(progress_callback * callback) {
             return m_kernel.set_progress_callback(callback);
         }
+
+        void display(std::ostream & out) const {
+            // m_kernel.display(out); <<< for external users it is just junk
+            // TODO: it will be replaced with assertion_stack.display
+            unsigned num = m_kernel.get_num_asserted_formulas();
+            expr * const * fms = m_kernel.get_asserted_formulas();
+            out << "(kernel";
+            for (unsigned i = 0; i < num; i++) {
+                out << "\n  " << mk_ismt2_pp(fms[i], m(), 2);
+            }
+            out << ")";
+        }
         
         void assert_expr(expr * e) {
             TRACE("smt_kernel", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";);
@@ -99,8 +111,8 @@ namespace smt {
             return m_kernel.check(num_assumptions, assumptions);
         }
 
-        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
-            return m_kernel.get_consequences(assumptions, vars, conseq);
+        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) {
+            return m_kernel.get_consequences(assumptions, vars, conseq, unfixed);
         }
         
         void get_model(model_ref & m) const {
@@ -150,18 +162,6 @@ namespace smt {
         void get_guessed_literals(expr_ref_vector & result) {
             m_kernel.get_guessed_literals(result);
         }
-
-        void display(std::ostream & out) const {
-            // m_kernel.display(out); <<< for external users it is just junk
-            // TODO: it will be replaced with assertion_stack.display
-            unsigned num = m_kernel.get_num_asserted_formulas();
-            expr * const * fms = m_kernel.get_asserted_formulas();
-            out << "(kernel";
-            for (unsigned i = 0; i < num; i++) {
-                out << "\n  " << mk_ismt2_pp(fms[i], m(), 2);
-            }
-            out << ")";
-        }
         
         void collect_statistics(::statistics & st) const {
             m_kernel.collect_statistics(st);
@@ -268,8 +268,8 @@ namespace smt {
         return r;
     }
 
-    lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
-        return m_imp->get_consequences(assumptions, vars, conseq);
+    lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) {
+        return m_imp->get_consequences(assumptions, vars, conseq, unfixed);
     }
 
     void kernel::get_model(model_ref & m) const {
diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
index 4cf170681..a10961207 100644
--- a/src/smt/smt_kernel.h
+++ b/src/smt/smt_kernel.h
@@ -129,7 +129,8 @@ namespace smt {
         /**
            \brief extract consequences among variables.
         */
-        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq);
+        lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 
+                               expr_ref_vector& conseq, expr_ref_vector& unfixed);
 
         /**
            \brief Return the model associated with the last check command.
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index ec874ed8f..f9da1bf60 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -23,6 +23,7 @@ Notes:
 #include"smt_params_helper.hpp"
 #include"mus.h"
 
+
 namespace smt {
 
     class solver : public solver_na2as {
@@ -68,7 +69,8 @@ namespace smt {
         }
 
         virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
-            return m_context.get_consequences(assumptions, vars, conseq);
+            expr_ref_vector unfixed(m_context.m());
+            return m_context.get_consequences(assumptions, vars, conseq, unfixed);
         }
 
         virtual void assert_expr(expr * t) {
@@ -143,8 +145,7 @@ namespace smt {
             r.append(tmp.size(), tmp.c_ptr());
         }
 
-        virtual ast_manager& get_manager() { return m_context.m(); }
-
+        virtual ast_manager& get_manager() const { return m_context.m(); }
 
         virtual void set_progress_callback(progress_callback * callback) {
             m_callback = callback;
@@ -158,15 +159,8 @@ namespace smt {
         virtual expr * get_assertion(unsigned idx) const {
             SASSERT(idx < get_num_assertions());
             return m_context.get_formulas()[idx];
-        }
-
-        virtual std::ostream& display(std::ostream & out) const {
-            m_context.display(out);
-            return out;
-        }
-   
+        }   
     };
-
 };
 
 solver * mk_smt_solver(ast_manager & m, params_ref const & p, symbol const & logic) {
diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h
index 3da6b72a7..36eadd97d 100644
--- a/src/solver/check_sat_result.h
+++ b/src/solver/check_sat_result.h
@@ -58,7 +58,7 @@ public:
     virtual std::string reason_unknown() const = 0;
     virtual void set_reason_unknown(char const* msg) = 0;
     virtual void get_labels(svector<symbol> & r) = 0;
-    virtual ast_manager& get_manager() = 0;
+    virtual ast_manager& get_manager() const = 0;
 
 };
 
@@ -75,7 +75,7 @@ struct simple_check_sat_result : public check_sat_result {
 
     simple_check_sat_result(ast_manager & m);
     virtual ~simple_check_sat_result();
-    virtual ast_manager& get_manager() { return m_proof.get_manager(); }
+    virtual ast_manager& get_manager() const { return m_proof.get_manager(); }
     virtual void collect_statistics(statistics & st) const;
     virtual void get_unsat_core(ptr_vector<expr> & r);
     virtual void get_model(model_ref & m);
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 30b387b98..fc76f85c1 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -101,7 +101,7 @@ private:
         m_inc_unknown_behavior = static_cast<inc_unknown_behavior>(p.solver2_unknown());
     }
 
-    virtual ast_manager& get_manager() { return m_solver1->get_manager(); }
+    virtual ast_manager& get_manager() const { return m_solver1->get_manager(); }
 
     bool has_quantifiers() const {
         unsigned sz = get_num_assertions();
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index b0ae6a540..5e732075d 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -20,6 +20,7 @@ Notes:
 #include"model_evaluator.h"
 #include"ast_util.h"
 #include"ast_pp.h"
+#include"ast_pp_util.h"
 
 unsigned solver::get_num_assertions() const {
     NOT_IMPLEMENTED_YET();
@@ -32,7 +33,13 @@ expr * solver::get_assertion(unsigned idx) const {
 }
 
 std::ostream& solver::display(std::ostream & out) const {
-    return out << "(solver)";
+    expr_ref_vector fmls(get_manager());
+    get_assertions(fmls);
+    ast_pp_util visitor(get_manager());
+    visitor.collect(fmls);
+    visitor.display_decls(out);
+    visitor.display_asserts(out, fmls, true);
+    return out;
 }
 
 void solver::get_assertions(expr_ref_vector& fmls) const {
@@ -69,6 +76,7 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector
         tmp = vars[i];
         val = eval(tmp);
         if (!m.is_value(val)) {
+            // vars[i] is unfixed
             continue;
         }
         if (m.is_bool(tmp) && is_uninterp_const(tmp)) {
@@ -81,6 +89,7 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector
                 lit = m.mk_not(tmp);
             }
             else {
+                // vars[i] is unfixed
                 continue;
             }
             scoped_assumption_push _scoped_push(asms1, nlit);
@@ -89,6 +98,7 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector
             case l_undef: 
                 return is_sat;
             case l_true:
+                // vars[i] is unfixed
                 break;
             case l_false:
                 get_unsat_core(core);
@@ -114,6 +124,7 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector
             case l_undef: 
                 return is_sat;
             case l_true:
+                // vars[i] is unfixed
                 break;
             case l_false:
                 get_unsat_core(core);
@@ -124,3 +135,5 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector
     }
     return l_true;
 }
+
+
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 2a00d7195..f53301948 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -21,7 +21,6 @@ Notes:
 --*/
 #include"solver_na2as.h"
 #include"tactic.h"
-#include"ast_pp_util.h"
 #include"ast_translation.h"
 #include"mus.h"
 
@@ -75,11 +74,10 @@ public:
     virtual unsigned get_num_assertions() const;
     virtual expr * get_assertion(unsigned idx) const;
 
-    virtual std::ostream& display(std::ostream & out) const;
-    virtual ast_manager& get_manager(); 
+    virtual ast_manager& get_manager() const; 
 };
 
-ast_manager& tactic2solver::get_manager() { return m_assertions.get_manager(); }
+ast_manager& tactic2solver::get_manager() const { return m_assertions.get_manager(); }
 
 tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic):
     solver_na2as(m),
@@ -243,22 +241,6 @@ expr * tactic2solver::get_assertion(unsigned idx) const {
     return m_assertions.get(idx);
 }
 
-std::ostream& tactic2solver::display(std::ostream & out) const {
-    ast_pp_util visitor(m_assertions.m());
-    visitor.collect(m_assertions);
-    visitor.display_decls(out);
-    visitor.display_asserts(out, m_assertions, true);
-#if 0
-    ast_manager & m = m_assertions.m();
-    unsigned num = m_assertions.size();
-    out << "(solver";
-    for (unsigned i = 0; i < num; i++) {
-        out << "\n  " << mk_ismt2_pp(m_assertions.get(i), m, 2);
-    }
-    out << ")";
-#endif
-    return out;
-}
 
 solver * mk_tactic2solver(ast_manager & m, 
                           tactic * t,