mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 07:27:57 +00:00
Code Activity

respect smt configuration parameter in elim_unconstrained simplifier

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-07-24 16:22:08 -07:00
parent a6c51df144
commit 01633f7ce2
2 changed files with 20 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -112,7 +112,7 @@ eliminate:
--*/ --*/
#include "params/smt_params_helper.hpp"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/recfun_decl_plugin.h" #include "ast/recfun_decl_plugin.h"
@ -166,7 +166,7 @@ void elim_unconstrained::eliminate() {
expr_ref rr(m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz), m); expr_ref rr(m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz), m);
bool inverted = m_inverter(t->get_decl(), t->get_num_args(), m_args.data() + sz, r); bool inverted = m_inverter(t->get_decl(), t->get_num_args(), m_args.data() + sz, r);
proof_ref pr(m); proof_ref pr(m);
if (inverted && m_enable_proofs) { if (inverted && m_config.m_enable_proofs) {
expr * s = m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz); expr * s = m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz);
expr * eq = m.mk_eq(s, r); expr * eq = m.mk_eq(s, r);
proof * pr1 = m.mk_def_intro(eq); proof * pr1 = m.mk_def_intro(eq);
@ -267,7 +267,7 @@ void elim_unconstrained::reset_nodes() {
*/ */
void elim_unconstrained::init_nodes() { void elim_unconstrained::init_nodes() {
m_enable_proofs = false; m_config.m_enable_proofs = false;
m_trail.reset(); m_trail.reset();
m_fmls.freeze_suffix(); m_fmls.freeze_suffix();
@ -276,7 +276,7 @@ void elim_unconstrained::init_nodes() {
auto [f, p, d] = m_fmls[i](); auto [f, p, d] = m_fmls[i]();
terms.push_back(f); terms.push_back(f);
if (p) if (p)
m_enable_proofs = true; m_config.m_enable_proofs = true;
} }
m_heap.reset(); m_heap.reset();
@ -303,7 +303,7 @@ void elim_unconstrained::init_nodes() {
for (expr* e : terms) for (expr* e : terms)
get_node(e).set_top(); get_node(e).set_top();
m_inverter.set_produce_proofs(m_enable_proofs); m_inverter.set_produce_proofs(m_config.m_enable_proofs);
} }
@ -422,6 +422,8 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
} }
void elim_unconstrained::reduce() { void elim_unconstrained::reduce() {
if (!m_config.m_enabled)
return;
generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained"); generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
m_inverter.set_model_converter(mc.get()); m_inverter.set_model_converter(mc.get());
m_created_compound = true; m_created_compound = true;
@ -436,3 +438,8 @@ void elim_unconstrained::reduce() {
mc->reset(); mc->reset();
} }
} }
void elim_unconstrained::updt_params(params_ref const& p) {
smt_params_helper sp(p);
m_config.m_enabled = sp.elim_unconstrained();
}

9
src/ast/simplifiers/elim_unconstrained.h
View file

@ -79,6 +79,10 @@ class elim_unconstrained : public dependent_expr_simplifier {
unsigned m_num_eliminated = 0; unsigned m_num_eliminated = 0;
void reset() { m_num_eliminated = 0; } void reset() { m_num_eliminated = 0; }
}; };
struct config {
bool m_enabled = true;
bool m_enable_proofs = false;
};
expr_inverter m_inverter; expr_inverter m_inverter;
ptr_vector<node> m_nodes; ptr_vector<node> m_nodes;
var_lt m_lt; var_lt m_lt;
@ -86,8 +90,8 @@ class elim_unconstrained : public dependent_expr_simplifier {
expr_ref_vector m_trail; expr_ref_vector m_trail;
expr_ref_vector m_args; expr_ref_vector m_args;
stats m_stats; stats m_stats;
config m_config;
bool m_created_compound = false; bool m_created_compound = false;
bool m_enable_proofs = false;
bool is_var_lt(int v1, int v2) const; bool is_var_lt(int v1, int v2) const;
node& get_node(unsigned n) const { return *m_nodes[n]; } node& get_node(unsigned n) const { return *m_nodes[n]; }
@ -119,4 +123,7 @@ public:
void collect_statistics(statistics& st) const override { st.update("elim-unconstrained", m_stats.m_num_eliminated); } void collect_statistics(statistics& st) const override { st.update("elim-unconstrained", m_stats.m_num_eliminated); }
void reset_statistics() override { m_stats.reset(); } void reset_statistics() override { m_stats.reset(); }
void updt_params(params_ref const& p) override;
}; };