diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 9c1eec649..27071bd9e 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -25,6 +25,7 @@ Revision History: #include"theory_arith_params.h" #include"theory_array_params.h" #include"theory_bv_params.h" +#include"theory_str_params.h" #include"theory_pb_params.h" #include"theory_datatype_params.h" #include"preprocessor_params.h" @@ -75,6 +76,7 @@ struct smt_params : public preprocessor_params, public theory_arith_params, public theory_array_params, public theory_bv_params, + public theory_str_params, public theory_pb_params, public theory_datatype_params { bool m_display_proof; diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index a9f6ccc18..49a786e69 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -61,5 +61,6 @@ def_module_params(module_name='smt', ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'), ('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') + ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'), + ('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms') )) diff --git a/src/smt/params/theory_str_params.cpp b/src/smt/params/theory_str_params.cpp new file mode 100644 index 000000000..c1fcb0412 --- /dev/null +++ b/src/smt/params/theory_str_params.cpp @@ -0,0 +1,24 @@ +/*++ +Module Name: + + theory_str_params.cpp + +Abstract: + + Parameters for string theory plugin + +Author: + + Murphy Berzish (mtrberzi) 2016-12-13 + +Revision History: + +--*/ + +#include"theory_str_params.h" +#include"smt_params_helper.hpp" + +void theory_str_params::updt_params(params_ref const & _p) { + smt_params_helper p(_p); + m_AssertStrongerArrangements = p.str_strong_arrangements(); +} diff --git a/src/smt/params/theory_str_params.h b/src/smt/params/theory_str_params.h new file mode 100644 index 000000000..480ad1479 --- /dev/null +++ b/src/smt/params/theory_str_params.h @@ -0,0 +1,42 @@ +/*++ +Module Name: + + theory_str_params.h + +Abstract: + + Parameters for string theory plugin + +Author: + + Murphy Berzish (mtrberzi) 2016-12-13 + +Revision History: + +--*/ + +#ifndef THEORY_STR_PARAMS_H +#define THEORY_STR_PARAMS_H + +#include"params.h" + +struct theory_str_params { + /* + * If AssertStrongerArrangements is set to true, + * the implications that would normally be asserted during arrangement generation + * will instead be asserted as equivalences. + * This is a stronger version of the standard axiom. + * The Z3str2 axioms can be simulated by setting this to false. + */ + bool m_AssertStrongerArrangements; + + theory_str_params(params_ref const & p = params_ref()): + m_AssertStrongerArrangements(true) + { + updt_params(p); + } + + void updt_params(params_ref const & p); +}; + +#endif /* THEORY_STR_PARAMS_H */ diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 117b606fd..7cbfd0b2e 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -707,7 +707,7 @@ namespace smt { void setup::setup_QF_S() { m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); - m_context.register_plugin(alloc(smt::theory_str, m_manager)); + m_context.register_plugin(alloc(smt::theory_str, m_manager, m_params)); } bool is_arith(static_features const & st) { @@ -839,7 +839,7 @@ namespace smt { void setup::setup_str() { setup_arith(); - m_context.register_plugin(alloc(theory_str, m_manager)); + m_context.register_plugin(alloc(theory_str, m_manager, m_params)); } void setup::setup_unknown() { diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index b9e9e748f..4eb15d6ad 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -29,8 +29,9 @@ Revision History: namespace smt { -theory_str::theory_str(ast_manager & m): +theory_str::theory_str(ast_manager & m, theory_str_params const & params): theory(m.mk_family_id("str")), + m_params(params), /* Options */ opt_AggressiveLengthTesting(false), opt_AggressiveValueTesting(false), @@ -44,7 +45,6 @@ theory_str::theory_str(ast_manager & m): opt_CheckVariableScope(true), opt_UseFastLengthTesterCache(true), opt_UseFastValueTesterCache(true), - opt_AssertStrongerArrangements(false), /* Internal setup */ search_started(false), m_autil(m), @@ -2911,7 +2911,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { add_cut_info_merge(t1, sLevel, m); add_cut_info_merge(t1, sLevel, y); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); assert_axiom(ax_strong); } else { @@ -2963,7 +2963,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { add_cut_info_merge(t2, sLevel, x); add_cut_info_merge(t2, sLevel, n); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); assert_axiom(ax_strong); } else { @@ -3071,7 +3071,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { if (!arrangement_disjunction.empty()) { expr_ref premise(ctx.mk_eq_atom(concatAst1, concatAst2), mgr); expr_ref conclusion(mk_or(arrangement_disjunction), mgr); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(premise, conclusion), mgr); assert_axiom(ax_strong); } else { @@ -3272,7 +3272,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { add_cut_info_merge(temp1, sLevel, y); add_cut_info_merge(temp1, sLevel, m); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); assert_axiom(ax_strong); } else { @@ -3340,7 +3340,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { expr_ref ax_l(mk_and(l_items), mgr); expr_ref ax_r(mk_and(r_items), mgr); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); assert_axiom(ax_strong); } else { @@ -3404,7 +3404,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { if (!arrangement_disjunction.empty()) { expr_ref implyR(mk_or(arrangement_disjunction), mgr); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref implyLHS(ctx.mk_eq_atom(concatAst1, concatAst2), mgr); expr_ref ax_strong(ctx.mk_eq_atom(implyLHS, implyR), mgr); assert_axiom(ax_strong); @@ -3592,7 +3592,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { r_items.push_back(ctx.mk_eq_atom(x, prefixAst)); r_items.push_back(ctx.mk_eq_atom(y, suf_n_concat)); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, mk_and(r_items)), mgr); assert_axiom(ax_strong); } else { @@ -3612,7 +3612,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { expr_ref ax_l(mgr.mk_and(ax_l1, ax_l2), mgr); expr_ref ax_r(mgr.mk_and(ctx.mk_eq_atom(x, strAst), ctx.mk_eq_atom(y, n)), mgr); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); assert_axiom(ax_strong); } else { @@ -3650,7 +3650,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { add_cut_info_merge(temp1, sLevel, x); add_cut_info_merge(temp1, sLevel, n); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr); assert_axiom(ax_strong); } else { @@ -3731,7 +3731,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { if (!arrangement_disjunction.empty()) { expr_ref implyR(mk_or(arrangement_disjunction), mgr); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_lhs(ctx.mk_eq_atom(concatAst1, concatAst2), mgr); expr_ref ax_strong(ctx.mk_eq_atom(ax_lhs, implyR), mgr); assert_axiom(ax_strong); @@ -3813,7 +3813,7 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) { if (!in_same_eqc(tmpAst, n)) { // break down option 4-1 expr_ref implyR(ctx.mk_eq_atom(n, tmpAst), mgr); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -3825,7 +3825,7 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) { //break down option 4-2 expr_ref implyR(ctx.mk_eq_atom(n, y), mgr); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -3838,7 +3838,7 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) { if (!in_same_eqc(y, tmpAst)) { //break down option 4-3 expr_ref implyR(ctx.mk_eq_atom(y, tmpAst), mgr); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -3915,7 +3915,7 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { expr_ref x_deltaStr(mk_concat(x, m_strutil.mk_string(deltaStr)), mgr); if (!in_same_eqc(m, x_deltaStr)) { expr_ref implyR(ctx.mk_eq_atom(m, x_deltaStr), mgr); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -3926,7 +3926,7 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { // test if (!in_same_eqc(x, m)) { expr_ref implyR(ctx.mk_eq_atom(x, m), mgr); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -3938,7 +3938,7 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { expr_ref m_deltaStr(mk_concat(m, m_strutil.mk_string(deltaStr)), mgr); if (!in_same_eqc(x, m_deltaStr)) { expr_ref implyR(ctx.mk_eq_atom(x, m_deltaStr), mgr); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -4156,7 +4156,7 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { expr_ref implyR(mk_or(arrangement_disjunction), mgr); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr); assert_axiom(ax_strong); } else { @@ -6266,7 +6266,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { assert_axiom(negate_ast); } else { implyR1 = mk_or(arrangement_disjunction); - if (opt_AssertStrongerArrangements) { + if (m_params.m_AssertStrongerArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(implyL, implyR1), m); assert_axiom(ax_strong); } else { diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index b3667bdec..30bf0b080 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -18,6 +18,7 @@ Revision History: #define _THEORY_STR_H_ #include"smt_theory.h" +#include"theory_str_params.h" #include"trail.h" #include"th_rewriter.h" #include"value_factory.h" @@ -97,7 +98,7 @@ namespace smt { typedef map > string_map; protected: - // Some options that control how the solver operates. + theory_str_params const & m_params; /* * If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities @@ -189,15 +190,6 @@ namespace smt { */ bool opt_UseFastValueTesterCache; - /* - * If AssertStrongerArrangements is set to true, - * the implications that would normally be asserted during arrangement generation - * will instead be asserted as equivalences. - * This is a stronger version of the regular axiom. - * The default (Z3str2) behaviour is to set this to false. - */ - bool opt_AssertStrongerArrangements; - bool search_started; arith_util m_autil; str_util m_strutil; @@ -548,7 +540,7 @@ namespace smt { void refresh_theory_var(expr * e); public: - theory_str(ast_manager & m); + theory_str(ast_manager & m, theory_str_params const & params); virtual ~theory_str(); virtual char const * get_name() const { return "strings"; } @@ -569,7 +561,7 @@ namespace smt { virtual void new_eq_eh(theory_var, theory_var); virtual void new_diseq_eh(theory_var, theory_var); - virtual theory* mk_fresh(context*) { return alloc(theory_str, get_manager()); } + virtual theory* mk_fresh(context*) { return alloc(theory_str, get_manager(), m_params); } virtual void init_search_eh(); virtual void relevant_eh(app * n); virtual void assign_eh(bool_var v, bool is_true);