forked from OCamlPro/alt-ergo
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[models] Add support for printing arrays
This patch adds the support for printing arrays in the models output. Rather than printing default values, we print smtlib abstract values (@xxx) for the unknown elements, because we don't have a default value available easily otherwise. The example model in OCamlPro#555 now displays as: ```smtlib2 ( (define-fun x () Int 0) (define-fun y () Int 0) (define-fun a1 () (Array Int Int) (store (as @A1 (Array Int Int)) 0 0)) ) ``` This also removes the "Functions" / "Constants" / "Arrays" sections because they were now wrong (some arrays were in constants, other in arrays) and hence somewhat confusing. Instead, the "values" section is added then printing with `--model-type constraints`. Uses of Printer.print_fmt have also been replaced with Format.fprintf because they were causing weird looking outputs with some combinations of options. Only the final value is printer with `print_fmt`, which should do the appropriate (actually, I don't think it is needed here, but better safe than sorry) cleanup dance only once. Fixes OCamlPro#555
- Loading branch information
1 parent
47fbd74
commit 50b7d93
Showing
4 changed files
with
85 additions
and
33 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -1085,4 +1085,3 @@ let save_cache () = | |
|
||
let reinit_cache () = | ||
LX.reinit_cache () | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
; From https://github.com/OCamlPro/alt-ergo/issues/555 | ||
(set-logic ALL) | ||
(declare-const x Int) | ||
(declare-const y Int) | ||
(declare-const a1 (Array Int Int)) | ||
(declare-const a2 (Array Int Int)) | ||
(assert (= (select a1 x) x)) | ||
(assert (= (store a1 x y) a1)) | ||
(check-sat) | ||
(get-model) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters