mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 12:51:22 +00:00
Code Activity

Added rlimit.inc() for expensive interval exponentiation in the non-linear arithmetic theory.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-04-19 13:07:04 +01:00
parent a02a7f4443
commit 0a0b17540f
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_arith_nl.h
View file

@ -339,8 +339,13 @@ namespace smt {
tout << mk_pp(var, get_manager()) << "\n"; tout << mk_pp(var, get_manager()) << "\n";
tout << "power " << power << ": " << expt(i, power) << "\n"; tout << "power " << power << ": " << expt(i, power) << "\n";
display_interval(tout << "target before: ", target); tout << "\n";); display_interval(tout << "target before: ", target); tout << "\n";);
i.expt(power); i.expt(power);
target *= i; target *= i;
get_manager().limit().inc((target.is_lower_open() || target.minus_infinity()) ? 1 : target.get_lower_value().bitsize());
get_manager().limit().inc((target.is_upper_open() || target.plus_infinity()) ? 1 : target.get_upper_value().bitsize());
TRACE("non_linear", display_interval(tout << "target after: ", target); tout << "\n";); TRACE("non_linear", display_interval(tout << "target after: ", target); tout << "\n";);
} }