bclement-ocp
commented
4 months ago This function:
logic match_bool : bool, 'a, 'a -> 'awhich is at the top of every Alt-Ergo file generated by Why3 does not seem to translate with -o psmt2:
$ dolmen match_bool.ae -o psmt2
(set-logic QF_UF)
(declare-fun match_bool (par (Error Uncaught exception:
Failure("cannot find binding for id")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Dolmen_smtlib2_poly__Print.Make.ty_var in file "src/languages/smtlib2/poly/print.ml", line 299, characters 15-36
Called from Stdlib__Format.output_acc in file "format.ml", line 1307, characters 32-48
Called from Stdlib__Format.output_acc in file "format.ml", line 1295, characters 4-20
Called from Stdlib__Format.output_acc in file "format.ml", line 1307, characters 32-48
Called from Stdlib__Format.output_acc in file "format.ml", line 1308, characters 32-48
Called from Stdlib__Format.output_acc in file "format.ml", line 1307, characters 32-48
Called from Stdlib__Format.output_acc in file "format.ml", line 1295, characters 4-20
Called from Stdlib__Format.output_acc in file "format.ml", line 1308, characters 32-48
Called from Stdlib__Format.output_acc in file "format.ml", line 1305, characters 32-48
Called from Stdlib__Format.output_acc in file "format.ml", line 1295, characters 4-20
Called from Stdlib__Format.kfprintf.(fun) in file "format.ml", line 1356, characters 16-34
Called from Stdlib__Format.output_acc in file "format.ml", line 1295, characters 4-20
Called from Stdlib__Format.kfprintf.(fun) in file "format.ml", line 1356, characters 16-34
Called from Dolmen_loop__Export.Smtlib2.pp_stmt in file "src/loop/export.ml", line 244, characters 4-40
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Dolmen_loop__Export.Make.export in file "src/loop/export.ml", line 605, characters 16-44
Called from Dolmen_loop__Pipeline.Make.eval_op in file "src/loop/pipeline.ml", line 87, characters 8-17
Finally it is here !
This PR adds a printer for smtlib2.6 to
dolmen. The goal of the printer is to take arbitrary typed expressions, and print them in a way that respects the smtlib syntax.The fact that it is designed to take arbitrary expressions explain part of why it is complex: great care must be taken to make sure that identifiers respect the syntax convention (i.e. which characters are allowed), are not shadowed, etc... Additionally, in typical dolmen fashion, the printers are functorized so that they can be more easily re-used by other projects who'd wish to print their own typed terms in smtlib format.
For quick tests:
will parse and type the contents of
input_file.smt2and then print them inoutput_file.smt2. Alternatively, one can also doto have the output printed on the standard output.
Note: this is still a work in progress (not all builtins are yet printed, and some features related to avoiding shadowing are not yet implemented), and slightly experimental (no large scale testing has been done yet).