Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

HolSmt: fix Z3 proof replay in real arithmetic with rational coefficients #1188

Merged
merged 2 commits into from
Jan 28, 2024
Merged

HolSmt: fix Z3 proof replay in real arithmetic with rational coefficients #1188

merged 2 commits into from
Jan 28, 2024

Commits on Jan 26, 2024

  1. 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.
    @someplaceguy
    someplaceguy committed Jan 26, 2024
    Configuration menu
    Copy the full SHA
    b3d238c View commit details
    Browse the repository at this point in the history

  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.
    @someplaceguy
    someplaceguy committed Jan 26, 2024
    Configuration menu
    Copy the full SHA
    7b32ff2 View commit details
    Browse the repository at this point in the history