From a2ffe1e479b72ab193445555bac134184369190d Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Fri, 12 Aug 2022 13:45:52 -0700 Subject: [PATCH] Add a test case for asserting universally-quantified statements. Fixes #1037 --- intTests/test_univ_assert/README | 4 ++++ intTests/test_univ_assert/test.saw | 33 ++++++++++++++++++++++++++++++ intTests/test_univ_assert/test.sh | 1 + 3 files changed, 38 insertions(+) create mode 100644 intTests/test_univ_assert/README create mode 100644 intTests/test_univ_assert/test.saw create mode 100644 intTests/test_univ_assert/test.sh diff --git a/intTests/test_univ_assert/README b/intTests/test_univ_assert/README new file mode 100644 index 0000000000..eab6f5c36f --- /dev/null +++ b/intTests/test_univ_assert/README @@ -0,0 +1,4 @@ +This is a test of the capability to assert first-order statements +to the solver. Here, we are reasoning abstractly over about +generic properties of addition and multiplication (essentially, +some of the ring axioms). diff --git a/intTests/test_univ_assert/test.saw b/intTests/test_univ_assert/test.saw new file mode 100644 index 0000000000..7e97ced8fa --- /dev/null +++ b/intTests/test_univ_assert/test.saw @@ -0,0 +1,33 @@ +enable_experimental; + +let {{ + type vec_t = [384] + mul : vec_t -> vec_t -> vec_t + mul x y = undefined // this would be e.g. multiplication modulo p + add : vec_t -> vec_t -> vec_t + add x y = undefined + + term1 x y z1 z2 z3 = add (mul (add (mul (add (mul x y) z1) x) z2) x) z3 + term2 x y z1 z2 z3 = add (mul y (mul x (mul x x))) (add (mul z1 (mul x x)) (add (mul z2 x) z3)) +}}; + +// Assume some of the ring axioms +lemmas <- for + [ {{ \x y -> mul x y == mul y x }} + , {{ \x y -> add x y == add y x }} + , {{ \x y z -> mul (mul x y) z == mul x (mul y z) }} + , {{ \x y z -> add (add x y) z == add x (add y z) }} + , {{ \x y z -> mul (add x y) z == add (mul x z) (mul y z) }} + ] + (prove_print assume_unsat); + +// Use those axioms to prove a nonmtrivial equality +thm <- prove_print + (do { + unfolding ["term1","term2"]; + for lemmas goal_insert; + w4_unint_z3 ["mul","add"]; + }) + {{ \x y z1 z2 z3 -> term1 x y z1 z2 z3 == term2 x y z1 z2 z3 }}; + +print thm; diff --git a/intTests/test_univ_assert/test.sh b/intTests/test_univ_assert/test.sh new file mode 100644 index 0000000000..0b864017cd --- /dev/null +++ b/intTests/test_univ_assert/test.sh @@ -0,0 +1 @@ +$SAW test.saw