Commit 5b739da7 authored by Pietro Abate's avatar Pietro Abate
Browse files

Fix fresh variable generation

parent 6caf0353
......@@ -604,7 +604,7 @@ let substfree t =
v
end
in
substfree_aux (subvar (Hashtbl.create 197)) t
substfree_aux (subvar (Hashtbl.create 17)) t
(* substitute all variables with s *)
let substvariance t =
......@@ -2796,7 +2796,7 @@ module Tallying = struct
exception Step2Fail
let tallying l =
let n = List.fold_left (fun acc (s,t) -> CS.prod acc (norm(diff s t))) CS.S.empty l in
let n = List.fold_left (fun acc (s,t) -> CS.prod acc (norm(diff s t))) CS.sat l in
if CS.S.is_empty n 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
if CS.ES.is_empty m then raise Step2Fail else
......
......@@ -65,9 +65,9 @@ end
let mk ?fresh ?variance id =
`Var (make_id ?fresh ?variance id)
let fresh ?variance : unit -> [> var ] =
let fresh : ?variance:[ `None| `Both | `ContraVariant | `Covariant ] -> unit -> [> var ] =
let counter = ref 0 in
fun _ ->
fun ?variance -> fun _ ->
let id = (Printf.sprintf "_fresh_%d" !counter) in
let v = mk ~fresh:true ?variance id in
incr counter;
......
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