Commit 880ea5e9 authored by Pietro Abate's avatar Pietro Abate
Browse files

Add clean_type to tallying algorithm

parent e18e076b
......@@ -3260,32 +3260,23 @@ let apply_raw s t =
(* cell i of ai contains /\k<=i s_k, cell j of aj contains /\k<=j t_k *)
let ai = ref [| |]
and aj = ref [| |] in
(* let result = ref any in *)
let tallying i j =
try
let s = get ai i in
let t = arrow (cons (get aj j)) cgamma in
let sl = Tallying.tallying [ (s,t) ] in
let new_res =
List.fold_left (fun tacc e ->
let res =
Tallying.CS.E.fold (fun var subst acc ->
Positive.substitute acc (var,subst)
) e gamma
in
cap tacc res
) any sl
Positive.clean_type (
List.fold_left (fun tacc e ->
let res =
Tallying.CS.E.fold (fun var subst acc ->
Positive.substitute acc (var,subst)
) e gamma
in
cap tacc res
) any sl
)
in
(* Uncomment only if we are looking for the most-precise 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))
with
Tallying.Step1Fail -> (assert (i == 0 && j == 0); raise (Tallying.UnSatConstr "apply_raw step1"))
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment