Proof Log Command line uses

[HarryBryant99]

Hi

I am using Z3 version 4.12.2 and playing around with the proof logs. I want to experiment with the command: set_param("solver.proof.check_rup", False) however when I run Z3 it returns that this is an unknown parameter 'proof.check_rup' at module 'solver'.

Is there another command I need to use? I have tried using the python/z3/parameter methods and all say the same thing.

Any advice would be greatly appriecated.

[NikolajBjorner]

I must have missed moving it from sat params.

sat.smt.proof.check_rup (bool) apply forward RUP proof checking (default: true)

[HarryBryant99]

Thank you. This is now being accepted and parses.

Although even though I have set it to false my proof log still includes:
(declare-fun rup () Proof)
(infer rup)

I am following the example from the Z3 Guide Proof Log page (https://microsoft.github.io/z3guide/programming/Proof%20Logs/) and is as follows:

(set-option :sat.euf true)
(set-option :tactic.default_tactic smt)
(set-option :solver.proof.log no_rup.smt2)

(set-option :sat.smt.proof.check_rup false)

(declare-fun d (Int Int) Int)
(declare-fun t (Int Int Real) (Array Int (Array Int Real)))
(assert (forall ((u Int) (v Real)) (= v (select (select (t v (d 1 0) (d 0 u)) 0) 0))))
(check-sat)

Apologies if this what it is supposed to do, I just assumed that by setting "sat.smt.proof.check_rup" to false I would get a different proof.

Thank you again
Harry

[NikolajBjorner]

The option controls whether rup inferences are checked. The inferences are still logged.
Inferences can be checked online during search or they can be checked offline by reparsing the log.
So you can choose to log, then check theory axioms only (by disabling rup checking) or you can check both.
Checking theory axioms is local. The self-checker has some fast-paths for checking theory axioms. Specifically for euf.
For arithmetic it is currently much more ad-hoc: it tries a fast path and falls back to calling the SMT solver.
For other theories it is at this point even less "fast-path", but may still be a useful aid in debugging unsoundness.
Proof checking can be accomplished outside of z3, of course, but somebody has to write the proof checker first :-)

[HarryBryant99]

Thank you for your help and explanation :)