Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Models for reals must be in real format #926

Closed
bclement-ocp opened this issue Nov 8, 2023 · 0 comments · Fixed by #931
Closed

Models for reals must be in real format #926

bclement-ocp opened this issue Nov 8, 2023 · 0 comments · Fixed by #931
Assignees
@Halbaroth
Labels
bug models This issue is related to model generation.

Comments

@bclement-ocp
Copy link
Collaborator

Alt-Ergo can output things like: (declare-fun x () Real 2) but this is not correct it must be (declare-fun x () Real 2.0).
@bclement-ocp bclement-ocp added bug models This issue is related to model generation. labels Nov 8, 2023
@Halbaroth Halbaroth self-assigned this Nov 9, 2023
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue Nov 13, 2023
@Halbaroth
Fix issue 926
1009833 
This PR fixes the issue OCamlPro#926 about printing reals in models.

The current printer always displays positive reals as rational number of the
form `(/ x.0 y.0)` where `x` and `y` are positive integers. Negative
reals are prefixed by their sign and simplify the expression if the
denominator is one.
@Halbaroth Halbaroth mentioned this issue Nov 13, 2023
Merged
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue Nov 13, 2023
@Halbaroth
Fix issue 926
65569cc 
This PR fixes the issue OCamlPro#926 about printing reals in models.

The current printer always displays positive reals as rational number of the
form `(/ x.0 y.0)` 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.
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue Nov 13, 2023
@Halbaroth
Fix issue 926
40ab25e 
This PR fixes the issue OCamlPro#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.
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue Nov 13, 2023
@Halbaroth
Fix issue 926
b83f0fd 
This PR fixes the issue OCamlPro#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.
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue Nov 13, 2023
@Halbaroth
Fix issue 926
854ab2b 
This PR fixes the issue OCamlPro#926 about printing reals in models.

The current printer always displays positive reals as rational numbers of the
form `(/ x y)` where `x` and `y` are positive integers. Negative reals are
represented by the expression `(/ (- x) y)` where `x` and `y` are positive
integers. 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.
@Halbaroth Halbaroth linked a pull request Nov 13, 2023 that will close this issue
Fix issue 926 #931
Merged
bclement-ocp pushed a commit that referenced this issue Nov 13, 2023
@Halbaroth
Fix issue 926 (#931)
551300f 
This PR fixes the issue #926 about printing reals in models.

The current printer always displays positive reals as rational numbers of the
form `(/ x y)` where `x` and `y` are positive integers. Negative reals are
represented by the expression `(/ (- x) y)` where `x` and `y` are positive
integers. 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Halbaroth Halbaroth

Labels
bug models This issue is related to model generation.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix issue 926 Halbaroth/alt-ergo
2 participants
@Halbaroth @bclement-ocp