mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

update ml example to 64 bit

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-24 04:33:52 -08:00
parent 15d853dc04
commit 47c7ed3b17
2 changed files with 15 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

8
examples/ml/ml_example.ml
View file

@ -30,11 +30,11 @@ let model_converter_test ( ctx : context ) =
let xr = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Real.mk_sort ctx)) in
let yr = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Real.mk_sort ctx)) in
let g4 = (mk_goal ctx true false false ) in
(Goal.add g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10 1)) ]) ;
(Goal.add g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10L 1L)) ]) ;
(Goal.add g4 [ (mk_eq ctx
yr
(Arithmetic.mk_add ctx [ xr; (Real.mk_numeral_nd ctx 1 1) ])) ]) ;
(Goal.add g4 [ (mk_gt ctx yr (Real.mk_numeral_nd ctx 1 1)) ]) ;
(Arithmetic.mk_add ctx [ xr; (Real.mk_numeral_nd ctx 1L 1L) ])) ]) ;
(Goal.add g4 [ (mk_gt ctx yr (Real.mk_numeral_nd ctx 1L 1L)) ]) ;
(
let ar = (Tactic.apply (mk_tactic ctx "simplify") g4 None) in
if ((get_num_subgoals ar) == 1 &&
@ -163,7 +163,7 @@ let basic_tests ( ctx : context ) =
) ;
model_converter_test ctx ;
(* Real num/den test. *)
let rn = Real.mk_numeral_nd ctx 42 43 in
let rn = Real.mk_numeral_nd ctx 42L 43L in
let inum = (get_numerator rn) in
let iden = get_denominator rn in
Printf.printf "Numerator: %s Denominator: %s\n" (Real.numeral_to_string inum) (Real.numeral_to_string iden) ;

13
src/ast/simplifiers/bound_simplifier.cpp
View file

@ -200,13 +200,22 @@ void bound_simplifier::tighten_bound(dependent_expr const& de) {
return;
rational n, k;
expr* x, *y, *f = de.fml();
expr* z, *u;
expr* z, * u, * v, * w;
bool strict;
if (a.is_le(f, x, y)) {
// x <= (x + k) mod N && x >= 0 -> x + k < N
if (a.is_mod(y, z, u) && a.is_numeral(u, n) && has_lower(x, k, strict) && k >= 0 && is_offset(z, x, k) && k > 0 && k < n)
assert_upper(x, n - k, true);
// x <= (x + y) mod N && x >= 0 && 0 <= y < N => x + y < N
if (a.is_mod(y, z, u) && a.is_numeral(u, n) && n > 0) {
assert_upper(x, n, true);
if (has_lower(x, k, strict) && k >= 0 && a.is_add(z, v, w)) {
if (x == v && has_upper(w, k, strict) && k < n)
assert_upper(z, n, true);
if (x == w && has_upper(v, k, strict) && k < n)
assert_upper(z, n, true);
}
}
}