refactoring

scripts/mk_project.py

@@ -71,18 +71,17 @@ def init_project_def():
     add_lib('duality_intf', ['muz', 'transforms', 'duality'], 'muz/duality')
     add_lib('fp',  ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp')
     add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt')
-    add_lib('smtlogic_tactics', ['ackr', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
-    add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
     add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
     add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver')
-    add_lib('ackr_tactics', ['bv_tactics', 'smt_tactic', 'aig_tactic', 'sat_solver', 'ackr', 'smtlogic_tactics'], 'tactic/ackr_tactics')
+    add_lib('smtlogic_tactics', ['ackr', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
+    add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
     add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp',  'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
     add_lib('smtparser', ['portfolio'], 'parsers/smt')
     add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt')
     API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_interp.h', 'z3_fpa.h']
     add_lib('api', ['portfolio', 'smtparser', 'realclosure', 'interp', 'opt'],
             includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
-    add_exe('shell', ['api', 'sat', 'extra_cmds','opt','ackr_tactics'], exe_name='z3')
+    add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3')
     add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False)
     _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
                               reexports=['api'],

src/tactic/ackr/ackr_model_converter.h

@@ -21,4 +21,5 @@ Revision History:
 
 model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model);
 model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info);
+
 #endif /* LACKR_MODEL_CONVERTER_H_ */

src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp

@@ -1,153 +0,0 @@
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
-Module Name:
-
-qfufbv_ackr_tactic.cpp
-
-Abstract:
-
-Author:
-
-Mikolas Janota
-
-Revision History:
---*/
-#include"tactical.h"
-///////////////
-#include"solve_eqs_tactic.h"
-#include"simplify_tactic.h"
-#include"propagate_values_tactic.h"
-#include"bit_blaster_tactic.h"
-#include"elim_uncnstr_tactic.h"
-#include"max_bv_sharing_tactic.h"
-#include"bv_size_reduction_tactic.h"
-#include"ctx_simplify_tactic.h"
-#include"smt_tactic.h"
-///////////////
-#include"model_smt2_pp.h"
-#include"cooperate.h"
-#include"lackr.h"
-#include"ackr_tactics_params.hpp"
-#include"ackr_model_converter.h"
-///////////////
-#include"inc_sat_solver.h"
-#include"qfaufbv_tactic.h"
-#include"qfbv_tactic.h"
-#include"tactic2solver.h"
-///////////////
-
-
-class qfufbv_ackr_tactic : public tactic {
-public:
-    qfufbv_ackr_tactic(ast_manager& m, params_ref const& p)
-        : m_m(m)
-        , m_p(p)
-        , m_use_sat(false)
-    {}
-
-    virtual ~qfufbv_ackr_tactic() { }
-
-    virtual void operator()(goal_ref const & g,
-        goal_ref_buffer & result,
-        model_converter_ref & mc,
-        proof_converter_ref & pc,
-        expr_dependency_ref & core) {
-        mc = 0;
-        ast_manager& m(g->m());
-        tactic_report report("qfufbv_ackr", *g);
-        fail_if_unsat_core_generation("qfufbv_ackr", g);
-        fail_if_proof_generation("qfufbv_ackr", g);
-
-        TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n"););
-        // running implementation
-        expr_ref_vector flas(m);
-        const unsigned sz = g->size();
-        for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
-        scoped_ptr<solver> uffree_solver = setup_sat();
-        scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas, uffree_solver.get());
-        const lbool o = imp->operator()();
-        flas.reset();
-        // report result
-        goal_ref resg(alloc(goal, *g, true));
-        if (o == l_false) resg->assert_expr(m.mk_false());
-        if (o != l_undef) result.push_back(resg.get());
-        // report model
-        if (g->models_enabled() && (o == l_true)) {
-            model_ref abstr_model = imp->get_model();
-            mc = mk_ackr_model_converter(m, imp->get_info(), abstr_model);
-        }
-    }
-
-    void updt_params(params_ref const & _p) {
-        ackr_tactics_params p(_p);
-        m_use_sat = p.sat_backend();
-    }
-
-    virtual void collect_statistics(statistics & st) const {
-        ackr_params p(m_p);
-        if (!p.eager()) st.update("lackr-its", m_st.m_it);
-        st.update("ackr-constraints", m_st.m_ackrs_sz);
-    }
-
-    virtual void reset_statistics() { m_st.reset(); }
-
-    virtual void cleanup() { }
-
-    virtual tactic* translate(ast_manager& m) {
-        return alloc(qfufbv_ackr_tactic, m, m_p);
-    }
-private:
-    ast_manager&                         m_m;
-    params_ref                           m_p;
-    lackr_stats                          m_st;
-    bool                                 m_use_sat;
-
-    solver* setup_sat() {
-        solver * sat(NULL);
-        if (m_use_sat) {
-            tactic_ref t = mk_qfbv_tactic(m_m, m_p);
-            sat = mk_tactic2solver(m_m, t.get(), m_p);
-        }
-        else {
-            tactic_ref t = mk_qfaufbv_tactic(m_m, m_p);
-            sat = mk_tactic2solver(m_m, t.get(), m_p);
-        }
-        SASSERT(sat != NULL);
-        sat->set_produce_models(true);
-        return sat;
-    }
-
-
-};
-
-tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) {
-    params_ref simp2_p = p;
-    simp2_p.set_bool("som", true);
-    simp2_p.set_bool("pull_cheap_ite", true);
-    simp2_p.set_bool("push_ite_bv", false);
-    simp2_p.set_bool("local_ctx", true);
-    simp2_p.set_uint("local_ctx_limit", 10000000);
-
-    simp2_p.set_bool("ite_extra_rules", true);
-    simp2_p.set_bool("mul2concat", true);
-
-    params_ref ctx_simp_p;
-    ctx_simp_p.set_uint("max_depth", 32);
-    ctx_simp_p.set_uint("max_steps", 5000000);
-
-    tactic * const preamble_t = and_then(
-        mk_simplify_tactic(m),
-        mk_propagate_values_tactic(m),
-        //using_params(mk_ctx_simplify_tactic(m_m), ctx_simp_p),
-        mk_solve_eqs_tactic(m),
-        mk_elim_uncnstr_tactic(m),
-        if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
-        mk_max_bv_sharing_tactic(m),
-        using_params(mk_simplify_tactic(m), simp2_p)
-        );
-
-    tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p);
-    return and_then(preamble_t,
-        cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic()));
-}

src/tactic/ackr_tactics/qfufbv_ackr_tactic.h

@@ -1,28 +0,0 @@
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
-Module Name:
-
-qfufbv_ackr_tactic.h
-
-Abstract:
-
-Author:
-
-Mikolas Janota
-
-Revision History:
---*/
-
-#ifndef _QFUFBV_ACKR_TACTIC_H_
-#define _QFUFBV_ACKR_TACTIC_H_
-#include"tactical.h"
-
-tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p);
-
-/*
-  ADD_TACTIC("qfufbv_ackr", "A tactic for solving QF_UFBV based on Ackermannization.", "mk_qfufbv_ackr_tactic(m, p)")
-*/
-
-#endif
-

src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp

@@ -0,0 +1,22 @@
+/*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  qfufbv_ackr_model_converter.cpp
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota (MikolasJanota)
+
+ Revision History:
+--*/
+#include"qfufbv_ackr_model_converter.h"
+#include"ackr_model_converter.h"
+
+model_converter * mk_qfufbv_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model) {
+   return mk_ackr_model_converter(m, info, abstr_model);
+}

src/tactic/smtlogics/qfufbv_ackr_model_converter.h

@@ -0,0 +1,25 @@
+ /*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  qfufbv_ackr_model_converter.h
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota (MikolasJanota)
+
+ Revision History:
+ --*/
+#ifndef QFUFBV_ACKR_MODEL_CONVERTER_H_
+#define QFUFBV_ACKR_MODEL_CONVERTER_H_
+
+#include"model_converter.h"
+#include"ackr_info.h"
+
+model_converter * mk_qfufbv_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model);
+
+#endif /* QFUFBV_ACKR_MODEL_CONVERTER_H_ */

src/tactic/smtlogics/qfufbv_tactic.cpp

@@ -12,6 +12,7 @@ Abstract:
 Author:
 
     Leonardo (leonardo) 2012-02-27
+    Mikolas Janota
 
 Notes:
 
@@ -26,27 +27,164 @@ Notes:
 #include"bv_size_reduction_tactic.h"
 #include"reduce_args_tactic.h"
 #include"qfbv_tactic.h"
+#include"qfufbv_tactic_params.hpp"
+///////////////
+#include"model_smt2_pp.h"
+#include"cooperate.h"
+#include"lackr.h"
+#include"qfufbv_ackr_model_converter.h"
+///////////////
+#include"inc_sat_solver.h"
+#include"qfaufbv_tactic.h"
+#include"qfbv_tactic.h"
+#include"tactic2solver.h"
+///////////////
+
+class qfufbv_ackr_tactic : public tactic {
+public:
+    qfufbv_ackr_tactic(ast_manager& m, params_ref const& p)
+        : m_m(m)
+        , m_p(p)
+        , m_use_sat(false)
+    {}
+
+    virtual ~qfufbv_ackr_tactic() { }
+
+    virtual void operator()(goal_ref const & g,
+        goal_ref_buffer & result,
+        model_converter_ref & mc,
+        proof_converter_ref & pc,
+        expr_dependency_ref & core) {
+        mc = 0;
+        ast_manager& m(g->m());
+        tactic_report report("qfufbv_ackr", *g);
+        fail_if_unsat_core_generation("qfufbv_ackr", g);
+        fail_if_proof_generation("qfufbv_ackr", g);
+
+        TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n"););
+        // running implementation
+        expr_ref_vector flas(m);
+        const unsigned sz = g->size();
+        for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
+        scoped_ptr<solver> uffree_solver = setup_sat();
+        scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas, uffree_solver.get());
+        const lbool o = imp->operator()();
+        flas.reset();
+        // report result
+        goal_ref resg(alloc(goal, *g, true));
+        if (o == l_false) resg->assert_expr(m.mk_false());
+        if (o != l_undef) result.push_back(resg.get());
+        // report model
+        if (g->models_enabled() && (o == l_true)) {
+            model_ref abstr_model = imp->get_model();
+            mc = mk_qfufbv_ackr_model_converter(m, imp->get_info(), abstr_model);
+        }
+    }
+
+    void updt_params(params_ref const & _p) {
+        qfufbv_tactic_params p(_p);
+        m_use_sat = p.sat_backend();
+    }
+
+    virtual void collect_statistics(statistics & st) const {
+        ackr_params p(m_p);
+        if (!p.eager()) st.update("lackr-its", m_st.m_it);
+        st.update("ackr-constraints", m_st.m_ackrs_sz);
+    }
+
+    virtual void reset_statistics() { m_st.reset(); }
+
+    virtual void cleanup() { }
+
+    virtual tactic* translate(ast_manager& m) {
+        return alloc(qfufbv_ackr_tactic, m, m_p);
+    }
+private:
+    ast_manager&                         m_m;
+    params_ref                           m_p;
+    lackr_stats                          m_st;
+    bool                                 m_use_sat;
+
+    solver* setup_sat() {
+        solver * sat(NULL);
+        if (m_use_sat) {
+            tactic_ref t = mk_qfbv_tactic(m_m, m_p);
+            sat = mk_tactic2solver(m_m, t.get(), m_p);
+        }
+        else {
+            tactic_ref t = mk_qfaufbv_tactic(m_m, m_p);
+            sat = mk_tactic2solver(m_m, t.get(), m_p);
+        }
+        SASSERT(sat != NULL);
+        sat->set_produce_models(true);
+        return sat;
+    }
+
+
+};
+
+tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
+    params_ref simp2_p = p;
+    simp2_p.set_bool("pull_cheap_ite", true);
+    simp2_p.set_bool("push_ite_bv", false);
+    simp2_p.set_bool("local_ctx", true);
+    simp2_p.set_uint("local_ctx_limit", 10000000);
+
+    simp2_p.set_bool("ite_extra_rules", true);
+    simp2_p.set_bool("mul2concat", true);
+
+    params_ref ctx_simp_p;
+    ctx_simp_p.set_uint("max_depth", 32);
+    ctx_simp_p.set_uint("max_steps", 5000000);
+
+    return and_then(
+        mk_simplify_tactic(m),
+        mk_propagate_values_tactic(m),
+        //using_params(mk_ctx_simplify_tactic(m_m), ctx_simp_p),
+        mk_solve_eqs_tactic(m),
+        mk_elim_uncnstr_tactic(m),
+        if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
+        mk_max_bv_sharing_tactic(m),
+        using_params(mk_simplify_tactic(m), simp2_p)
+        );
+}
+
+tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) {
+    params_ref main_p;
+    main_p.set_bool("elim_and", true);
+    main_p.set_bool("blast_distinct", true);
+
+    return and_then(mk_simplify_tactic(m),
+        mk_propagate_values_tactic(m),
+        mk_solve_eqs_tactic(m),
+        mk_elim_uncnstr_tactic(m),
+        if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
+        if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
+        mk_max_bv_sharing_tactic(m)
+        );
+}
 
 tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
     params_ref main_p;
     main_p.set_bool("elim_and", true);
     main_p.set_bool("blast_distinct", true);
 
-    tactic * preamble_st = and_then(mk_simplify_tactic(m),
+    tactic * const preamble_st = mk_qfufbv_preamble(m, p);
-                                    mk_propagate_values_tactic(m),
-                                    mk_solve_eqs_tactic(m),
-                                    mk_elim_uncnstr_tactic(m),
-                                    if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
-                                    if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
-                                    mk_max_bv_sharing_tactic(m)
-                                    );
 
     tactic * st = using_params(and_then(preamble_st,
-                                        cond(mk_is_qfbv_probe(),
+        cond(mk_is_qfbv_probe(),
-                                            mk_qfbv_tactic(m),
+            mk_qfbv_tactic(m),
-                                            mk_smt_tactic())),
+            mk_smt_tactic())),
-                               main_p);
+        main_p);
 
     st->updt_params(p);
     return st;
 }
+
+tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) {
+    tactic * const preamble_t = mk_qfufbv_preamble(m, p);
+
+    tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p);
+    return and_then(preamble_t,
+        cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic()));
+}

src/tactic/smtlogics/qfufbv_tactic.h

@@ -25,8 +25,11 @@ class tactic;
 
 tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p = params_ref());
 
+tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p);
+
 /*
   ADD_TACTIC("qfufbv", "builtin strategy for solving QF_UFBV problems.", "mk_qfufbv_tactic(m, p)")
+  ADD_TACTIC("qfufbv_ackr", "A tactic for solving QF_UFBV based on Ackermannization.", "mk_qfufbv_ackr_tactic(m, p)")
 */
 
 #endif

src/tactic/smtlogics/qfufbv_tactic_params.pyg

@@ -1,5 +1,6 @@
-def_module_params('ackr_tactics',
+def_module_params('ackermannization',
                   description='tactics based on solving UF-theories via ackermannization (see also ackr module)',
+                  class_name='qfufbv_tactic_params',
                   export=True,
                   params=(
                           ('sat_backend', BOOL, False, 'use SAT rather than SMT in qfufbv_ackr_tactic'),