Skip to content

Commit

Permalink
Change the cram tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@Halbaroth
Halbaroth committed Sep 21, 2023
1 parent d22f993 commit 3a4c393
Show file tree
Hide file tree
Showing 2 changed files with 47 additions and 47 deletions.
14 changes: 7 additions & 7 deletions tests/cram.t/run.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,27 +59,27 @@ This should be the case Tableaux solver as well:
(error "Model generation disabled (try --produce-models)")

The messages above mention `--produce-models`, but we can also use
`set-option`. This requires the Tableaux solver, however:
`set-option`.

$ echo '(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2
(error "No model produced.")

$ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2
(error "No model produced.")

$ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2
(error "Model generation requires the Tableaux solver (try --produce-models)")
(error "Model generation disabled (try --produce-models)")

And now some cases where it should work (using either `--produce-models` or
`Tableaux` with `set-option`):
And now some cases where it should work (using either `--produce-models` or `set-option`):

$ echo '(check-sat)(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2 2>/dev/null

unknown
(
)

$ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2 2>/dev/null

unknown
(
)
$ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2 2>/dev/null

unknown
Expand Down
80 changes: 40 additions & 40 deletions tests/dune.inc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -175627,8 +175627,8 @@
; Auto-generated part begin
(subdir issues
(rule
(target 777.models.fail_tableaux.output)
(deps (:input 777.models.fail.smt2))
(target 777.models_tableaux.output)
(deps (:input 777.models.smt2))
(package alt-ergo)
(action
(chdir %{workspace_root}
Expand All @@ -175643,11 +175643,11 @@
--sat-solver Tableaux
%{input})))))))
(rule
(deps 777.models.fail_tableaux.output)
(deps 777.models_tableaux.output)
(alias runtest-quick)
(package alt-ergo)
(action
(ignore-stdout (with-accepted-exit-codes (not 0) (run diff 777.models.fail.expected 777.models.fail_tableaux.output)))))
(diff 777.models.expected 777.models_tableaux.output)))
(rule
(target 696_ci_cdcl_no_minimal_bj.output)
(deps (:input 696.ae))
Expand Down Expand Up @@ -176459,8 +176459,8 @@
(action
(diff 645.expected 645_fpa.output)))
(rule
(target 555.models.fail_tableaux.output)
(deps (:input 555.models.fail.smt2))
(target 555.models_tableaux.output)
(deps (:input 555.models.smt2))
(package alt-ergo)
(action
(chdir %{workspace_root}
Expand All @@ -176475,11 +176475,11 @@
--sat-solver Tableaux
%{input})))))))
(rule
(deps 555.models.fail_tableaux.output)
(deps 555.models_tableaux.output)
(alias runtest-quick)
(package alt-ergo)
(action
(ignore-stdout (with-accepted-exit-codes (not 0) (run diff 555.models.fail.expected 555.models.fail_tableaux.output)))))
(diff 555.models.expected 555.models_tableaux.output)))
(rule
(target 479_ci_cdcl_no_minimal_bj.output)
(deps (:input 479.smt2))
Expand Down Expand Up @@ -192240,8 +192240,8 @@
; Auto-generated part begin
(subdir models/arith
(rule
(target arith2.models.fail_tableaux.output)
(deps (:input arith2.models.fail.smt2))
(target arith2.models_tableaux.output)
(deps (:input arith2.models.smt2))
(package alt-ergo)
(action
(chdir %{workspace_root}
Expand All @@ -192256,14 +192256,14 @@
--sat-solver Tableaux
%{input})))))))
(rule
(deps arith2.models.fail_tableaux.output)
(deps arith2.models_tableaux.output)
(alias runtest-quick)
(package alt-ergo)
(action
(ignore-stdout (with-accepted-exit-codes (not 0) (run diff arith2.models.fail.expected arith2.models.fail_tableaux.output)))))
(diff arith2.models.expected arith2.models_tableaux.output)))
(rule
(target arith1.models.fail_tableaux.output)
(deps (:input arith1.models.fail.smt2))
(target arith1.models_tableaux.output)
(deps (:input arith1.models.smt2))
(package alt-ergo)
(action
(chdir %{workspace_root}
Expand All @@ -192278,19 +192278,19 @@
--sat-solver Tableaux
%{input})))))))
(rule
(deps arith1.models.fail_tableaux.output)
(deps arith1.models_tableaux.output)
(alias runtest-quick)
(package alt-ergo)
(action
(ignore-stdout (with-accepted-exit-codes (not 0) (run diff arith1.models.fail.expected arith1.models.fail_tableaux.output))))))
(diff arith1.models.expected arith1.models_tableaux.output))))
; Auto-generated part end
; File auto-generated by gentests

; Auto-generated part begin
(subdir models/bool
(rule
(target bool2.models.fail_tableaux.output)
(deps (:input bool2.models.fail.smt2))
(target bool2.models_tableaux.output)
(deps (:input bool2.models.smt2))
(package alt-ergo)
(action
(chdir %{workspace_root}
Expand All @@ -192305,14 +192305,14 @@
--sat-solver Tableaux
%{input})))))))
(rule
(deps bool2.models.fail_tableaux.output)
(deps bool2.models_tableaux.output)
(alias runtest-quick)
(package alt-ergo)
(action
(ignore-stdout (with-accepted-exit-codes (not 0) (run diff bool2.models.fail.expected bool2.models.fail_tableaux.output)))))
(diff bool2.models.expected bool2.models_tableaux.output)))
(rule
(target bool1.models.fail_tableaux.output)
(deps (:input bool1.models.fail.smt2))
(target bool1.models_tableaux.output)
(deps (:input bool1.models.smt2))
(package alt-ergo)
(action
(chdir %{workspace_root}
Expand All @@ -192327,11 +192327,11 @@
--sat-solver Tableaux
%{input})))))))
(rule
(deps bool1.models.fail_tableaux.output)
(deps bool1.models_tableaux.output)
(alias runtest-quick)
(package alt-ergo)
(action
(ignore-stdout (with-accepted-exit-codes (not 0) (run diff bool1.models.fail.expected bool1.models.fail_tableaux.output))))))
(diff bool1.models.expected bool1.models_tableaux.output))))
; Auto-generated part end
; File auto-generated by gentests

Expand Down Expand Up @@ -192365,8 +192365,8 @@
; Auto-generated part begin
(subdir models/issues/715
(rule
(target 715_2.models.fail_tableaux.output)
(deps (:input 715_2.models.fail.smt2))
(target 715_2.models_tableaux.output)
(deps (:input 715_2.models.smt2))
(package alt-ergo)
(action
(chdir %{workspace_root}
Expand All @@ -192381,11 +192381,11 @@
--sat-solver Tableaux
%{input})))))))
(rule
(deps 715_2.models.fail_tableaux.output)
(deps 715_2.models_tableaux.output)
(alias runtest-quick)
(package alt-ergo)
(action
(ignore-stdout (with-accepted-exit-codes (not 0) (run diff 715_2.models.fail.expected 715_2.models.fail_tableaux.output)))))
(diff 715_2.models.expected 715_2.models_tableaux.output)))
(rule
(target 715_1.models_tableaux.output)
(deps (:input 715_1.models.ae))
Expand Down Expand Up @@ -192414,8 +192414,8 @@
; Auto-generated part begin
(subdir models/records
(rule
(target record1.models.fail_tableaux.output)
(deps (:input record1.models.fail.smt2))
(target record1.models_tableaux.output)
(deps (:input record1.models.smt2))
(package alt-ergo)
(action
(chdir %{workspace_root}
Expand All @@ -192430,19 +192430,19 @@
--sat-solver Tableaux
%{input})))))))
(rule
(deps record1.models.fail_tableaux.output)
(deps record1.models_tableaux.output)
(alias runtest-quick)
(package alt-ergo)
(action
(ignore-stdout (with-accepted-exit-codes (not 0) (run diff record1.models.fail.expected record1.models.fail_tableaux.output))))))
(diff record1.models.expected record1.models_tableaux.output))))
; Auto-generated part end
; File auto-generated by gentests

; Auto-generated part begin
(subdir models/uf
(rule
(target uf2.models.fail_tableaux.output)
(deps (:input uf2.models.fail.smt2))
(target uf2.models_tableaux.output)
(deps (:input uf2.models.smt2))
(package alt-ergo)
(action
(chdir %{workspace_root}
Expand All @@ -192457,14 +192457,14 @@
--sat-solver Tableaux
%{input})))))))
(rule
(deps uf2.models.fail_tableaux.output)
(deps uf2.models_tableaux.output)
(alias runtest-quick)
(package alt-ergo)
(action
(ignore-stdout (with-accepted-exit-codes (not 0) (run diff uf2.models.fail.expected uf2.models.fail_tableaux.output)))))
(diff uf2.models.expected uf2.models_tableaux.output)))
(rule
(target uf1.models.fail_tableaux.output)
(deps (:input uf1.models.fail.smt2))
(target uf1.models_tableaux.output)
(deps (:input uf1.models.smt2))
(package alt-ergo)
(action
(chdir %{workspace_root}
Expand All @@ -192479,11 +192479,11 @@
--sat-solver Tableaux
%{input})))))))
(rule
(deps uf1.models.fail_tableaux.output)
(deps uf1.models_tableaux.output)
(alias runtest-quick)
(package alt-ergo)
(action
(ignore-stdout (with-accepted-exit-codes (not 0) (run diff uf1.models.fail.expected uf1.models.fail_tableaux.output))))))
(diff uf1.models.expected uf1.models_tableaux.output))))
; Auto-generated part end
; File auto-generated by gentests

Expand Down

0 comments on commit 3a4c393

Please sign in to comment.