From 92755b0185e32a31d0ed1e2d700b9971f1523087 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 2 May 2017 17:16:35 -0400 Subject: [PATCH] smt_setup framework, all hooks to theory_str are redirected to theory_seq --- src/smt/params/smt_params.cpp | 1 + src/smt/params/smt_params.h | 10 +++++++- src/smt/params/smt_params_helper.pyg | 1 + src/smt/smt_setup.cpp | 38 ++++++++++++++++++++++++---- src/smt/smt_setup.h | 4 ++- src/solver/smt_logics.cpp | 6 ++++- src/solver/smt_logics.h | 1 + 7 files changed, 53 insertions(+), 8 deletions(-) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 4b7920596..3d0b59c88 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -40,6 +40,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_max_conflicts = p.max_conflicts(); m_core_validate = p.core_validate(); m_logic = _p.get_sym("logic", m_logic); + m_string_solver = p.string_solver(); model_params mp(_p); m_model_compact = mp.compact(); if (_p.get_bool("arith.greatest_error_pivot", false)) diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index c03eaeaef..b44e782fd 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -213,6 +213,13 @@ struct smt_params : public preprocessor_params, bool m_dump_goal_as_smt; bool m_auto_config; + // ----------------------------------- + // + // Solver selection + // + // ----------------------------------- + symbol m_string_solver; + smt_params(params_ref const & p = params_ref()): m_display_proof(false), m_display_dot_proof(false), @@ -281,7 +288,8 @@ struct smt_params : public preprocessor_params, m_at_labels_cex(false), m_check_at_labels(false), m_dump_goal_as_smt(false), - m_auto_config(true) { + m_auto_config(true), + m_string_solver(symbol("seq")){ updt_local_params(p); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index faa48400d..a06a37f2a 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -62,6 +62,7 @@ def_module_params(module_name='smt', ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'), ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'), + ('string_solver', SYMBOL, 'seq', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver)'), ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'), ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'), ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'), diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index ee92c4f61..84e3dee32 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -120,6 +120,8 @@ namespace smt { setup_QF_FP(); else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP") setup_QF_FPBV(); + else if (m_logic == "QF_S") + setup_QF_S(); else setup_unknown(); } @@ -161,6 +163,8 @@ namespace smt { setup_QF_BVRE(); else if (m_logic == "QF_AUFLIA") setup_QF_AUFLIA(st); + else if (m_logic == "QF_S") + setup_QF_S(); else if (m_logic == "AUFLIA") setup_AUFLIA(st); else if (m_logic == "AUFLIRA") @@ -201,7 +205,7 @@ namespace smt { void setup::setup_QF_BVRE() { setup_QF_BV(); setup_QF_LIA(); - setup_seq(); + m_context.register_plugin(alloc(theory_seq, m_manager)); } void setup::setup_QF_UF(static_features const & st) { @@ -700,6 +704,10 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_fpa, m_manager)); } + void setup::setup_QF_S() { + m_context.register_plugin(alloc(smt::theory_seq, m_manager)); + } + bool is_arith(static_features const & st) { return st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0; } @@ -814,8 +822,21 @@ namespace smt { m_context.register_plugin(mk_theory_dl(m_manager)); } - void setup::setup_seq() { - m_context.register_plugin(alloc(theory_seq, m_manager)); + void setup::setup_seq(static_features const & st) { + // check params for what to do here when it's ambiguous + if (m_params.m_string_solver == "z3str3") { + setup_str(); + } else if (m_params.m_string_solver == "seq") { + m_context.register_plugin(alloc(smt::theory_seq, m_manager)); + } else if (m_params.m_string_solver == "auto") { + if (st.m_has_seq_non_str) { + m_context.register_plugin(alloc(smt::theory_seq, m_manager)); + } else { + setup_str(); + } + } else { + throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'"); + } } void setup::setup_card() { @@ -827,13 +848,20 @@ namespace smt { m_context.register_plugin(alloc(theory_fpa, m_manager)); } + void setup::setup_str() { + m_context.register_plugin(alloc(smt::theory_seq, m_manager)); + } + void setup::setup_unknown() { + static_features st(m_manager); + st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas()); + setup_arith(); setup_arrays(); setup_bv(); setup_datatypes(); setup_dl(); - setup_seq(); + setup_seq(st); setup_card(); setup_fpa(); } @@ -848,7 +876,7 @@ namespace smt { setup_datatypes(); setup_bv(); setup_dl(); - setup_seq(); + setup_seq(st); setup_card(); setup_fpa(); return; diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 68cd5703c..d30c896e5 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -77,6 +77,7 @@ namespace smt { void setup_QF_AUFLIA(static_features const & st); void setup_QF_FP(); void setup_QF_FPBV(); + void setup_QF_S(); void setup_LRA(); void setup_AUFLIA(bool simple_array = true); void setup_AUFLIA(static_features const & st); @@ -93,11 +94,12 @@ namespace smt { void setup_bv(); void setup_arith(); void setup_dl(); - void setup_seq(); + void setup_seq(static_features const & st); void setup_card(); void setup_i_arith(); void setup_mi_arith(); void setup_fpa(); + void setup_str(); public: setup(context & c, smt_params & params); diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index 210a09f96..c4ead74df 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -24,7 +24,7 @@ Revision History: bool smt_logics::supported_logic(symbol const & s) { return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) || logic_has_arith(s) || logic_has_bv(s) || - logic_has_array(s) || logic_has_seq(s) || + logic_has_array(s) || logic_has_seq(s) || logic_has_str(s) || logic_has_horn(s) || logic_has_fpa(s); } @@ -132,6 +132,10 @@ bool smt_logics::logic_has_seq(symbol const & s) { return s == "QF_BVRE" || s == "QF_S" || s == "ALL"; } +bool smt_logics::logic_has_str(symbol const & s) { + return s == "QF_S" || s == "ALL"; +} + bool smt_logics::logic_has_fpa(symbol const & s) { return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "ALL"; } diff --git a/src/solver/smt_logics.h b/src/solver/smt_logics.h index 72c3b8764..702431cdd 100644 --- a/src/solver/smt_logics.h +++ b/src/solver/smt_logics.h @@ -30,6 +30,7 @@ public: static bool logic_has_bv(symbol const & s); static bool logic_has_array(symbol const & s); static bool logic_has_seq(symbol const & s); + static bool logic_has_str(symbol const & s); static bool logic_has_fpa(symbol const & s); static bool logic_has_horn(symbol const& s); static bool logic_has_pb(symbol const& s);