more merges with qsat

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/qe/qe_tactic.cpp

@@ -22,6 +22,7 @@ Revision History:
 #include"qe.h"
 
 class qe_tactic : public tactic {
+    statistics               m_st;
     struct     imp {
         ast_manager &            m;
         smt_params               m_fparams;
@@ -78,10 +79,19 @@ class qe_tactic : public tactic {
                 g->update(i, new_f, new_pr, g->dep(i));                
             }
             g->inc_depth();
+            g->elim_true();
             result.push_back(g.get());
             TRACE("qe", g->display(tout););
             SASSERT(g->is_well_sorted());
         }
+
+        void collect_statistics(statistics & st) const {
+            m_qe.collect_statistics(st);
+        }
+
+        void reset_statistics() {            
+        }
+
     };
     
     imp *      m_imp;
@@ -117,7 +127,19 @@ public:
                             proof_converter_ref & pc,
                             expr_dependency_ref & core) {
         (*m_imp)(in, result, mc, pc, core);
+        m_st.reset();
+        m_imp->collect_statistics(m_st);
+        
     }
+
+    virtual void collect_statistics(statistics & st) const {
+        st.copy(m_st);
+    }
+
+    virtual void reset_statistics() {
+        m_st.reset();
+    }
+
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;

src/sat/tactic/goal2sat.cpp

@@ -509,7 +509,7 @@ struct sat2goal::imp {
         // This information may be stored as a vector of pairs.
         // The mapping is only created during the model conversion.
         expr_ref_vector             m_var2expr;
-        ref<filter_model_converter> m_fmc; // filter for eliminating fresh variables introduced in the assertion-set --> sat conversion
+        filter_model_converter_ref  m_fmc; // filter for eliminating fresh variables introduced in the assertion-set --> sat conversion
         
         sat_model_converter(ast_manager & m):
             m_var2expr(m) {

src/smt/smt_kernel.h

@@ -122,6 +122,10 @@ namespace smt {
         */
         lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0);
 
+        lbool check(expr_ref_vector const& asms) { return check(asms.size(), asms.c_ptr()); }
+
+        lbool check(app_ref_vector const& asms) { return check(asms.size(), (expr* const*)asms.c_ptr()); }
+
         /**
            \brief Return the model associated with the last check command.
         */

src/smt/smt_theory.h

@@ -315,10 +315,7 @@ namespace smt {
             return m_var2enode_lim[m_var2enode_lim.size() - num_scopes];
         }
         
-        virtual void display(std::ostream & out) const {
+        virtual void display(std::ostream & out) const = 0;
-            out << "Theory " << static_cast<int>(get_id()) << typeid(*this).name() << " does not have a display method\n";
-            display_var2enode(out);
-        }
 
         virtual void display_var2enode(std::ostream & out) const;
         

src/smt/theory_dummy.h

@@ -43,6 +43,7 @@ namespace smt {
         virtual bool build_models() const { 
             return false;
         }
+        virtual void display(std::ostream& out) const {}
 
     public:
         theory_dummy(family_id fid, char const * name);

src/smt/theory_seq_empty.h

@@ -122,6 +122,7 @@ namespace smt {
         virtual void new_diseq_eh(theory_var, theory_var) {}
         virtual theory* mk_fresh(context* new_ctx) { return alloc(theory_seq_empty, new_ctx->get_manager()); }
         virtual char const * get_name() const { return "seq-empty"; }
+        virtual void display(std::ostream& out) const {}
     public:
         theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}
         virtual void init_model(model_generator & mg) {

src/smt/theory_wmaxsat.h

@@ -94,6 +94,7 @@ namespace smt {
         virtual bool internalize_term(app * term) { return false; }
         virtual void new_eq_eh(theory_var v1, theory_var v2) { }
         virtual void new_diseq_eh(theory_var v1, theory_var v2) { }
+        virtual void display(std::ostream& out) const {}
 
         virtual void collect_statistics(::statistics & st) const {
             st.update("wmaxsat num blocks", m_stats.m_num_blocks);