From cc3f76b0ad23f96b3f7d79c218db73fd000298ce Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 27 Oct 2020 12:17:51 -0700
Subject: [PATCH] [sledge] Strengthen normalization of conditional terms

Summary:
Apply normalization to conditional terms similar to conditional
formulas: evaluate terms with literal conditions, equal branches, and
ensure the condition is not negative.

Reviewed By: jvillard

Differential Revision: D24532344

fbshipit-source-id: 7818dc496
---
 sledge/src/fml.mli               |  4 ++++
 sledge/src/fol.ml                | 20 ++++++++++++++++----
 sledge/src/propositional_intf.ml |  1 +
 sledge/src/test/fol_test.ml      |  7 ++++---
 4 files changed, 25 insertions(+), 7 deletions(-)

diff --git a/sledge/src/fml.mli b/sledge/src/fml.mli
index 98abc3f45..520fb5a18 100644
--- a/sledge/src/fml.mli
+++ b/sledge/src/fml.mli
@@ -70,3 +70,7 @@ val map_trms : t -> f:(Trm.t -> Trm.t) -> t
 (** Traverse *)
 
 val vars : t -> Var.t iter
+
+(** Query *)
+
+val is_negative : t -> bool
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index affd33ee5..fbeb419cb 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -51,6 +51,18 @@ let pp = ppx (fun _ -> None)
  * and formulas stratified below conditional terms and then expressions.
  *)
 
+let _Ite cnd thn els =
+  match (cnd : Fml.t) with
+  (* (tt ? t : e) ==> t *)
+  | Tt -> thn
+  (* (ff ? t : e) ==> e *)
+  | Not Tt -> els
+  (* (c ? t : t) ==> t *)
+  | _ when equal_cnd thn els -> thn
+  (* (¬c ? t : e) ==> (c ? e : t) *)
+  | _ when Fml.is_negative cnd -> `Ite (Fml.not_ cnd, els, thn)
+  | _ -> `Ite (cnd, thn, els)
+
 (** Map a unary function on terms over the leaves of a conditional term,
     rebuilding the tree of conditionals with the supplied ite construction
     function. *)
@@ -67,7 +79,7 @@ let rec map_cnd : (fml -> 'a -> 'a -> 'a) -> (trm -> 'a) -> cnd -> 'a =
 let embed_into_cnd : exp -> cnd = function
   | #cnd as c -> c
   (* p ==> (p ? 1 : 0) *)
-  | `Fml fml -> `Ite (fml, `Trm Trm.one, `Trm Trm.zero)
+  | `Fml fml -> _Ite fml (`Trm Trm.one) (`Trm Trm.zero)
 
 (** Project out a formula that is embedded into a conditional term.
 
@@ -89,8 +101,8 @@ let ite : fml -> exp -> exp -> exp =
   match (thn, els) with
   | `Fml pos, `Fml neg -> `Fml (cond cnd pos neg)
   | _ -> (
-      let c = `Ite (cnd, embed_into_cnd thn, embed_into_cnd els) in
-      match project_out_fml c with Some f -> `Fml f | None -> c )
+      let c = _Ite cnd (embed_into_cnd thn) (embed_into_cnd els) in
+      match project_out_fml c with Some f -> `Fml f | None -> (c :> exp) )
 
 (** Embed a conditional term into a formula (associating 0 with false and
     non-0 with true, lifted over the tree mapping conditional terms to
@@ -303,7 +315,7 @@ module Term = struct
         let thn' = map_vars_c ~f thn in
         let els' = map_vars_c ~f els in
         if cnd' == cnd && thn' == thn && els' == els then c
-        else `Ite (cnd', thn', els')
+        else _Ite cnd' thn' els'
     | `Trm t ->
         let t' = Trm.map_vars ~f t in
         if t' == t then c else `Trm t'
diff --git a/sledge/src/propositional_intf.ml b/sledge/src/propositional_intf.ml
index 187f4123a..c7ccacb40 100644
--- a/sledge/src/propositional_intf.ml
+++ b/sledge/src/propositional_intf.ml
@@ -50,6 +50,7 @@ module type FORMULA = sig
   val _Lit : Predsym.t -> trm array -> t
   val and_ : t -> t -> t
   val or_ : t -> t -> t
+  val is_negative : t -> bool
   val trms : t -> trm iter
 end
 
diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml
index 9f114318a..531c56f2d 100644
--- a/sledge/src/test/fol_test.ml
+++ b/sledge/src/test/fol_test.ml
@@ -420,13 +420,14 @@ let%test_module _ =
           {sat= true;
            rep= [[%x_5 ↦ 1];
                  [%y_6 ↦ ];
-                 [(%x_5 ≠ 0) ↦ -1];
-                 [(%y_6 ≠ 0) ↦ -1];
+                 [(%x_5 = 0) ↦ 0];
+                 [(%y_6 = 0) ↦ 0];
                  [-1 ↦ ];
                  [0 ↦ ]]} |}]
 
     let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
-    let%test _ = implies_eq r14 b (Formula.inject Formula.tt)
+    (* incomplete *)
+    let%test _ = not (implies_eq r14 b (Formula.inject Formula.tt))
 
     let b = Formula.inject (Formula.dq x !0)
     let r15 = of_eqs [(b, b); (x, !1)]