Minimizing dependencies to assertion_set

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

scripts/mk_make.py

@@ -43,7 +43,7 @@ add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier
 # code to the new tactic framework.
 add_lib('assertion_set', ['cmd_context'])
 add_lib('substitution', ['ast'], 'ast/substitution')
-add_lib('normal_forms', ['tactic', 'assertion_set'])
+add_lib('normal_forms', ['tactic', 'old_params'])
 add_lib('pattern', ['normal_forms'], 'ast/pattern')
 add_lib('spc', ['simplifier', 'substitution', 'old_params', 'pattern'])
 add_lib('parser_util', ['ast'])
@@ -52,7 +52,7 @@ add_lib('macros', ['simplifier', 'old_params'], 'ast/macros')
 add_lib('grobner', ['ast'], 'math/grobner')
 add_lib('euclid', ['util'], 'math/euclid')
 add_lib('proof_checker', ['rewriter', 'spc'], 'ast/proof_checker')
-add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params', 'tactic', 'assertion_set'], 'tactic/bit_blaster')
+add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params', 'tactic'], 'tactic/bit_blaster')
 add_lib('smt', ['assertion_set', 'bit_blaster', 'macros', 'normal_forms', 'cmd_context', 
                 'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util'])
 add_lib('user_plugin', ['smt'], 'smt/user_plugin')

src/normal_forms/nnf.cpp

@@ -29,10 +29,6 @@ Notes:
 
 #include"ast_smt2_pp.h"
 
-// Old strategy framework
-#include"assertion_set_strategy.h"
-
-// New framework
 #include"tactical.h"
 
 class skolemizer {
@@ -365,9 +361,9 @@ struct nnf::imp {
     void checkpoint() {
         cooperate("nnf");
         if (memory::get_allocation_size() > m_max_memory)
-            throw nnf_exception(STE_MAX_MEMORY_MSG);
+            throw nnf_exception(TACTIC_MAX_MEMORY_MSG);
         if (m_cancel)
-            throw nnf_exception(STE_CANCELED_MSG);
+            throw nnf_exception(TACTIC_CANCELED_MSG);
     }
 
     void set_new_child_flag() {
@@ -931,100 +927,3 @@ void nnf::reset_cache() {
     m_imp->reset_cache();
 }
 
-// TODO: delete after conversion to new tactic framework is done.
-class nnf_strategy : public assertion_set_strategy {
-    params_ref    m_params;
-    nnf *         m_nnf;
-
-    struct set_nnf {
-        nnf_strategy & m_owner;
-        
-        set_nnf(nnf_strategy & owner, nnf & n):
-            m_owner(owner) {
-            #pragma omp critical (nnf_strategy)
-            {
-                m_owner.m_nnf = &n;
-            }
-        }
-        
-        ~set_nnf() {
-            #pragma omp critical (nnf_strategy)
-            {
-                m_owner.m_nnf = 0;
-            }
-        }
-    };
-public:
-    nnf_strategy(params_ref const & p):
-        m_params(p),
-        m_nnf(0) {
-        TRACE("nnf", tout << "nnf_strategy constructor: " << p << "\n";);
-    }
-
-    virtual ~nnf_strategy() {}
-
-    virtual void updt_params(params_ref const & p) { m_params = p; }
-    static void get_param_descrs(param_descrs & r) { nnf::get_param_descrs(r); }
-    virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
-
-    virtual void operator()(assertion_set & s, model_converter_ref & mc) {
-        TRACE("nnf", tout << "params: " << m_params << "\n"; s.display(tout););
-        SASSERT(is_well_sorted(s));
-        as_st_report report("nnf", s);
-        mc = 0;
-        if (s.inconsistent())
-            return;
-        ast_manager & m = s.m();
-        defined_names dnames(m);
-        nnf local_nnf(m, dnames, m_params);
-        set_nnf setter(*this, local_nnf);
-        
-        expr_ref_vector defs(m);
-        proof_ref_vector def_prs(m);
-        
-        expr_ref   new_curr(m);
-        proof_ref  new_pr(m);
-        
-        unsigned sz = s.size();
-        for (unsigned i = 0; i < sz; i++) {
-            expr * curr = s.form(i);
-            local_nnf(curr, defs, def_prs, new_curr, new_pr);
-            if (m.proofs_enabled()) {
-                proof * pr = s.pr(i);
-                new_pr     = m.mk_modus_ponens(pr, new_pr);
-            }
-            s.update(i, new_curr, new_pr);
-        }
-        
-        sz = defs.size();
-        for (unsigned i = 0; i < sz; i++) {
-            if (m.proofs_enabled())
-                s.assert_expr(defs.get(i), def_prs.get(i));
-            else
-                s.assert_expr(defs.get(i), 0);
-        }
-        TRACE("nnf", s.display(tout););
-        SASSERT(is_well_sorted(s));
-    }
-
-    virtual void cleanup() {}
-    virtual void set_cancel(bool f) {
-        #pragma omp critical (nnf_strategy)
-        {
-            if (m_nnf)
-                m_nnf->set_cancel(f);
-        }
-    }
-};
-
-as_st * mk_snf(params_ref const & p) {
-    return alloc(nnf_strategy, p);
-}
-
-as_st * mk_nnf(params_ref const & p) {
-    params_ref new_p(p);
-    new_p.set_sym(":nnf-mode", symbol("full"));
-    TRACE("nnf", tout << "mk_nnf: " << new_p << "\n";);
-    return using_params(mk_snf(), new_p);
-}
-

src/normal_forms/nnf.h

@@ -51,14 +51,6 @@ public:
     void reset_cache();
 };
 
-// Old strategy framework
-class assertion_set_strategy;
-// Skolem Normal Form
-assertion_set_strategy * mk_snf(params_ref const & p = params_ref());
-// Negation Normal Form
-assertion_set_strategy * mk_nnf(params_ref const & p = params_ref());
-
-// New strategy framework
 class tactic;
 // Skolem Normal Form
 tactic * mk_snf_tactic(ast_manager & m, params_ref const & p = params_ref());

src/tactic/bit_blaster/bit_blaster_tpl.h

@@ -20,7 +20,6 @@ Revision History:
 #define _BIT_BLASTER_TPL_H_
 
 #include"rational.h"
-#include"strategy_exception.h"
 
 template<typename Cfg>
 class bit_blaster_tpl : public Cfg {

src/tactic/bit_blaster/bit_blaster_tpl_def.h

@@ -20,13 +20,14 @@ Revision History:
 #include"rational.h"
 #include"ast_pp.h"
 #include"cooperate.h"
+#include"tactic_exception.h"
 
 template<typename Cfg>
 void bit_blaster_tpl<Cfg>::checkpoint() {
     if (memory::get_allocation_size() > m_max_memory)
-        throw strategy_exception(STE_MAX_MEMORY_MSG);
+        throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
     if (m_cancel)
-        throw strategy_exception(STE_CANCELED_MSG);
+        throw tactic_exception(TACTIC_CANCELED_MSG);
     cooperate("bit-blaster");
 }
 

src/tactic/core_tactics/reduce_args_tactic.cpp

@@ -17,7 +17,6 @@ Notes:
 
 --*/
 #include"tactical.h"
-#include"reduce_args.h"
 #include"cooperate.h"
 #include"ast_smt2_pp.h"
 #include"map.h"

src/tactic/sls_tactic/sls_tactic.cpp

@@ -26,8 +26,6 @@ Notes:
 #include"model_pp.h"
 #include"model_evaluator.h"
 #include"solve_eqs_tactic.h"
-#include"assertion_set_rewriter.h"
-#include"shallow_context_simplifier.h"
 #include"elim_uncnstr_tactic.h"
 #include"bv_size_reduction_tactic.h"
 #include"max_bv_sharing_tactic.h"