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

WIP

parent 6d76a68b
......@@ -2592,9 +2592,10 @@ module Positive = struct
|`Neg v -> Format.fprintf ppf "`Neg(%a)" aux v
end
in
aux v
aux ppf v
let printf = pp Format.std_formatter
let dump ppf t = pp ppf (decompose t)
(* returns a recursive type where all occurrences of alpha n t
* are substituted with a recursive variable X *)
......@@ -3038,14 +3039,18 @@ module Tallying = struct
(* norm generates a constraint set for the costraint t <= 0 *)
let rec norm (t,delta,mem) =
Format.eprintf "In norm %a@\n" Print.pp_type t;
Format.eprintf "Mem is: @\n";
DescrSet.iter (fun e -> Format.eprintf "%a@\n" Print.pp_type e) mem;
Format.eprintf "------------------@\n";
(* if we already evaluated it, it is sat *)
if DescrSet.mem t mem || is_empty t then begin
(*Format.printf "Sat for type %a\n%!" Print.print t; *)
CS.sat end
else begin
if is_empty t then CS.sat
(* if there is only one variable then is it A <= 0 or 1 <= A *)
else if is_var t then
if is_var t then
let (v,p) = TLV.max t.toplvars in
if Var.Set.mem v delta then CS.unsat
else
......@@ -3055,7 +3060,14 @@ module Tallying = struct
else if (*no_var t*) Var.Set.subset t.toplvars.TLV.fv delta
then CS.unsat
else begin
Format.eprintf "Mem before is: @\n";
DescrSet.iter (fun e -> Format.eprintf "%a@\n" Print.pp_type e) mem;
Format.eprintf "------------------@\n";
let mem = DescrSet.add t mem in
Format.eprintf "Mem after adding %a is: @\n" Print.pp_type t;
DescrSet.iter (fun e -> Format.eprintf "%a@\n" Print.pp_type e) mem;
Format.eprintf "=============================@\n";
let aux single norm_aux acc l = big_prod delta (toplevel delta single norm_aux mem) acc l in
let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in
......@@ -3065,7 +3077,6 @@ module Tallying = struct
let acc = aux single_xml normpair acc (BoolPair.get t.xml) in
let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in
(* XXX normrec is not tested at all !!! *)
aux single_record normrec acc (BoolRec.get t.record)
end
......@@ -3380,6 +3391,7 @@ let squaresubtype delta s t =
| Tallying.Step2Fail -> () (* continue *)
in
let rec loop i =
Format.eprintf "Tallying at step %i@\n" i;
try
let ss =
if i = 0 then s
......
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