Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
cffa3177
Commit
cffa3177
authored
Mar 14, 2017
by
Sylvain Dailler
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Q217-025 minor typo
Change-Id: Id165717756375db150031589740470cc1e08b8ac
parent
a303ae72
Changes
6
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
17 additions
and
16 deletions
+17
-16
src/driver/collect_data_model.ml
src/driver/collect_data_model.ml
+6
-6
src/driver/collect_data_model.mli
src/driver/collect_data_model.mli
+2
-2
src/driver/parse_smtv2_model_parser.mly
src/driver/parse_smtv2_model_parser.mly
+1
-1
src/driver/smt2_model_defs.ml
src/driver/smt2_model_defs.ml
+3
-3
src/driver/smt2_model_defs.mli
src/driver/smt2_model_defs.mli
+3
-3
src/transform/intro_projections_counterexmp.ml
src/transform/intro_projections_counterexmp.ml
+2
-1
No files found.
src/driver/collect_data_model.ml
View file @
cffa3177
...
...
@@ -5,7 +5,7 @@ open Strings
exception
Not_value
(* Adds all referenced cvc4 variables found in the term t to table *)
let
rec
get_variables_term
(
table
:
correspond
a
nce_table
)
t
=
let
rec
get_variables_term
(
table
:
correspond
e
nce_table
)
t
=
match
t
with
|
Variable
_
|
Function_Local_Variable
_
|
Boolean
_
|
Integer
_
|
Decimal
_
|
Other
_
|
Bitvector
_
->
table
...
...
@@ -40,7 +40,7 @@ and get_variables_array table a =
let
table
=
get_variables_term
table
t1
in
get_variables_term
table
t2
let
get_all_var
(
table
:
correspond
a
nce_table
)
=
let
get_all_var
(
table
:
correspond
e
nce_table
)
=
Mstr
.
fold
(
fun
_key
element
table
->
match
element
with
|
_
,
Noelement
->
table
...
...
@@ -89,7 +89,7 @@ let remove_end_num s =
(* Add the variables that can be deduced from ITE to the table of variables *)
let
add_vars_to_table
table
value
=
let
rec
add_vars_to_table
(
table
:
correspond
a
nce_table
)
value
=
let
rec
add_vars_to_table
(
table
:
correspond
e
nce_table
)
value
=
let
t
=
match
(
snd
value
)
with
|
Term
t
->
t
|
Function
(
_
,
t
)
->
t
...
...
@@ -184,7 +184,7 @@ and refine_function table term =
To_array
(
refine_function
table
t
)
and
refine_variable_value
(
table
:
correspond
a
nce_table
)
key
v
=
and
refine_variable_value
(
table
:
correspond
e
nce_table
)
key
v
=
let
(
b
,
t
)
=
v
in
if
b
then
table
...
...
@@ -319,7 +319,7 @@ let corres_else_element table to_rep of_rep =
in
corres_else_element
table
to_rep
of_rep
let
to_rep_of_rep
(
table
:
correspond
a
nce_table
)
=
let
to_rep_of_rep
(
table
:
correspond
e
nce_table
)
=
let
to_reps
=
List
.
sort
(
fun
x
y
->
String
.
compare
(
fst
x
)
(
fst
y
))
(
Mstr
.
fold
(
fun
key
value
acc
->
...
...
@@ -342,7 +342,7 @@ let to_rep_of_rep (table: correspondance_table) =
to_rep_of_rep
table
to_reps
of_reps
let
create_list
(
table
:
correspond
a
nce_table
)
=
let
create_list
(
table
:
correspond
e
nce_table
)
=
(* First populate the table with all references to a cvc variable *)
let
table
=
get_all_var
table
in
...
...
src/driver/collect_data_model.mli
View file @
cffa3177
(* Debugging function *)
val
print_table
:
Smt2_model_defs
.
correspond
a
nce_table
->
unit
Smt2_model_defs
.
correspond
e
nce_table
->
unit
(* From the table generated by the parser, build a list of model_element *)
val
create_list
:
Smt2_model_defs
.
correspond
a
nce_table
->
Model_parser
.
model_element
list
Smt2_model_defs
.
correspond
e
nce_table
->
Model_parser
.
model_element
list
src/driver/parse_smtv2_model_parser.mly
View file @
cffa3177
...
...
@@ -12,7 +12,7 @@
%
{
%
}
%
start
<
Smt2_model_defs
.
correspond
a
nce_table
>
output
%
start
<
Smt2_model_defs
.
correspond
e
nce_table
>
output
%
token
<
string
>
SPACE
%
token
<
string
>
ATOM
%
token
MODEL
...
...
src/driver/smt2_model_defs.ml
View file @
cffa3177
...
...
@@ -27,9 +27,9 @@ type definition =
|
Noelement
(* Type returned by parsing of model.
An hashtable that makes a correspond
a
nce between names (string) and
An hashtable that makes a correspond
e
nce between names (string) and
associated definition (complex stuff) *)
type
correspond
a
nce_table
=
(
bool
*
definition
)
Mstr
.
t
type
correspond
e
nce_table
=
(
bool
*
definition
)
Mstr
.
t
let
rec
print_array
fmt
a
=
match
a
with
...
...
@@ -63,7 +63,7 @@ let print_def fmt d =
|
Term
t
->
Format
.
fprintf
fmt
"TERM : %a"
print_term
t
|
Noelement
->
Format
.
fprintf
fmt
"NOELEMENT"
let
add_element
x
(
t
:
correspond
a
nce_table
)
b
=
let
add_element
x
(
t
:
correspond
e
nce_table
)
b
=
match
x
with
|
None
->
t
|
Some
(
key
,
value
)
->
...
...
src/driver/smt2_model_defs.mli
View file @
cffa3177
...
...
@@ -29,13 +29,13 @@ type definition =
|
Noelement
(* Type returned by parsing of model.
An hashtable that makes a correspond
a
nce between names (string) and
An hashtable that makes a correspond
e
nce between names (string) and
associated definition (complex stuff) *)
(* The boolean is true when the term has no external variable *)
type
correspond
a
nce_table
=
(
bool
*
definition
)
Mstr
.
t
type
correspond
e
nce_table
=
(
bool
*
definition
)
Mstr
.
t
val
add_element
:
(
string
*
definition
)
option
->
correspond
a
nce_table
->
bool
->
correspond
a
nce_table
correspond
e
nce_table
->
bool
->
correspond
e
nce_table
val
make_local
:
variable
list
->
term
->
term
...
...
src/transform/intro_projections_counterexmp.ml
View file @
cffa3177
...
...
@@ -124,7 +124,8 @@ let get_list_projs t map_projs =
let
rec
projections_for_term
ls
term
proj_name
applied_projs
env
map_projs
=
(* Return declarations for projections of the term.
Parameter proj_name is the name of the projection
Parameter applied_proj_f is a set of projection functions already applied to the term *)
Parameter applied_proj_f is a set of projection functions already applied
to the term *)
match
(
Opt
.
get
term
.
t_ty
)
.
ty_node
with
|
Tyapp
(
ts
,
[
_t_from
;
_t_to
])
when
ts
.
ts_name
.
id_string
=
"map"
->
begin
let
pfs
=
get_list_projs
term
map_projs
in
...
...
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