cleanup: remove labels, use a sum type for negated formulas

sat/sat.ml

@@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+module FI = Formula_intf
+
 module Fsat = struct
 
   exception Bad_atom
@@ -25,7 +27,7 @@ module Fsat = struct
   let dummy = 0
 
   let neg a = - a
-  let norm a = abs a, a < 0
+  let norm a = abs a, if a < 0 then FI.Negated else FI.Same_sign
   let abs = abs
   let sign i = i > 0
   let apply_sign b i = if b then i else neg i
@@ -35,10 +37,6 @@ module Fsat = struct
   let equal (a:int) b = a=b
   let compare (a:int) b = Pervasives.compare a b
 
-  let _str = Hstring.make ""
-  let label a = _str
-  let add_label _ _ = ()
-
   let make i = _make (2 * i)
 
   let fresh, iter =

smt/expr.ml

@@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+module FI = Formula_intf
+
 exception Invalid_var
 
 type var = string
@@ -38,19 +40,15 @@ let neg = function
   | Distinct (a, b) -> Equal (a, b)
 
 let norm = function
-  | Prop i -> Prop (abs i), i < 0
+  | Prop i -> Prop (abs i), if i < 0 then FI.Negated else FI.Same_sign
-  | Equal (a, b) -> Equal (a, b), false
+  | Equal (a, b) -> Equal (a, b), FI.Same_sign
-  | Distinct (a, b) -> Equal (a, b), true
+  | Distinct (a, b) -> Equal (a, b), FI.Negated
 
 (* Only used after normalisation, so usual functions should work *)
 let hash = Hashtbl.hash
 let equal = (=)
 let compare = Pervasives.compare
 
-let s = Hstring.make ""
-let label _ = s
-let add_label _ _ = ()
-
 let print fmt = function
   | Prop i -> Format.fprintf fmt "%s%s%d" (if i < 0 then "¬ " else "") (if i mod 2 = 0 then "v" else "f") ((abs i) / 2)
   | Equal (a, b) -> Format.fprintf fmt "%s = %s" a b

smt/expr.mli

@@ -13,6 +13,8 @@ type formula = private
 type t = formula
 type proof = unit
 
+include Formula_intf.S with type t := formula and type proof := proof
+
 val dummy : t
 
 val fresh : unit -> t
@@ -21,18 +23,6 @@ val mk_prop : int -> t
 val mk_eq : var -> var -> t
 val mk_neq : var -> var -> t
 
-val neg : t -> t
-val norm : t -> t * bool
-
-val hash : t -> int
-val equal : t -> t -> bool
-val compare : t -> t -> int
-
-val label : t -> Hstring.t
-val add_label : Hstring.t -> t -> unit
-
-val print : Format.formatter -> t -> unit
-
 module Term : sig
   type t = var
   val hash : t -> int

solver/expr_intf.ml

@@ -37,9 +37,11 @@ module type S = sig
   val neg : Formula.t -> Formula.t
   (** Formula negation *)
 
-  val norm : Formula.t -> Formula.t * bool
+  val norm : Formula.t -> Formula.t * Formula_intf.negated
-  (** Returns a 'normalized' form of the formula, possibly negated (in which case return true).
+  (** Returns a 'normalized' form of the formula, possibly negated
-      [norm] must be so that [a] and [neg a] normalises to the same formula. *)
+      (in which case return [Negated]).
+      [norm] must be so that [a] and [neg a] normalise to the same formula,
+      but one returns [Negated] and the other [Same_sign]. *)
 
 end
 

solver/formula_intf.ml

@@ -4,6 +4,10 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+type negated =
+  | Negated (* changed sign *)
+  | Same_sign (* kept sign *)
+
 module type S = sig
   (** Signature of formulas that parametrises the SAT/SMT Solver Module. *)
 
@@ -22,19 +26,17 @@ module type S = sig
   val neg : t -> t
   (** Formula negation *)
 
-  val norm : t -> t * bool
+  val norm : t -> t * negated
-  (** Returns a 'normalized' form of the formula, possibly negated (in which case return true).
+  (** Returns a 'normalized' form of the formula, possibly negated
-      [norm] must be so that [a] and [neg a] normalises to the same formula. *)
+      (in which case return [Negated]).
+      [norm] must be so that [a] and [neg a] normalise to the same formula,
+      but one returns [Same_sign] and one returns [Negated] *)
 
   val hash : t -> int
   val equal : t -> t -> bool
   val compare : t -> t -> int
   (** Usual hash and comparison functions. Given to Map and Hash functors. *)
 
-  val label : t -> Hstring.t
-  val add_label : Hstring.t -> t -> unit
-  (** Optional. Not yet used in Solver. *)
-
   val print : Format.formatter -> t -> unit
   (** Printing function used for debugging. *)
 end

solver/internal.ml

@@ -1095,7 +1095,10 @@ module Make
     then raise UndecidedLit
     else assert (var.v_level >= 0);
     let truth = var.pa.is_true in
-    let value = if negated then not truth else truth in
+    let value = match negated with
+      | Formula_intf.Negated -> not truth
+      | Formula_intf.Same_sign -> truth
+    in
     value, var.v_level
 
   let eval lit = fst (eval_level lit)

solver/solver_types.ml

@@ -139,7 +139,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       Vec.push vars (Either.mk_left res);
       res
 
-  let make_boolean_var =
+  let make_boolean_var : formula -> var * Formula_intf.negated =
     fun lit ->
       let lit, negated = E.norm lit in
       try MF.find f_map lit, negated
@@ -177,7 +177,9 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
 
   let add_atom lit =
     let var, negated = make_boolean_var lit in
-    if negated then var.na else var.pa
+    match negated with
+      | Formula_intf.Negated -> var.na
+      | Formula_intf.Same_sign -> var.pa
 
   let make_clause ?tag name ali sz_ali is_learnt premise lvl =
     let atoms = Vec.from_list ali sz_ali dummy_atom in

solver/solver_types_intf.ml

@@ -109,7 +109,7 @@ module type S = sig
   (** Returns the variable associated with the term *)
   val add_atom : formula -> atom
   (** Returns the atom associated with the given formula *)
-  val make_boolean_var : formula -> var * bool
+  val make_boolean_var : formula -> var * Formula_intf.negated
   (** Returns the variable linked with the given formula, and wether the atom associated with the formula
       is [var.pa] or [var.na] *)