[sledge] Improve printing

Reviewed By: jvillard

Differential Revision: D24532359

fbshipit-source-id: 53c02684a

sledge/src/arithmetic.ml

@@ -263,6 +263,10 @@ struct
       | Some (c, p_c) -> (p_c, c)
       | None -> (poly, Q.zero)
 
+    let partition_sign poly =
+      Sum.partition_map poly ~f:(fun _ coeff ->
+          if Q.sign coeff >= 0 then Left coeff else Right (Q.neg coeff) )
+
     let map poly ~f =
       let p, p' = (poly, Sum.empty) in
       let p, p' =

sledge/src/arithmetic_intf.ml

@@ -53,6 +53,10 @@ module type S = sig
       non-constant parts. That is, [split_const a] is [(b, c)] such that
       [a = b + c] and the absolute value of [c] is maximal. *)
 
+  val partition_sign : t -> t * t
+  (** [partition_sign a] is [(p, n)] such that [a] = [p - n] and all
+      coefficients in [p] and [n] are non-negative. *)
+
   val map : t -> f:(trm -> trm) -> t
   (** [map ~f a] is [a] with each indeterminate transformed by [f]. Viewing
       [a] as a polynomial,

sledge/src/fml.ml

@@ -20,11 +20,27 @@ let pp_boxed fs fmt =
 
 let ppx strength fs fml =
   let pp_t = Trm.ppx strength in
+  let pp_a = Trm.Arith.ppx strength in
   let rec pp fs fml =
     let pf fmt = pp_boxed fs fmt in
+    let pp_binop x = pf "(%a@ @<2>%s %a)" x in
+    let pp_arith_op x op y =
+      let flip = Trm.Arith.compare x y > 0 in
+      let x, y = if flip then (y, x) else (x, y) in
+      match op with
+      | ">" -> pp_binop pp_a x (if flip then "<" else ">") pp_a y
+      | "≤" -> pp_binop pp_a x (if flip then "≥" else "≤") pp_a y
+      | op -> pp_binop pp_a x op pp_a y
+    in
     let pp_arith op x =
-      let a, c = Trm.Arith.split_const (Trm.Arith.trm x) in
-      pf "(%a@ @<2>%s %a)" Q.pp (Q.neg c) op (Trm.Arith.ppx strength) a
+      let p_c, n_d = Trm.Arith.partition_sign (Trm.Arith.trm x) in
+      if Trm.Arith.equal (Trm.Arith.const Q.zero) p_c then
+        let n, d = Trm.Arith.split_const n_d in
+        pp_arith_op n op (Trm.Arith.const (Q.neg d))
+      else if Trm.Arith.equal (Trm.Arith.const Q.zero) n_d then
+        let p, c = Trm.Arith.split_const p_c in
+        pp_arith_op p op (Trm.Arith.const (Q.neg c))
+      else pp_arith_op p_c op n_d
     in
     let pp_join sep pos neg =
       pf "(%a%t%a)" (Set.pp ~sep pp) pos
@@ -37,12 +53,12 @@ let ppx strength fs fml =
     match fml with
     | Tt -> pf "tt"
     | Not Tt -> pf "ff"
-    | Eq (x, y) -> pf "(%a@ = %a)" pp_t x pp_t y
-    | Not (Eq (x, y)) -> pf "(%a@ @<2>≠ %a)" pp_t x pp_t y
+    | Eq (x, y) -> pp_binop pp_t x "=" pp_t y
+    | Not (Eq (x, y)) -> pp_binop pp_t x "≠" pp_t y
     | Eq0 x -> pp_arith "=" x
     | Not (Eq0 x) -> pp_arith "≠" x
-    | Pos x -> pp_arith "<" x
-    | Not (Pos x) -> pp_arith "≥" x
+    | Pos x -> pp_arith ">" x
+    | Not (Pos x) -> pp_arith "≤" x
     | Not x -> pf "@<1>¬%a" pp x
     | And {pos; neg} -> pp_join "@ @<2>∧ " pos neg
     | Or {pos; neg} -> pp_join "@ @<2>∨ " pos neg

sledge/src/test/sh_test.ml

@@ -156,7 +156,7 @@ let%test_module _ =
         {|
         ∃ %x_6 .   %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp
 
-          (tt ∧ (-1 = (-1×%y_7 + %y_7^))) ∧ emp
+          (tt ∧ ((1 + %y_7^) = %y_7)) ∧ emp
 
           (-1 + %y_7) = %y_7^ ∧ emp |}]