diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 32b634626..8901697b7 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -26,6 +26,7 @@ Revision History: #include "smt/params/theory_array_params.h" #include "smt/params/theory_bv_params.h" #include "smt/params/theory_str_params.h" +#include "smt/params/theory_seq_params.h" #include "smt/params/theory_pb_params.h" #include "smt/params/theory_datatype_params.h" #include "smt/params/preprocessor_params.h" @@ -79,6 +80,7 @@ struct smt_params : public preprocessor_params, public theory_array_params, public theory_bv_params, public theory_str_params, + public theory_seq_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 816764896..3f4105c34 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -71,6 +71,7 @@ def_module_params(module_name='smt', ('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'), + ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'), ('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/params/theory_seq_params.cpp b/src/smt/params/theory_seq_params.cpp new file mode 100644 index 000000000..e521298d3 --- /dev/null +++ b/src/smt/params/theory_seq_params.cpp @@ -0,0 +1,23 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + theory_seq_params.cpp + +Abstract: + + Parameters for sequence theory plugin + +Revision History: + + +--*/ + +#include "smt/params/theory_seq_params.h" +#include "smt/params/smt_params_helper.hpp" + +void theory_seq_params::updt_params(params_ref const & _p) { + smt_params_helper p(_p); + m_split_w_len = p.seq_split_w_len(); +} diff --git a/src/smt/params/theory_seq_params.h b/src/smt/params/theory_seq_params.h new file mode 100644 index 000000000..24e67b8ff --- /dev/null +++ b/src/smt/params/theory_seq_params.h @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + theory_seq_params.h + +Abstract: + + Parameters for sequence theory plugin + +Revision History: + + +--*/ + +#ifndef THEORY_SEQ_PARAMS_H +#define THEORY_SEQ_PARAMS_H + +#include "util/params.h" + +struct theory_seq_params { + /* + * Enable splitting guided by length constraints + */ + bool m_split_w_len; + + + theory_seq_params(params_ref const & p = params_ref()): + m_split_w_len(true) + { + updt_params(p); + } + + void updt_params(params_ref const & p); +}; + +#endif /* THEORY_SEQ_PARAMS_H */ diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 294aa7b08..6e996e409 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -222,7 +222,7 @@ namespace smt { void setup::setup_QF_BVRE() { setup_QF_BV(); setup_QF_LIA(); - m_context.register_plugin(alloc(theory_seq, m_manager)); + m_context.register_plugin(alloc(theory_seq, m_manager, m_params)); } void setup::setup_QF_UF(static_features const & st) { @@ -895,7 +895,7 @@ namespace smt { } void setup::setup_seq() { - m_context.register_plugin(alloc(smt::theory_seq, m_manager)); + m_context.register_plugin(alloc(smt::theory_seq, m_manager, m_params)); } void setup::setup_unknown() { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 26ab92665..ffa0b857a 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -191,9 +191,10 @@ void theory_seq::exclusion_table::display(std::ostream& out) const { } -theory_seq::theory_seq(ast_manager& m): +theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params): theory(m.mk_family_id("seq")), m(m), + m_params(params), m_rep(m, m_dm), m_reset_cache(false), m_eq_id(0), @@ -273,7 +274,7 @@ final_check_status theory_seq::final_check_eh() { TRACE("seq", tout << ">>zero_length\n";); return FC_CONTINUE; } - if (len_based_split()) { + if (m_params.m_split_w_len && len_based_split()) { ++m_stats.m_branch_variable; TRACE("seq", tout << ">>split_based_on_length\n";); return FC_CONTINUE; diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index b5ce30236..f32b6254b 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -49,6 +49,8 @@ namespace smt { typedef union_find th_union_find; class seq_value_proc; + + theory_seq_params const & m_params; // cache to track evaluations under equalities class eval_cache { @@ -361,7 +363,7 @@ namespace smt { void pop_scope_eh(unsigned num_scopes) override; void restart_eh() override; void relevant_eh(app* n) override; - theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager()); } + theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), m_params); } char const * get_name() const override { return "seq"; } theory_var mk_var(enode* n) override; void apply_sort_cnstr(enode* n, sort* s) override; @@ -621,7 +623,7 @@ namespace smt { void display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const; void display_nc(std::ostream& out, nc const& nc) const; public: - theory_seq(ast_manager& m); + theory_seq(ast_manager& m, theory_seq_params const & params); ~theory_seq() override; // model building