mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

Enable macro-finder fallback for auto_config=false mbqi=false

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-13 04:59:52 +00:00 • committed by GitHub
parent a4eeeceb52
commit dc8fcb93a6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 31 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/params/smt_params.cpp
View file

@ -71,6 +71,12 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_lemmas2console = sp.lemmas2console();
m_instantiations2console = sp.instantiations2console();
m_proof_log = sp.proof_log();
if (!m_auto_config && !m_mbqi &&
!_p.contains("macro_finder") && !_p.contains("smt.macro_finder") &&
!_p.contains("quasi_macros") && !_p.contains("smt.quasi_macros")) {
m_macro_finder = true;
}
}
@ -433,4 +439,3 @@ void smt_params::setup_LRA() {
m_arith_propagate_eqs = false;
m_eliminate_term_ite = true;
}

25
src/test/quant_solve.cpp
View file

@ -198,6 +198,30 @@ static void test_qe_regression_4175() {
}
}
static void test_macro_finder_fallback_8052() {
ast_manager m;
reg_decl_plugins(m);
cmd_context ctx(false, &m);
ctx.set_ignore_check(true);
std::istringstream is(R"(
(declare-fun f (Int) Int)
(declare-const x Int)
(assert (forall ((i Int)) (! (= (f i) i) :pattern ((f i)) :weight 0)))
(assert (> x (f 0)))
)");
VERIFY(parse_smt2_commands(ctx, is));
params_ref p;
p.set_bool("auto_config", false);
p.set_bool("mbqi", false);
p.set_uint("relevancy", 0);
smt_params params(p);
smt::kernel solver(m, params);
for (unsigned i = 0; i < ctx.assertions().size(); ++i)
solver.assert_expr(ctx.assertions().get(i));
VERIFY(l_true == solver.check());
}
static void test_quant_solve1() {
ast_manager m;
@ -284,6 +308,7 @@ void tst_quant_solve() {
test_quant_solve1();
test_qe_regression_4175();
test_macro_finder_fallback_8052();
#if 0
memory::finalize();