diff --git a/sledge/lib/equality_test.ml b/sledge/lib/equality_test.ml index a0f468d9f..0c6d25599 100644 --- a/sledge/lib/equality_test.ml +++ b/sledge/lib/equality_test.ml @@ -15,7 +15,7 @@ let%test_module _ = * Trace.init ~margin:160 * ~config:(Result.ok_exn (Trace.parse "+Equality")) * () - * + * * [@@@warning "-32"] *) let printf pp = Format.printf "@\n%a@." pp @@ -365,10 +365,10 @@ let%test_module _ = [%expect {| {sat= false; - rep= [[%x_5 ↦ (((u8) %y_6) + 3)]; - [%y_6 ↦ (((u8) %y_6) + 2)]; - [((u8) (%x_5 + -1)) ↦ (((u8) %y_6) + 5)]; - [((u8) %y_6) ↦ ]]} |}] + rep= [[%x_5 ↦ (((u8) (%x_5 + -1)) + -2)]; + [%y_6 ↦ (((u8) (%x_5 + -1)) + -3)]; + [((u8) %y_6) ↦ (((u8) (%x_5 + -1)) + -5)]; + [((u8) (%x_5 + -1)) ↦ ]]} |}] let%test _ = is_false r16 @@ -398,9 +398,9 @@ let%test_module _ = [((u8) %x_5) ↦ %x_5]; [((u8) %y_6) ↦ ]]} - (((u8) %y_6) + 1) = %y_6 - ∧ %x_5 = ((u8) %x_5) - ∧ ((u8) %y_6) = ((u8) (((u8) %y_6) + 1)) |}] + %x_5 = ((u8) %x_5) + ∧ ((u8) %y_6) = ((u8) (((u8) %y_6) + 1)) + ∧ (((u8) %y_6) + 1) = %y_6 |}] let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)] @@ -413,7 +413,8 @@ let%test_module _ = let%expect_test _ = Equality.replay - {|(Solve_for_vars (() () ((Var (id 8) (name m)) (Var (id 9) (name n)))) - ((xs ()) (sat true) (rep (((Var (id 9) (name n)) (Var (id 8) (name m)))))))|} ; - [%expect {||}] + {|(And_eq () (Var (id 10) (name v)) + (Mul (((Var (id 8) (name v)) 1) ((Var (id 9) (name v)) 1))) + ((xs ()) (sat true) (rep ())))|} ; + [%expect {| |}] end ) diff --git a/sledge/lib/sh_test.ml b/sledge/lib/sh_test.ml index fbfc00f5b..fe68382d3 100644 --- a/sledge/lib/sh_test.ml +++ b/sledge/lib/sh_test.ml @@ -137,18 +137,18 @@ let%test_module _ = [%expect {| ∃ %x_6 . - (((u8) %y_7) + 1) = %y_7 - ∧ %x_6 = ((u8) %x_6) + %x_6 = ((u8) %x_6) ∧ ((u8) %y_7) = ((u8) (((u8) %y_7) + 1)) + ∧ (((u8) %y_7) + 1) = %y_7 ∧ emp - (((u8) %y_7) + 1) = %y_7 - ∧ ((u8) %y_7) = ((u8) (((u8) %y_7) + 1)) - ∧ ((%y_7 + -1) = ((u8) %y_7)) + ((u8) %y_7) = ((u8) (((u8) %y_7) + 1)) + ∧ (((u8) %y_7) + 1) = %y_7 + ∧ (((u8) %y_7) = (%y_7 + -1)) ∧ emp - (((u8) %y_7) + 1) = %y_7 - ∧ ((u8) %y_7) = ((u8) (((u8) %y_7) + 1)) + ((u8) %y_7) = ((u8) (((u8) %y_7) + 1)) + ∧ (((u8) %y_7) + 1) = %y_7 ∧ emp |}] let%expect_test _ = diff --git a/sledge/lib/solver_test.ml b/sledge/lib/solver_test.ml index 8828f715f..aa4c72902 100644 --- a/sledge/lib/solver_test.ml +++ b/sledge/lib/solver_test.ml @@ -238,8 +238,7 @@ let%test_module _ = [%expect {| ( infer_frame: - (%l_6 + 8 × %n_9) -[ %l_6, 16 )-> ⟨(-8 × %n_9 + 16),%a_3⟩ - * %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩ + %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(-8 × %n_9 + 16),%a_3⟩ * ( ( 2 = %n_9 ∧ emp) ∨ ( 0 = %n_9 ∧ emp) ∨ ( 1 = %n_9 ∧ emp) @@ -273,8 +272,7 @@ let%test_module _ = {| ( infer_frame: (%n_9 ≤ 2) - ∧ (%l_6 + 8 × %n_9) -[ %l_6, 16 )-> ⟨(-8 × %n_9 + 16),%a_3⟩ - * %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩ + ∧ %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(-8 × %n_9 + 16),%a_3⟩ \- ∃ %a_1, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩ ) infer_frame: |}] diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml index 5c5758b7b..0f31eee2e 100644 --- a/sledge/lib/term.ml +++ b/sledge/lib/term.ml @@ -58,14 +58,14 @@ and T : sig type qset = Qset.t [@@deriving compare, equal, hash, sexp] type t = - | Add of qset - | Mul of qset | Var of {id: int; name: string} | Ap1 of op1 * t | Ap2 of op2 * t * t | Ap3 of op3 * t * t * t | ApN of opN * t iarray | RecN of recN * t iarray (** NOTE: cyclic *) + | Add of qset + | Mul of qset | Label of {parent: string; name: string} | Nondet of {msg: string} | Float of {data: string} @@ -75,14 +75,14 @@ end = struct type qset = Qset.t [@@deriving compare, equal, hash, sexp] type t = - | Add of qset - | Mul of qset | Var of {id: int; name: string} | Ap1 of op1 * t | Ap2 of op2 * t * t | Ap3 of op3 * t * t * t | ApN of opN * t iarray | RecN of recN * t iarray (** NOTE: cyclic *) + | Add of qset + | Mul of qset | Label of {parent: string; name: string} | Nondet of {msg: string} | Float of {data: string} diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli index ba24c85ae..5adb1c9c9 100644 --- a/sledge/lib/term.mli +++ b/sledge/lib/term.mli @@ -73,8 +73,6 @@ and T : sig type qset = Qset.t [@@deriving compare, equal, hash, sexp] and t = private - | Add of qset (** Sum of terms with rational coefficients *) - | Mul of qset (** Product of terms with rational exponents *) | Var of {id: int; name: string} (** Local variable / virtual register *) | Ap1 of op1 * t (** Unary application *) @@ -85,6 +83,8 @@ and T : sig (** Recursive n-ary application, may recursively refer to itself (transitively) from its args. NOTE: represented by cyclic values. *) + | Add of qset (** Sum of terms with rational coefficients *) + | Mul of qset (** Product of terms with rational exponents *) | Label of {parent: string; name: string} (** Address of named code block within parent function *) | Nondet of {msg: string} diff --git a/sledge/lib/term_test.ml b/sledge/lib/term_test.ml index 16918b33e..7be43cc99 100644 --- a/sledge/lib/term_test.ml +++ b/sledge/lib/term_test.ml @@ -75,7 +75,7 @@ let%test_module _ = let%expect_test _ = pp ((!2 * z * z) + (!3 * z) + !4) ; - [%expect {| (2 × (%z_2^2) + 3 × %z_2 + 4) |}] + [%expect {| (3 × %z_2 + 2 × (%z_2^2) + 4) |}] let%expect_test _ = pp @@ -88,9 +88,9 @@ let%test_module _ = + (!9 * z * z * z) ) ; [%expect {| - (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) + 3 × %y_1 - + 2 × %z_2 + 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) ; @@ -142,7 +142,7 @@ let%test_module _ = let%expect_test _ = pp (((!3 * y) + !2) * (!4 + (!5 * z))) ; - [%expect {| (15 × (%y_1 × %z_2) + 12 × %y_1 + 10 × %z_2 + 8) |}] + [%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))) ; @@ -170,19 +170,19 @@ let%test_module _ = let%expect_test _ = pp (!3 * y = z = true_) ; - [%expect {| ((3 × %y_1) = %z_2) |}] + [%expect {| (%z_2 = (3 × %y_1)) |}] let%expect_test _ = pp (true_ = (!3 * y = z)) ; - [%expect {| ((3 × %y_1) = %z_2) |}] + [%expect {| (%z_2 = (3 × %y_1)) |}] let%expect_test _ = pp (!3 * y = z = false_) ; - [%expect {| ((3 × %y_1) ≠ %z_2) |}] + [%expect {| (%z_2 ≠ (3 × %y_1)) |}] let%expect_test _ = pp (false_ = (!3 * y = z)) ; - [%expect {| ((3 × %y_1) ≠ %z_2) |}] + [%expect {| (%z_2 ≠ (3 × %y_1)) |}] let%expect_test _ = pp (y - (!(-3) * y) + !4) ; @@ -194,11 +194,11 @@ let%test_module _ = let%expect_test _ = pp (y = (!(-3) * y) + !4) ; - [%expect {| ((-3 × %y_1 + 4) = %y_1) |}] + [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}] let%expect_test _ = pp ((!(-3) * y) + !4 = y) ; - [%expect {| ((-3 × %y_1 + 4) = %y_1) |}] + [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}] let%expect_test _ = pp (sub true_ (z = !4)) ; @@ -206,7 +206,7 @@ let%test_module _ = 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)) ; @@ -255,7 +255,7 @@ let%test_module _ = pp (z1_2 * z1_2) ; [%expect {| - ((%z_2^2) + 2 × %z_2 + 1) + (2 × %z_2 + (%z_2^2) + 1) - (6 × (%z_2^2) + 4 × (%z_2^3) + (%z_2^4) + 4 × %z_2 + 1) |}] + (4 × %z_2 + 6 × (%z_2^2) + 4 × (%z_2^3) + (%z_2^4) + 1) |}] end )