diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 2882e905d..030b244e5 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -273,6 +273,10 @@ public: bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); } + bool is_string_term(expr const * n) const { + sort * s = get_sort(n); + return is_sort_of(s, m_fid, _STRING_SORT); + } MATCH_BINARY(is_concat); MATCH_UNARY(is_length); diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index 328128794..9958b3d50 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -25,6 +25,7 @@ static_features::static_features(ast_manager & m): m_bvutil(m), m_arrayutil(m), m_fpautil(m), + m_sequtil(m), m_bfid(m.get_basic_family_id()), m_afid(m.mk_family_id("arith")), m_lfid(m.mk_family_id("label")), @@ -77,6 +78,8 @@ void static_features::reset() { m_has_real = false; m_has_bv = false; m_has_fpa = false; + m_has_str = false; + m_has_seq_non_str = false; m_has_arrays = false; m_arith_k_sum .reset(); m_num_arith_terms = 0; @@ -279,6 +282,10 @@ void static_features::update_core(expr * e) { m_has_fpa = true; if (!m_has_arrays && m_arrayutil.is_array(e)) m_has_arrays = true; + if (!m_has_str && m_sequtil.str.is_string_term(e)) + m_has_str = true; + if (!m_has_seq_non_str && m_sequtil.is_seq(e)) + m_has_seq_non_str = 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 8b20c5463..e7f69e041 100644 --- a/src/ast/static_features.h +++ b/src/ast/static_features.h @@ -24,6 +24,7 @@ Revision History: #include"bv_decl_plugin.h" #include"array_decl_plugin.h" #include"fpa_decl_plugin.h" +#include"seq_decl_plugin.h" #include"map.h" struct static_features { @@ -32,6 +33,7 @@ struct static_features { bv_util m_bvutil; array_util m_arrayutil; fpa_util m_fpautil; + seq_util m_sequtil; family_id m_bfid; family_id m_afid; family_id m_lfid; @@ -77,6 +79,8 @@ struct static_features { bool m_has_real; // bool m_has_bv; // bool m_has_fpa; // + bool m_has_str; // has String-typed terms + bool m_has_seq_non_str; // has non-String-typed Sequence terms bool m_has_arrays; // rational m_arith_k_sum; // sum of the numerals in arith atoms. unsigned m_num_arith_terms; diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index dcf396531..b8d5fe7b5 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -41,6 +41,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.get_sym("string_solver", m_string_solver); model_params mp(_p); m_model_compact = mp.compact(); if (_p.get_bool("arith.greatest_error_pivot", false)) @@ -157,4 +158,4 @@ void smt_params::display(std::ostream & out) const { DISPLAY_PARAM(m_check_at_labels); DISPLAY_PARAM(m_dump_goal_as_smt); DISPLAY_PARAM(m_auto_config); -} \ No newline at end of file +} diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index a86123a33..295e141cc 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -216,6 +216,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), @@ -286,7 +293,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("auto")){ updt_local_params(p); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 133d1d527..f99c2df16 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'), ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'), + ('string_solver', SYMBOL, 'auto', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver)'), ('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'), ('str.aggressive_length_testing', BOOL, False, 'prioritize testing concrete length values over generating more options'), ('str.aggressive_value_testing', BOOL, False, 'prioritize testing concrete string constant values over generating more options'), diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 78a295e27..c295801ad 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -206,7 +206,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) { @@ -824,10 +824,21 @@ namespace smt { m_context.register_plugin(mk_theory_dl(m_manager)); } - void setup::setup_seq() { - // TODO proper negotiation of theory_str vs. theory_seq - //m_context.register_plugin(alloc(theory_seq, m_manager)); - setup_str(); + 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(theory_seq, m_manager)); + } else if (m_params.m_string_solver == "auto") { + if (st.m_has_seq_non_str) { + m_context.register_plugin(alloc(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() { @@ -850,10 +861,10 @@ namespace smt { setup_bv(); setup_datatypes(); setup_dl(); - setup_seq(); + // setup_seq() + m_context.register_plugin(alloc(theory_seq, m_manager)); setup_card(); setup_fpa(); - setup_str(); } void setup::setup_unknown(static_features & st) { @@ -866,7 +877,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 031c65c1f..d30c896e5 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -94,7 +94,7 @@ 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(); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 01123a22c..be268ec5c 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4844,7 +4844,7 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) { // we only want to inspect the Contains terms where either of strAst or substrAst // are equal to varNode. - TRACE("t_str_detail", tout << "considering Contains with strAst = "str", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;); + TRACE("t_str_detail", tout << "considering Contains with strAst = " << mk_pp(strAst, m) << ", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;); if (varNode != strAst && varNode != substrAst) { TRACE("str", tout << "varNode not equal to strAst or substrAst, skip" << std::endl;); @@ -4873,7 +4873,7 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) { zstring subStrConst; u.str.is_string(substrValue, subStrConst); - TRACE("t_str_detail", tout << "strConst = "str", subStrConst = " << subStrConst << "\n";); + TRACE("t_str_detail", tout << "strConst = " << strConst << ", subStrConst = " << subStrConst << "\n";); if (strConst.contains(subStrConst)) { //implyR = ctx.mk_eq(ctx, boolVar, Z3_mk_true(ctx)); @@ -4983,7 +4983,7 @@ void theory_str::check_contain_by_substr(expr * varNode, expr_ref_vector & willE // we only want to inspect the Contains terms where either of strAst or substrAst // are equal to varNode. - TRACE("t_str_detail", tout << "considering Contains with strAst = "str", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;); + TRACE("t_str_detail", tout << "considering Contains with strAst = " << mk_pp(strAst, m) << ", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;); if (varNode != strAst && varNode != substrAst) { TRACE("str", tout << "varNode not equal to strAst or substrAst, skip" << std::endl;); @@ -6181,7 +6181,6 @@ void nfa::convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u) { } make_transition(last, str[(str.length() - 1)], end); TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); - TRACE("t_str_rw", tout << "str", end = " << end << std::endl;); } else { TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;); m_valid = false;