pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge] Do not reverse Map.to_iter

Browse Source 
Summary:
Preceding commit reversed Map.to_iter to match the previous behavior
of to_list.

Reviewed By: jvillard

Differential Revision: D24306051

fbshipit-source-id: aad12e434
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent 4780b92584
commit 46abb011cb
6 changed files with 156 additions and 155 deletions
Show Stats Download Patch File Download Diff File

2
sledge/nonstdlib/map.ml
Unescape View File

@ -161,7 +161,7 @@ end) : S with type key = Key.t = struct
let fold m ~init ~f = M.fold (fun key data acc -> f ~key ~data acc) m init
let keys = M.keys
let values = M.values
let to_iter m = Iter.rev (M.to_iter m)
let to_iter = M.to_iter
let to_iter2 l r =
let seq = ref Iter.empty in

22
sledge/src/test/equality_test.ml
Unescape View File

@ -62,17 +62,17 @@ let%test_module _ =
= (%y_6 rem %t_1)
{sat= true;
rep= [[0 ↦ ];
[-1 ↦ ];
[(%y_6 rem %z_7) ↦ %t_1];
[(%y_6 rem %v_3) ↦ %t_1];
[%z_7 ↦ %t_1];
[%y_6 ↦ ];
[%x_5 ↦ %t_1];
[%w_4 ↦ %t_1];
[%v_3 ↦ %t_1];
rep= [[%t_1 ↦ ];
[%u_2 ↦ %t_1];
[%t_1 ↦ ]]} |}]
[%v_3 ↦ %t_1];
[%w_4 ↦ %t_1];
[%x_5 ↦ %t_1];
[%y_6 ↦ ];
[%z_7 ↦ %t_1];
[(%y_6 rem %v_3) ↦ %t_1];
[(%y_6 rem %z_7) ↦ %t_1];
[-1 ↦ ];
[0 ↦ ]]} |}]
let%test _ = implies_eq r3 t z
@ -83,7 +83,7 @@ let%test_module _ =
pp r15 ;
[%expect
{|
{sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [(%x_5 ≠ 0) ↦ -1]; [%x_5 ↦ 1]]} |}]
{sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]; [-1 ↦ ]; [0 ↦ ]]} |}]
let%test _ = implies_eq r15 b (Term.signed 1 !1)
let%test _ = implies_eq r15 (Term.unsigned 1 b) !1

178
sledge/src/test/fol_test.ml
Unescape View File

@ -66,7 +66,7 @@ let%test_module _ =
let%expect_test _ =
pp_raw f1 ;
[%expect {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]]} |}]
[%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
let%test _ = is_unsat (add_eq !1 !1 f1)
@ -76,7 +76,7 @@ let%test_module _ =
let%expect_test _ =
pp_raw f2 ;
[%expect {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ ]]} |}]
[%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
let f3 = of_eqs [(x + !0, x + !1)]
@ -84,7 +84,7 @@ let%test_module _ =
let%expect_test _ =
pp_raw f3 ;
[%expect {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ ]]} |}]
[%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
let f4 = of_eqs [(x, y); (x + !0, y + !1)]
@ -93,7 +93,7 @@ let%test_module _ =
let%expect_test _ =
pp_raw f4 ;
[%expect
{| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]} |}]
{| {sat= false; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}]
let t1 = of_eqs [(!1, !1)]
@ -109,7 +109,7 @@ let%test_module _ =
let%expect_test _ =
pp_raw r0 ;
[%expect {| {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]]} |}]
[%expect {| {sat= true; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
let%expect_test _ =
pp r0 ;
@ -128,7 +128,7 @@ let%test_module _ =
%x_5 = %y_6
{sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]} |}]
{sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}]
let%test _ = implies_eq r1 x y
@ -142,12 +142,12 @@ let%test_module _ =
%x_5 = %y_6 = %z_7 = %x_5^
{sat= true;
rep= [[0 ↦ ];
[-1 ↦ ];
[%x_5^ ↦ %x_5];
[%z_7 ↦ %x_5];
rep= [[%x_5 ↦ ];
[%y_6 ↦ %x_5];
[%x_5 ↦ ]]} |}]
[%z_7 ↦ %x_5];
[%x_5^ ↦ %x_5];
[-1 ↦ ];
[0 ↦ ]]} |}]
let%test _ = implies_eq r2 x z
let%test _ = implies_eq (inter r1 r2) x y
@ -169,12 +169,12 @@ let%test_module _ =
[%expect
{|
{sat= true;
rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %w_4]; [%y_6 ↦ %w_4]; [%w_4 ↦ ]]}
rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]; [-1 ↦ ]; [0 ↦ ]]}
{sat= true;
rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %x_5]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]}
rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]}
{sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %y_6]; [%y_6 ↦ ]]} |}]
{sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]; [-1 ↦ ]; [0 ↦ ]]} |}]
let%test _ =
let r = of_eqs [(w, y); (y, z)] in
@ -189,21 +189,21 @@ let%test_module _ =
pp_raw r3 ;
[%expect
{|
(1 × (%z_7 × %y_6^2)) = %t_1
∧ %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (1 × (%z_7 × %y_6))
%z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (1 × (%y_6 × %z_7))
∧ (1 × (%y_6^2 × %z_7)) = %t_1
{sat= true;
rep= [[0 ↦ ];
[-1 ↦ ];
[(%z_7 × %y_6^2) ↦ ];
[(%z_7 × %y_6) ↦ %z_7];
[%z_7 ↦ ];
[%y_6 ↦ ];
[%x_5 ↦ %z_7];
[%w_4 ↦ %z_7];
[%v_3 ↦ %z_7];
rep= [[%t_1 ↦ (%y_6^2 × %z_7)];
[%u_2 ↦ %z_7];
[%t_1 ↦ (%z_7 × %y_6^2)]]} |}]
[%v_3 ↦ %z_7];
[%w_4 ↦ %z_7];
[%x_5 ↦ %z_7];
[%y_6 ↦ ];
[%z_7 ↦ ];
[(%y_6 × %z_7) ↦ %z_7];
[(%y_6^2 × %z_7) ↦ ];
[-1 ↦ ];
[0 ↦ ]]} |}]
let%test _ = not (implies_eq r3 t z) (* incomplete *)
let%test _ = implies_eq r3 x z
@ -216,17 +216,17 @@ let%test_module _ =
pp_raw r4 ;
[%expect
{|
(1 × (%z_7) + 8) = %x_5
∧ (1 × (%z_7) + 3) = %w_4
∧ (1 × (%z_7) + -4) = %y_6
(-4 + 1 × (%z_7)) = %y_6
∧ (3 + 1 × (%z_7)) = %w_4
∧ (8 + 1 × (%z_7)) = %x_5
{sat= true;
rep= [[0 ↦ ];
[-1 ↦ ];
rep= [[%w_4 ↦ (%z_7 + 3)];
[%x_5 ↦ (%z_7 + 8)];
[%y_6 ↦ (%z_7 + -4)];
[%z_7 ↦ ];
[%y_6 ↦ (-4 + %z_7)];
[%x_5 ↦ (8 + %z_7)];
[%w_4 ↦ (3 + %z_7)]]} |}]
[-1 ↦ ];
[0 ↦ ]]} |}]
let%test _ = implies_eq r4 x (w + !5)
let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5))
@ -244,7 +244,7 @@ let%test_module _ =
{|
1 = %x_5 = %y_6
{sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ 1]; [%x_5 ↦ 1]]} |}]
{sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
let%test _ = implies_eq r6 x y
@ -257,25 +257,25 @@ let%test_module _ =
pp (add_eq x z r7) ;
[%expect
{|
%w_4 = %y_6 = %z_7 ∧ %v_3 = %x_5
%v_3 = %x_5 ∧ %w_4 = %y_6 = %z_7
{sat= true;
rep= [[0 ↦ ];
[-1 ↦ ];
[%z_7 ↦ %w_4];
[%y_6 ↦ %w_4];
[%x_5 ↦ %v_3];
rep= [[%v_3 ↦ ];
[%w_4 ↦ ];
[%v_3 ↦ ]]}
[%x_5 ↦ %v_3];
[%y_6 ↦ %w_4];
[%z_7 ↦ %w_4];
[-1 ↦ ];
[0 ↦ ]]}
{sat= true;
rep= [[0 ↦ ];
[-1 ↦ ];
[%z_7 ↦ %v_3];
[%y_6 ↦ %v_3];
[%x_5 ↦ %v_3];
rep= [[%v_3 ↦ ];
[%w_4 ↦ %v_3];
[%v_3 ↦ ]]}
[%x_5 ↦ %v_3];
[%y_6 ↦ %v_3];
[%z_7 ↦ %v_3];
[-1 ↦ ];
[0 ↦ ]]}
%v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}]
@ -301,13 +301,13 @@ let%test_module _ =
%v_3 = %w_4 = %x_5 = %y_6 = %z_7
{sat= true;
rep= [[0 ↦ ];
[-1 ↦ ];
[%z_7 ↦ %v_3];
[%y_6 ↦ %v_3];
[%x_5 ↦ %v_3];
rep= [[%v_3 ↦ ];
[%w_4 ↦ %v_3];
[%v_3 ↦ ]]} |}]
[%x_5 ↦ %v_3];
[%y_6 ↦ %v_3];
[%z_7 ↦ %v_3];
[-1 ↦ ];
[0 ↦ ]]} |}]
let%test _ = normalize r7' w |> Term.equal v
@ -324,10 +324,10 @@ let%test_module _ =
pp_raw r8 ;
[%expect
{|
(13 × (%z_7)) = %x_5 ∧ 14 = %y_6
14 = %y_6 ∧ (13 × (%z_7)) = %x_5
{sat= true;
rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%y_6 ↦ 14]; [%x_5 ↦ (13 × %z_7)]]} |}]
rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
let%test _ = implies_eq r8 y !14
@ -339,10 +339,10 @@ let%test_module _ =
[%expect
{|
{sat= true;
rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
{sat= true;
rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]} |}]
rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
@ -358,16 +358,16 @@ let%test_module _ =
[%expect
{|
{sat= true;
rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
{sat= true;
rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
(1 × (%z_7) + -1 × (%x_5) + -8)
(-8 + -1 × (%x_5) + 1 × (%z_7))
8
(-1 × (%z_7) + 1 × (%x_5) + 8)
(8 + 1 × (%x_5) + -1 × (%z_7))
-8 |}]
@ -380,13 +380,13 @@ let%test_module _ =
let%expect_test _ =
pp r11 ;
[%expect {| (1 × (%z_7) + -16) = %x_5 |}]
[%expect {| (-16 + 1 × (%z_7)) = %x_5 |}]
let r12 = of_eqs [(!16, z - x); (x + !8 - z, z + !16 + !8 - z)]
let%expect_test _ =
pp r12 ;
[%expect {| (1 × (%z_7) + -16) = %x_5 |}]
[%expect {| (-16 + 1 × (%z_7)) = %x_5 |}]
let r13 =
of_eqs
@ -397,7 +397,7 @@ let%test_module _ =
let%expect_test _ =
pp_raw r13 ;
[%expect
{| {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %y_6]; [%y_6 ↦ ]]} |}]
{| {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]; [-1 ↦ ]; [0 ↦ ]]} |}]
let%test _ = not (is_unsat r13) (* incomplete *)
@ -408,7 +408,7 @@ let%test_module _ =
pp_raw r14 ;
[%expect
{|
{sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ 1]]} |}]
{sat= true; rep= [[%x_5 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
@ -420,12 +420,12 @@ let%test_module _ =
[%expect
{|
{sat= true;
rep= [[0 ↦ ];
[-1 ↦ ];
[(%y_6 ≠ 0) ↦ -1];
[(%x_5 ≠ 0) ↦ -1];
rep= [[%x_5 ↦ 1];
[%y_6 ↦ ];
[%x_5 ↦ 1]]} |}]
[(%x_5 ≠ 0) ↦ -1];
[(%y_6 ≠ 0) ↦ -1];
[-1 ↦ ];
[0 ↦ ]]} |}]
let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
let%test _ = implies_eq r14 b (Formula.inject Formula.tt)
@ -437,7 +437,7 @@ let%test_module _ =
pp_raw r15 ;
[%expect
{|
{sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ 1]]} |}]
{sat= true; rep= [[%x_5 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
(* f(x−1)−1=x+1, f(y)+1=y−1, y+1=x ⊢ false *)
let r16 =
@ -448,12 +448,12 @@ let%test_module _ =
[%expect
{|
{sat= false;
rep= [[0 ↦ ];
[-1 ↦ ];
[(-1 + %x_5)^ ↦ (3 + %y_6)];
[%y_6^ ↦ (-2 + %y_6)];
rep= [[%x_5 ↦ (%y_6 + 1)];
[%y_6 ↦ ];
[%x_5 ↦ (1 + %y_6)]]} |}]
[%y_6^ ↦ (%y_6 + -2)];
[(%x_5 + -1)^ ↦ (%y_6 + 3)];
[-1 ↦ ];
[0 ↦ ]]} |}]
let%test _ = is_unsat r16
@ -465,12 +465,12 @@ let%test_module _ =
[%expect
{|
{sat= false;
rep= [[0 ↦ ];
[-1 ↦ ];
[%y_6^ ↦ (-1 + %x_5)];
[%x_5^ ↦ %x_5];
rep= [[%x_5 ↦ ];
[%y_6 ↦ %x_5];
[%x_5 ↦ ]]} |}]
[%x_5^ ↦ %x_5];
[%y_6^ ↦ (%x_5 + -1)];
[-1 ↦ ];
[0 ↦ ]]} |}]
let%test _ = is_unsat r17
@ -481,14 +481,14 @@ let%test_module _ =
[%expect
{|
{sat= true;
rep= [[0 ↦ ];
[-1 ↦ ];
[%y_6^ ↦ (-1 + %y_6)];
[%x_5^ ↦ %x_5];
rep= [[%x_5 ↦ ];
[%y_6 ↦ ];
[%x_5 ↦ ]]}
[%x_5^ ↦ %x_5];
[%y_6^ ↦ (%y_6 + -1)];
[-1 ↦ ];
[0 ↦ ]]}
(1 × (%y_6) + -1) = %y_6^ ∧ %x_5 = %x_5^ |}]
%x_5 = %x_5^ ∧ (-1 + 1 × (%y_6)) = %y_6^ |}]
let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)]
@ -497,7 +497,7 @@ let%test_module _ =
[%expect
{|
{sat= true;
rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ 0]; [%y_6 ↦ 0]; [%x_5 ↦ 0]]} |}]
rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]; [-1 ↦ ]; [0 ↦ ]]} |}]
let%test _ = implies_eq r19 z !0

6
sledge/src/test/sh_test.ml
Unescape View File

@ -154,11 +154,11 @@ let%test_module _ =
pp q' ;
[%expect
{|
∃ %x_6 . (1 × (%y_7) + -1) = %y_7^ ∧ %x_6 = %x_6^ ∧ emp
∃ %x_6 . %x_6 = %x_6^ ∧ (-1 + 1 × (%y_7)) = %y_7^ ∧ emp
(tt ∧ ((1 × (%y_7) + -1) = %y_7^)) ∧ emp
(tt ∧ ((-1 + 1 × (%y_7)) = %y_7^)) ∧ emp
(1 × (%y_7) + -1) = %y_7^ ∧ emp |}]
(-1 + 1 × (%y_7)) = %y_7^ ∧ emp |}]
let%expect_test _ =
let q =

40
sledge/src/test/solver_test.ml
Unescape View File

@ -143,7 +143,7 @@ let%test_module _ =
{|
( infer_frame:
%l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3 . %l_6 -[)-> ⟨16,%a_3⟩
) infer_frame: (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ %a_2 = _ ∧ emp |}]
) infer_frame: %a_2 = _ ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
let%expect_test _ =
check_frame
@ -159,7 +159,7 @@ let%test_module _ =
\- ∃ %a_3, %m_8 .
%l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩
) infer_frame:
(⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 16 = %m_8 ∧ %a_2 = _ ∧ emp |}]
%a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
let%expect_test _ =
check_frame
@ -175,7 +175,7 @@ let%test_module _ =
\- ∃ %a_3, %m_8 .
%l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩
) infer_frame:
(⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 16 = %m_8 ∧ %a_2 = _ ∧ emp |}]
%a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
let%expect_test _ =
check_frame
@ -194,10 +194,10 @@ let%test_module _ =
%k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩
) infer_frame:
∃ %a0_10, %a1_11 .
(⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
%a_2 = %a0_10
∧ 16 = %m_8 = %n_9
∧ %a_2 = %a0_10
∧ (1 × (%k_5) + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
∧ (16 + 1 × (%k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
let%expect_test _ =
infer_frame
@ -216,10 +216,10 @@ let%test_module _ =
%k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩
) infer_frame:
∃ %a0_10, %a1_11 .
(⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
%a_2 = %a0_10
∧ 16 = %m_8 = %n_9
∧ %a_2 = %a0_10
∧ (1 × (%k_5) + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
∧ (16 + 1 × (%k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
let seg_split_symbolically =
Sh.star
@ -238,7 +238,7 @@ let%test_module _ =
{|
( infer_frame:
%l_6
-[ %l_6, 16 )-> ⟨(8 × (%n_9)),%a_2⟩^⟨(-8 × (%n_9) + 16),%a_3⟩
-[ %l_6, 16 )-> ⟨(8 × (%n_9)),%a_2⟩^⟨(16 + -8 × (%n_9)),%a_3⟩
* ( ( 1 = %n_9 ∧ emp)
∨ ( 0 = %n_9 ∧ emp)
∨ ( 2 = %n_9 ∧ emp)
@ -246,19 +246,19 @@ let%test_module _ =
\- ∃ %a_1, %m_8 .
%l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
) infer_frame:
( ( (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
∧ 16 = %m_8
( ( %a_3 = _
∧ 1 = %n_9
∧ %a_3 = _
∧ 16 = %m_8
∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
∧ emp)
∨ ( 16 = %m_8
∨ ( %a_1 = %a_2
∧ 2 = %n_9
∧ %a_1 = %a_2
∧ (1 × (%l_6) + 16) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
∨ ( (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
∧ 16 = %m_8
∧ (16 + 1 × (%l_6)) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
∨ ( %a_3 = _
∧ 0 = %n_9
∧ %a_3 = _
∧ 16 = %m_8
∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
∧ emp)
) |}]
@ -271,9 +271,9 @@ let%test_module _ =
[%expect
{|
( infer_frame:
(0 ≥ (1 × (%n_9) + -2))
(0 ≥ (-2 + 1 × (%n_9)))
∧ %l_6
-[ %l_6, 16 )-> ⟨(8 × (%n_9)),%a_2⟩^⟨(-8 × (%n_9) + 16),%a_3⟩
-[ %l_6, 16 )-> ⟨(8 × (%n_9)),%a_2⟩^⟨(16 + -8 × (%n_9)),%a_3⟩
\- ∃ %a_1, %m_8 .
%l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
) infer_frame: |}]

63
sledge/src/test/term_test.ml
Unescape View File

@ -54,7 +54,7 @@ let%test_module _ =
let%expect_test _ =
pp (z + !42 + !13) ;
[%expect {| (55 + %z_2) |}]
[%expect {| (%z_2 + 55) |}]
let%expect_test _ =
pp (z + !42 + !(-42)) ;
@ -62,15 +62,15 @@ let%test_module _ =
let%expect_test _ =
pp (z * y) ;
[%expect {| (%z_2 × %y_1) |}]
[%expect {| (%y_1 × %z_2) |}]
let%expect_test _ =
pp (y * z * y) ;
[%expect {| (%z_2 × %y_1^2) |}]
[%expect {| (%y_1^2 × %z_2) |}]
let%expect_test _ =
pp ((!2 * z * z) + (!3 * z) + !4) ;
[%expect {| (4 + 2 × (%z_2^2) + 3 × %z_2) |}]
[%expect {| (3 × %z_2 + 2 × (%z_2^2) + 4) |}]
let%expect_test _ =
pp
@ -85,8 +85,9 @@ let%test_module _ =
+ (!9 * z * z * z) ) ;
[%expect
{|
(1 + 9 × (%z_2^3) + 4 × (%z_2^2) + 7 × (%z_2 × %y_1^2) + 5 × (%y_1^2)
+ 8 × (%z_2^2 × %y_1) + 6 × (%z_2 × %y_1) + 2 × %z_2 + 3 × %y_1) |}]
(3 × %y_1 + 2 × %z_2 + 6 × (%y_1 × %z_2) + 8 × (%y_1 × %z_2^2)
+ 5 × (%y_1^2) + 7 × (%y_1^2 × %z_2) + 4 × (%z_2^2) + 9 × (%z_2^3)
+ 1) |}]
let%expect_test _ =
pp (!0 * z * y) ;
@ -94,19 +95,19 @@ let%test_module _ =
let%expect_test _ =
pp (!1 * z * y) ;
[%expect {| (%z_2 × %y_1) |}]
[%expect {| (%y_1 × %z_2) |}]
let%expect_test _ =
pp (!7 * z * (!2 * y)) ;
[%expect {| (14 × (%z_2 × %y_1)) |}]
[%expect {| (14 × (%y_1 × %z_2)) |}]
let%expect_test _ =
pp (!13 + (!42 * z)) ;
[%expect {| (13 + 42 × %z_2) |}]
[%expect {| (42 × %z_2 + 13) |}]
let%expect_test _ =
pp ((!13 * z) + !42) ;
[%expect {| (42 + 13 × %z_2) |}]
[%expect {| (13 × %z_2 + 42) |}]
let%expect_test _ =
pp ((!2 * z) - !3 + ((!(-2) * z) + !3)) ;
@ -114,31 +115,31 @@ let%test_module _ =
let%expect_test _ =
pp ((!3 * y) + (!13 * z) + !42) ;
[%expect {| (42 + 13 × %z_2 + 3 × %y_1) |}]
[%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}]
let%expect_test _ =
pp ((!13 * z) + !42 + (!3 * y)) ;
[%expect {| (42 + 13 × %z_2 + 3 × %y_1) |}]
[%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}]
let%expect_test _ =
pp ((!13 * z) + !42 + (!3 * y) + (!2 * z)) ;
[%expect {| (42 + 15 × %z_2 + 3 × %y_1) |}]
[%expect {| (3 × %y_1 + 15 × %z_2 + 42) |}]
let%expect_test _ =
pp ((!13 * z) + !42 + (!3 * y) + (!(-13) * z)) ;
[%expect {| (42 + 3 × %y_1) |}]
[%expect {| (3 × %y_1 + 42) |}]
let%expect_test _ =
pp (z + !42 + ((!3 * y) + (!(-1) * z))) ;
[%expect {| (42 + 3 × %y_1) |}]
[%expect {| (3 × %y_1 + 42) |}]
let%expect_test _ =
pp (!(-1) * (z + (!(-1) * y))) ;
[%expect {| (-1 × %z_2 + %y_1) |}]
[%expect {| (%y_1 + -1 × %z_2) |}]
let%expect_test _ =
pp (((!3 * y) + !2) * (!4 + (!5 * z))) ;
[%expect {| (8 + 15 × (%z_2 × %y_1) + 10 × %z_2 + 12 × %y_1) |}]
[%expect {| (12 × %y_1 + 10 × %z_2 + 15 × (%y_1 × %z_2) + 8) |}]
let%expect_test _ =
pp (((!2 * z) - !3 + ((!(-2) * z) + !3)) * (!4 + (!5 * z))) ;
@ -146,7 +147,7 @@ let%test_module _ =
let%expect_test _ =
pp ((!13 * z) + !42 - ((!3 * y) + (!13 * z))) ;
[%expect {| (42 + -3 × %y_1) |}]
[%expect {| (-3 × %y_1 + 42) |}]
let%expect_test _ =
pp (z = y) ;
@ -182,47 +183,47 @@ let%test_module _ =
let%expect_test _ =
pp (y - (!(-3) * y) + !4) ;
[%expect {| (4 + 4 × %y_1) |}]
[%expect {| (4 × %y_1 + 4) |}]
let%expect_test _ =
pp ((!(-3) * y) + !4 - y) ;
[%expect {| (4 + -4 × %y_1) |}]
[%expect {| (-4 × %y_1 + 4) |}]
let%expect_test _ =
pp (y = (!(-3) * y) + !4) ;
[%expect {| (%y_1 = (4 + -3 × %y_1)) |}]
[%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
let%expect_test _ =
pp ((!(-3) * y) + !4 = y) ;
[%expect {| (%y_1 = (4 + -3 × %y_1)) |}]
[%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
let%expect_test _ =
pp (sub true_ (z = !4)) ;
[%expect {| (-1 + -1 × (%z_2 = 4)) |}]
[%expect {| (-1 × (%z_2 = 4) + -1) |}]
let%expect_test _ =
pp (add true_ (z = !4) = (z = !4)) ;
[%expect {| ((%z_2 = 4) = (-1 + (%z_2 = 4))) |}]
[%expect {| ((%z_2 = 4) = ((%z_2 = 4) + -1)) |}]
let%expect_test _ =
pp ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ;
[%expect {| ((13 × %z_2 + 3 × %y_1) = (42 + 13 × %z_2)) |}]
[%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
let%expect_test _ =
pp ((!13 * z) + !(-42) = (!3 * y) + (!13 * z)) ;
[%expect {| ((13 × %z_2 + 3 × %y_1) = (-42 + 13 × %z_2)) |}]
[%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
let%expect_test _ =
pp ((!13 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
[%expect {| ((13 × %z_2 + -3 × %y_1) = (42 + 13 × %z_2)) |}]
[%expect {| ((-3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
let%expect_test _ =
pp ((!10 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
[%expect {| ((13 × %z_2 + -3 × %y_1) = (42 + 10 × %z_2)) |}]
[%expect {| ((-3 × %y_1 + 13 × %z_2) = (10 × %z_2 + 42)) |}]
let%expect_test _ =
pp ~~((!13 * z) + !(-42) != (!3 * y) + (!13 * z)) ;
[%expect {| ((13 × %z_2 + 3 × %y_1) = (-42 + 13 × %z_2)) |}]
[%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
let%expect_test _ =
pp ~~(!2 < y && z <= !3) ;
@ -251,7 +252,7 @@ let%test_module _ =
pp (z1_2 * z1_2) ;
[%expect
{|
(1 + (%z_2^2) + 2 × %z_2)
(2 × %z_2 + (%z_2^2) + 1)
(1 + (%z_2^4) + 4 × (%z_2^3) + 6 × (%z_2^2) + 4 × %z_2) |}]
(4 × %z_2 + 6 × (%z_2^2) + 4 × (%z_2^3) + (%z_2^4) + 1) |}]
end )

Write Preview
Loading…
Cancel
Save