mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

initialize additional assumptions after setup_context is called the first time

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-25 12:50:11 -08:00
parent 36204fafa0
commit 5bc4c9809e
1 changed files with 24 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
src/smt/smt_context.cpp
View file

@ -3202,10 +3202,8 @@ namespace smt {
}); });
validate_unsat_core(); validate_unsat_core();
// theory validation of unsat core // theory validation of unsat core
ptr_vector<theory>::iterator th_it = m_theory_set.begin(); for (theory* th : m_theory_set) {
ptr_vector<theory>::iterator th_end = m_theory_set.end(); lbool theory_result = th->validate_unsat_core(m_unsat_core);
for (; th_it != th_end; ++th_it) {
lbool theory_result = (*th_it)->validate_unsat_core(m_unsat_core);
if (theory_result == l_undef) { if (theory_result == l_undef) {
return l_undef; return l_undef;
} }
@ -3296,10 +3294,8 @@ namespace smt {
#ifndef _EXTERNAL_RELEASE #ifndef _EXTERNAL_RELEASE
if (m_fparams.m_display_installed_theories) { if (m_fparams.m_display_installed_theories) {
std::cout << "(theories"; std::cout << "(theories";
ptr_vector<theory>::iterator it = m_theory_set.begin(); for (theory* th : m_theory_set) {
ptr_vector<theory>::iterator end = m_theory_set.end(); std::cout << " " << th->get_name();
for (; it != end; ++it) {
std::cout << " " << (*it)->get_name();
} }
std::cout << ")" << std::endl; std::cout << ")" << std::endl;
} }
@ -3316,17 +3312,13 @@ namespace smt {
m_fparams.m_relevancy_lemma = false; m_fparams.m_relevancy_lemma = false;
// setup all the theories // setup all the theories
ptr_vector<theory>::iterator it = m_theory_set.begin(); for (theory* th : m_theory_set)
ptr_vector<theory>::iterator end = m_theory_set.end(); th->setup();
for (; it != end; ++it)
(*it)->setup();
} }
void context::add_theory_assumptions(expr_ref_vector & theory_assumptions) { void context::add_theory_assumptions(expr_ref_vector & theory_assumptions) {
ptr_vector<theory>::iterator it = m_theory_set.begin(); for (theory* th : m_theory_set) {
ptr_vector<theory>::iterator end = m_theory_set.end(); th->add_theory_assumptions(theory_assumptions);
for (; it != end; ++it) {
(*it)->add_theory_assumptions(theory_assumptions);
} }
} }
@ -3342,18 +3334,7 @@ namespace smt {
if (!check_preamble(reset_cancel)) if (!check_preamble(reset_cancel))
return l_undef; return l_undef;
expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions);
if (!already_did_theory_assumptions) {
add_theory_assumptions(all_assumptions);
}
unsigned num_assumptions = all_assumptions.size();
expr * const * assumptions = all_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";); TRACE("check_bug", tout << "inconsistent: " << inconsistent() << ", m_unsat_core.empty(): " << m_unsat_core.empty() << "\n";);
TRACE("unsat_core_bug", for (unsigned i = 0; i < num_assumptions; i++) { tout << mk_pp(assumptions[i], m_manager) << "\n";});
pop_to_base_lvl(); pop_to_base_lvl();
TRACE("before_search", display(tout);); TRACE("before_search", display(tout););
SASSERT(at_base_level()); SASSERT(at_base_level());
@ -3363,6 +3344,18 @@ namespace smt {
} }
else { else {
setup_context(false); setup_context(false);
expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions);
if (!already_did_theory_assumptions) {
add_theory_assumptions(all_assumptions);
}
unsigned num_assumptions = all_assumptions.size();
expr * const * assumptions = all_assumptions.c_ptr();
if (!validate_assumptions(num_assumptions, assumptions))
return l_undef;
TRACE("unsat_core_bug", tout << all_assumptions << "\n";);
internalize_assertions(); internalize_assertions();
TRACE("after_internalize_assertions", display(tout);); TRACE("after_internalize_assertions", display(tout););
if (m_asserted_formulas.inconsistent()) { if (m_asserted_formulas.inconsistent()) {
@ -3551,10 +3544,9 @@ namespace smt {
pop_scope(m_scope_lvl - curr_lvl); pop_scope(m_scope_lvl - curr_lvl);
SASSERT(at_search_level()); SASSERT(at_search_level());
} }
ptr_vector<theory>::iterator it = m_theory_set.begin(); for (theory* th : m_theory_set) {
ptr_vector<theory>::iterator end = m_theory_set.end(); if (!inconsistent()) th->restart_eh();
for (; it != end && !inconsistent(); ++it) }
(*it)->restart_eh();
TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";); TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";);
if (!inconsistent()) { if (!inconsistent()) {
m_qmanager->restart_eh(); m_qmanager->restart_eh();
@ -4070,10 +4062,7 @@ namespace smt {
bool include = false; bool include = false;
if (at_lbls) { if (at_lbls) {
// include if there is a label with the '@' sign. // include if there is a label with the '@' sign.
buffer<symbol>::const_iterator it = lbls.begin(); for (symbol const& s : lbls) {
buffer<symbol>::const_iterator end = lbls.end();
for (; it != end; ++it) {
symbol const & s = *it;
if (s.contains('@')) { if (s.contains('@')) {
include = true; include = true;
break; break;