diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index db09552ef..412e7b13d 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3211,11 +3211,11 @@ namespace smt { m_assumptions.reset(); } - void context::mk_unsat_core() { + lbool context::mk_unsat_core() { SASSERT(inconsistent()); if (!tracking_assumptions()) { SASSERT(m_assumptions.empty()); - return; + return l_false; } uint_set already_found_assumptions; literal_vector::const_iterator it = m_conflict_resolution->begin_unsat_core(); @@ -3240,7 +3240,19 @@ namespace smt { for (unsigned i = 0; i < sz; i++) { tout << mk_pp(m_unsat_core.get(i), m_manager) << "\n"; }); - validate_unsat_core(); + validate_unsat_core(); + // theory validation of unsat core + + ptr_vector::iterator th_it = m_theory_set.begin(); + ptr_vector::iterator th_end = m_theory_set.end(); + for (; th_it != th_end; ++th_it) { + lbool theory_result = (*th_it)->validate_unsat_core(m_unsat_core); + if (theory_result == l_undef) { + return l_undef; + } + } + + return l_false; } /** @@ -3267,45 +3279,6 @@ namespace smt { if (r == l_true && get_cancel_flag()) { r = l_undef; } - - /* - // PATCH for theory_str: - // UNSAT + overlapping variables => UNKNOWN - 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; } @@ -3323,23 +3296,6 @@ namespace smt { 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); - } - */ - expr_ref_vector theory_assumptions(m_manager); ptr_vector::iterator it = m_theory_set.begin(); ptr_vector::iterator end = m_theory_set.end(); @@ -3413,7 +3369,7 @@ namespace smt { (*it)->setup(); } - lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel) { + lbool context::check(unsigned ext_num_assumptions, expr * const * ext_assumptions, bool reset_cancel) { m_stats.m_num_checks++; TRACE("check_bug", tout << "STARTING check(num_assumptions, assumptions)\n"; tout << "inconsistent: " << inconsistent() << ", m_unsat_core.empty(): " << m_unsat_core.empty() << "\n"; @@ -3424,6 +3380,22 @@ namespace smt { m_unsat_core.reset(); if (!check_preamble(reset_cancel)) return l_undef; + + expr_ref_vector theory_assumptions(m_manager); + for (unsigned i = 0; i < ext_num_assumptions; ++i) { + theory_assumptions.push_back(ext_assumptions[i]); + } + ptr_vector::iterator it = m_theory_set.begin(); + ptr_vector::iterator end = m_theory_set.end(); + for (; it != end; ++it) { + (*it)->add_theory_assumptions(theory_assumptions); + } + if (!theory_assumptions.empty()) { + TRACE("search", tout << "Adding theory assumptions to context" << std::endl;); + } + unsigned num_assumptions = theory_assumptions.size(); + expr * const * assumptions = theory_assumptions.c_ptr(); + if (!validate_assumptions(num_assumptions, assumptions)) return l_undef; TRACE("check_bug", tout << "inconsistent: " << inconsistent() << ", m_unsat_core.empty(): " << m_unsat_core.empty() << "\n";); @@ -3447,13 +3419,13 @@ namespace smt { TRACE("after_internalization", display(tout);); if (inconsistent()) { VERIFY(!resolve_conflict()); // build the proof - mk_unsat_core(); - r = l_false; + r = mk_unsat_core(); } else { r = search(); - if (r == l_false) - mk_unsat_core(); + if (r == l_false) { + r = mk_unsat_core(); // validation may change an l_false to l_undef here + } } } } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 0667f622e..0943662e8 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1094,7 +1094,7 @@ namespace smt { void reset_assumptions(); - void mk_unsat_core(); + lbool mk_unsat_core(); void validate_unsat_core(); diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index e412f2f1b..ff29c7413 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -199,6 +199,14 @@ namespace smt { return FC_DONE; } + /** + \brief This method is called from the smt_context when an unsat core is generated. + The theory may change the answer to UNKNOWN by returning l_undef from this method. + */ + virtual lbool validate_unsat_core(expr_ref_vector & unsat_core) { + return l_false; + } + /** \brief Parametric theories (e.g. Arrays) should implement this method. See example in context::is_shared diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 354589318..bddd0b78e 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -7302,6 +7302,28 @@ void theory_str::add_theory_assumptions(expr_ref_vector & assumptions) { assumptions.push_back(get_manager().mk_not(m_theoryStrOverlapAssumption_term)); } +lbool theory_str::validate_unsat_core(expr_ref_vector & unsat_core) { + bool assumptionFound = false; + + app * target_term = to_app(get_manager().mk_not(m_theoryStrOverlapAssumption_term)); + internalize_term(target_term); + for (unsigned i = 0; i < unsat_core.size(); ++i) { + app * core_term = to_app(unsat_core.get(i)); + // not sure if this is the correct way to compare terms in this context + enode * e1; + enode * e2; + e1 = get_context().get_enode(target_term); + e2 = get_context().get_enode(core_term); + if (e1 == e2) { + TRACE("t_str", tout << "overlap detected in unsat core, changing UNSAT to UNKNOWN" << std::endl;); + assumptionFound = true; + return l_undef; + } + } + + return l_false; +} + void theory_str::init_search_eh() { ast_manager & m = get_manager(); context & ctx = get_context(); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 3c273d4e2..7c2df9e12 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -629,6 +629,7 @@ namespace smt { virtual theory* mk_fresh(context*) { return alloc(theory_str, get_manager(), m_params); } virtual void init_search_eh(); virtual void add_theory_assumptions(expr_ref_vector & assumptions); + virtual lbool validate_unsat_core(expr_ref_vector & unsat_core); virtual void relevant_eh(app * n); virtual void assign_eh(bool_var v, bool is_true); virtual void push_scope_eh();