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

expose parameters to control behavior for #5660

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-10 22:06:19 -08:00
parent 1c7ff72ae2
commit 8970a54eaa
6 changed files with 40 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_solver/sat_smt_preprocess.cpp
View file

@ -46,9 +46,9 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep
smt_params smtp(p);
if (sp.euf() || sp.smt()) {
s.add_simplifier(alloc(rewriter_simplifier, m, p, st));
s.add_simplifier(alloc(propagate_values, m, p, st));
s.add_simplifier(alloc(euf::solve_eqs, m, st));
s.add_simplifier(alloc(elim_unconstrained, m, st));
if (smtp.m_propagate_values) s.add_simplifier(alloc(propagate_values, m, p, st));
if (smtp.m_solve_eqs) s.add_simplifier(alloc(euf::solve_eqs, m, st));
if (smtp.m_elim_unconstrained) s.add_simplifier(alloc(elim_unconstrained, m, st));
if (smtp.m_nnf_cnf) s.add_simplifier(alloc(cnf_nnf_simplifier, m, p, st));
if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st));
if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifer(m, p, st));

1
src/sat/smt/euf_solver.cpp
View file

@ -540,6 +540,7 @@ namespace euf {
sat::check_result solver::check() {
++m_stats.m_final_checks;
TRACE("euf", s().display(tout););
TRACE("final_check", s().display(tout););
bool give_up = false;
bool cont = false;

9
src/sat/smt/q_ematch.cpp
View file

@ -69,9 +69,12 @@ namespace q {
[&](euf::enode* n) {
m_mam->add_node(n, false);
};
ctx.get_egraph().set_on_merge(_on_merge);
if (!ctx.relevancy_enabled())
ctx.get_egraph().set_on_make(_on_make);
if (ctx.get_config().m_ematching) {
ctx.get_egraph().set_on_merge(_on_merge);
if (!ctx.relevancy_enabled())
ctx.get_egraph().set_on_make(_on_make);
}
m_mam = mam::mk(ctx, *this);
}

5
src/smt/params/preprocessor_params.cpp
View file

@ -26,6 +26,9 @@ void preprocessor_params::updt_local_params(params_ref const & _p) {
m_restricted_quasi_macros = p.restricted_quasi_macros();
m_pull_nested_quantifiers = p.pull_nested_quantifiers();
m_refine_inj_axiom = p.refine_inj_axioms();
m_propagate_values = p.propagate_values();
m_elim_unconstrained = p.elim_unconstrained();
m_solve_eqs = p.solve_eqs();
m_ng_lift_ite = static_cast<lift_ite_kind>(p.q_lift_ite());
}
@ -47,6 +50,8 @@ void preprocessor_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_eliminate_term_ite);
DISPLAY_PARAM(m_macro_finder);
DISPLAY_PARAM(m_propagate_values);
DISPLAY_PARAM(m_solve_eqs);
DISPLAY_PARAM(m_elim_unconstrained);
DISPLAY_PARAM(m_refine_inj_axiom);
DISPLAY_PARAM(m_eliminate_bounds);
DISPLAY_PARAM(m_simplify_bit2int);

52
src/smt/params/preprocessor_params.h
View file

@ -31,43 +31,29 @@ struct preprocessor_params : public pattern_inference_params,
public bit_blaster_params {
lift_ite_kind m_lift_ite;
lift_ite_kind m_ng_lift_ite; // lift ite for non ground terms
bool m_pull_cheap_ite;
bool m_pull_nested_quantifiers;
bool m_eliminate_term_ite;
bool m_macro_finder;
bool m_propagate_values;
bool m_refine_inj_axiom;
bool m_eliminate_bounds;
bool m_simplify_bit2int;
bool m_nnf_cnf;
bool m_distribute_forall;
bool m_reduce_args;
bool m_quasi_macros;
bool m_restricted_quasi_macros;
bool m_max_bv_sharing;
bool m_pre_simplifier;
bool m_nlquant_elim;
bool m_pull_cheap_ite = false;
bool m_pull_nested_quantifiers = false;
bool m_eliminate_term_ite = false;
bool m_macro_finder = false;
bool m_propagate_values = true;
bool m_elim_unconstrained = true;
bool m_solve_eqs = true;
bool m_refine_inj_axiom = true;
bool m_eliminate_bounds = false;
bool m_simplify_bit2int = false;
bool m_nnf_cnf = true;
bool m_distribute_forall = false;
bool m_reduce_args = false;
bool m_quasi_macros = false;
bool m_restricted_quasi_macros = false;
bool m_max_bv_sharing = true;
bool m_pre_simplifier = true;
bool m_nlquant_elim = false;
public:
preprocessor_params(params_ref const & p = params_ref()):
m_lift_ite(lift_ite_kind::LI_NONE),
m_ng_lift_ite(lift_ite_kind::LI_NONE),
m_pull_cheap_ite(false),
m_pull_nested_quantifiers(false),
m_eliminate_term_ite(false),
m_macro_finder(false),
m_propagate_values(true),
m_refine_inj_axiom(true),
m_eliminate_bounds(false),
m_simplify_bit2int(false),
m_nnf_cnf(true),
m_distribute_forall(false),
m_reduce_args(false),
m_quasi_macros(false),
m_restricted_quasi_macros(false),
m_max_bv_sharing(true),
m_pre_simplifier(true),
m_nlquant_elim(false) {
m_ng_lift_ite(lift_ite_kind::LI_NONE) {
updt_local_params(p);
}

9
src/smt/params/smt_params_helper.pyg
View file

@ -18,8 +18,11 @@ def_module_params(module_name='smt',
('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity'),
('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'),
('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
('elim_unconstrained', BOOL, True, 'pre-processing: eliminate unconstrained subterms'),
('solve_eqs', BOOL, True, 'pre-processing: solve equalities'),
('propagate_values', BOOL, True, 'pre-processing: propagate values'),
('pull_nested_quantifiers', BOOL, False, 'pre-processing: pull nested quantifiers'),
('refine_inj_axioms', BOOL, True, 'pre-processing: refine injectivity axioms'),
('candidate_models', BOOL, False, 'create candidate models even when quantifier or theory reasoning is incomplete'),
('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
@ -50,7 +53,7 @@ def_module_params(module_name='smt',
('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'),
('bv.delay', BOOL, False, 'delay internalize expensive bit-vector operations'),
('bv.eq_axioms', BOOL, True, 'enable redundant equality axioms for bit-vectors'),
('bv.size_reduce', BOOL, False, 'turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'),
('bv.size_reduce', BOOL, False, 'pre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),