Skip to content

Commit 635df44

Browse files
wadoonwadoon
committed
work on define-fun
1 parent fa659af commit 635df44

File tree

4 files changed

+163
-98
lines changed

4 files changed

+163
-98
lines changed

‎bin/dune

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,4 +2,4 @@
22
(public_name smt2key)
33
(name main)
44
(libraries sexplib pprint)
5-
(flags (:standard -w -33)))
5+
(flags (:standard -w -33 -w -27)))

‎bin/main.ml

+156-92
Original file line numberDiff line numberDiff line change
@@ -1,51 +1,7 @@
11
open Sexplib
22
open PPrint
33

4-
let pHeader filename =
5-
print_endline (String.concat " " [ "// KeY File generated of"; filename ])
6-
7-
let pSection name fn sexprs =
8-
let x = List.filter_map fn sexprs in
9-
let doc = PPrint.separate PPrint.hardline x in
10-
print_endline (String.concat "" [ "\\"; name; "{" ]);
11-
ToChannel.pretty 0.9 80 stdout doc;
12-
print_endline "}"
13-
14-
let pSort = function
15-
| Sexp.List [ Sexp.Atom "define-sort"; Sexp.Atom name ] ->
16-
Some
17-
(PPrint.concat [ PPrint.utf8string name; PPrint.semi; PPrint.hardline ])
18-
| _ -> None
19-
20-
let pFunction = function
21-
| Sexp.List [ Sexp.Atom "declare-fun";
22-
Sexp.Atom name;
23-
Sexp.List args;
24-
Sexp.Atom ret ] ->
25-
if ret = "bool" then None
26-
else if (List.length args) = 0 then
27-
Some
28-
(PPrint.concat [ PPrint.string ret; PPrint.space; PPrint.utf8string name; PPrint.semi; ])
29-
else
30-
Some
31-
(PPrint.concat [PPrint.string ret; PPrint.space;
32-
PPrint.utf8string name;
33-
PPrint.parens
34-
(PPrint.separate_map
35-
(PPrint.precede PPrint.comma PPrint.space)
36-
(fun x -> match x with
37-
|Sexp.Atom y -> PPrint.string y
38-
|Sexp.List _ -> PPrint.empty) args);
39-
PPrint.semi;])
40-
| _ -> None
41-
42-
let pPredicate = function
43-
| Sexp.List [ Sexp.Atom "define-fun"; Sexp.Atom name; _; Sexp.Atom "Bool" ]
44-
->
45-
Some
46-
(PPrint.concat [ PPrint.utf8string name; PPrint.semi; PPrint.hardline ])
47-
| _ -> None
48-
4+
(*----------------------------------------------------------------------------*)
495
let op_prec = function
506
| "and" -> 100
517
| "or" -> 110
@@ -60,43 +16,152 @@ let rec op_prec_sexpr = function
6016
let unpackAtom = function Sexp.Atom a -> a | _ -> "n/a"
6117

6218
let rec expandTerm op exprs =
63-
let opd = PPrint.string op in
19+
let opd = space ^^ PPrint.string op ^^ space in
6420
let prec = op_prec op in
6521
PPrint.flow opd
6622
(List.map
6723
(fun x ->
6824
if prec >= op_prec_sexpr x then term2KeY x
69-
else PPrint.concat [ PPrint.lparen; term2KeY x; PPrint.rparen ])
25+
else PPrint.parens (term2KeY x))
7026
exprs)
7127

7228
and term2KeY = function
7329
| Sexp.Atom a -> PPrint.string a
74-
| Sexp.List args ->
75-
let hd = unpackAtom (List.hd args) in
76-
let tl = List.tl args in
77-
match hd with
78-
| "and" -> expandTerm "&" tl
79-
| "or" -> expandTerm "|" tl
80-
| "=>" -> expandTerm "->" tl
81-
| "+" -> expandTerm "+" tl
82-
| "-" -> expandTerm "-" tl
83-
| "*" -> expandTerm "*" tl
84-
| "/" -> expandTerm "/" tl
85-
| "mod" -> expandTerm "%" tl
86-
| "<" -> expandTerm "%" tl
87-
| "<=" -> expandTerm "<=" tl
88-
| ">" -> expandTerm ">" tl
89-
| ">=" -> expandTerm ">=" tl
90-
| "=" -> expandTerm "=" tl
91-
| _ ->
30+
| Sexp.List args -> (
31+
let hd = unpackAtom (List.hd args) in
32+
let tl = List.tl args in
33+
match hd with
34+
| "and" -> expandTerm "&" tl
35+
| "or" -> expandTerm "|" tl
36+
| "=>" -> expandTerm "->" tl
37+
| "+" -> expandTerm "+" tl
38+
| "-" -> expandTerm "-" tl
39+
| "*" -> expandTerm "*" tl
40+
| "/" -> expandTerm "/" tl
41+
| "mod" -> expandTerm "%" tl
42+
| "<" -> expandTerm "%" tl
43+
| "<=" -> expandTerm "<=" tl
44+
| ">" -> expandTerm ">" tl
45+
| ">=" -> expandTerm ">=" tl
46+
| "=" -> expandTerm "=" tl
47+
| _ ->
9248
PPrint.precede (PPrint.string hd)
93-
(PPrint.parens (PPrint.separate_map (PPrint.precede PPrint.space PPrint.comma) term2KeY tl))
49+
(PPrint.parens
50+
(PPrint.nest 4 (PPrint.separate_map
51+
(PPrint.precede PPrint.space PPrint.comma)
52+
term2KeY tl))))
53+
54+
(*----------------------------------------------------------------------------*)
9455

56+
let pHeader filename =
57+
(* Gives the Header of the KeY file *)
58+
string "// KeY File generated of" ^^ space ^^ string filename ^^ hardline
59+
60+
let pSection name fn sexprs =
61+
let x = List.filter_map fn sexprs in
62+
let doc = PPrint.separate PPrint.hardline x in
63+
hardline ^^ string "\\" ^^ !^name ^^ braces (nest 4 (hardline ^^ doc)^^hardline)
64+
65+
let pSort = function
66+
| Sexp.List [ Sexp.Atom "define-sort"; Sexp.Atom name ] ->
67+
Some
68+
(PPrint.concat [ PPrint.utf8string name; PPrint.semi; PPrint.hardline ])
69+
| _ -> None
70+
71+
let rec pFunction = function
72+
| Sexp.List
73+
[ Sexp.Atom "declare-fun"; Sexp.Atom name; Sexp.List args; Sexp.Atom ret ]
74+
->
75+
buildFunction name args ret
76+
| Sexp.List
77+
[
78+
Sexp.Atom "define-fun"; Sexp.Atom name; Sexp.List args; Sexp.Atom ret; _;
79+
] ->
80+
buildFunction name args ret
81+
(* (List.map (fun x -> match x with
82+
| Sexp.List n::_ -> n
83+
| _ -> Sexp.Atom "") args)*)
84+
| _ -> None
85+
86+
and buildFunction name args ret =
87+
if ret = "bool" then None
88+
else if List.length args = 0 then
89+
Some
90+
(PPrint.concat
91+
[
92+
PPrint.string ret; PPrint.space; PPrint.utf8string name; PPrint.semi;
93+
])
94+
else
95+
Some
96+
(PPrint.concat
97+
[
98+
PPrint.string ret;
99+
PPrint.space;
100+
PPrint.utf8string name;
101+
PPrint.parens
102+
(PPrint.separate_map
103+
(PPrint.precede PPrint.comma PPrint.space)
104+
(fun x ->
105+
match x with
106+
| Sexp.Atom y -> PPrint.string y
107+
| Sexp.List [ Sexp.Atom n ] -> PPrint.string n
108+
| _ -> PPrint.empty)
109+
args);
110+
PPrint.semi;
111+
])
112+
113+
let pPredicate = function
114+
| Sexp.List [ Sexp.Atom "define-fun"; Sexp.Atom name; _; Sexp.Atom "Bool" ] ->
115+
Some
116+
(PPrint.concat [ PPrint.utf8string name; PPrint.semi; PPrint.hardline ])
117+
| _ -> None
118+
119+
120+
let break0 = break 0
121+
let break1 = break 1
122+
123+
let buildRuleForFunction name args ret def =
124+
string ("def" ^ name) ^^ space
125+
^^ braces
126+
(nest 4
127+
(break0 ^^
128+
(PPrint.separate_map break0
129+
(fun x ->
130+
match x with
131+
| Sexp.List [ Sexp.Atom name; Sexp.Atom sort ] ->
132+
!^"\\schemaVar" ^^ space ^^ !^"\\term " ^^ !^sort ^^ space
133+
^^ !^name ^^semi
134+
| _ -> empty)
135+
args
136+
^^ break0
137+
^^ string "\\find"
138+
^^ parens(!^name ^^ parens
139+
(nest 4
140+
(PPrint.separate_map (comma ^^ space)
141+
(fun x ->
142+
match x with
143+
| Sexp.List [ Sexp.Atom name; _ ] -> !^name
144+
| _ -> empty)
145+
args)))
146+
^^ break0 ^^ !^"\\replacewith" ^^ PPrint.parens (term2KeY def)))^^break0)
147+
148+
149+
let pRule = function
150+
(* Tries to construct proof rules for declare functions *)
151+
| Sexp.List
152+
[
153+
Sexp.Atom "define-fun";
154+
Sexp.Atom name;
155+
Sexp.List args;
156+
Sexp.Atom ret;
157+
def
158+
] ->
159+
Some (buildRuleForFunction name args ret def)
160+
| _ -> None
95161

96162
let pprint doc = ToChannel.pretty 0.9 80 stdout doc
97163

98164
let pProblem sexprs =
99-
print_endline "\\problem {";
100165
let assertions =
101166
List.filter_map
102167
(function
@@ -106,47 +171,46 @@ let pProblem sexprs =
106171
let a = Sexp.Atom "and" :: assertions in
107172
let sexpr = Sexp.List a in
108173
let term = term2KeY sexpr in
109-
pprint term;
110-
print_endline "}"
174+
hardline ^^ !^"\\problem" ^^ braces (term ^^ space ^^ !^ "==>")
111175

112-
let pFooter =
113-
print_endline "\n";
114-
()
176+
let pFooter = hardline
115177

116178
let build_goals sexprs =
117179
let rec loop sexprs goals stack =
118180
match sexprs with
119181
| Sexp.List (Sexp.Atom "check-sat" :: _) :: rest ->
120-
loop rest (List.rev (List.flatten stack) :: goals) stack
182+
loop rest (List.rev (List.flatten stack) :: goals) stack
121183
| Sexp.List (Sexp.Atom "pop" :: _) :: rest ->
122-
loop rest goals (List.tl stack)
123-
| Sexp.List (Sexp.Atom "push" :: _) :: rest ->
124-
loop rest goals ([] :: stack)
125-
| (_ as term)::rest ->
126-
let firstStack =
127-
if 0 = List.length stack then [] else List.hd stack
128-
in
129-
let restStack = if 0 = List.length stack then [] else List.tl stack in
130-
loop rest goals ((term :: firstStack) :: restStack)
184+
loop rest goals (List.tl stack)
185+
| Sexp.List (Sexp.Atom "push" :: _) :: rest -> loop rest goals ([] :: stack)
186+
| (_ as term) :: rest ->
187+
let firstStack = if 0 = List.length stack then [] else List.hd stack in
188+
let restStack = if 0 = List.length stack then [] else List.tl stack in
189+
loop rest goals ((term :: firstStack) :: restStack)
131190
| [] -> goals
132191
in
133192
loop sexprs [] []
134193

135194
let smt2key filename =
136195
let sexprs = Sexp.load_sexps filename in
137196
let goals = build_goals sexprs in
138-
List.iter (fun dt ->
139-
pHeader filename;
140-
pSection "sorts" pSort dt;
141-
pSection "functions" pFunction dt;
142-
pSection "predicates" pSort dt;
143-
pProblem dt;
144-
pFooter) goals
197+
198+
let docs =
199+
List.map
200+
(fun dt ->
201+
pHeader filename ^^ pSection "sorts" pSort dt
202+
^^ pSection "functions" pFunction dt
203+
^^ pSection "predicates" pSort dt
204+
^^ pSection "rules" pRule dt
205+
^^ pProblem dt ^^ pFooter)
206+
goals
207+
in
208+
List.iter (fun doc -> ToChannel.pretty 0.9 80 stdout doc) docs
145209

146210
open Sys
211+
147212
let () =
148-
if (Array.length Sys.argv) > 1 then
213+
if Array.length Sys.argv > 1 then
149214
let arg = Array.get Sys.argv 1 in
150215
smt2key arg
151-
else
152-
print_endline "Insufficient Arguments"
216+
else print_endline "Insufficient Arguments"

‎smt2key.opam

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
# This file is generated by dune, edit dune-project instead
22
opam-version: "2.0"
3-
synopsis: "An OCaml library for HTTP clients and servers"
4-
description: "A longer description"
3+
synopsis: "xxx"
4+
description: "xxx"
55
maintainer: ["[email protected]"]
66
authors: ["Alexander Weigl"]
77
license: "GPLv3"
8-
homepage: "https://github.com/mirage/ocaml-cohttp"
9-
bug-reports: "https://github.com/mirage/ocaml-cohttp/issues"
8+
homepage: "https://github.com/wadoon/smt2key"
9+
bug-reports: "https://github.com/wadoon/smt2key/issues"
1010
depends: [
1111
"dune" {>= "2.9"}
1212
"alcotest" {with-test}
@@ -30,4 +30,4 @@ build: [
3030
]
3131
["dune" "install" "-p" name "--create-install-files" name]
3232
]
33-
dev-repo: "git+https://github.com/mirage/ocaml-cohttp.git"
33+
dev-repo: "git+https://github.com/wadoon/smt2key.git"

‎test/a.smt2

+1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
(declare-fun f (Int) Int)
22
(declare-fun a () Int) ; a is a constant
3+
(define-fun q ((i Int)) Int (* 2 i))
34
(declare-const b Int) ; syntax sugar for (declare-fun b () Int)
45
(assert (> a 20))
56
(assert (> b a))

0 commit comments

Comments
 (0)