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

Smtlib Printer #211

Open
wants to merge 37 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
37 commits
Select commit Hold shift + click to select a range
100ea5d
WIP
Gbury Dec 1, 2021
761cadb
starting to take shape
Gbury Mar 20, 2024
1c5696b
still in progress
Gbury Mar 22, 2024
a916707
WIP
Gbury Mar 28, 2024
b35091a
Working
Gbury Mar 29, 2024
776f897
Add some builtins + handling of assoc/chain
Gbury Apr 2, 2024
7f2d83a
Working well
Gbury Apr 5, 2024
939cfca
Adding builtins
Gbury Apr 5, 2024
f7a0861
WIP
Gbury Apr 8, 2024
a67c2c9
working better
Gbury Apr 8, 2024
a40d35c
Fixes + psmt2 printing
Gbury Apr 10, 2024
0115b5c
Code factorization
Gbury Apr 16, 2024
be334c6
Add logic detection
Gbury Apr 26, 2024
c63d602
WIP
Gbury Apr 29, 2024
a795882
Add new tests
Gbury Apr 29, 2024
2c3729e
Fixes
Gbury Apr 30, 2024
458bec8
more fixes
Gbury May 2, 2024
3ed4cd4
cleanup + fix univ type in smt2 printer
Gbury May 14, 2024
4eac25a
WIP
Gbury May 29, 2024
f468654
Fix bug
Gbury Jul 24, 2024
69d38ab
fixes
Gbury Jul 28, 2024
2eda6fc
Fix + Add one test
Gbury Aug 30, 2024
81a234b
Adding errors
Gbury Aug 31, 2024
070362e
rebase error
Gbury Aug 31, 2024
feb6d56
Promote test result
Gbury Aug 31, 2024
fc66227
WIP: try and use a tmpfile (not working yet...)
Gbury Aug 26, 2024
3b25c09
Fix temp file usage
Gbury Sep 1, 2024
7d0d055
More Proper errors
Gbury Sep 1, 2024
399f929
typo
Gbury Sep 4, 2024
25b3bca
changes
Gbury Sep 5, 2024
99f5440
WIP
Gbury Sep 10, 2024
3605eca
Fix printing of decimals
Gbury Sep 10, 2024
c3c571b
Some more tests
Gbury Sep 10, 2024
9419ec5
Add zarith in opam file + some misc fixes
Gbury Sep 11, 2024
e74fc4d
Fixes for real lits
Gbury Sep 12, 2024
19bf4ea
Fix misclassification of to_int/Floor_to_int
Gbury Sep 14, 2024
7e18fa9
two minor fixes
Gbury Sep 14, 2024
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
Promote test result
Gbury committed Sep 10, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit feb6d5668678dc97acbae0cbd3db987774042ad7
4 changes: 3 additions & 1 deletion tests/print/smtlib/poly/poly.expected
Original file line number Diff line number Diff line change
@@ -1 +1,3 @@
run 'make promote' to update this file
(set-logic QF_UF)
(declare-fun match_bool (par (|'a|) (Bool |'a| |'a|) |'a|))
(exit)
14 changes: 13 additions & 1 deletion tests/print/smtlib/v2.6/poly.expected
Original file line number Diff line number Diff line change
@@ -1 +1,13 @@
run 'make promote' to update this file
(set-logic QF_UF)
Error Uncaught exception:
Dolmen_smtlib2_v6_script__Print.Cannot_print("polymorphic function declaration")
Raised at Dolmen_smtlib2_v6_script__Print._cannot_print.(fun) in file "src/languages/smtlib2/v2.6/script/print.ml", line 16, characters 31-55
Called from Stdlib__Format.output_acc in file "format.ml", line 1355, characters 4-20
Called from Stdlib__Format.kfprintf.(fun) in file "format.ml", line 1416, characters 16-34
Called from Dolmen_loop__Export.Smtlib2.pp_stmt in file "src/loop/export.ml", line 263, characters 4-40
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Dolmen_loop__Export.Make.export.(fun) in file "src/loop/export.ml", line 645, characters 26-45
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Dolmen_loop__Export.Make.export in file "src/loop/export.ml", line 644, characters 8-208
Called from Dolmen_loop__Pipeline.Make.eval_op in file "src/loop/pipeline.ml", line 87, characters 8-17