mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
pre-init assumptions and unsat core validation for smt theories
This commit is contained in:
parent
2642ef47ce
commit
a1bb1f2a13
|
@ -3072,11 +3072,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();
|
||||
|
@ -3101,7 +3101,17 @@ 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<theory>::iterator th_it = m_theory_set.begin();
|
||||
ptr_vector<theory>::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;
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -3144,6 +3154,14 @@ namespace smt {
|
|||
SASSERT(m_scope_lvl == 0);
|
||||
SASSERT(!m_setup.already_configured());
|
||||
setup_context(m_fparams.m_auto_config);
|
||||
|
||||
expr_ref_vector theory_assumptions(m_manager);
|
||||
get_theory_assumptions(theory_assumptions);
|
||||
if (!theory_assumptions.empty()) {
|
||||
TRACE("search", tout << "Adding theory assumptions to context" << std::endl;);
|
||||
return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel, true);
|
||||
}
|
||||
|
||||
internalize_assertions();
|
||||
lbool r = l_undef;
|
||||
if (m_asserted_formulas.inconsistent()) {
|
||||
|
@ -3205,7 +3223,15 @@ namespace smt {
|
|||
(*it)->setup();
|
||||
}
|
||||
|
||||
lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel) {
|
||||
void context::get_theory_assumptions(expr_ref_vector & theory_assumptions) {
|
||||
ptr_vector<theory>::iterator it = m_theory_set.begin();
|
||||
ptr_vector<theory>::iterator end = m_theory_set.end();
|
||||
for (; it != end; ++it) {
|
||||
(*it)->add_theory_assumptions(theory_assumptions);
|
||||
}
|
||||
}
|
||||
|
||||
lbool context::check(unsigned ext_num_assumptions, expr * const * ext_assumptions, bool reset_cancel, bool already_did_theory_assumptions) {
|
||||
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";
|
||||
|
@ -3216,6 +3242,22 @@ namespace smt {
|
|||
m_unsat_core.reset();
|
||||
if (!check_preamble(reset_cancel))
|
||||
return l_undef;
|
||||
|
||||
expr_ref_vector all_assumptions(m_manager);
|
||||
for (unsigned i = 0; i < ext_num_assumptions; ++i) {
|
||||
all_assumptions.push_back(ext_assumptions[i]);
|
||||
}
|
||||
if (!already_did_theory_assumptions) {
|
||||
ptr_vector<theory>::iterator it = m_theory_set.begin();
|
||||
ptr_vector<theory>::iterator end = m_theory_set.end();
|
||||
for (; it != end; ++it) {
|
||||
(*it)->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";);
|
||||
|
|
|
@ -1059,7 +1059,9 @@ namespace smt {
|
|||
|
||||
void reset_assumptions();
|
||||
|
||||
void mk_unsat_core();
|
||||
void get_theory_assumptions(expr_ref_vector & theory_assumptions);
|
||||
|
||||
lbool mk_unsat_core();
|
||||
|
||||
void validate_unsat_core();
|
||||
|
||||
|
@ -1441,7 +1443,7 @@ namespace smt {
|
|||
|
||||
void pop(unsigned num_scopes);
|
||||
|
||||
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true);
|
||||
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true, bool already_did_theory_assumptions = false);
|
||||
|
||||
lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed);
|
||||
|
||||
|
|
|
@ -177,6 +177,22 @@ namespace smt {
|
|||
virtual void restart_eh() {
|
||||
}
|
||||
|
||||
/**
|
||||
\brief This method is called by smt_context before the search starts
|
||||
to get any extra assumptions the theory wants to use.
|
||||
(See theory_str for an example)
|
||||
*/
|
||||
virtual void add_theory_assumptions(expr_ref_vector & assumptions) {
|
||||
}
|
||||
|
||||
/**
|
||||
\brief This method is called from 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 This method is invoked before the search starts.
|
||||
*/
|
||||
|
|
Loading…
Reference in a new issue