Skip to content

Commit

Permalink
HolSmt: add full battery of quot and rem tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@someplaceguy
someplaceguy committed Mar 14, 2024
1 parent 6220a17 commit e14320c
Showing 1 changed file with 93 additions and 0 deletions.
93 changes: 93 additions & 0 deletions src/HolSmt/selftest.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -425,6 +425,55 @@ in
(``(x:int) < 0 ==> (x / ~1 = ~x / 1)``,
[thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),

(``(~42:int) quot ~42 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~1:int) quot ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(0:int) quot ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(1:int) quot ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(42:int) quot ~42 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~42:int) quot ~1 = 42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~1:int) quot ~1 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(0:int) quot ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(1:int) quot ~1 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(42:int) quot ~1 = ~42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~42:int) quot 1 = ~42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~1:int) quot 1 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(0:int) quot 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(1:int) quot 1 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(42:int) quot 1 = 42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~42:int) quot 42 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~1:int) quot 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(0:int) quot 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(1:int) quot 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(42:int) quot 42 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) quot 1 = x``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) quot ~1 = ~x``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) quot 42 <= x``, [sat_CVC, sat_Z3, sat_Z3p]),
(``(x:int) quot 42 <= ABS x``,
[thm_AUTO, (*thm_CVC,*) thm_Z3_v4, thm_Z3p_v4]),
(``((x:int) quot 42 = x) = (x = 0)``,
[thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) quot 42 = x <=> x = 0 \/ x = ~1``, [sat_CVC, sat_Z3, sat_Z3p]),
(``(x:int) quot 0 = x``, [sat_CVC, sat_Z3, sat_Z3p]),
(``(x:int) quot 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
(``(0:int) quot 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
(``(0:int) quot 0 = 1``, [sat_CVC, sat_Z3, sat_Z3p]),
(``(0:int) quot 0 = 1 quot 0``, [sat_CVC, sat_Z3, sat_Z3p]),
(``(x:int) quot 0 = x quot 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),

(* cf. integerTheory.int_quot *)
(``(x:int) < 0 ==> (x quot 1 = ~(~x quot 1))``,
[thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) < 0 ==> (x quot 42 = ~(~x quot 42))``,
[thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``0 <= (x:int) ==> (x quot ~42 = ~(x quot 42))``,
[thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``0 <= (x:int) ==> (x quot ~1 = ~(x quot 1))``,
[thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) < 0 ==> (x quot ~42 = ~x quot 42)``,
[thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) < 0 ==> (x quot ~1 = ~x quot 1)``,
[thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),

(``(~42:int) % ~42 = 0``,
[thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
(``(~1:int) % ~42 = ~1``,
Expand Down Expand Up @@ -487,6 +536,50 @@ in
(``(x:int) % 42 = x - x / 42 * 42``,
[thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),

(``(~42:int) rem ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~1:int) rem ~42 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(0:int) rem ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(1:int) rem ~42 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(42:int) rem ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~42:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~1:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(0:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(1:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(42:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~42:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~1:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(0:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(1:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(42:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~42:int) rem 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(~1:int) rem 42 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(0:int) rem 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(1:int) rem 42 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(42:int) rem 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) rem 42 < 42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``((x:int) rem 42 = x) = (x < 42)``, [sat_CVC, sat_Z3, sat_Z3p]),
(``((x:int) rem 42 = x) <=> (0 <= x) /\ (x < 42)``,
[sat_CVC, sat_Z3, sat_Z3p]),
(``((x:int) rem 42 = x) <=> (-42 < x) /\ (x < 42)``,
[thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) rem 0 = x``, [sat_CVC, sat_Z3, sat_Z3p]),
(``(x:int) rem 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
(``(0:int) rem 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
(``(0:int) rem 0 = 1``, [sat_CVC, sat_Z3, sat_Z3p]),
(``(x:int) rem 0 = x rem 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),

(* cf. integerTheory.int_rem *)
(``(x:int) rem ~42 = x - x quot ~42 * ~42``,
[thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) rem ~1 = x - x quot ~1 * ~1``,
[thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) rem 1 = x - x quot 1 * 1``,
[thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
(``(x:int) rem 42 = x - x quot 42 * 42``,
[thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),

(``ABS (x:int) >= 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),
(``(ABS (x:int) = 0) = (x = 0)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),
(``(x:int) >= 0 ==> (ABS x = x)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),
Expand Down

0 comments on commit e14320c

Please sign in to comment.