Commit 7608d9a5 authored by Pietro Abate's avatar Pietro Abate

Fix uppercase/lowercase variable bug

parent 0850fe98
......@@ -3189,6 +3189,14 @@ module Tallying = struct
(* check if there exists a toplevel variable : fun (pos,neg) *)
let toplevel delta single norm_rec mem p n =
let _compare delta v1 v2 =
let monov1 = Var.Set.mem v1 delta in
let monov2 = Var.Set.mem v2 delta in
if monov1 == monov2 then
Var.compare v1 v2
else
if monov1 then 1 else -1
in
match (p,n) with
|([],(`Var x)::neg) ->
let t = single (false,x,[],neg) in
......@@ -3199,7 +3207,7 @@ module Tallying = struct
CS.singleton (Pos (`Var x,t))
|((`Var x)::pos, (`Var y)::neg) ->
if Var.compare (`Var x) (`Var y) < 0 then
if _compare delta (`Var x) (`Var y) < 0 then
let t = single (true,x,pos,n) in
CS.singleton (Pos (`Var x,t))
else
......@@ -3223,6 +3231,7 @@ module Tallying = struct
let rec norm (t,delta,mem) =
(* if we already evaluated it, it is sat *)
let res =
if DescrSet.mem t mem || is_empty t then CS.sat
else if is_var t then begin
(* if there is only one variable then is it A <= 0 or 1 <= A *)
......@@ -3255,8 +3264,9 @@ module Tallying = struct
res
in
res
end
end
in
(* Format.printf "Normalizing %a yields %a\n%!" Print.pp_type t CS.pp_s res; *) res
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P
* (s1,s2) \in N
......
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