[sledge] Classify Memory and Concat terms as Simplified

Summary:
It is necessary to normalize subterms of Memory and Concat terms or
else Equality.entails_eq is incomplete. They ought to be Interpreted,
but the solver for the byte-array theory is not yet ready for that.

Reviewed By: ngorogiannis

Differential Revision: D19282635

fbshipit-source-id: c06b6ca6d

sledge/src/symbheap/equality.ml

@@ -15,7 +15,8 @@ type kind = Interpreted | Simplified | Atomic | Uninterpreted
 let classify e =
   match (e : Term.t) with
   | Add _ | Mul _ -> Interpreted
-  | Ap2 ((Eq | Dq), _, _) -> Simplified
+  | Ap2 ((Eq | Dq), _, _) | Ap2 (Memory, _, _) | ApN (Concat, _) ->
+      Simplified
   | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ -> Uninterpreted
   | RecN _ | Var _ | Integer _ | Float _ | Nondet _ | Label _ -> Atomic
 
@@ -266,8 +267,8 @@ let rec canon r a =
 (** add a term to the carrier *)
 let rec extend a r =
   match classify a with
-  | Interpreted | Simplified -> Term.fold ~f:extend a ~init:r
+  | Interpreted -> Term.fold ~f:extend a ~init:r
-  | Uninterpreted -> (
+  | Simplified | Uninterpreted -> (
     match Subst.extend a r.rep with
     | Some rep -> Term.fold ~f:extend a ~init:{r with rep}
     | None -> r )

sledge/src/symbheap/equality_test.ml

@@ -320,7 +320,9 @@ let%test_module _ =
     let r14 = of_eqs [(a, a); (x, !1)]
 
     let%expect_test _ =
-      pp r14 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}]
+      pp r14 ;
+      [%expect
+        {| {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]]} |}]
 
     let%test _ = entails_eq r14 a Term.true_
 
@@ -331,7 +333,7 @@ let%test_module _ =
       pp r14 ;
       [%expect
         {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [(%y_6 ≠ 0) ↦ -1]]} |}]
+          {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]; [(%y_6 ≠ 0) ↦ -1]]} |}]
 
     let%test _ = entails_eq r14 a Term.true_
     let%test _ = entails_eq r14 b Term.true_
@@ -340,7 +342,9 @@ let%test_module _ =
     let r15 = of_eqs [(b, b); (x, !1)]
 
     let%expect_test _ =
-      pp r15 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}]
+      pp r15 ;
+      [%expect
+        {| {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]]} |}]
 
     let%test _ = entails_eq r15 b (Term.signed 1 !1)
     let%test _ = entails_eq r15 (Term.unsigned 1 b) !1

sledge/src/symbheap/solver_test.ml

@@ -185,8 +185,7 @@ let%test_module _ =
         ) infer_frame:
           ∃ %a0_10, %a1_11 .
             %a_2 = %a0_10
-          ∧ ⟨%n_9,%a0_10⟩ = ⟨16,%a_2⟩
+          ∧ ⟨32,%a_1⟩ = ⟨16,%a_2⟩^⟨16,%a1_11⟩
-          ∧ ⟨32,%a_1⟩ = ⟨%n_9,%a0_10⟩^⟨16,%a1_11⟩
           ∧ 16 = %m_8 = %n_9
           ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]