mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix #6343
The bug was that axiom generation was not enabled on last_index, so no axioms got created to constrain last-index. With default settings the solver is now very slow on this example. It is related to that the smallest size of a satisfying assignment is above 24. Pending a good heuristic to find initial seeds and increments for iterative deepening, I am adding another parameter smt.seq.min_unfolding that when set to 30 helps for this example.
This commit is contained in:
parent
16ef89905d
commit
c47ca341b7
|
@ -509,6 +509,8 @@ namespace seq {
|
|||
}
|
||||
|
||||
/**
|
||||
i = last_indexof(t, s):
|
||||
|
||||
!contains(t, s) => i = -1
|
||||
|t| = 0 => |s| = 0 or i = -1
|
||||
|t| = 0 & |s| = 0 => i = 0
|
||||
|
|
|
@ -107,6 +107,7 @@ def_module_params(module_name='smt',
|
|||
('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'),
|
||||
('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'),
|
||||
('seq.max_unfolding', UINT, 1000000000, 'maximal unfolding depth for checking string equations and regular expressions'),
|
||||
('seq.min_unfolding', UINT, 1, 'initial bound for strings whose lengths are bounded by iterative deepening. Set this to a higher value if there are only models with larger string lengths'),
|
||||
('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'),
|
||||
|
|
|
@ -22,4 +22,5 @@ void theory_seq_params::updt_params(params_ref const & _p) {
|
|||
m_split_w_len = p.seq_split_w_len();
|
||||
m_seq_validate = p.seq_validate();
|
||||
m_seq_max_unfolding = p.seq_max_unfolding();
|
||||
m_seq_min_unfolding = p.seq_min_unfolding();
|
||||
}
|
||||
|
|
|
@ -25,6 +25,7 @@ struct theory_seq_params {
|
|||
bool m_split_w_len = false;
|
||||
bool m_seq_validate = false;
|
||||
unsigned m_seq_max_unfolding = UINT_MAX/4;
|
||||
unsigned m_seq_min_unfolding = 1;
|
||||
|
||||
theory_seq_params(params_ref const & p = params_ref()) {
|
||||
updt_params(p);
|
||||
|
|
|
@ -304,6 +304,7 @@ void theory_seq::init() {
|
|||
m_ax.add_axiom5 = add_ax;
|
||||
m_ax.mk_eq_empty2 = mk_eq_emp;
|
||||
m_arith_value.init(&ctx);
|
||||
m_max_unfolding_depth = ctx.get_fparams().m_seq_min_unfolding;
|
||||
}
|
||||
|
||||
#define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(20, verbose_stream() << s << "\n"); }
|
||||
|
@ -3256,6 +3257,7 @@ void theory_seq::relevant_eh(app* n) {
|
|||
m_util.str.is_from_code(n) ||
|
||||
m_util.str.is_to_code(n) ||
|
||||
m_util.str.is_unit(n) ||
|
||||
m_util.str.is_last_index(n) ||
|
||||
m_util.str.is_length(n) ||
|
||||
/* m_util.str.is_replace_all(n) || uncomment to enable axiomatization */
|
||||
m_util.str.is_le(n)) {
|
||||
|
|
Loading…
Reference in a new issue