mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

revert change to setup_context that delays it until there are assertions

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-21 11:53:46 +01:00
parent db9f45dfec
commit da6a5facca
3 changed files with 9 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_consequences.cpp
View file

@ -533,7 +533,7 @@ namespace smt {
lbool context::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) { lbool context::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
pop_to_base_lvl(); pop_to_base_lvl();
cores.reset(); cores.reset();
setup_context(false, !asms.empty()); setup_context(false);
internalize_assertions(); internalize_assertions();
if (m_asserted_formulas.inconsistent() || inconsistent()) { if (m_asserted_formulas.inconsistent() || inconsistent()) {
return l_false; return l_false;

17
src/smt/smt_context.cpp
View file

@ -177,7 +177,7 @@ namespace smt {
dst_ctx.assert_expr(fml1); dst_ctx.assert_expr(fml1);
} }
dst_ctx.setup_context(dst_ctx.m_fparams.m_auto_config, true); dst_ctx.setup_context(dst_ctx.m_fparams.m_auto_config);
dst_ctx.internalize_assertions(); dst_ctx.internalize_assertions();
dst_ctx.copy_user_propagator(src_ctx, true); dst_ctx.copy_user_propagator(src_ctx, true);
@ -2908,7 +2908,7 @@ namespace smt {
user_propagator::push_eh_t& push_eh, user_propagator::push_eh_t& push_eh,
user_propagator::pop_eh_t& pop_eh, user_propagator::pop_eh_t& pop_eh,
user_propagator::fresh_eh_t& fresh_eh) { user_propagator::fresh_eh_t& fresh_eh) {
setup_context(false, true); setup_context(false);
m_user_propagator = alloc(theory_user_propagator, *this); m_user_propagator = alloc(theory_user_propagator, *this);
m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh); m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
for (unsigned i = m_scopes.size(); i-- > 0; ) for (unsigned i = m_scopes.size(); i-- > 0; )
@ -3004,7 +3004,7 @@ namespace smt {
void context::push() { void context::push() {
pop_to_base_lvl(); pop_to_base_lvl();
setup_context(false, false); setup_context(false);
bool was_consistent = !inconsistent(); bool was_consistent = !inconsistent();
try { try {
internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
@ -3611,7 +3611,7 @@ namespace smt {
if (!check_preamble(reset_cancel)) return l_undef; if (!check_preamble(reset_cancel)) return l_undef;
SASSERT(m_scope_lvl == 0); SASSERT(m_scope_lvl == 0);
SASSERT(!m_setup.already_configured()); SASSERT(!m_setup.already_configured());
setup_context(m_fparams.m_auto_config, false); setup_context(m_fparams.m_auto_config);
if (m_fparams.m_threads > 1 && !m.has_trace_stream()) { if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {
parallel p(*this); parallel p(*this);
@ -3644,10 +3644,7 @@ namespace smt {
return CFG_LOGIC; return CFG_LOGIC;
} }
void context::setup_context(bool use_static_features, bool has_assumptions) { void context::setup_context(bool use_static_features) {
unsigned nf = m_asserted_formulas.get_num_formulas();
if (nf == 0 && !has_assumptions)
return;
if (m_setup.already_configured() || inconsistent()) { if (m_setup.already_configured() || inconsistent()) {
m_relevancy_lvl = std::min(m_fparams.m_relevancy_lvl, m_relevancy_lvl); m_relevancy_lvl = std::min(m_fparams.m_relevancy_lvl, m_relevancy_lvl);
return; return;
@ -3680,7 +3677,7 @@ namespace smt {
lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel) { lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel) {
if (!check_preamble(reset_cancel)) return l_undef; if (!check_preamble(reset_cancel)) return l_undef;
SASSERT(at_base_level()); SASSERT(at_base_level());
setup_context(false, num_assumptions > 0); setup_context(false);
if (m_fparams.m_threads > 1 && !m.has_trace_stream()) { if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {
expr_ref_vector asms(m, num_assumptions, assumptions); expr_ref_vector asms(m, num_assumptions, assumptions);
parallel p(*this); parallel p(*this);
@ -3710,7 +3707,7 @@ namespace smt {
lbool context::check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) { lbool context::check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) {
if (!check_preamble(true)) return l_undef; if (!check_preamble(true)) return l_undef;
TRACE("before_search", display(tout);); TRACE("before_search", display(tout););
setup_context(false, !cube.empty() || !clauses.empty()); setup_context(false);
lbool r = l_undef; lbool r = l_undef;
do { do {
pop_to_base_lvl(); pop_to_base_lvl();

2
src/smt/smt_context.h
View file

@ -1566,7 +1566,7 @@ namespace smt {
void init(); void init();
void flush(); void flush();
config_mode get_config_mode(bool use_static_features) const; config_mode get_config_mode(bool use_static_features) const;
virtual void setup_context(bool use_static_features, bool has_assumptions); virtual void setup_context(bool use_static_features);
void setup_components(); void setup_components();
void pop_to_base_lvl(); void pop_to_base_lvl();
void pop_to_search_lvl(); void pop_to_search_lvl();