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
cduce
cduce
Commits
880ea5e9
Commit
880ea5e9
authored
May 22, 2014
by
Pietro Abate
Browse files
Add clean_type to tallying algorithm
parent
e18e076b
Changes
1
Show whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
10 additions
and
19 deletions
+10
19
types/types.ml
types/types.ml
+10
19
No files found.
types/types.ml
View file @
880ea5e9
...
@@ 3260,13 +3260,13 @@ let apply_raw s t =
...
@@ 3260,13 +3260,13 @@ let apply_raw s t =
(* cell i of ai contains /\k<=i s_k, cell j of aj contains /\k<=j t_k *)
(* cell i of ai contains /\k<=i s_k, cell j of aj contains /\k<=j t_k *)
let
ai
=
ref
[


]
let
ai
=
ref
[


]
and
aj
=
ref
[


]
in
and
aj
=
ref
[


]
in
(* let result = ref any in *)
let
tallying
i
j
=
let
tallying
i
j
=
try
try
let
s
=
get
ai
i
in
let
s
=
get
ai
i
in
let
t
=
arrow
(
cons
(
get
aj
j
))
cgamma
in
let
t
=
arrow
(
cons
(
get
aj
j
))
cgamma
in
let
sl
=
Tallying
.
tallying
[
(
s
,
t
)
]
in
let
sl
=
Tallying
.
tallying
[
(
s
,
t
)
]
in
let
new_res
=
let
new_res
=
Positive
.
clean_type
(
List
.
fold_left
(
fun
tacc
e
>
List
.
fold_left
(
fun
tacc
e
>
let
res
=
let
res
=
Tallying
.
CS
.
E
.
fold
(
fun
var
subst
acc
>
Tallying
.
CS
.
E
.
fold
(
fun
var
subst
acc
>
...
@@ 3275,17 +3275,8 @@ let apply_raw s t =
...
@@ 3275,17 +3275,8 @@ let apply_raw s t =
in
in
cap
tacc
res
cap
tacc
res
)
any
sl
)
any
sl
)
in
in
(* Uncomment only if we are looking for the mostprecise solution *)
(* if subtype new_res !result && not (subtype !result new_res)
then begin
(* strictly improved the result, continue *)
Format.printf "Found a partial solution at %i, %i: %a@\n@."
i j Print.print new_res;
result := new_res
end
else
*)
raise
(
Found
(
new_res
,
i
,
j
,
sl
))
raise
(
Found
(
new_res
,
i
,
j
,
sl
))
with
with
Tallying
.
Step1Fail
>
(
assert
(
i
==
0
&&
j
==
0
);
raise
(
Tallying
.
UnSatConstr
"apply_raw step1"
))
Tallying
.
Step1Fail
>
(
assert
(
i
==
0
&&
j
==
0
);
raise
(
Tallying
.
UnSatConstr
"apply_raw step1"
))
...
...
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