mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #3683

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-04 18:56:10 -07:00
parent 7e8753cd3f
commit 0fc8ebc8cc
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/math/polynomial/algebraic_numbers.cpp
View file

@ -2404,8 +2404,8 @@ namespace algebraic_numbers {
// all remaining variables are assigned. // all remaining variables are assigned.
// the unassigned variable vanished when we replaced the rational values. // the unassigned variable vanished when we replaced the rational values.
DEBUG_CODE({ DEBUG_CODE({
for (unsigned i = 0; i < xs.size(); i++) { for (auto x : xs) {
SASSERT(x2v.contains(xs[i])); SASSERT(x2v.contains(x));
} }
}); });
return; return;
@ -2415,7 +2415,7 @@ namespace algebraic_numbers {
polynomial_ref q(ext_pm); polynomial_ref q(ext_pm);
q = p_prime; q = p_prime;
polynomial_ref p_y(ext_pm); polynomial_ref p_y(ext_pm);
for (unsigned i = 0; i < xs.size() - 1; i++) { for (unsigned i = 0; i + 1 < xs.size(); i++) {
checkpoint(); checkpoint();
polynomial::var y = xs[i]; polynomial::var y = xs[i];
SASSERT(x2v.contains(y)); SASSERT(x2v.contains(y));

2
src/math/polynomial/algebraic_params.pyg
View file

@ -1,5 +1,5 @@
def_module_params('algebraic', def_module_params('algebraic',
description='real algebraic number package', description='real algebraic number package. Non-default parameter settings are not supported',
export=True, export=True,
params=(('zero_accuracy', UINT, 0, 'one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k)'), params=(('zero_accuracy', UINT, 0, 'one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k)'),
('min_mag', UINT, 16, 'Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16'), ('min_mag', UINT, 16, 'Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16'),