mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

fix internalization on post-visit, increase delay to 100

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-14 17:20:39 -07:00
parent 8412ecbdbf
commit 155738088f
3 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -92,6 +92,7 @@ namespace euf {
m_args.push_back(m_egraph.find(to_app(e)->get_arg(i))); m_args.push_back(m_egraph.find(to_app(e)->get_arg(i)));
if (root && internalize_root(to_app(e), sign, m_args)) if (root && internalize_root(to_app(e), sign, m_args))
return false; return false;
SASSERT(!get_enode(e));
if (auto* s = expr2solver(e)) if (auto* s = expr2solver(e))
s->internalize(e, m_is_redundant); s->internalize(e, m_is_redundant);
else else

2
src/sat/smt/sat_th.cpp
View file

@ -45,7 +45,7 @@ namespace euf {
if (!visit(arg)) if (!visit(arg))
goto loop; goto loop;
} }
if (!post_visit(e, sign, root && a == e)) if (!visited(e) && !post_visit(e, sign, root && a == e))
return false; return false;
m_stack.pop_back(); m_stack.pop_back();
} }

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

@ -71,7 +71,7 @@ def_module_params(module_name='smt',
('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'), ('arith.nl.delay', UINT, 100, 'number of calls to final check before invoking bounded nlsat check'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'), ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'),