Internal variables in proofs

[m-fleury]

On the following input file:

SMT: Problem:
       ; smt.random_seed=1 smt.refine_inj_axioms=false -T:1000000 -smt2
       (set-option :produce-proofs true)
       (set-logic AUFLIA)
       (declare-fun a$ () Bool)
       (declare-fun b$ () Bool)
       (declare-fun c$ () Bool)
       (declare-fun d$ () Bool)
       (assert (! (not (=> (or (and a$ b$) (and c$ d$)) (or (and a$ b$) (and c$ d$)))) :named a0))
       (check-sat)
       (get-proof)

z3 produces a proof with two new variables k!00 and k!10.

       unsat
       ((set-logic AUFLIA)
       (declare-fun k!10 () Bool)
       (declare-fun k!00 () Bool)
       (proof
       (let (($x67 (not k!10)))
        (let (($x28 (and c$ d$)))
        (let (($x41 (not $x28)))
        (let (($x37 (not (or (and a$ b$) $x28 (not (or (and a$ b$) $x28))))))
        (let (($x31 (not (=> (or (and a$ b$) $x28) (or (and a$ b$) $x28)))))
        (let ((@x35 (mp (asserted $x31) (rewrite (= $x31 $x37)) $x37)))
        (let ((@x42 (not-or-elim @x35 $x41)))
        (let ((@x69 (mp (mp @x42 (rewrite (= $x41 $x41)) $x41) (rewrite (= $x41 $x67)) $x67)))
        (let (($x58 (not k!00)))
        (let (($x25 (and a$ b$)))
        (let (($x36 (not $x25)))
        (let ((@x39 (not-or-elim @x35 $x36)))
        (let ((@x60 (mp (mp @x39 (rewrite (= $x36 $x36)) $x36) (rewrite (= $x36 $x58)) $x58)))
        (let (($x71 (or k!00 k!10)))
        (let (($x29 (or $x25 $x28)))
        (let ((@x43 (not-or-elim @x35 $x29)))
        (let ((@x73 (mp (mp @x43 (rewrite (= $x29 $x29)) $x29) (rewrite (= $x29 $x71)) $x71)))
        (unit-resolution @x73 @x60 @x69 false)))))))))))))))))))) 

From the proof step (rewrite (= $x36 $x58)) (namely ((a$ ∧ b$) ∨ (c$ ∧ d$)) = (k!00 ∨ k!10)), I assume that k!00 and k10 are internal variables (maybe to achieve lazy CNF transformation?). Would it be possible to introduce them with let and produce a proper definition?

[NikolajBjorner]

I will not have bandwidth to dig into this. You are welcome to investigate further.

[NikolajBjorner]

this one does not repro with internal constants. Generally, the solver is permitted to introduce fresh functions/constants and the proof mode or checker would need to be fixed/adapted.

[m-fleury]

Interesting. As far as I know, this behavior is not mentioned anywhere, including in the latest reconstruction for Z3 proofs, namely KeY from 2021.

Thanks a lot for digging into that issue!

[m-fleury]

For the sake of documentation: according to bisecting, this seems to have been fixed by

commit b1606487f08cec8d950be078ac31881fc36a7bea
Author: Nikolaj Bjorner <nbjorner@microsoft.com>
Date:   Sun May 30 10:32:30 2021 -0700

    fix #5289

 src/ackermannization/ackr_model_converter.cpp | 16 +++++++-------
 src/ast/recfun_decl_plugin.cpp                | 14 +++++++++++-
 src/ast/recfun_decl_plugin.h                  |  2 ++
 src/ast/rewriter/var_subst.cpp                |  2 +-
 src/cmd_context/cmd_context.cpp               | 32 +++++++++++++++++++++++----
 src/cmd_context/cmd_context.h                 |  1 +
 src/model/model.cpp                           | 30 +++++++++++++++++++++++++
 src/model/model.h                             |  1 +
 src/smt/smt_context.cpp                       | 27 ++--------------------
 9 files changed, 86 insertions(+), 39 deletions(-)

[m-fleury]

For documentation purpose (because I just tried): the internal variables like k!00 are here again (in version z3-4.12.2)

EDIT: I bisected it: 689af3b is the last known good and 0b83732 the first known bad, as the ones in between do not compile.