[sledge] Strengthen handling of existential segments

Summary:
Due to strengthened existential witnessing, the incomplete ad hoc
witness guessing is no longer needed.

Reviewed By: ngorogiannis

Differential Revision: D20120277

fbshipit-source-id: 8ee1656dd

sledge/src/symbheap/solver.ml

@@ -498,9 +498,7 @@ let excise_seg ({sub} as goal) msg ssg =
         )
     (* k-l = 0 so k = l *)
     | Zero -> (
-      match Equality.difference sub.cong o n with
+        let* o_n = Equality.difference sub.cong o n in
-      | None -> Some {goal with sub= Sh.and_ (Term.eq o n) goal.sub}
-      | Some o_n -> (
         match Int.sign (Z.sign o_n) with
         (* o-n < 0      [k; o)
          * so o < n   ⊢ [l;   n) *)
@@ -510,7 +508,7 @@ let excise_seg ({sub} as goal) msg ssg =
         | Zero -> Some (excise_seg_same goal msg ssg)
         (* o-n > 0      [k;   o)
          * so o > n   ⊢ [l; n) *)
-        | Pos -> Some (excise_seg_sub_prefix goal msg ssg o_n) ) )
+        | Pos -> Some (excise_seg_sub_prefix goal msg ssg o_n) )
     (* k-l > 0 so k > l *)
     | Pos -> (
         let ko = Term.add k o in

sledge/src/symbheap/solver_test.ml

@@ -194,8 +194,6 @@ let%test_module _ =
           ∧ 16 = %m_8 = %n_9
           ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
-    (* Incompleteness: changing the order of the subtrahend leads to
-       different existential instantiation, which fails *)
     let%expect_test _ =
       infer_frame
         (Sh.star
@@ -211,7 +209,12 @@ let%test_module _ =
             %k_5 -[ %k_5, 16 )-> ⟨32,%a_1⟩ * %l_6 -[)-> ⟨8,16⟩
           \- ∃ %a_2, %m_8, %n_9 .
               %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩
-        ) infer_frame: |}]
+        ) infer_frame:
+          ∃ %a0_10, %a1_11 .
+            %a_2 = %a0_10
+          ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
+          ∧ 16 = %m_8 = %n_9
+          ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let seg_split_symbolically =
       Sh.star