removed dead code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/smt/params/qi_params.h

@@ -52,8 +52,6 @@ struct qi_params {
     bool               m_mbqi_trace;
     unsigned           m_mbqi_force_template;
 
-    bool               m_instgen;
-
     qi_params(params_ref const & p = params_ref()):
         /*
           The "weight 0" performance bug
@@ -99,8 +97,7 @@ struct qi_params {
         m_mbqi_max_cexs_incr(1),
         m_mbqi_max_iterations(1000),
         m_mbqi_trace(false),
-        m_mbqi_force_template(10),
-        m_instgen(false) {
+        m_mbqi_force_template(10) {
         updt_params(p);
     }
 

src/smt/smt_internalizer.cpp

@@ -23,7 +23,6 @@ Revision History:
 #include"ast_smt2_pp.h"
 #include"smt_model_finder.h"
 #include"for_each_expr.h"
-#include"theory_instgen.h"
 
 namespace smt {
 
@@ -530,11 +529,6 @@ namespace smt {
         SASSERT(!b_internalized(q));
         SASSERT(q->is_forall());
         SASSERT(check_patterns(q));
-        if (m_fparams.m_instgen) {
-            theory* th = m_theories.get_plugin(m_manager.get_family_id("inst_gen"));
-            static_cast<theory_instgen*>(th)->internalize_quantifier(q);
-            return;
-        }
         bool_var v             = mk_bool_var(q);
         unsigned generation    = m_generation;
         unsigned _generation;

src/smt/smt_setup.cpp

@@ -28,7 +28,6 @@ Revision History:
 #include"theory_datatype.h"
 #include"theory_dummy.h"
 #include"theory_dl.h"
-#include"theory_instgen.h"
 #include"theory_seq_empty.h"
 
 namespace smt {
@@ -772,11 +771,6 @@ namespace smt {
     void setup::setup_seq() {
         m_context.register_plugin(alloc(theory_seq_empty, m_manager));
     }
-    void setup::setup_instgen() {
-        if (m_params.m_instgen) {
-            m_context.register_plugin(mk_theory_instgen(m_manager, m_params));
-        }
-    }
 
     void setup::setup_unknown() {
         setup_arith();
@@ -784,7 +778,6 @@ namespace smt {
         setup_bv();
         setup_datatypes();
         setup_dl();
-        setup_instgen();
         setup_seq();
     }
 

src/smt/theory_instgen.h

@@ -1,45 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
-    theory_instgen.h
-
-Abstract:
-
-    InstGen (iProver) style theory solver.
-    It provides an instantiation based engine
-    based on InstGen methods together with
-    unit propagation.
-
-
-Author:
-
-    Krystof Hoder (t-khoder) 
-    Nikolaj Bjorner (nbjorner) 2011-10-6
-
-Revision History:
-
---*/
-#ifndef _THEORY_INST_GEN_H_
-#define _THEORY_INST_GEN_H_
-
-#include "smt_theory.h"
-#include "smt_params.h"
-
-namespace smt {
-
-    class theory_instgen : public theory {
-    public:
-        theory_instgen(family_id fid) : theory(fid) {}
-        virtual ~theory_instgen() {}
-        virtual void internalize_quantifier(quantifier* q) = 0;
-        virtual char const * get_name() const { return "instgen"; }
-    };
-
-    theory_instgen* mk_theory_instgen(ast_manager& m, smt_params& p);
-
-};
-
-#endif /* _THEORY_INST_GEN_H_ */
-