From 2679b7454330b20d729413e5b3f050f4f2179b97 Mon Sep 17 00:00:00 2001
From: mikolas <mikolas.janota@gmail.com>
Date: Wed, 3 Feb 2016 13:53:52 +0000
Subject: [PATCH] refactoring
---
scripts/mk_project.py | 7 +-
src/tactic/ackr/ackr_model_converter.h | 1 +
.../ackr_tactics/qfufbv_ackr_tactic.cpp | 153 -----------------
src/tactic/ackr_tactics/qfufbv_ackr_tactic.h | 28 ---
.../smtlogics/qfufbv_ackr_model_converter.cpp | 22 +++
.../smtlogics/qfufbv_ackr_model_converter.h | 25 +++
src/tactic/smtlogics/qfufbv_tactic.cpp | 162 ++++++++++++++++--
src/tactic/smtlogics/qfufbv_tactic.h | 3 +
.../qfufbv_tactic_params.pyg} | 3 +-
9 files changed, 206 insertions(+), 198 deletions(-)
delete mode 100644 src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp
delete mode 100644 src/tactic/ackr_tactics/qfufbv_ackr_tactic.h
create mode 100644 src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp
create mode 100644 src/tactic/smtlogics/qfufbv_ackr_model_converter.h
rename src/tactic/{ackr_tactics/ackr_tactics.pyg => smtlogics/qfufbv_tactic_params.pyg} (77%)
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index d99956652..82cdc04d0 100644
--- a/scripts/mk_project.py
+++ b/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'],
diff --git a/src/tactic/ackr/ackr_model_converter.h b/src/tactic/ackr/ackr_model_converter.h
index 98c03f381..2c1f0c78c 100644
--- a/src/tactic/ackr/ackr_model_converter.h
+++ b/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_ */
diff --git a/src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp b/src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp
deleted file mode 100644
index a8a76e698..000000000
--- a/src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp
+++ /dev/null
@@ -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()));
-}
diff --git a/src/tactic/ackr_tactics/qfufbv_ackr_tactic.h b/src/tactic/ackr_tactics/qfufbv_ackr_tactic.h
deleted file mode 100644
index 57b32bf75..000000000
--- a/src/tactic/ackr_tactics/qfufbv_ackr_tactic.h
+++ /dev/null
@@ -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
-
diff --git a/src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp b/src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp
new file mode 100644
index 000000000..4d20631b1
--- /dev/null
+++ b/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);
+}
diff --git a/src/tactic/smtlogics/qfufbv_ackr_model_converter.h b/src/tactic/smtlogics/qfufbv_ackr_model_converter.h
new file mode 100644
index 000000000..a361a78e0
--- /dev/null
+++ b/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_ */
diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index 816d69b1f..526d72faa 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/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),
- 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 * const preamble_st = mk_qfufbv_preamble(m, p);
tactic * st = using_params(and_then(preamble_st,
- cond(mk_is_qfbv_probe(),
- mk_qfbv_tactic(m),
- mk_smt_tactic())),
- main_p);
+ cond(mk_is_qfbv_probe(),
+ mk_qfbv_tactic(m),
+ mk_smt_tactic())),
+ 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()));
+}
\ No newline at end of file
diff --git a/src/tactic/smtlogics/qfufbv_tactic.h b/src/tactic/smtlogics/qfufbv_tactic.h
index ceb125517..1f1431d70 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.h
+++ b/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
diff --git a/src/tactic/ackr_tactics/ackr_tactics.pyg b/src/tactic/smtlogics/qfufbv_tactic_params.pyg
similarity index 77%
rename from src/tactic/ackr_tactics/ackr_tactics.pyg
rename to src/tactic/smtlogics/qfufbv_tactic_params.pyg
index 8f391bc91..6c4bd5b8e 100644
--- a/src/tactic/ackr_tactics/ackr_tactics.pyg
+++ b/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'),