This is a large pull request introducing the new low-level proof format.
The patch has become quite big, mostly because it also introduces a new LambdaTerm in Library-SMTLIB. This required to change all TermWalker to accept this new term. This new lambda term is used for the choose function in the proof format. We may in the future also remove QuantifiedFormula and instead use an application term on a lambda term, similar to what is planned for SMTLIB-3.0.
Another incompatible change is that theory.term now returns Term instead of ApplicationTerm. The reason is the automatic normalization of integers/rationals: The term (- 15) is now always represented by a ConstantTerm of Rational instead of application term, even if it was created by the function Theory.term(FunctionSymbol, Term...). This fixes a problem with strange proofs when the input formula contains (let ((x 15)) (f (- x))).
The old proofs also changed somewhat. In particular the @clause rule has changed and the proved clause has moved to the annotation (and no longer includes the or). Also the @split rule has been removed and instead @tautology and @res need to be combined. Also and and => is no longer rewritten to or by the TermCompiler and double negation is now implicitly handled by the proof checker. But most of the other changes are below the clause-level and should therefore not affect the interpolator. The :quoted annotations have been removed. In the future I may remove more :quotedCC, :quotedLA, and :quotedQuant annotations to simplify the low-level proofs.
The solver now supports three different proof levels: CLAUSE, FULL and LOWLEVEL. There is a new option :proof-level to choose the proof level. The interpolator needs CLAUSE or FULL proofs, as the low-level proofs do not include information about the partition and they introduce a lot more "very mixed" terms that are bad for interpolation. Proofs are generated in the old format (either CLAUSE or FULL). Low-level proofs, are then generated from FULL proofs, by the ProofSimplifier.
@danieldietsch I included you, so that you are aware of the changes, especially the incompatibilities that may apply to Ultimate: There may be some compilation issues: Term manipulating classes may need to be adapted for LambdaTerm (especially TermWalker), some casts to ApplicationTerm may need to be manually introduced. Also SMTLIBOptions has been renamed to SMTLIBConstants.
It would also be great if you can test if this breaks other things in Ultimate.
Known Bug: FormulaLet on formulas in new proof format can lead to problems with define-fun scope in the new proof format (that FormulaLet doesn't know about).
This is a large pull request introducing the new low-level proof format.
The patch has become quite big, mostly because it also introduces a new LambdaTerm in Library-SMTLIB. This required to change all TermWalker to accept this new term. This new lambda term is used for the choose function in the proof format. We may in the future also remove QuantifiedFormula and instead use an application term on a lambda term, similar to what is planned for SMTLIB-3.0.
Another incompatible change is that theory.term now returns Term instead of ApplicationTerm. The reason is the automatic normalization of integers/rationals: The term
(- 15)is now always represented by a ConstantTerm of Rational instead of application term, even if it was created by the functionTheory.term(FunctionSymbol, Term...). This fixes a problem with strange proofs when the input formula contains(let ((x 15)) (f (- x))).The old proofs also changed somewhat. In particular the
@clauserule has changed and the proved clause has moved to the annotation (and no longer includes theor). Also the@splitrule has been removed and instead@tautologyand@resneed to be combined. Alsoandand=>is no longer rewritten toorby the TermCompiler and double negation is now implicitly handled by the proof checker. But most of the other changes are below the clause-level and should therefore not affect the interpolator. The:quotedannotations have been removed. In the future I may remove more:quotedCC,:quotedLA, and:quotedQuantannotations to simplify the low-level proofs.The solver now supports three different proof levels: CLAUSE, FULL and LOWLEVEL. There is a new option
:proof-levelto choose the proof level. The interpolator needs CLAUSE or FULL proofs, as the low-level proofs do not include information about the partition and they introduce a lot more "very mixed" terms that are bad for interpolation. Proofs are generated in the old format (either CLAUSE or FULL). Low-level proofs, are then generated from FULL proofs, by theProofSimplifier.@danieldietsch I included you, so that you are aware of the changes, especially the incompatibilities that may apply to Ultimate: There may be some compilation issues: Term manipulating classes may need to be adapted for LambdaTerm (especially TermWalker), some casts to ApplicationTerm may need to be manually introduced. Also SMTLIBOptions has been renamed to SMTLIBConstants. It would also be great if you can test if this breaks other things in Ultimate.
Known Bug: FormulaLet on formulas in new proof format can lead to problems with define-fun scope in the new proof format (that FormulaLet doesn't know about).