From 40ab25e5102097c85e19767d1149326cd990c4f5 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 13 Nov 2023 11:59:08 +0100 Subject: [PATCH] Fix issue 926 This PR fixes the issue #926 about printing reals in models. The current printer always displays positive reals as rational number of the form `(/ x y)` where `x` and `y` are positive integers. Negative reals are prefixed by their sign and the printer simplifies the expression if the denominator is one. Notice that by the current implementation of Zarith: ```ocaml type t = { num: Z.t; (** Numerator. *) den: Z.t; (** Denominator, >= 0 *) } (* Type of rationals. Invariants: - den is always >= 0; - num and den have no common factor; - if den=0, then num is -1, 0 or 1. - if num=0, then den is -1, 0 or 1. *) ``` Any rational number of the form `0/q` satisfies `q = -1` or `q = 0` or `q = 1`. Thus the printer will always output `0.0` in this case but for the case `0/0` which shouldn't occur. --- src/lib/reasoners/arith.ml | 40 +++++++++++--------- src/lib/util/numbers.ml | 1 + src/lib/util/numbers.mli | 1 + tests/dune.inc | 22 +++++++++++ tests/float/test_float2.models.expected | 2 +- tests/issues/926.models.expected | 11 ++++++ tests/issues/926.models.smt2 | 16 ++++++++ tests/models/arith/arith10.optimize.expected | 4 +- tests/models/arith/arith11.optimize.expected | 2 +- tests/models/arith/arith5.optimize.expected | 6 +-- tests/models/arith/arith7.optimize.expected | 4 +- tests/models/arith/arith9.optimize.expected | 4 +- 12 files changed, 84 insertions(+), 29 deletions(-) create mode 100644 tests/issues/926.models.expected create mode 100644 tests/issues/926.models.smt2 diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 36e7bb341a..8045825b5c 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -813,23 +813,27 @@ module Shostak cpt := Q.add Q.one (max_constant distincts !cpt); Some (term_of_cst (Q.to_string !cpt), true) - - - let pprint_const_for_model = - let pprint_positive_const c = - let num = Q.num c in - let den = Q.den c in - if Z.is_one den then Z.to_string num - else Format.sprintf "(/ %s %s)" (Z.to_string num) (Z.to_string den) - in - fun r -> - match P.is_const (embed r) with - | None -> assert false - | Some c -> - let sg = Q.sign c in - if sg = 0 then "0" - else if sg > 0 then pprint_positive_const c - else Format.sprintf "(- %s)" (pprint_positive_const (Q.abs c)) + let pp_positive_real ppf q = + if Z.equal (Q.den q) Z.one then + Fmt.pf ppf "%a.0" Z.pp_print (Q.num q) + else + Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q) + + let pp_constant ppf r = + match P.is_const (embed r), X.type_info r with + | Some q, Ty.Tint -> + assert (Z.equal (Q.den q) Z.one); + let i = Q.num q in + if Z.sign i = -1 then + Fmt.pf ppf "(- %a)" Z.pp_print (Z.abs i) + else + Fmt.pf ppf "%a" Z.pp_print i + | Some q, Ty.Treal -> + if Q.sign q = -1 then + Fmt.pf ppf "(- %a)" pp_positive_real (Q.abs q) + else + Fmt.pf ppf "%a" pp_positive_real q + | _ -> assert false let choose_adequate_model t r l = if Options.get_debug_interpretation () then @@ -854,6 +858,6 @@ module Shostak List.iter (fun (_,x) -> assert (X.equal x r)) l; r in - r, pprint_const_for_model r + r, Fmt.str "%a" pp_constant r end diff --git a/src/lib/util/numbers.ml b/src/lib/util/numbers.ml index c878b32461..8377eed58a 100644 --- a/src/lib/util/numbers.ml +++ b/src/lib/util/numbers.ml @@ -58,6 +58,7 @@ module Z = struct let from_string s = Z.of_string s let to_string t = Z.to_string t let print fmt z = Format.fprintf fmt "%s" (to_string z) + let pp_print = Z.pp_print let my_gcd a b = if is_zero a then b diff --git a/src/lib/util/numbers.mli b/src/lib/util/numbers.mli index fac3e45b6e..a15b41645d 100644 --- a/src/lib/util/numbers.mli +++ b/src/lib/util/numbers.mli @@ -59,6 +59,7 @@ module Z : sig val from_int : int -> t val from_string : string -> t val to_string : t -> string + val pp_print : t Fmt.t (** convert to machine integer. returns None in case of overflow *) val to_machine_int : t -> int option diff --git a/tests/dune.inc b/tests/dune.inc index 5179e503e4..3a9ff782c4 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -176036,6 +176036,28 @@ ; Auto-generated part begin (subdir issues + (rule + (target 926.models_tableaux.output) + (deps (:input 926.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps 926.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 926.models.expected 926.models_tableaux.output))) (rule (target 889_ci_cdcl_no_minimal_bj.output) (deps (:input 889.smt2)) diff --git a/tests/float/test_float2.models.expected b/tests/float/test_float2.models.expected index e9e394a51f..40d81afc6d 100644 --- a/tests/float/test_float2.models.expected +++ b/tests/float/test_float2.models.expected @@ -1,5 +1,5 @@ unknown ( - (define-fun x () Real (/ 1 4)) + (define-fun x () Real (/ 1.0 4.0)) ) diff --git a/tests/issues/926.models.expected b/tests/issues/926.models.expected new file mode 100644 index 0000000000..226f7e74af --- /dev/null +++ b/tests/issues/926.models.expected @@ -0,0 +1,11 @@ + +unknown +( + (define-fun x1 () Int 5) + (define-fun x2 () Int (- 5)) + (define-fun y1 () Real (/ 3.0 2.0)) + (define-fun y2 () Real 4.0) + (define-fun y3 () Real (/ 16.0 5.0)) + (define-fun y4 () Real (- (/ 3.0 2.0))) + (define-fun y5 () Real 0.0) +) diff --git a/tests/issues/926.models.smt2 b/tests/issues/926.models.smt2 new file mode 100644 index 0000000000..2c9860dae8 --- /dev/null +++ b/tests/issues/926.models.smt2 @@ -0,0 +1,16 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x1 Int) +(declare-const x2 Int) +(declare-const y1 Real) +(declare-const y2 Real) +(declare-const y3 Real) +(declare-const y4 Real) +(assert (= x1 5)) +(assert (= x2 (- 5))) +(assert (= y1 (/ (- 3.0) (- 2.0)))) +(assert (= y2 (/ (- 4.0) (- 1.0)))) +(assert (= y3 3.2)) +(assert (= y4 (/ 3.0 (- 2.0)))) +(check-sat) +(get-model) diff --git a/tests/models/arith/arith10.optimize.expected b/tests/models/arith/arith10.optimize.expected index 821c9704f8..0431bebaa2 100644 --- a/tests/models/arith/arith10.optimize.expected +++ b/tests/models/arith/arith10.optimize.expected @@ -1,6 +1,6 @@ unknown ( - (define-fun x () Real 0) - (define-fun y () Real 10) + (define-fun x () Real 0.0) + (define-fun y () Real 10.0) ) diff --git a/tests/models/arith/arith11.optimize.expected b/tests/models/arith/arith11.optimize.expected index 2e6f3872c4..81826bf452 100644 --- a/tests/models/arith/arith11.optimize.expected +++ b/tests/models/arith/arith11.optimize.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun x () Real 2) + (define-fun x () Real 2.0) (define-fun p1 () Bool false) (define-fun p2 () Bool true) ) diff --git a/tests/models/arith/arith5.optimize.expected b/tests/models/arith/arith5.optimize.expected index 79fc5a3b8f..01dd47be8e 100644 --- a/tests/models/arith/arith5.optimize.expected +++ b/tests/models/arith/arith5.optimize.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun x () Real (- (/ 1 18))) - (define-fun y () Real (- (/ 1 36))) - (define-fun z () Real (- (/ 7 9))) + (define-fun x () Real (- (/ 1.0 18.0))) + (define-fun y () Real (- (/ 1.0 36.0))) + (define-fun z () Real (- (/ 7.0 9.0))) ) diff --git a/tests/models/arith/arith7.optimize.expected b/tests/models/arith/arith7.optimize.expected index c8aef236fb..0e2fdbb39f 100644 --- a/tests/models/arith/arith7.optimize.expected +++ b/tests/models/arith/arith7.optimize.expected @@ -1,10 +1,10 @@ unknown ( - (define-fun x () Real 0) + (define-fun x () Real 0.0) ) unknown ( - (define-fun x () Real (- (/ 3 2))) + (define-fun x () Real (- (/ 3.0 2.0))) ) diff --git a/tests/models/arith/arith9.optimize.expected b/tests/models/arith/arith9.optimize.expected index 767881680d..419bdb3c30 100644 --- a/tests/models/arith/arith9.optimize.expected +++ b/tests/models/arith/arith9.optimize.expected @@ -1,6 +1,6 @@ unknown ( - (define-fun x () Real 4) - (define-fun y () Real 4) + (define-fun x () Real 4.0) + (define-fun y () Real 4.0) )