Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
2aa275ac
Commit
2aa275ac
authored
Apr 28, 2015
by
François Bobot
Browse files
[Smtv2] fix logic decl printing
introduced in
cc774eb2
parent
9b1dcc92
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/printer/smtv2.ml
View file @
2aa275ac
...
...
@@ -319,15 +319,16 @@ let print_param_decl info fmt ls =
(
print_type_value
info
)
ls
.
ls_value
let
print_logic_decl
info
fmt
(
ls
,
def
)
=
if
Mid
.
mem
ls
.
ls_name
info
.
info_syn
then
()
else
collect_model_ls
info
ls
;
let
vsl
,
expr
=
Decl
.
open_ls_defn
def
in
fprintf
fmt
"@[<hov 2>(define-fun %a (%a) %a %a)@]@
\n
@
\n
"
print_ident
ls
.
ls_name
(
print_var_list
info
)
vsl
(
print_type_value
info
)
ls
.
ls_value
(
print_expr
info
)
expr
;
List
.
iter
forget_var
vsl
if
Mid
.
mem
ls
.
ls_name
info
.
info_syn
then
()
else
begin
collect_model_ls
info
ls
;
let
vsl
,
expr
=
Decl
.
open_ls_defn
def
in
fprintf
fmt
"@[<hov 2>(define-fun %a (%a) %a %a)@]@
\n
@
\n
"
print_ident
ls
.
ls_name
(
print_var_list
info
)
vsl
(
print_type_value
info
)
ls
.
ls_value
(
print_expr
info
)
expr
;
List
.
iter
forget_var
vsl
end
let
print_prop_decl
args
info
fmt
k
pr
f
=
match
k
with
|
Paxiom
->
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment