@ -86,7 +86,7 @@ let%test_module _ =
let r0 = true _
let r0 = true _
let % expect_test _ = pp r0 ; [ % expect { | { sat = true ; rep = [] } | } ]
let % expect_test _ = pp r0 ; [ % expect { | { sat = true ; rep = [] } | } ]
let % expect_test _ = pp_classes r0 ; [ % expect { | | } ]
let % expect_test _ = pp_classes r0 ; [ % expect { | | } ]
let % test _ = difference r0 ( f x ) ( f x ) | > Poly . equal ( Some ( Z . of_int 0 ) )
let % test _ = difference r0 ( f x ) ( f x ) | > Poly . equal ( Some ( Z . of_int 0 ) )
let % test _ = difference r0 ! 4 ! 3 | > Poly . equal ( Some ( Z . of_int 1 ) )
let % test _ = difference r0 ! 4 ! 3 | > Poly . equal ( Some ( Z . of_int 1 ) )
@ -310,9 +310,7 @@ let%test_module _ =
let r11 = of_eqs [ ( ! 16 , z - x ) ; ( x + ! 8 - z , z - ! 16 + ! 8 - z ) ]
let r11 = of_eqs [ ( ! 16 , z - x ) ; ( x + ! 8 - z , z - ! 16 + ! 8 - z ) ]
let % expect_test _ =
let % expect_test _ = pp_classes r11 ; [ % expect { | ( % z_7 + - 16 ) = % x_5 | } ]
pp_classes r11 ; [ % expect { |
( % z_7 + - 16 ) = % x_5 | } ]
let r12 = of_eqs [ ( ! 16 , z - x ) ; ( x + ! 8 - z , z + ! 16 + ! 8 - z ) ]
let r12 = of_eqs [ ( ! 16 , z - x ) ; ( x + ! 8 - z , z + ! 16 + ! 8 - z ) ]
@ -343,8 +341,7 @@ let%test_module _ =
let % expect_test _ =
let % expect_test _ =
pp r14 ;
pp r14 ;
[ % expect
[ % expect
{ |
{ | { sat = true ; rep = [ [ % x_5 ↦ 1 ] ; [ ( % y_6 ≠ 0 ) ↦ - 1 ] ] } | } ]
{ sat = true ; rep = [ [ % x_5 ↦ 1 ] ; [ ( % y_6 ≠ 0 ) ↦ - 1 ] ] } | } ]
let % test _ = entails_eq r14 a Term . true_
let % test _ = entails_eq r14 a Term . true_
let % test _ = entails_eq r14 b Term . true_
let % test _ = entails_eq r14 b Term . true_