[sledge] Move normalization of literals out of Propositional

Summary:
Normalization of literal formulas is determined by their term
arguments. Logically, this is part of the theories, so move this code
out of the Propositional module which is theory-independent and into
Fol, which is theory-sensitive.

Reviewed By: jvillard

Differential Revision: D24371081

fbshipit-source-id: f80a19ab8

sledge/src/fol.ml

@@ -250,28 +250,40 @@ let one = _Z Z.one
  * Formulas
  *)
 
-include Propositional.Make (struct
-  include Trm
+module Prop = Propositional.Make (Trm)
 
-  let zero = zero
+module Fml = struct
+  include Prop.Fml
 
-  let eval_eq d e =
-    match (d, e) with
-    | Z y, Z z -> Some (Z.equal y z)
-    | Q q, Q r -> Some (Q.equal q r)
-    | _ -> None
+  let tt = mk_Tt ()
+  let ff = _Not tt
+  let bool b = if b then tt else ff
 
-  let eval_eq0 = function
-    | Z z -> Some (Z.equal Z.zero z)
-    | Q q -> Some (Q.equal Q.zero q)
-    | _ -> None
+  let _Eq0 = function
+    | Z z -> bool (Z.equal Z.zero z)
+    | Q q -> bool (Q.equal Q.zero q)
+    | x -> _Eq0 x
 
-  let eval_pos = function
-    | Z z -> Some (Z.gt z Z.zero)
-    | Q q -> Some (Q.gt q Q.zero)
-    | _ -> None
-end)
+  let _Pos = function
+    | Z z -> bool (Z.gt z Z.zero)
+    | Q q -> bool (Q.gt q Q.zero)
+    | x -> _Pos x
+
+  let _Eq x y =
+    if x == zero then _Eq0 y
+    else if y == zero then _Eq0 x
+    else
+      match (x, y) with
+      | Z y, Z z -> bool (Z.equal y z)
+      | Q q, Q r -> bool (Q.equal q r)
+      | _ -> (
+        match Sign.of_int (compare_trm x y) with
+        | Neg -> _Eq x y
+        | Zero -> tt
+        | Pos -> _Eq y x )
+end
 
+module Fmls = Prop.Fmls
 open Fml
 
 (*

sledge/src/propositional.ml

@@ -69,29 +69,6 @@ module Make (Trm : TERM) = struct
     let mk_Tt () = tt
     let bool b = if b then tt else ff
 
-    let _Eq0 x =
-      (match eval_eq0 x with Some b -> bool b | None -> Eq0 x)
-      |> check invariant
-
-    let _Eq x y =
-      ( if x == zero then _Eq0 y
-      else if y == zero then _Eq0 x
-      else
-        match eval_eq x y with
-        | Some b -> bool b
-        | None -> (
-          match Sign.of_int (compare_trm x y) with
-          | Neg -> Eq (x, y)
-          | Zero -> tt
-          | Pos -> Eq (y, x) ) )
-      |> check invariant
-
-    let _Pos x =
-      (match eval_pos x with Some b -> bool b | None -> Pos x)
-      |> check invariant
-
-    let _Lit p xs = Lit (p, xs) |> check invariant
-
     let rec _Not p =
       ( match p with
       | Not x -> x
@@ -209,5 +186,10 @@ module Make (Trm : TERM) = struct
         (* (c ? p : n) *)
         | _ -> Cond {cnd; pos; neg} ) )
       |> check invariant
+
+    let _Eq x y = Eq (x, y) |> check invariant
+    let _Eq0 x = Eq0 x |> check invariant
+    let _Pos x = Pos x |> check invariant
+    let _Lit p xs = Lit (p, xs) |> check invariant
   end
 end

sledge/src/propositional_intf.ml

@@ -11,11 +11,6 @@ open Ses
 
 module type TERM = sig
   type trm [@@deriving compare, equal, sexp]
-
-  val zero : trm
-  val eval_eq : trm -> trm -> bool option
-  val eval_eq0 : trm -> bool option
-  val eval_pos : trm -> bool option
 end
 
 (** Formulas, built from literals with predicate symbols from various