Commit e174dcd5 authored by Pietro Abate's avatar Pietro Abate
Browse files

remove unused argument from Tallying.CS.singleton

parent 5bcd5da0
...@@ -3131,7 +3131,7 @@ module Tallying = struct ...@@ -3131,7 +3131,7 @@ module Tallying = struct
type sl = sigma list type sl = sigma list
let singleton _delta c = let singleton c =
let constr = let constr =
match c with match c with
|Pos (v,s) -> M.singleton v (empty,s) |Pos (v,s) -> M.singleton v (empty,s)
...@@ -3187,28 +3187,28 @@ module Tallying = struct ...@@ -3187,28 +3187,28 @@ module Tallying = struct
let single_arrow = single_aux (fun p -> { empty with arrow = BoolPair.atom (`Atm p) }) let single_arrow = single_aux (fun p -> { empty with arrow = BoolPair.atom (`Atm p) })
(* check if there exists a toplevel varaible : fun (pos,neg) *) (* check if there exists a toplevel variable : fun (pos,neg) *)
let toplevel delta single norm_rec mem p n = let toplevel delta single norm_rec mem p n =
match (p,n) with match (p,n) with
|([],(`Var x)::neg) -> |([],(`Var x)::neg) ->
let t = single (false,x,[],neg) in let t = single (false,x,[],neg) in
CS.singleton delta (Neg (t,`Var x)) CS.singleton (Neg (t,`Var x))
|((`Var x)::pos,[]) -> |((`Var x)::pos,[]) ->
let t = single (true,x,pos,[]) in let t = single (true,x,pos,[]) in
CS.singleton delta (Pos (`Var x,t)) CS.singleton (Pos (`Var x,t))
|((`Var x)::pos, (`Var y)::neg) -> |((`Var x)::pos, (`Var y)::neg) ->
if Var.compare (`Var x) (`Var y) < 0 then if Var.compare (`Var x) (`Var y) < 0 then
let t = single (true,x,pos,n) in let t = single (true,x,pos,n) in
CS.singleton delta (Pos (`Var x,t)) CS.singleton (Pos (`Var x,t))
else else
let t = single (false,y,p,neg) in let t = single (false,y,p,neg) in
CS.singleton delta (Neg (t,`Var y)) CS.singleton (Neg (t,`Var y))
|([`Atm a], (`Var x)::neg) -> |([`Atm a], (`Var x)::neg) ->
let t = single (false,x,p,neg) in let t = single (false,x,p,neg) in
CS.singleton delta (Neg (t,`Var x)) CS.singleton (Neg (t,`Var x))
|([`Atm t], []) -> norm_rec (t,delta,mem) |([`Atm t], []) -> norm_rec (t,delta,mem)
|_,_ -> assert false |_,_ -> assert false
...@@ -3230,7 +3230,7 @@ module Tallying = struct ...@@ -3230,7 +3230,7 @@ module Tallying = struct
if Var.Set.mem v delta then CS.unsat if Var.Set.mem v delta then CS.unsat
else else
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
CS.singleton delta s CS.singleton s
(* if there are no vars, and it is not empty then unsat *) (* if there are no vars, and it is not empty then unsat *)
end else if no_var t then CS.unsat end else if no_var t then CS.unsat
else begin else begin
......
...@@ -418,7 +418,7 @@ module Tallying : sig ...@@ -418,7 +418,7 @@ module Tallying : sig
val pp_sl : Format.formatter -> sl -> unit val pp_sl : Format.formatter -> sl -> unit
(* val merge : m -> m -> m *) (* val merge : m -> m -> m *)
val singleton : Var.Set.t -> constr -> s val singleton : constr -> s
val sat : s val sat : s
val unsat : s val unsat : s
val union : s -> s -> s val union : s -> s -> 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