From b3d238c842728fd2fd8881e872d20c1b2e970b8d Mon Sep 17 00:00:00 2001 From: someplaceguy Date: Fri, 26 Jan 2024 02:16:10 +0000 Subject: [PATCH 1/2] HolSmt: fix Z3 proof replay in real arith w/ rational coefficients It turns out that the existing Z3 proof reconstruction code was using RealArith.REAL_ARITH to replay linear arithmetic steps in proofs. However, RealArith.REAL_ARITH only handles integral coefficients and therefore proof steps such as `(x: real) / 1r = x` were failing. To fix this, we simply switch to RealField.REAL_ARITH, which supports rational coefficients. This allows us to enable proof reconstruction for 3 more self-tests, all related to the reals. This also means that all real-related tests in the self-tests now work with proof reconstruction. The RealArith->RealField change in the "rewrite" rule handler fixes proof steps such as these: `(rewrite (= (/ v0 1.0) v0))` and allows us to reenable the first self-test. The identical change in the "th_lemma[arith]" rule handler fixes proof steps such as the following: ((_ |th-lemma| arith farkas -41/42 1) @x76 @x77 false) ... corresponding to: [.] |- ~(x <= 0r)), [.] |- 41r / 42r * x <= 0r], F ... which allows us to reenable proof reconstruction for the other two self-tests. --- src/HolSmt/Z3_ProofReplay.sml | 4 ++-- src/HolSmt/selftest.sml | 9 +++------ 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml index 872f2d3164..e647588be8 100644 --- a/src/HolSmt/Z3_ProofReplay.sml +++ b/src/HolSmt/Z3_ProofReplay.sml @@ -798,7 +798,7 @@ local handle Feedback.HOL_ERR _ => if term_contains_real_ty t then - profile "rewrite(11.1)(REAL_ARITH)" RealArith.REAL_ARITH t + profile "rewrite(11.1)(REAL_ARITH)" RealField.REAL_ARITH t else profile "rewrite(11.2)(ARITH_PROVE)" intLib.ARITH_PROVE t in @@ -836,7 +836,7 @@ local (* this is just a heuristic - it is quite conceivable that a term that contains type real is provable by integer arithmetic *) - profile "th_lemma[arith](3.1)(real)" RealArith.REAL_ARITH t' + profile "th_lemma[arith](3.1)(real)" RealField.REAL_ARITH t' else profile "th_lemma[arith](3.2)(int)" intLib.ARITH_PROVE t' val subst = List.map (fn (term, var) => {redex = var, residue = term}) diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml index 8841a4a104..6a501bfcca 100644 --- a/src/HolSmt/selftest.sml +++ b/src/HolSmt/selftest.sml @@ -213,9 +213,6 @@ in (* real *) - (* Z3 2.19 prints reals as integers in its proofs; I see no way to - reliably distinguish between them. *) - (``0r = 0r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), (``1r = 1r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), (``0r = 1r``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), @@ -450,9 +447,9 @@ in (``1 * (x:real) = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), (``(x:real) * 42 = 42 * x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), - (``(x:real) / 1 = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3(*, thm_Z3p*)]), - (``x > 0 ==> (x:real) / 42 < x``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3(*, thm_Z3p*)]), - (``x < 0 ==> (x:real) / 42 > x``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3(*, thm_Z3p*)]), + (``(x:real) / 1 = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), + (``x > 0 ==> (x:real) / 42 < x``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3, thm_Z3p]), + (``x < 0 ==> (x:real) / 42 > x``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3, thm_Z3p]), (``abs (x:real) >= 0``, [thm_AUTO, thm_YO]), (``(abs (x:real) = 0) = (x = 0)``, [thm_AUTO, thm_YO]), From 7b32ff2446b6017d8f2945b88788040a611eda1a Mon Sep 17 00:00:00 2001 From: someplaceguy Date: Fri, 26 Jan 2024 02:37:46 +0000 Subject: [PATCH 2/2] HolSmt: convert test cases to use reals instead of nums These test cases were almost surely intended to test the reals, since they are in the `reals` section and identical test cases covering the nums already exist in the `nums` section. Since cvc5 and Z3 can reason about the reals (unlike the nums, currently) we can enable them for these tests. This includes Z3 with proof reconstruction. --- src/HolSmt/selftest.sml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml index 6a501bfcca..1cebbf5813 100644 --- a/src/HolSmt/selftest.sml +++ b/src/HolSmt/selftest.sml @@ -548,10 +548,10 @@ in (``(x:real) < x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), (``(x:real) < y ==> 42 * x < 42 * y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), - (``0n <= 1n``, [thm_AUTO, thm_YO]), - (``1n <= 0n``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), - (``(x:num) <= x``, [thm_AUTO, thm_YO]), - (``(x:num) <= y ==> 2 * x <= 2 * y``, [thm_AUTO, thm_YO]), + (``0r <= 1r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), + (``1r <= 0r``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]), + (``(x:real) <= x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), + (``(x:real) <= y ==> 42 * x <= 42 * y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), (``1r > 0r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]), (``0r > 1r``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),