diff --git a/bench/valid/int.why b/bench/valid/int.why index f4936ebbddbaa5c83d259ca200c0593f62af46bc..d0ccab74b4e1e66e3ac6a0ac3396e699947b7862 100644 --- a/bench/valid/int.why +++ b/bench/valid/int.why @@ -2,4 +2,14 @@ theory Test use import int.Int goal G1 : 5 * 10 = 50 goal G2 : forall x:int. x + x - x + x = 2 * x + + goal CompatOrderAdd : forall x y z : int. x <= y -> x + z <= y + z + goal CompatOrderMult : forall x y z : int. x <= y -> 0 <= z -> x * z <= y * z + + goal InvMult : forall x y : int. (-x) * y = - (x * y) = x * (-y) + goal InvSquare : forall x : int. x * x = (-x) * (-x) + goal ZeroMult : forall x : int. x * 0 = 0 = 0 * x + goal SquareNonNeg1 : forall x : int. x <= 0 -> 0 <= x * x + goal SquareNonNeg : forall x : int. 0 <= x * x + goal ZeroLessOne : 0 <= 1 end diff --git a/drivers/alt_ergo.drv b/drivers/alt_ergo.drv index c192132d68260e48ff4c0db801dac03d3cccbbf8..a82be90658cabc49ee2b74e83afeb938dc650db7 100644 --- a/drivers/alt_ergo.drv +++ b/drivers/alt_ergo.drv @@ -59,6 +59,8 @@ theory int.Int remove prop Trans remove prop Total remove prop Antisymm + remove prop NonTrivialRing + remove prop CompatOrderAdd end @@ -102,6 +104,8 @@ theory real.Real remove prop Total remove prop Antisymm remove prop Inverse + remove prop NonTrivialRing + remove prop CompatOrderAdd end diff --git a/drivers/coq.drv b/drivers/coq.drv index 9a094dc0f67656102f52d2006c8b6702c6952ff0..5709bfd8a679010c19e2263f7a09313589320424 100644 --- a/drivers/coq.drv +++ b/drivers/coq.drv @@ -72,6 +72,10 @@ theory int.Int remove prop Trans remove prop Antisymm remove prop Total + remove prop NonTrivialRing + remove prop CompatOrderAdd + remove prop CompatOrderMult + end theory int.Abs @@ -125,6 +129,9 @@ theory real.Real remove prop Comm.Comm remove prop Unitary remove prop Inverse + remove prop NonTrivialRing + remove prop CompatOrderAdd + remove prop CompatOrderMult end diff --git a/drivers/cvc3.drv b/drivers/cvc3.drv index a28dd7ae409b25ec3cd817446a7ec4967b581e3f..3655922f5e05fecb63d7dc2350e0f30343b68d3f 100644 --- a/drivers/cvc3.drv +++ b/drivers/cvc3.drv @@ -58,6 +58,8 @@ theory int.Int remove prop Trans remove prop Antisymm remove prop Total + remove prop NonTrivialRing + remove prop CompatOrderAdd meta "encoding : kept" type int @@ -96,6 +98,8 @@ theory real.Real remove prop Trans remove prop Antisymm remove prop Total + remove prop NonTrivialRing + remove prop CompatOrderAdd meta "encoding : kept" type real diff --git a/drivers/simplify.drv b/drivers/simplify.drv index bfb578e9da53c87a70afd65a9504f2f4d2147924..65b4ae32469caf2e1d7d58914957332432fecc50 100644 --- a/drivers/simplify.drv +++ b/drivers/simplify.drv @@ -62,6 +62,8 @@ theory int.Int remove prop Trans remove prop Antisymm remove prop Total + remove prop NonTrivialRing + remove prop CompatOrderAdd (* use with explicit polymorphism *) meta "enco_poly" "explicit" diff --git a/drivers/z3.drv b/drivers/z3.drv index 399f67495d166b75daa99814d92455e2a44cf4af..e46c5f23ae5e2804db14bee85cb46b3fffcbb3d7 100644 --- a/drivers/z3.drv +++ b/drivers/z3.drv @@ -58,6 +58,8 @@ theory int.Int remove prop Trans remove prop Antisymm remove prop Total + remove prop NonTrivialRing + remove prop CompatOrderAdd meta "encoding : kept" type int @@ -96,6 +98,8 @@ theory real.Real remove prop Trans remove prop Antisymm remove prop Total + remove prop NonTrivialRing + remove prop CompatOrderAdd meta "encoding : kept" type real