Commit f57b8c86 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Cosmetic changes.

parent d0b41871
...@@ -3007,9 +3007,9 @@ module Tallying = struct ...@@ -3007,9 +3007,9 @@ module Tallying = struct
let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in
let acc = aux single_chars normchars acc (BoolChars.get t.chars) in let acc = aux single_chars normchars acc (BoolChars.get t.chars) in
let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in
let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
let acc = aux single_times normpair acc (BoolPair.get t.times) in let acc = aux single_times normpair acc (BoolPair.get t.times) in
let acc = aux single_xml normpair acc (BoolPair.get t.xml) in let acc = aux single_xml normpair acc (BoolPair.get t.xml) in
let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
(* XXX normrec is not tested at all !!! *) (* XXX normrec is not tested at all !!! *)
aux single_record normrec acc (BoolRec.get t.record) aux single_record normrec acc (BoolRec.get t.record)
...@@ -3290,9 +3290,10 @@ module Tallying = struct ...@@ -3290,9 +3290,10 @@ module Tallying = struct
let d = diff s t in let d = diff s t in
if is_empty d then CS.sat else if is_empty d then CS.sat else
if no_var d then CS.unsat else if no_var d then CS.unsat else
CS.prod acc (norm d)) CS.sat l in CS.prod acc (norm d)) CS.sat l
in
(* Format.printf "Norm : %a\n" CS.pp_s n;*) (* Format.printf "Norm : %a\n" CS.pp_s n;*)
if CS.S.is_empty n then raise Step1Fail else if Pervasives.(n = CS.unsat) then raise Step1Fail else
let m = CS.S.fold (fun c acc -> try CS.ES.union (solve (merge c)) acc with UnSatConstr _ -> acc) n CS.ES.empty in let m = CS.S.fold (fun c acc -> try CS.ES.union (solve (merge c)) acc with UnSatConstr _ -> acc) n CS.ES.empty in
(* Format.printf "Union/Merge : %a \n" CS.ES.print m;*) (* Format.printf "Union/Merge : %a \n" CS.ES.print m;*)
if CS.ES.is_empty m then raise Step2Fail else if CS.ES.is_empty m then raise Step2Fail else
...@@ -3324,7 +3325,9 @@ let apply_raw s t = ...@@ -3324,7 +3325,9 @@ let apply_raw s t =
let gamma = var (Var.mk ~variance:`Covariant "Gamma") in let gamma = var (Var.mk ~variance:`Covariant "Gamma") in
let rec aux (i,acc1) (j,acc2) t1 t2 () = let rec aux (i,acc1) (j,acc2) t1 t2 () =
let acc1 = Lazy.force acc1 and acc2 = Lazy.force acc2 in let acc1 = Lazy.force acc1 and acc2 = Lazy.force acc2 in
try (Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]) , (acc1, acc2) try
(Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]),
(acc1, acc2)
with with
|Tallying.Step1Fail -> raise (Tallying.UnSatConstr "apply_raw step1") |Tallying.Step1Fail -> raise (Tallying.UnSatConstr "apply_raw step1")
|Tallying.Step2Fail -> begin |Tallying.Step2Fail -> begin
......
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