From 4792c5fb7c91b24b3eb21fcdcf04adfbf21919d4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 8 Feb 2015 16:53:08 +0000 Subject: [PATCH] Fixed bugs in static features and smt setup Signed-off-by: Christoph M. Wintersteiger --- src/ast/static_features.cpp | 8 +++++++- src/ast/static_features.h | 7 +++++-- src/smt/smt_setup.cpp | 10 +++++++++- 3 files changed, 21 insertions(+), 4 deletions(-) diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index e725df691..1634f8df4 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -23,6 +23,7 @@ static_features::static_features(ast_manager & m): m_manager(m), m_autil(m), m_bvutil(m), + m_arrayutil(m), m_fpautil(m), m_bfid(m.get_basic_family_id()), m_afid(m.mk_family_id("arith")), @@ -72,7 +73,10 @@ void static_features::reset() { m_num_eqs = 0; m_has_rational = false; m_has_int = false; - m_has_real = false; + m_has_real = false; + m_has_bv = false; + m_has_fpa = false; + m_has_arrays = false; m_arith_k_sum .reset(); m_num_arith_terms = 0; m_num_arith_eqs = 0; @@ -272,6 +276,8 @@ void static_features::update_core(expr * e) { m_has_bv = true; if (!m_has_fpa && (m_fpautil.is_float(e) || m_fpautil.is_rm(e))) m_has_fpa = true; + if (!m_has_arrays && m_arrayutil.is_array(e)) + m_has_arrays = true; if (is_app(e)) { family_id fid = to_app(e)->get_family_id(); mark_theory(fid); diff --git a/src/ast/static_features.h b/src/ast/static_features.h index 2d6213ded..d27d026cf 100644 --- a/src/ast/static_features.h +++ b/src/ast/static_features.h @@ -22,6 +22,7 @@ Revision History: #include"ast.h" #include"arith_decl_plugin.h" #include"bv_decl_plugin.h" +#include"array_decl_plugin.h" #include"fpa_decl_plugin.h" #include"map.h" @@ -29,6 +30,7 @@ struct static_features { ast_manager & m_manager; arith_util m_autil; bv_util m_bvutil; + array_util m_arrayutil; fpa_util m_fpautil; family_id m_bfid; family_id m_afid; @@ -72,8 +74,9 @@ struct static_features { bool m_has_rational; // bool m_has_int; // bool m_has_real; // - bool m_has_bv; // - bool m_has_fpa; // + bool m_has_bv; // + bool m_has_fpa; // + bool m_has_arrays; // rational m_arith_k_sum; // sum of the numerals in arith atoms. unsigned m_num_arith_terms; unsigned m_num_arith_eqs; // equalities of the form t = k where k is a numeral diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 7abd40399..a89422ee0 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -888,7 +888,15 @@ namespace smt { return; } - // TODO QF_AUFBV, QF_AUFLIA + if (st.num_theories() == 1 && st.m_has_arrays) + setup_QF_AX(); + + if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_bv) + setup_QF_AUFBV(); + + if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_int) + setup_QF_AUFLIA(); + setup_unknown(); }