mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

set relevancy = 0 in auto-config mode when there are bit-vectors and no quantifiers, #7484

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-12-20 18:10:46 +01:00
parent 114cae50a5
commit db9f45dfec
5 changed files with 23 additions and 9 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) {
pop_to_base_lvl();
cores.reset();
setup_context(false);
setup_context(false, !asms.empty());
internalize_assertions();
if (m_asserted_formulas.inconsistent() || inconsistent()) {
return l_false;

17
src/smt/smt_context.cpp
View file

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

2
src/smt/smt_context.h
View file

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

10
src/smt/smt_setup.cpp
View file

@ -826,6 +826,16 @@ namespace smt {
setup_fpa();
setup_special_relations();
setup_polymorphism();
setup_relevancy(st);
}
//
// quantifier free problems with bit-vectors should always use relevancy = 0
// there are some other cases where relevancy propagation is harmful.
//
void setup::setup_relevancy(static_features& st) {
if (st.m_has_bv && st.m_num_quantifiers == 0)
m_params.m_relevancy_lvl = 0;
}
void setup::setup_unknown(static_features & st) {

1
src/smt/smt_setup.h
View file

@ -109,6 +109,7 @@ namespace smt {
void setup_lra_arith();
void setup_fpa();
void setup_str();
void setup_relevancy(static_features& st);
public:
setup(context & c, smt_params & params);