mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

Wire term graph into spacer normalizer

Browse source
This commit is contained in:
Arie Gurfinkel 2017-12-13 16:25:00 -05:00
parent be77b1de39
commit 09d54c10a6
1 changed files with 18 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/muz/spacer/spacer_util.cpp
View file

@ -9,6 +9,7 @@ Abstract:
Utility functions for SPACER. Utility functions for SPACER.
Author: Author:
Krystof Hoder (t-khoder) 2011-8-19. Krystof Hoder (t-khoder) 2011-8-19.
@ -64,6 +65,7 @@ Notes:
#include "tactic/arith/arith_bounds_tactic.h" #include "tactic/arith/arith_bounds_tactic.h"
#include "ast/factor_equivs.h" #include "ast/factor_equivs.h"
#include "muz/spacer/spacer_term_graph.h"
namespace spacer { namespace spacer {
@ -1061,14 +1063,24 @@ void normalize (expr *e, expr_ref &out,
simplify_bounds (v); simplify_bounds (v);
} }
if (use_factor_eqs) { if (use_factor_eqs) {
// pick non-constant value representative for // -- refactor equivalence classes and choose a representative
// equivalence classes spacer::term_graph egraph(out.m());
expr_equiv_class eq_classes(out.m()); egraph.add_lits (v);
factor_eqs(v, eq_classes); v.reset();
rewrite_eqs(v, eq_classes); egraph.to_lits(v);
equiv_to_expr(eq_classes, v);
} }
TRACE("spacer_normalize",
tout << "Normalized:\n"
<< out << "\n"
<< "to\n"
<< mk_and(v) << "\n";);
TRACE("spacer_normalize",
spacer::term_graph egraph(out.m());
for (unsigned i = 0, sz = v.size(); i < sz; ++i)
egraph.add_lit (to_app(v.get(i)));
tout << "Reduced app:\n"
<< mk_pp(egraph.to_app(), out.m()) << "\n";);
out = mk_and (v); out = mk_and (v);
} }
} }