diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 4fd027031..dfe396f2b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -37,7 +37,7 @@ Revision History: #include"model_pp.h" #include"ast_smt2_pp.h" #include"ast_translation.h" -#include"theory_str.h" +#include"theory_seq.h" namespace smt { @@ -76,6 +76,8 @@ namespace smt { m_unsat_proof(m), m_unknown("unknown"), m_unsat_core(m), + m_use_theory_str_overlap_assumption(false), + m_theoryStrOverlapAssumption_term(m_manager), #ifdef Z3DEBUG m_trail_enabled(true), #endif @@ -3269,21 +3271,38 @@ namespace smt { // PATCH for theory_str: // UNSAT + overlapping variables => UNKNOWN - if (r == l_false) { - ptr_vector::iterator it = m_theory_set.begin(); - ptr_vector::iterator end = m_theory_set.end(); - for (; it != end; ++it) { - theory * th = *it; - if (strcmp(th->get_name(), "strings") == 0) { - theory_str * str = (theory_str*)th; - if (str->overlapping_variables_detected()) { - TRACE("t_str", tout << "WARNING: overlapping variables detected, UNSAT changed to UNKNOWN!" << std::endl;); - TRACE("context", tout << "WARNING: overlapping variables detected in theory_str. UNSAT changed to UNKNOWN!" << std::endl;); - r = l_undef; - } + if (r == l_false && use_theory_str_overlap_assumption()) { + // check the unsat core for an assumption from theory_str relating to overlaps. + // if we find this assumption, we have to answer UNKNOWN + // otherwise, we can pass through UNSAT + TRACE("t_str", tout << "unsat core:\n"; + unsigned sz = m_unsat_core.size(); + for (unsigned i = 0; i < sz; i++) { + tout << mk_pp(m_unsat_core.get(i), m_manager) << "\n"; + }); + + bool assumptionFound = false; + unsigned sz = m_unsat_core.size(); + app * target_term = to_app(m_manager.mk_not(m_theoryStrOverlapAssumption_term)); + internalize_term(target_term); + for (unsigned i = 0; i < sz; ++i) { + app * core_term = to_app(m_unsat_core.get(i)); + // not sure if this is the correct way to compare exprs in this context + enode * e1; + enode * e2; + e1 = get_enode(target_term); + e2 = get_enode(core_term); + if (e1 == e2) { + // found match + TRACE("t_str", tout << "overlap detected in unsat core; changing UNSAT to UNKNOWN" << std::endl;); + assumptionFound = true; + r = l_undef; break; } } + if (!assumptionFound) { + TRACE("t_str", tout << "no overlaps detected in unsat core, answering UNSAT" << std::endl;); + } } return r; @@ -3302,6 +3321,22 @@ namespace smt { SASSERT(m_scope_lvl == 0); SASSERT(!m_setup.already_configured()); setup_context(m_fparams.m_auto_config); + + // theory_str requires the context to be set up with a special assumption. + // we need to wait until after setup_context() to know whether this is the case + if (m_use_theory_str_overlap_assumption) { + TRACE("t_str", tout << "enabling theory_str overlap assumption" << std::endl;); + // TODO maybe refactor this a bit + symbol strOverlap("!!TheoryStrOverlapAssumption!!"); + expr_ref_vector assumption(get_manager()); + seq_util m_sequtil(m_manager); + sort * s = m_manager.mk_bool_sort(); + m_theoryStrOverlapAssumption_term = expr_ref(m_manager.mk_const(strOverlap, s), m_manager); + assumption.push_back(m_manager.mk_not(m_theoryStrOverlapAssumption_term)); + // this might work, even though we already did a bit of setup + return check(assumption.size(), assumption.c_ptr(), reset_cancel); + } + internalize_assertions(); lbool r = l_undef; if (m_asserted_formulas.inconsistent()) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 47ed5d671..0cf3f8d68 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -226,6 +226,9 @@ namespace smt { literal2assumption m_literal2assumption; // maps an expression associated with a literal to the original assumption expr_ref_vector m_unsat_core; + // Unsat core assumption hint for theory_str + bool m_use_theory_str_overlap_assumption; + // ----------------------------------- // // Theory case split @@ -846,6 +849,23 @@ namespace smt { */ void add_theory_aware_branching_info(bool_var v, double priority, lbool phase); + // unsat core assumption hint for theory_str + void set_use_theory_str_overlap_assumption(bool f) { + m_use_theory_str_overlap_assumption = f; + } + + bool use_theory_str_overlap_assumption() const { + return m_use_theory_str_overlap_assumption; + } + + expr_ref get_theory_str_overlap_assumption_term() { + return m_theoryStrOverlapAssumption_term; + } + + protected: + expr_ref m_theoryStrOverlapAssumption_term; + public: + // helper function for trail void undo_th_case_split(literal l); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 78a295e27..fdcf33c0e 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -706,6 +706,7 @@ namespace smt { } void setup::setup_QF_S() { + m_context.set_use_theory_str_overlap_assumption(true); m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_str, m_manager, m_params)); } @@ -841,6 +842,7 @@ namespace smt { void setup::setup_str() { setup_arith(); + m_context.set_use_theory_str_overlap_assumption(true); m_context.register_plugin(alloc(theory_str, m_manager, m_params)); } diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index ff32e6f38..b69ebda4c 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4304,6 +4304,8 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { add_nonempty_constraint(commonVar); } + bool overlapAssumptionUsed = false; + expr_ref_vector arrangement_disjunction(mgr); int pos = 1; @@ -4339,6 +4341,12 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { } else { TRACE("t_str", tout << "AVOID LOOP: SKIPPED." << std::endl;); TRACE("t_str", print_cut_var(m, tout); print_cut_var(y, tout);); + + // only add the overlap assumption one time + if (!overlapAssumptionUsed) { + arrangement_disjunction.push_back(ctx.get_theory_str_overlap_assumption_term()); + overlapAssumptionUsed = true; + } } } @@ -7239,6 +7247,9 @@ void theory_str::init_search_eh() { ast_manager & m = get_manager(); context & ctx = get_context(); + // safety + SASSERT(ctx.use_theory_str_overlap_assumption()); + TRACE("t_str_detail", tout << "dumping all asserted formulas:" << std::endl; unsigned nFormulas = ctx.get_num_asserted_formulas(); @@ -7301,6 +7312,7 @@ void theory_str::new_eq_eh(theory_var x, theory_var y) { //TRACE("t_str_detail", tout << "new eq: v#" << x << " = v#" << y << std::endl;); TRACE("t_str", tout << "new eq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " = " << mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;); + /* if (m_find.find(x) == m_find.find(y)) { return; diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 3ea4db7d4..a8857de24 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -389,7 +389,6 @@ namespace smt { // finite model finding data // maps a finite model tester var to a list of variables that will be tested obj_map > finite_model_test_varlists; - protected: void assert_axiom(expr * e); void assert_implication(expr * premise, expr * conclusion);