diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index a9a91ab2a..a822be37a 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1767,6 +1767,7 @@ void ast_manager::delete_node(ast * n) { TRACE("ast", tout << "Deleting object " << n->m_id << " " << n << "\n";); CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";); TRACE("mk_var_bug", tout << "del_ast: " << n->m_id << "\n";); + TRACE("t_str_refcount_hack", tout << "delete ast " << n->m_id << std::endl;); TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";); SASSERT(m_ast_table.contains(n)); diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 8222c3d60..a5b3e4867 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -31,6 +31,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_restart_strategy = static_cast(p.restart_strategy()); m_restart_factor = p.restart_factor(); m_case_split_strategy = static_cast(p.case_split()); + m_theory_case_split = p.theory_case_split(); m_delay_units = p.delay_units(); m_delay_units_threshold = p.delay_units_threshold(); m_preprocess = _p.get_bool("preprocess", true); // hidden parameter diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 27071bd9e..55346d34f 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -111,6 +111,7 @@ struct smt_params : public preprocessor_params, case_split_strategy m_case_split_strategy; unsigned m_rel_case_split_order; bool m_lookahead_diseq; + bool m_theory_case_split; // ----------------------------------- // @@ -241,6 +242,7 @@ struct smt_params : public preprocessor_params, m_case_split_strategy(CS_ACTIVITY_DELAY_NEW), m_rel_case_split_order(0), m_lookahead_diseq(false), + m_theory_case_split(false), m_delay_units(false), m_delay_units_threshold(32), m_theory_resolve(false), diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index cf861a28a..3f2c6a54a 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -67,6 +67,6 @@ def_module_params(module_name='smt', ('str.aggressive_value_testing', BOOL, False, 'prioritize testing concrete string constant values over generating more options'), ('str.aggressive_unroll_testing', BOOL, True, 'prioritize testing concrete regex unroll counts over generating more options'), ('str.fast_length_tester_cache', BOOL, False, 'cache length tester constants instead of regenerating them'), - ('str.fast_value_tester_cache', BOOL, True, 'cache value tester constants instead of regenerating them') - + ('str.fast_value_tester_cache', BOOL, True, 'cache value tester constants instead of regenerating them'), + ('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.') )) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 8958eae5f..741525dd2 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2377,6 +2377,9 @@ namespace smt { */ unsigned context::pop_scope_core(unsigned num_scopes) { + TRACE("t_str_refcount_hack", tout << "begin pop_scope_core in smt_context" << std::endl;); + + if (m_manager.has_trace_stream()) m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n"; @@ -2423,8 +2426,11 @@ namespace smt { ptr_vector::iterator it = m_theory_set.begin(); ptr_vector::iterator end = m_theory_set.end(); - for (; it != end; ++it) + for (; it != end; ++it) { + TRACE("t_str_refcount_hack", tout << "begin theory pop_scope_eh" << std::endl;); (*it)->pop_scope_eh(num_scopes); + TRACE("t_str_refcount_hack", tout << "end theory pop_scope_eh" << std::endl;); + } del_justifications(m_justifications, s.m_justifications_lim); @@ -2450,6 +2456,9 @@ namespace smt { reassert_units(units_to_reassert_lim); TRACE("pop_scope_detail", tout << "end of pop_scope: \n"; display(tout);); CASSERT("context", check_invariant()); + + TRACE("t_str_refcount_hack", tout << "end pop_scope_core in smt_context" << std::endl;); + return num_bool_vars; } diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 503485293..25a045ee8 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1805,6 +1805,7 @@ void theory_str::reset_eh() { * Then add an assertion: (y2 == (Concat ce m2)) AND ("str3" == (Concat abc x2)) -> (y2 != "str3") */ bool theory_str::new_eq_check(expr * lhs, expr * rhs) { + TRACE("t_str_refcount_hack", tout << "begin new_eq_check in theory_str" << std::endl;); context & ctx = get_context(); ast_manager & m = get_manager(); @@ -1830,6 +1831,7 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) { expr_ref to_assert(m.mk_not(ctx.mk_eq_atom(eqc_nn1, eqc_nn2)), m); assert_axiom(to_assert); // this shouldn't use the integer theory at all, so we don't allow the option of quick-return + TRACE("t_str_refcount_hack", tout << "end new_eq_check in theory_str" << std::endl;); return false; } if (!check_length_consistency(eqc_nn1, eqc_nn2)) { @@ -1837,6 +1839,7 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) { if (opt_NoQuickReturn_IntegerTheory){ TRACE("t_str_detail", tout << "continuing in new_eq_check() due to opt_NoQuickReturn_IntegerTheory" << std::endl;); } else { + TRACE("t_str_refcount_hack", tout << "end new_eq_check in theory_str" << std::endl;); return false; } } @@ -1855,6 +1858,7 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) { } // okay, all checks here passed + TRACE("t_str_refcount_hack", tout << "end new_eq_check in theory_str" << std::endl;); return true; } @@ -6859,14 +6863,20 @@ void theory_str::check_variable_scope() { } void theory_str::pop_scope_eh(unsigned num_scopes) { + TRACE("t_str_refcount_hack", tout << "begin pop_scope_eh in theory_str" << std::endl;); + sLevel -= num_scopes; TRACE("t_str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;); // TODO: figure out what's going out of scope and why context & ctx = get_context(); ast_manager & m = get_manager(); + // { // expr_ref_vector assignments(m); // ctx.get_assignments(assignments); + // TRACE("t_str_refcount_hack", tout << "assignment vector about to go out of scope" << std::endl;); + // } + // TRACE("t_str_refcount_hack", tout << "assignment vector has gone out of scope" << std::endl;); TRACE_CODE(if (is_trace_enabled("t_str_dump_assign_on_scope_change")) { dump_assignments(); }); @@ -6937,6 +6947,8 @@ void theory_str::pop_scope_eh(unsigned num_scopes) { theory::pop_scope_eh(num_scopes); //check_variable_scope(); + + TRACE("t_str_refcount_hack", tout << "end pop_scope_eh in theory_str" << std::endl;); } void theory_str::dump_assignments() {