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

Do not generate any constraint (even trivial ones) for monomorphic variables.

parent d7d6e9b3
......@@ -2791,12 +2791,13 @@ module Tallying = struct
with
Not_found -> inf, sup
in
if Var.Set.mem v delta then
if ((equal inf empty) && (equal sup any)) ||
if Var.Set.mem v delta then map
(* if ((equal inf empty) && (equal sup any)) ||
(equal (var v) inf && equal (var v) sup) then
map
else
raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v)))
*)
else
VarMap.add v (new_i, new_s) map
......@@ -2945,14 +2946,14 @@ module Tallying = struct
let singleton delta = function
|Pos (v,s) ->
if Var.Set.mem v delta then
if equal s any || equal (var v) s then S.singleton M.empty
else raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v)))
(*if equal s any || equal (var v) s then *)S.singleton M.empty
(*else raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v))) *)
else
S.singleton (M.singleton v (empty,s))
|Neg (s,v) ->
if Var.Set.mem v delta then
if equal s any || equal (var v) s then S.singleton M.empty
else raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v)))
(*if equal s any || equal (var v) s then *)S.singleton M.empty
(*else raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v))) *)
else
S.singleton (M.singleton v (s,any))
......
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