mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Fix mbp to respect reduce_all_selects option

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-29 18:27:45 -07:00 • committed by Arie Gurfinkel
parent 0c2e3c0894
commit ebfb2a4a1e
1 changed files with 9 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/qe/qe_mbp.cpp
View file

@ -592,10 +592,11 @@ public:
flatten_and(fml); flatten_and(fml);
do_qe_lite(vars, fml);
while (!vars.empty()) { while (!vars.empty()) {
do_qe_lite(vars, fml);
do_qe_bool(mdl, vars, fml); do_qe_bool(mdl, vars, fml);
// sort out vars into bools, arith (int/real), and arrays // sort out vars into bools, arith (int/real), and arrays
@ -613,21 +614,19 @@ public:
vars.reset (); vars.reset ();
// project arrays // project arrays
if (!array_vars.empty()) { qe::array_project_plugin ap(m);
qe::array_project_plugin ap(m); ap(mdl, array_vars, fml, vars, m_reduce_all_selects);
ap(mdl, array_vars, fml, vars, m_reduce_all_selects); SASSERT (array_vars.empty ());
SASSERT (array_vars.empty ()); m_rw (fml);
m_rw (fml); SASSERT (!m.is_false (fml));
SASSERT (!m.is_false (fml));
}
TRACE ("qe", TRACE ("qe",
tout << "extended model:\n"; tout << "extended model:\n";
model_pp (tout, mdl); model_pp (tout, mdl);
tout << "Vars: " << vars << "\n"; tout << "Vars: " << vars << "\n";
); );
} }
// project reals, ints and other variables. // project reals, ints and other variables.
if (!other_vars.empty ()) { if (!other_vars.empty ()) {
TRACE ("qe", tout << "Other vars: " << other_vars << "\n"; TRACE ("qe", tout << "Other vars: " << other_vars << "\n";