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.

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

Model generation support for SatML #829

Merged
merged 28 commits into from
Sep 27, 2023
Merged
Changes from 1 commit
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
914d283
Theory: harden 'compute_concrete_model' function
iguerNL May 1, 2021
982bb92
Push the test 'get_case_split_policy() == origin' into Theory.do_case…
iguerNL May 1, 2021
de26aae
CS: functions return all the env instead of just 'gamma_finite'.
iguerNL May 1, 2021
fed58a7
Fun_sat: refactor the way models are handled/printed
iguerNL May 1, 2021
7447ca3
satML: add missing case-split strategies
iguerNL May 1, 2021
0c37f66
satML: implement models generation.
iguerNL May 1, 2021
1ace3d9
Make model tests negative
Halbaroth Sep 15, 2023
3ac006b
Reindent
Halbaroth Sep 21, 2023
4b03759
Update documentation about `output_concrete_model`
Halbaroth Sep 22, 2023
0251733
Document the timeout_reason ADT
Halbaroth Sep 22, 2023
9496cf6
poetry
Halbaroth Sep 22, 2023
115a16a
Restore the comment about `reinit_cpt`
Halbaroth Sep 22, 2023
986321d
Fix spelling
Halbaroth Sep 22, 2023
b39ecb8
Remainder to the issue 834
Halbaroth Sep 22, 2023
9507d63
Simplify get-model processing
Halbaroth Sep 22, 2023
1ca2286
Remove SAT solver choices while model generating
Halbaroth Sep 21, 2023
3d75176
Fix model output
Halbaroth Sep 21, 2023
be505b4
All the model tests are positive
Halbaroth Sep 21, 2023
afb8e44
Remove deprecated cram tests
Halbaroth Sep 21, 2023
e0c9b34
Test models with all the SAT solvers
Halbaroth Sep 21, 2023
b45ee04
Restoring dump-models option
Halbaroth Sep 22, 2023
a155756
Use the right post-solve SAT environment for models
Halbaroth Sep 22, 2023
709dc42
Print dump models on the channel models
Halbaroth Sep 26, 2023
cd998e7
Prevent printing internal names in models
Halbaroth Sep 26, 2023
819935b
Promote tests
Halbaroth Sep 26, 2023
a6caf6a
Revert "Simplify get-model processing"
Halbaroth Sep 26, 2023
d4301df
Review changes
Halbaroth Sep 26, 2023
3299ff7
Test only models with FunSAT
Halbaroth Sep 27, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Make model tests negative
Some tests about models failed in the OptimAE PR.
This commit allows to tag tests in `tests/` with `fail` tag
which means the test is supposed to fail.
Halbaroth committed Sep 26, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit 1ace3d9ead283cff5c4c5ec6d17161f8e2522930
97,144 changes: 46,970 additions & 50,174 deletions tests/dune.inc

Large diffs are not rendered by default.

File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
51 changes: 36 additions & 15 deletions tools/gentest.ml
Original file line number Diff line number Diff line change
@@ -109,11 +109,12 @@ end
module Test : sig
type t = private {
cmd: Cmd.t;
pb_file: string
pb_file: string;
should_succeed: bool
}
(** Type of a test. *)

val make: cmd: Cmd.t -> pb_file: string -> t
val make: cmd: Cmd.t -> pb_file: string -> should_succeed: bool -> t
(** Set up the test. *)

val pp_expected_output: t printer
@@ -124,10 +125,11 @@ module Test : sig
end = struct
type t = {
cmd: Cmd.t;
pb_file: string
pb_file: string;
should_succeed: bool
}

let make ~cmd ~pb_file = {cmd; pb_file}
let make ~cmd ~pb_file ~should_succeed = {cmd; pb_file; should_succeed}

let pp_output fmt tst =
let filename = Filename.chop_extension tst.pb_file in
@@ -139,6 +141,17 @@ end = struct
Format.fprintf fmt "%s.expected" filename

let pp_stanza fmt tst =
let pp_diff_command fmt tst =
if tst.should_succeed then
Format.fprintf fmt "@[(diff %a %a)@]"
pp_expected_output tst
pp_output tst
else
Format.fprintf fmt
"@[(ignore-stdout (with-accepted-exit-codes (not 0) (run diff %a %a)))@]"
pp_expected_output tst
pp_output tst
in
Format.fprintf fmt "\
@[<v 1>\
(rule@,\
@@ -152,15 +165,16 @@ end = struct
@[<v 1>(with-accepted-exit-codes 0@,\
@[<v 1>(run @[<hv>%a@])))))))@]@]@]@]@]@]@]@ \
@[<v 1>(rule@,\
@[<v 1>(deps %a)@,\
@[<v 1>(alias %s)@,\
@[<v 1>(package alt-ergo)@,\
@[<v 1>(action@ @[<hv 2>(diff@ %a@ %a)@]))@]@]@]@]"
@[<v 1>(action@ %a))@]@]@]@]@]"
pp_output tst
tst.pb_file
Cmd.pp tst.cmd
(Cmd.group tst.cmd)
pp_expected_output tst
pp_output tst
(Cmd.group tst.cmd)
pp_diff_command tst
end

module Batch : sig
@@ -192,25 +206,32 @@ end = struct

let make ~root ~path ~cmds ~pb_files =
let tests = List.fold_left (fun acc1 pb_file ->
let exclude, filters =
let exclude, filters, should_succeed =
List.fold_left (
fun (exclude, filters_opt) ->
fun (exclude, filters_opt, should_succeed) ->
function
| "fail" ->
exclude,
filters_opt,
false
| "dolmen" ->
"legacy" :: exclude,
Some ["dolmen"]
Some ["dolmen"],
should_succeed
| "models" ->
exclude,
Some ["tableaux"]
Some ["tableaux"],
should_succeed
| "fpa" ->
exclude,
Some ["fpa"]
| _ -> (exclude, filters_opt)
) ([], None) (String.split_on_char '.' pb_file)
Some ["fpa"],
should_succeed
| _ -> (exclude, filters_opt, should_succeed)
) ([], None, true) (String.split_on_char '.' pb_file)
in
List.fold_left (fun acc2 cmd ->
if filter ~exclude filters cmd then
Test.make ~cmd ~pb_file :: acc2
Test.make ~cmd ~pb_file ~should_succeed :: acc2
else
acc2
) acc1 cmds) [] pb_files