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
9b1dcc92
Commit
9b1dcc92
authored
Apr 28, 2015
by
François Bobot
Browse files
[Smtv2] fit lines in 80 columns
parent
21b1f3dd
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/printer/smtv2.ml
View file @
9b1dcc92
...
@@ -57,7 +57,8 @@ let ident_printer =
...
@@ -57,7 +57,8 @@ let ident_printer =
"concat"
;
"bvnot"
;
"bvand"
;
"bvor"
;
"bvneg"
;
"bvadd"
;
"bvmul"
;
"bvudiv"
;
"concat"
;
"bvnot"
;
"bvand"
;
"bvor"
;
"bvneg"
;
"bvadd"
;
"bvmul"
;
"bvudiv"
;
"bvurem"
;
"bvshl"
;
"bvlshr"
;
"bvult"
;
"bvnand"
;
"bvnor"
;
"bvxor"
;
"bvurem"
;
"bvshl"
;
"bvlshr"
;
"bvult"
;
"bvnand"
;
"bvnor"
;
"bvxor"
;
"bvcomp"
;
"bvsub"
;
"bvsdiv"
;
"bvsrem"
;
"bvsmod"
;
"bvashr"
;
"bvule"
;
"bvcomp"
;
"bvsub"
;
"bvsdiv"
;
"bvsrem"
;
"bvsmod"
;
"bvashr"
;
"bvule"
;
"bvugt"
;
"bvuge"
;
"bvslt"
;
"bvsle"
;
"bvsgt"
;
"bvsge"
;
"rotate_left"
;
"rotate_right"
;
"bvugt"
;
"bvuge"
;
"bvslt"
;
"bvsle"
;
"bvsgt"
;
"bvsge"
;
"rotate_left"
;
"rotate_right"
;
"cos"
;
"sin"
;
"tan"
;
"atan"
;
"pi"
;
"cos"
;
"sin"
;
"tan"
;
"atan"
;
"pi"
;
...
@@ -129,12 +130,10 @@ let print_var_list info fmt vsl =
...
@@ -129,12 +130,10 @@ let print_var_list info fmt vsl =
let
model_label
=
Ident
.
create_label
"model"
let
model_label
=
Ident
.
create_label
"model"
let
collect_model_ls
info
ls
=
let
collect_model_ls
info
ls
=
if
ls
.
ls_args
=
[]
&&
if
ls
.
ls_args
=
[]
&&
Slab
.
mem
model_label
ls
.
ls_name
.
id_label
then
Slab
.
mem
model_label
ls
.
ls_name
.
id_label
then
let
t
=
t_app
ls
[]
ls
.
ls_value
in
begin
info
.
info_model
<-
let
t
=
t_app
ls
[]
ls
.
ls_value
in
(
t_label
?
loc
:
ls
.
ls_name
.
id_loc
ls
.
ls_name
.
id_label
t
)
::
info
.
info_model
info
.
info_model
<-
(
t_label
?
loc
:
ls
.
ls_name
.
id_loc
ls
.
ls_name
.
id_label
t
)
::
info
.
info_model
end
(** expr *)
(** expr *)
let
rec
print_term
info
fmt
t
=
let
rec
print_term
info
fmt
t
=
...
...
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