mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

throttle som blowup by default factor of 10

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-11 17:11:54 -07:00
parent 4209eeaee7
commit 583098b8b0
2 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/rewriter/poly_rewriter_def.h
View file

@ -346,14 +346,16 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
SASSERT(sums.back()[0] == arg);
}
}
unsigned orig_size = sums.size();
expr_ref_buffer sum(m()); // must be ref_buffer because we may throw an exception
ptr_buffer<expr> m_args;
TRACE("som", tout << "starting som...\n";);
do {
TRACE("som", for (unsigned i = 0; i < it.size(); i++) tout << it[i] << " ";
tout << "\n";);
if (sum.size() > m_som_blowup)
throw rewriter_exception("sum of monomials blowup");
if (sum.size() > m_som_blowup * orig_size) {
return BR_FAILED;
}
m_args.reset();
for (unsigned i = 0; i < num_args; i++) {
expr * const * v = sums[i];

2
src/ast/rewriter/poly_rewriter_params.pyg
View file

@ -2,7 +2,7 @@ def_module_params(module_name='rewriter',
class_name='poly_rewriter_params',
export=True,
params=(("som", BOOL, False, "put polynomials in som-of-monomials form"),
("som_blowup", UINT, UINT_MAX, "maximum number of monomials generated when putting a polynomial in sum-of-monomials normal form"),
("som_blowup", UINT, 10, "maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form"),
("hoist_mul", BOOL, False, "hoist multiplication over summation to minimize number of multiplications"),
("hoist_cmul", BOOL, False, "hoist constant multiplication over summation to minimize number of multiplications"),
("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor")))