[sledge] Fix sorting of heap block subformulas when printing

Summary:
The sorting of heap blocks when printing formulas was broken by the
change to the direct representation of polynomials.

Reviewed By: bennostein

Differential Revision: D17665246

fbshipit-source-id: 4ebea9f20

sledge/src/symbheap/sh.ml

@@ -78,12 +78,12 @@ let rec pp vs all_xs fs {us; xs; cong; pure; heap; djns} =
          (List.map ~f:(map_seg ~f:(Equality.normalize cong)) heap)
          ~compare:(fun s1 s2 ->
            let b_o = function
-             | Term.App {op= App {op= Add _; arg}; arg= Integer {data; _}}
-               ->
-                 (arg, data)
-             | e -> (e, Z.zero)
+             | Term.Add poly as sum ->
+                 let const = Qset.count poly Term.one in
+                 (Term.sub sum (Term.rational const), const)
+             | e -> (e, Q.zero)
            in
-           [%compare: Term.t * (Term.t * Z.t)]
+           [%compare: Term.t * (Term.t * Q.t)]
              (s1.bas, b_o s1.loc)
              (s2.bas, b_o s2.loc) )) ;
   let first = first && List.is_empty heap in

sledge/src/symbheap/solver_test.ml

@@ -132,8 +132,8 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            (%l_6 + 8) -[ %l_6, 16 )-> ⟨8,%a_2⟩
-          * %l_6 -[ %l_6, 16 )-> ⟨8,%a_1⟩
+            %l_6 -[ %l_6, 16 )-> ⟨8,%a_1⟩
+          * (%l_6 + 8) -[ %l_6, 16 )-> ⟨8,%a_2⟩
           \- ∃ %a_3 .
               %l_6 -[)-> ⟨16,%a_3⟩
         ) infer_frame:
@@ -149,8 +149,8 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            (%l_6 + 8) -[ %l_6, 16 )-> ⟨8,%a_2⟩
-          * %l_6 -[ %l_6, 16 )-> ⟨8,%a_1⟩
+            %l_6 -[ %l_6, 16 )-> ⟨8,%a_1⟩
+          * (%l_6 + 8) -[ %l_6, 16 )-> ⟨8,%a_2⟩
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩
         ) infer_frame:
@@ -170,8 +170,8 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            (%l_6 + 8) -[ %l_6, 16 )-> ⟨8,%a_2⟩
-          * %l_6 -[ %l_6, 16 )-> ⟨8,%a_1⟩
+            %l_6 -[ %l_6, 16 )-> ⟨8,%a_1⟩
+          * (%l_6 + 8) -[ %l_6, 16 )-> ⟨8,%a_2⟩
           \- ∃ %a_3, %m_8 .
               %l_6 -[)-> ⟨%m_8,%a_3⟩
         ) infer_frame: