From 419e2c4899a55ea8e698a00cd6abff5638de7032 Mon Sep 17 00:00:00 2001 From: mikolas Date: Mon, 29 Feb 2016 11:39:52 +0000 Subject: [PATCH] Inc sat for ackr. --- src/tactic/smtlogics/qfufbv_tactic.cpp | 12 ++++++++++-- src/tactic/smtlogics/qfufbv_tactic_params.pyg | 1 + 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 421a76cc7..3ee97308a 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -47,6 +47,7 @@ public: : m_m(m) , m_p(p) , m_use_sat(false) + , m_inc_use_sat(false) {} virtual ~qfufbv_ackr_tactic() { } @@ -85,6 +86,7 @@ public: void updt_params(params_ref const & _p) { qfufbv_tactic_params p(_p); m_use_sat = p.sat_backend(); + m_inc_use_sat = p.inc_sat_backend(); } virtual void collect_statistics(statistics & st) const { @@ -105,12 +107,18 @@ private: params_ref m_p; lackr_stats m_st; bool m_use_sat; + bool m_inc_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); + if (m_inc_use_sat) { + sat = mk_inc_sat_solver(m_m, m_p); + } + else { + 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); diff --git a/src/tactic/smtlogics/qfufbv_tactic_params.pyg b/src/tactic/smtlogics/qfufbv_tactic_params.pyg index 6c4bd5b8e..b7640538d 100644 --- a/src/tactic/smtlogics/qfufbv_tactic_params.pyg +++ b/src/tactic/smtlogics/qfufbv_tactic_params.pyg @@ -4,5 +4,6 @@ def_module_params('ackermannization', export=True, params=( ('sat_backend', BOOL, False, 'use SAT rather than SMT in qfufbv_ackr_tactic'), + ('inc_sat_backend', BOOL, False, 'use incremental SAT'), ))