From 47c7ed3b1719266c0686c3caaa6f8cf5345e64e2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Jan 2023 04:33:52 -0800 Subject: [PATCH] update ml example to 64 bit Signed-off-by: Nikolaj Bjorner --- examples/ml/ml_example.ml | 8 ++++---- src/ast/simplifiers/bound_simplifier.cpp | 13 +++++++++++-- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml index 5b4e6e9ed..6fd795476 100644 --- a/examples/ml/ml_example.ml +++ b/examples/ml/ml_example.ml @@ -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) ; diff --git a/src/ast/simplifiers/bound_simplifier.cpp b/src/ast/simplifiers/bound_simplifier.cpp index 06302ab6f..1f4fb9b9d 100644 --- a/src/ast/simplifiers/bound_simplifier.cpp +++ b/src/ast/simplifiers/bound_simplifier.cpp @@ -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); + } + } }