From 3f2de059208c03e3c4d6307f40229ddc38c97c71 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 20 Oct 2020 02:36:32 -0700
Subject: [PATCH] [sledge] Add general uninterpreted predicates and use for
 "ord" and "uno"

Summary:
Generalize Fol.Predsym to separate Predsym module for arbitrary
uninterpreted predicate symbols.

Add uninterpreted predicate literals to Ses.Term.

Use uninterpreted predicates to represent "ord" and "uno".

Reviewed By: jvillard

Differential Revision: D24306105

fbshipit-source-id: bdd72a8be
---
 sledge/src/fol.ml          | 44 ++++++++++++++--------------
 sledge/src/fol.mli         |  4 +++
 sledge/src/ses/equality.ml |  3 +-
 sledge/src/ses/predsym.ml  | 16 ++++++++++
 sledge/src/ses/predsym.mli | 13 +++++++++
 sledge/src/ses/term.ml     | 60 +++++++++++++++++++++++---------------
 sledge/src/ses/term.mli    |  8 ++---
 7 files changed, 97 insertions(+), 51 deletions(-)
 create mode 100644 sledge/src/ses/predsym.ml
 create mode 100644 sledge/src/ses/predsym.mli

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 9330c02c2..66c583fa6 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -10,6 +10,7 @@ let pp_boxed fs fmt =
   Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
 
 module Funsym = Ses.Funsym
+module Predsym = Ses.Predsym
 
 (*
  * Terms
@@ -77,18 +78,6 @@ let _Tuple es = Tuple es
 let _Project ary idx tup = Project {ary; idx; tup}
 let _Apply f a = Apply (f, a)
 
-(*
- * (Uninterpreted) Predicate Symbols
- *)
-
-module Predsym = struct
-  type t = Ordered [@@deriving compare, equal, hash, sexp]
-
-  let pp fs p =
-    let pf fmt = pp_boxed fs fmt in
-    match p with Ordered -> pf "ordered"
-end
-
 (*
  * Formulas
  *)
@@ -817,6 +806,11 @@ let apNt : (trm list -> trm) -> exp array -> exp =
     (fun xs -> `Trm (f xs))
     (Array.fold ~f:(fun xs x -> embed_into_cnd x :: xs) ~init:[] xs)
 
+let apNf : (trm list -> fml) -> exp iarray -> fml =
+ fun f xs ->
+  rev_mapN_cnd _Cond f
+    (IArray.fold ~f:(fun xs x -> embed_into_cnd x :: xs) ~init:[] xs)
+
 (*
  * Terms: exposed interface
  *)
@@ -990,6 +984,11 @@ module Formula = struct
   let lt a b = gt b a
   let le a b = ge b a
 
+  (* uninterpreted *)
+
+  let uposlit p e = ap1f (_UPosLit p) e
+  let uneglit p e = ap1f (_UNegLit p) e
+
   (* connectives *)
 
   let and_ = _And
@@ -1164,11 +1163,11 @@ let rec f_to_ses : fml -> Ses.Term.t = function
   | Cond {cnd; pos; neg} ->
       Ses.Term.conditional ~cnd:(f_to_ses cnd) ~thn:(f_to_ses pos)
         ~els:(f_to_ses neg)
-  | UPosLit (Ordered, Tuple [|x; y|]) ->
-      Ses.Term.ord (t_to_ses x) (t_to_ses y)
-  | UNegLit (Ordered, Tuple [|x; y|]) ->
-      Ses.Term.uno (t_to_ses x) (t_to_ses y)
-  | (UPosLit (Ordered, _) | UNegLit (Ordered, _)) as f ->
+  | UPosLit (sym, Tuple args) ->
+      Ses.Term.poslit sym (IArray.of_array (Array.map ~f:t_to_ses args))
+  | UNegLit (sym, Tuple args) ->
+      Ses.Term.neglit sym (IArray.of_array (Array.map ~f:t_to_ses args))
+  | (UPosLit _ | UNegLit _) as f ->
       fail "cannot translate to Ses: %a" pp_f f ()
 
 let rec to_ses : exp -> Ses.Term.t = function
@@ -1196,10 +1195,11 @@ let uap1 f = ap1t (fun x -> Apply (f, Tuple [|x|]))
 let uap2 f = ap2t (fun x y -> Apply (f, Tuple [|x; y|]))
 let upos2 p = ap2f (fun x y -> _UPosLit p (Tuple [|x; y|]))
 let uneg2 p = ap2f (fun x y -> _UNegLit p (Tuple [|x; y|]))
+let uposN p = apNf (fun xs -> _UPosLit p (Tuple (Array.of_list xs)))
+let unegN p = apNf (fun xs -> _UNegLit p (Tuple (Array.of_list xs)))
 
 let rec uap_tt f a = uap1 f (of_ses a)
 and uap_ttt f a b = uap2 f (of_ses a) (of_ses b)
-and ap_ttf f a b = `Fml (f (of_ses a) (of_ses b))
 
 and ap2 mk_f mk_t a b =
   match (of_ses a, of_ses b) with
@@ -1238,8 +1238,8 @@ and of_ses : Ses.Term.t -> exp =
   | Ap2 (Dq, d, e) -> ap2_f xor dq d e
   | Ap2 (Lt, d, e) -> ap2_f (fun p q -> and_ (not_ p) q) lt d e
   | Ap2 (Le, d, e) -> ap2_f (fun p q -> or_ (not_ p) q) le d e
-  | Ap2 (Ord, d, e) -> ap_ttf (upos2 Ordered) d e
-  | Ap2 (Uno, d, e) -> ap_ttf (uneg2 Ordered) d e
+  | PosLit (p, es) -> `Fml (uposN p (IArray.map ~f:of_ses es))
+  | NegLit (p, es) -> `Fml (unegN p (IArray.map ~f:of_ses es))
   | Add sum -> (
     match Ses.Term.Qset.pop_min_elt sum with
     | None -> zero
@@ -1640,8 +1640,8 @@ module Term_of_Llair = struct
     | Ap2 (Ult, typ, d, e) -> usap_ttf lt typ d e
     | Ap2 (Uge, typ, d, e) -> usap_ttf ge typ d e
     | Ap2 (Ule, typ, d, e) -> usap_ttf le typ d e
-    | Ap2 (Ord, _, d, e) -> ap_ttf (upos2 Ordered) d e
-    | Ap2 (Uno, _, d, e) -> ap_ttf (uneg2 Ordered) d e
+    | Ap2 (Ord, _, d, e) -> ap_ttf (upos2 (Predsym.uninterp "ord")) d e
+    | Ap2 (Uno, _, d, e) -> ap_ttf (uneg2 (Predsym.uninterp "ord")) d e
     | Ap2 (Add, Integer {bits= 1; _}, p, q) -> ap_fff xor p q
     | Ap2 (Sub, Integer {bits= 1; _}, p, q) -> ap_fff xor p q
     | Ap2 (Mul, Integer {bits= 1; _}, p, q) -> ap_fff and_ p q
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 43706019f..5bda57189 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -131,6 +131,10 @@ and Formula : sig
   val lt : Term.t -> Term.t -> t
   val le : Term.t -> Term.t -> t
 
+  (* uninterpreted *)
+  val uposlit : Ses.Predsym.t -> Term.t -> t
+  val uneglit : Ses.Predsym.t -> Term.t -> t
+
   (* connectives *)
   val not_ : t -> t
   val and_ : t -> t -> t
diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml
index 89deb447a..e472507ad 100644
--- a/sledge/src/ses/equality.ml
+++ b/sledge/src/ses/equality.ml
@@ -16,7 +16,8 @@ let classify e =
   match (e : Term.t) with
   | Add _ | Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
       Interpreted
-  | Mul _ | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ | Apply _ | And _ | Or _ ->
+  | Mul _ | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ | Apply _ | PosLit _ | NegLit _
+   |And _ | Or _ ->
       Uninterpreted
   | Var _ | Integer _ | Rational _ | Float _ | Label _ | RecRecord _ ->
       Atomic
diff --git a/sledge/src/ses/predsym.ml b/sledge/src/ses/predsym.ml
new file mode 100644
index 000000000..0147f561a
--- /dev/null
+++ b/sledge/src/ses/predsym.ml
@@ -0,0 +1,16 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Uninterpreted Predicate Symbols *)
+
+type t = string [@@deriving compare, equal, hash, sexp]
+
+let pp ppf p =
+  let pf fmt = Format.fprintf ppf fmt in
+  pf "%s" p
+
+let uninterp p = p
diff --git a/sledge/src/ses/predsym.mli b/sledge/src/ses/predsym.mli
new file mode 100644
index 000000000..1f04a36b1
--- /dev/null
+++ b/sledge/src/ses/predsym.mli
@@ -0,0 +1,13 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Uninterpreted Predicate Symbols *)
+
+type t [@@deriving compare, equal, hash, sexp]
+
+val pp : t pp
+val uninterp : string -> t
diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml
index 905a98539..caaf56327 100644
--- a/sledge/src/ses/term.ml
+++ b/sledge/src/ses/term.ml
@@ -22,8 +22,6 @@ type op2 =
   | Dq
   | Lt
   | Le
-  | Ord
-  | Uno
   | Div
   | Rem
   | Xor
@@ -76,6 +74,8 @@ and T : sig
     | Rational of {data: Q.t}
     | RecRecord of int
     | Apply of Funsym.t * t iarray
+    | PosLit of Predsym.t * t iarray
+    | NegLit of Predsym.t * t iarray
   [@@deriving compare, equal, sexp]
 end = struct
   type set = Set.t [@@deriving compare, equal, sexp]
@@ -97,6 +97,8 @@ end = struct
     | Rational of {data: Q.t}
     | RecRecord of int
     | Apply of Funsym.t * t iarray
+    | PosLit of Predsym.t * t iarray
+    | NegLit of Predsym.t * t iarray
   [@@deriving compare, equal, sexp]
 
   (* Note: solve (and invariant) requires Qset.min_elt to return a
@@ -268,8 +270,6 @@ let rec ppx strength fs term =
     | Ap2 (Dq, x, y) -> pf "(%a@ @<2>≠ %a)" pp x pp y
     | Ap2 (Lt, x, y) -> pf "(%a@ < %a)" pp x pp y
     | Ap2 (Le, x, y) -> pf "(%a@ @<2>≤ %a)" pp x pp y
-    | Ap2 (Ord, x, y) -> pf "(%a@ ord %a)" pp x pp y
-    | Ap2 (Uno, x, y) -> pf "(%a@ uno %a)" pp x pp y
     | Add args ->
         let pp_poly_term fs (monomial, coefficient) =
           match monomial with
@@ -309,6 +309,10 @@ let rec ppx strength fs term =
     | RecRecord i -> pf "(rec_record %i)" i
     | Apply (sym, args) ->
         pf "(%a@ %a)" Funsym.pp sym (IArray.pp "@ " pp) args
+    | PosLit (sym, args) ->
+        pf "(%a@ %a)" Predsym.pp sym (IArray.pp "@ " pp) args
+    | NegLit (sym, args) ->
+        pf "¬(%a@ %a)" Predsym.pp sym (IArray.pp "@ " pp) args
   in
   pp fs term
   [@@warning "-9"]
@@ -743,6 +747,9 @@ and simp_concat xs =
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
+let simp_poslit sym args = PosLit (sym, args)
+let simp_neglit sym args = NegLit (sym, args)
+
 (* comparison *)
 
 let simp_lt x y =
@@ -757,9 +764,6 @@ let simp_le x y =
   | Rational {data= i}, Rational {data= j} -> bool (Q.leq i j)
   | _ -> Ap2 (Le, x, y)
 
-let simp_ord x y = Ap2 (Ord, x, y)
-let simp_uno x y = Ap2 (Uno, x, y)
-
 let rec simp_eq x y =
   match
     match Ordering.of_int (compare x y) with
@@ -839,10 +843,10 @@ and simp_not term =
   | Ap2 (Lt, x, y) -> simp_le y x
   (* ¬(x <= y) ==> y < x *)
   | Ap2 (Le, x, y) -> simp_lt y x
-  (* ¬(x ≠ nan ∧ y ≠ nan) ==> x = nan ∨ y = nan *)
-  | Ap2 (Ord, x, y) -> simp_uno x y
-  (* ¬(x = nan ∨ y = nan) ==> x ≠ nan ∧ y ≠ nan *)
-  | Ap2 (Uno, x, y) -> simp_ord x y
+  (* ¬p(xs) ==> (¬p)(xs) *)
+  | PosLit (p, xs) -> simp_neglit p xs
+  (* ¬(¬p)(xs) ==> p(xs) *)
+  | NegLit (p, xs) -> simp_poslit p xs
   (* ¬(a ∧ b) ==> ¬a ∨ ¬b *)
   | And xs -> simp_or (Set.map ~f:simp_not xs)
   (* ¬(a ∨ b) ==> ¬a ∧ ¬b *)
@@ -927,8 +931,6 @@ let norm2 op x y =
   | Dq -> simp_dq x y
   | Lt -> simp_lt x y
   | Le -> simp_le x y
-  | Ord -> simp_ord x y
-  | Uno -> simp_uno x y
   | Div -> simp_div x y
   | Rem -> simp_rem x y
   | Xor -> simp_xor x y
@@ -961,8 +963,6 @@ let eq = norm2 Eq
 let dq = norm2 Dq
 let lt = norm2 Lt
 let le = norm2 Le
-let ord = norm2 Ord
-let uno = norm2 Uno
 let neg e = simp_negate e |> check invariant
 let add e f = simp_add2 e f |> check invariant
 let addN args = simp_add args |> check invariant
@@ -991,6 +991,8 @@ let select ~rcd ~idx = norm1 (Select idx) rcd
 let update ~rcd ~idx ~elt = norm2 (Update idx) rcd elt
 let rec_record i = simp_rec_record i |> check invariant
 let apply sym args = simp_apply sym args |> check invariant
+let poslit sym args = simp_poslit sym args |> check invariant
+let neglit sym args = simp_neglit sym args |> check invariant
 
 let rec binary mk x y = mk (of_exp x) (of_exp y)
 
@@ -1017,8 +1019,12 @@ and of_exp e =
   | Ap2 (Uge, typ, x, y) -> ubinary le typ y x
   | Ap2 (Ult, typ, x, y) -> ubinary lt typ x y
   | Ap2 (Ule, typ, x, y) -> ubinary le typ x y
-  | Ap2 (Ord, _, x, y) -> binary ord x y
-  | Ap2 (Uno, _, x, y) -> binary uno x y
+  | Ap2 (Ord, _, x, y) ->
+      (poslit (Predsym.uninterp "ord"))
+        (IArray.of_array [|of_exp x; of_exp y|])
+  | Ap2 (Uno, _, x, y) ->
+      (neglit (Predsym.uninterp "ord"))
+        (IArray.of_array [|of_exp x; of_exp y|])
   | Ap2 (Add, _, x, y) -> binary add x y
   | Ap2 (Sub, _, x, y) -> binary sub x y
   | Ap2 (Mul, _, x, y) -> binary mul x y
@@ -1089,6 +1095,8 @@ let map e ~f =
   | Ap3 (op, x, y, z) -> map3 op ~f x y z
   | ApN (op, xs) -> mapN (normN op) ~f xs
   | Apply (sym, xs) -> mapN (simp_apply sym) ~f xs
+  | PosLit (sym, xs) -> mapN (simp_poslit sym) ~f xs
+  | NegLit (sym, xs) -> mapN (simp_neglit sym) ~f xs
   | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> e
 
 let fold_map e ~init ~f =
@@ -1140,7 +1148,8 @@ let iter e ~f =
       f x ;
       f y ;
       f z
-  | ApN (_, xs) | Apply (_, xs) -> IArray.iter ~f xs
+  | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
+      IArray.iter ~f xs
   | And args | Or args -> Set.iter ~f args
   | Add args | Mul args -> Qset.iter ~f:(fun arg _ -> f arg) args
   | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> ()
@@ -1150,7 +1159,8 @@ let exists e ~f =
   | Ap1 (_, x) -> f x
   | Ap2 (_, x, y) -> f x || f y
   | Ap3 (_, x, y, z) -> f x || f y || f z
-  | ApN (_, xs) | Apply (_, xs) -> IArray.exists ~f xs
+  | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
+      IArray.exists ~f xs
   | And args | Or args -> Set.exists ~f args
   | Add args | Mul args -> Qset.exists ~f:(fun arg _ -> f arg) args
   | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ ->
@@ -1161,7 +1171,8 @@ let for_all e ~f =
   | Ap1 (_, x) -> f x
   | Ap2 (_, x, y) -> f x && f y
   | Ap3 (_, x, y, z) -> f x && f y && f z
-  | ApN (_, xs) | Apply (_, xs) -> IArray.for_all ~f xs
+  | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
+      IArray.for_all ~f xs
   | And args | Or args -> Set.for_all ~f args
   | Add args | Mul args -> Qset.for_all ~f:(fun arg _ -> f arg) args
   | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> true
@@ -1171,7 +1182,7 @@ let fold e ~init:s ~f =
   | Ap1 (_, x) -> f x s
   | Ap2 (_, x, y) -> f y (f x s)
   | Ap3 (_, x, y, z) -> f z (f y (f x s))
-  | ApN (_, xs) | Apply (_, xs) ->
+  | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
       IArray.fold ~f:(fun s x -> f x s) xs ~init:s
   | And args | Or args -> Set.fold ~f:(fun s e -> f e s) args ~init:s
   | Add args | Mul args -> Qset.fold ~f:(fun e _ s -> f e s) args ~init:s
@@ -1187,7 +1198,8 @@ let rec iter_terms e ~f =
       iter_terms ~f x ;
       iter_terms ~f y ;
       iter_terms ~f z
-  | ApN (_, xs) | Apply (_, xs) -> IArray.iter ~f:(iter_terms ~f) xs
+  | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
+      IArray.iter ~f:(iter_terms ~f) xs
   | And args | Or args -> Set.iter args ~f:(iter_terms ~f)
   | Add args | Mul args ->
       Qset.iter args ~f:(fun arg _ -> iter_terms ~f arg)
@@ -1202,7 +1214,7 @@ let rec fold_terms e ~init:s ~f =
     | Ap1 (_, x) -> fold_terms f x s
     | Ap2 (_, x, y) -> fold_terms f y (fold_terms f x s)
     | Ap3 (_, x, y, z) -> fold_terms f z (fold_terms f y (fold_terms f x s))
-    | ApN (_, xs) | Apply (_, xs) ->
+    | ApN (_, xs) | Apply (_, xs) | PosLit (_, xs) | NegLit (_, xs) ->
         IArray.fold ~f:(fun s x -> fold_terms f x s) xs ~init:s
     | And args | Or args ->
         Set.fold args ~init:s ~f:(fun s x -> fold_terms f x s)
@@ -1239,7 +1251,7 @@ let rec height = function
   | Ap1 (_, a) -> 1 + height a
   | Ap2 (_, a, b) -> 1 + max (height a) (height b)
   | Ap3 (_, a, b, c) -> 1 + max (height a) (max (height b) (height c))
-  | ApN (_, v) | Apply (_, v) ->
+  | ApN (_, v) | Apply (_, v) | PosLit (_, v) | NegLit (_, v) ->
       1 + IArray.fold v ~init:0 ~f:(fun m a -> max m (height a))
   | And bs | Or bs ->
       1 + Set.fold bs ~init:0 ~f:(fun m a -> max m (height a))
diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli
index a7de812a7..08fa7d2d3 100644
--- a/sledge/src/ses/term.mli
+++ b/sledge/src/ses/term.mli
@@ -33,8 +33,6 @@ type op2 =
   | Dq  (** Disequal test *)
   | Lt  (** Less-than test *)
   | Le  (** Less-than-or-equal test *)
-  | Ord  (** Ordered test (neither arg is nan) *)
-  | Uno  (** Unordered test (some arg is nan) *)
   | Div  (** Division, for integers result is truncated toward zero *)
   | Rem
       (** Remainder of division, satisfies [a = b * div a b + rem a b] and
@@ -93,6 +91,8 @@ and T : sig
     | RecRecord of int  (** Reference to ancestor recursive record *)
     | Apply of Funsym.t * t iarray
         (** Uninterpreted function application *)
+    | PosLit of Predsym.t * t iarray
+    | NegLit of Predsym.t * t iarray
   [@@deriving compare, equal, sexp]
 end
 
@@ -146,8 +146,6 @@ val eq : t -> t -> t
 val dq : t -> t -> t
 val lt : t -> t -> t
 val le : t -> t -> t
-val ord : t -> t -> t
-val uno : t -> t -> t
 
 (* arithmetic *)
 val neg : t -> t
@@ -190,6 +188,8 @@ val rec_record : int -> t
 
 (* uninterpreted *)
 val apply : Funsym.t -> t iarray -> t
+val poslit : Predsym.t -> t iarray -> t
+val neglit : Predsym.t -> t iarray -> t
 
 (* convert *)
 val of_exp : Llair.Exp.t -> t