Skip to content

Commit b2adcb7

Browse files
GburyGbury
committed
Add printing of ids for psmt2
1 parent 4d356a3 commit b2adcb7

File tree

8 files changed

+163
-4
lines changed

8 files changed

+163
-4
lines changed

‎src/languages/smtlib2/poly/dolmen_smtlib2_poly.ml

+2
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@ module type Term = Ast.Term
66
module type Statement = Ast.Statement
77
module type Extension = Ast.Extension
88

9+
module Print = Print
10+
911
module Make
1012
(L : Dolmen_intf.Location.S)
1113
(I : Id)

‎src/languages/smtlib2/poly/dolmen_smtlib2_poly.mli

+3
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,9 @@ module type Statement = Ast.Statement
99
module type Extension = Ast.Extension
1010
(** Implementation requirement for the Smtlib format. *)
1111

12+
module Print = Print
13+
(** Printing functions. *)
14+
1215
module Make
1316
(L : Dolmen_intf.Location.S)
1417
(I : Id)

‎src/languages/smtlib2/poly/dune

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
(public_name dolmen.smtlib2.poly)
66
(instrumentation (backend bisect_ppx))
77
(libraries dolmen_std dolmen_intf menhirLib)
8-
(modules Dolmen_smtlib2_poly Tokens Lexer Parser Ast Syntax_messages)
8+
(modules Dolmen_smtlib2_poly Tokens Lexer Parser Ast Syntax_messages Print)
99
)
1010

1111
; Common include

‎src/languages/smtlib2/poly/print.ml

+116
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
2+
(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
3+
4+
(* Printing of identifiers *)
5+
(* ************************************************************************* *)
6+
7+
module L = Lexer
8+
9+
exception Cannot_print of string
10+
11+
let _cannot_print format =
12+
Format.kasprintf (fun msg -> raise (Cannot_print msg)) format
13+
14+
(* lexical definitions taken from the smtlib specification *)
15+
16+
let[@inline] is_whitespace c =
17+
let c = Char.code c in
18+
c = 9 (* tab *) || c = 10 (* line feed *) ||
19+
c = 13 (* cariage return *) || c = 32 (* space *)
20+
21+
let[@inline] is_printable c =
22+
let c = Char.code c in
23+
(32 <= c && c <= 126) || 128 <= c
24+
25+
let is_quoted_symbol_char c =
26+
(is_whitespace c || is_printable c) &&
27+
(c <> '|' && c <> '\\')
28+
29+
let[@inline] is_letter = function
30+
| 'a'..'z' | 'A'..'Z' -> true
31+
| _ -> false
32+
33+
let[@inline] is_digit = function
34+
| '0'..'9' -> true
35+
| _ -> false
36+
37+
let[@inline] is_other_simple_symbol_chars = function
38+
| '~' | '!' | '@' | '$' | '%' | '^' | '&' | '*' | '_'
39+
| '-' | '+' | '=' | '<' | '>' | '.' | '?' | '/' -> true
40+
| _ -> false
41+
42+
let is_simple_symbol_char c =
43+
is_letter c || is_digit c || is_other_simple_symbol_chars c
44+
45+
(* symbol categorization *)
46+
47+
type symbol =
48+
| Simple
49+
| Quoted
50+
| Unprintable
51+
52+
let categorize_symbol s =
53+
match s with
54+
| "" -> Unprintable
55+
| "_" | "!" | "as" | "let"
56+
| "exists" | "forall"
57+
| "match" | "par"
58+
| "assert"
59+
| "check-sat"
60+
| "check-sat-assuming"
61+
| "declare-const"
62+
| "declare-datatype"
63+
| "declare-datatypes"
64+
| "declare-fun"
65+
| "declare-sort"
66+
| "define-fun"
67+
| "define-fun-rec"
68+
| "define-funs-rec"
69+
| "define-sort"
70+
| "echo"
71+
| "exit"
72+
| "get-assertions"
73+
| "get-assignment"
74+
| "get-info"
75+
| "get-model"
76+
| "get-option"
77+
| "get-proof"
78+
| "get-unsat-assumptions"
79+
| "get-unsat-core"
80+
| "get-value"
81+
| "pop"
82+
| "push"
83+
| "reset"
84+
| "reset-assertions"
85+
| "set-info"
86+
| "set-logic"
87+
| "set-option" -> Quoted
88+
| _ ->
89+
(* we are guaranteed that `s` is not the empty string *)
90+
if not (is_digit s.[0]) && (String.for_all is_simple_symbol_char s) then
91+
Simple
92+
else if String.for_all is_quoted_symbol_char s then
93+
Quoted
94+
else
95+
Unprintable
96+
97+
let id fmt name =
98+
let aux fmt s =
99+
(* TODO: expose/add a cache to not redo the `categorize_symbol` computation each time *)
100+
match categorize_symbol s with
101+
| Simple -> Format.pp_print_string fmt s
102+
| Quoted -> Format.fprintf fmt "|%s|" s
103+
| Unprintable ->
104+
_cannot_print "symbol \"%s\" cannot be printed due to lexical constraints" s
105+
in
106+
match (name : Dolmen_std.Name.t) with
107+
| Simple s -> aux fmt s
108+
| Indexed { basename = _; indexes = [] } ->
109+
_cannot_print "indexed id with no indexes: %a" Dolmen_std.Name.print name
110+
| Indexed { basename; indexes; } ->
111+
let pp_sep fmt () = Format.fprintf fmt " " in
112+
Format.fprintf fmt "(_ %a %a)"
113+
aux basename (Format.pp_print_list ~pp_sep aux) indexes
114+
| Qualified _ ->
115+
_cannot_print "qualified identifier: %a" Dolmen_std.Name.print name
116+

‎tests/qcheck/generators.ml

+2
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11

2+
(* This file is free software, part of dolmen. See file "LICENSE" for more information. *)
3+
24
let name ~printable ~simple ~indexed ~qualified =
35
let string =
46
if printable

‎tests/qcheck/main.ml

+5-1
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,13 @@
11

2+
(* This file is free software, part of dolmen. See file "LICENSE" for more information. *)
3+
24
let () =
35
QCheck_runner.run_tests_main [
46
Print.smtlib2_id;
57
Print.smtlib2_id_printable;
6-
(* Maps.add_find; *)
8+
Print.poly_smtlib2_id;
9+
Print.poly_smtlib2_id_printable;
10+
Maps.add_find;
711
]
812

913

‎tests/qcheck/maps.ml

+2
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11

2+
(* This file is free software, part of dolmen. See file "LICENSE" for more information. *)
3+
24
module M = Map.Make(String)
35
module T = Dolmen_std.Maps.String
46

‎tests/qcheck/print.ml

+32-2
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11

2+
(* This file is free software, part of dolmen. See file "LICENSE" for more information. *)
3+
24
(* Functor instanciation *)
35
(* ************************************************************************* *)
46

@@ -13,8 +15,7 @@ module L = Dolmen.Class.Logic.Make
1315
(* ************************************************************************* *)
1416

1517
let identifier
16-
~print ~template ~name ~is_print_exn ~language ~gen
17-
=
18+
~print ~template ~name ~is_print_exn ~language ~gen =
1819
QCheck2.Test.make
1920
~count:1_000 ~long_factor:1_000
2021
~print:(fun name -> Format.asprintf template print name)
@@ -72,3 +73,32 @@ let smtlib2_id_printable =
7273
| Dolmen.Smtlib2.Script.V2_6.Print.Cannot_print _ -> true
7374
| _ -> false)
7475

76+
(* this test is mainly there to check that non-printable ids are correctly
77+
rejected by the printer, so we allow everything in the generator. *)
78+
let poly_smtlib2_id =
79+
identifier
80+
~language:(Smtlib2 `Poly)
81+
~print:Dolmen.Smtlib2.Script.Poly.Print.id
82+
~gen:(Generators.name ~printable:false
83+
~simple:true ~indexed:true ~qualified:true)
84+
~template:{|(assert %a)|}
85+
~name:"Print.smtlib2_poly.id"
86+
~is_print_exn:(function
87+
| Dolmen.Smtlib2.Script.Poly.Print.Cannot_print _ -> true
88+
| _ -> false)
89+
90+
(* this test is mainly there to check that printing of printable ids is correct,
91+
and is accepted by the parser, so we restrict the generated names to one that
92+
have reasonablke chances of being printed. *)
93+
let poly_smtlib2_id_printable =
94+
identifier
95+
~language:(Smtlib2 `V2_6)
96+
~print:Dolmen.Smtlib2.Script.Poly.Print.id
97+
~gen:(Generators.name ~printable:true
98+
~simple:true ~indexed:true ~qualified:false)
99+
~template:{|(assert %a)|}
100+
~name:"Print.smtlib2_poly.id_printable"
101+
~is_print_exn:(function
102+
| Dolmen.Smtlib2.Script.Poly.Print.Cannot_print _ -> true
103+
| _ -> false)
104+

0 commit comments

Comments
 (0)