Develop a common proof format and export proofs #458

gcarpio21 · 2025-03-19T12:29:15Z

Objective

This PR aims to expose proofs produced by supported solvers through the API, primarily via a getProof() method.

Key Changes

Introduced ProofNode, ProofDag, and ProofRule as the main components for handling proofs.
Implemented proof retrieval for the Z3 solver.
Explored a standardized format for proofs across different solvers.

Proof Format Conversion

To unify proof representation, this PR investigates converting solver-specific proofs into a common format, with RESOLUTE (used by SMTInterpol) as a candidate.

The proposed approach models proof rules in CNF and transforms them into resolution steps.
The Z3ToResoluteProofConverter provides an example of this transformation.

Task List

Next Steps

More flexibility while handling proofs could be provided through the ProofDag interface.

…getProof() in BasicProverEnvironment.java

…aviour of getProof to return unsupported operation.

…p_a_common_proof_format_and_export_proofs

…ts from SMTInterpol to a ResolutionProofDAG. Not working. Class SmtInterpolProofNode should help transform from the internal SMTInterpol proof representation to ResolutionProofDAG. Not working. Added some tests to evaluate proofs given back by SMTInterpol and the ResolutionProofDAG objects that should be returned.

Option requireProofs must be set to true through Configuration. Added a class for testing the proof generation of Z3. SMTInterpol: some documentation.

…roofs

Various changes to the ProofDAG interface and all classes inheriting it.

…roofs

…o multiple resolution steps.

…esolution steps.

…n now be converted to resolution proof rules.

- Renamed some classes for clarity - Z3: Made proof traversal non-recursive for efficiency.Added tests for proof-related functionality - CVC5: Implemented necessary classes for proof production - Improved documentation - Added test for retrieving proofs in ProverEnvironmentTest.java

…entation for when no formula is available.

… from Mathsat5

…object.

src/org/sosy_lab/java_smt/solvers/z3/Z3NonRecursiveProofProcessor.java

baierd

Some general things that i noticed (some may be mentioned in change requests, but apply generally):

Tests should be generalized and moved into the test package if they are not using native API. You can still have tests for a single solver in the test package by using the assume API and only allowing a single one. The name of the solver should be mentioned in the test name then.
Please add documentation to the new classes and interfaces. Especially mention which ones are used internally and which ones are public/usable by users and the purpose/background of the classes/interfaces.
You can have classes within classes, which is especially helpful to structure smaller components, e.g. nodes of a graph, within the context you are using them in. That makes the code much easier to read and structures it better.
Please avoid pushing print-outs or commented out code. If you are working on a feature thats not yet working, thats fine. Document it and don't use the component. Please add some documentation to the commented out code. Print-outs should never be pushed. Try using the logger or exceptions. In tests please use assertion instead of printouts. (It is OK to expect the current static output of a solver. If the test fails in the future, we devs are notified about changes that we might need to consider.)
Native API tests that just test that proofs work are good and can be added for all solvers supporting proofs.

baierd · 2025-03-21T17:20:26Z

src/org/sosy_lab/java_smt/ResProofRule.java

+ *
+ * @author Gabriel Carpio
+ */
+public class ResProofRule {


You could add sources (publication(s), reference sites etc.), the solvers that support this natively, as well as the usage/logic.

I added some documentation and will wait for further information on the format form Mathsat5 as it seems to be very similar.

baierd · 2025-03-21T17:37:31Z

src/org/sosy_lab/java_smt/ResolutionProofDag.java

+public class ResolutionProofDag extends AbstractProofDag {
+
+  /*
+  public ResolutionProofDAG() {


Is this class being worked on? If yes, in what form?

Please try to not push commented out code if possible. Also, please document this if it is supposed to be used in the future.

Made some adjustments to this.

baierd · 2025-03-21T17:40:31Z

src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java

+    try {
+      throw new UnsupportedOperationException("Proof generation isn't enabled.");
+    } catch (UnsupportedOperationException e) {
+      System.out.println(e.getMessage());


You can check if the prover is closed first, making sure that the prover is available.

It does not make much sense to throw an exception and catch it immediately again ;D
And please don't push print-outs. Try using the logger, exceptions if you want to notify the user.

Also, "Proof generation is not available for the chosen solver" is a better message for the exception type.

To check the state I will move this method to AbstractProver. There, there also a method checkGenerateProofs that mimics the behavior of the other check methods, I understand this should throw an Exception already. Aside from this, there is still the issue that, for example, for Z3 proof generation must be set as an Option in the configuration, so the solver should retrieve this information from the context in this case.

baierd · 2025-03-21T17:46:43Z

src/org/sosy_lab/java_smt/api/proofs/ProofDag.java

+import org.sosy_lab.java_smt.api.proofs.visitors.ProofVisitor;
+
+public interface ProofDag {
+  void addNode(ProofNode node);


The traversal of the proofs should be public API. Is this interface exposed to users?

Also, this is missing some comments and formatting.

This is supposed to be exposed to user, at least the get methods. However, this is still in the works and right now traversal should be only possible through the methods in ProofNode.

baierd · 2025-03-21T17:47:31Z

src/org/sosy_lab/java_smt/api/proofs/ProofFactory.java

+import org.sosy_lab.java_smt.ResProofRule.ResAxiom;
+
+public class ProofFactory {
+  public static ProofNode createSourceNode(ResAxiom rule, Formula formula) {


Building a proof should not be exposed to the user. Is ProofFactory available for users?

I'm currently trying to utilize this class to eliminate classes like Mathsat5ProofProcessor and Z3ToResoluteProofConverter. However, I'm facing an issue: ideally, the user shouldn't have direct access to these methods and should instead retrieve proofs via getProof from a ProverEnvironment instance. The challenge is that making the class non-public complicates its use within the solvers' packages.

baierd · 2025-03-21T18:26:19Z

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolProofsTest.java

+
+
+      //String proofStr = proof.toString();
+      System.out.println(invokeGetProofMode(smtinterpol).toString());


Please use assertions instead of printouts.

baierd · 2025-03-21T18:26:39Z

src/org/sosy_lab/java_smt/solvers/z3/Z3ProofsTest.java

+    ShutdownManager shutdown = ShutdownManager.create();
+
+    // Create new context with SMTInterpol
+    context = Z3SolverContext.create(


Why not use the SolverContextFactory?

baierd · 2025-03-21T18:28:00Z

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofsTest.java

+  }
+
+  private static Solver createEnvironment() throws CVC5ApiException {
+    Solver newSolver = new Solver();


This tests nothing currently. Also, native proof tests are good, but should be part of the CVC5 native test-class.

baierd · 2025-03-21T18:28:50Z

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java

@@ -79,6 +85,7 @@ public void createEnvironment() {
    long cfg = msat_create_config();

    msat_set_option_checked(cfg, "model_generation", "true");
+    msat_set_option_checked(cfg, "proof_generation", "true");


Why enable proofs for all tests and then build a new, dedicated solver environment for the proof test?

baierd · 2025-03-21T18:30:28Z

src/org/sosy_lab/java_smt/solvers/z3/Z3ToResoluteProofConverter.java

+ */
+
+@SuppressWarnings({"unchecked", "rawtypes", "unused", "static-access","ModifiedButNotUsed"})
+public class Z3ToResoluteProofConverter {


This class tackles a hard problem and should be documented with the used ideas and possible sources behind it.

I added further documentation

baierd · 2025-03-21T18:40:57Z

@leventeBajczi could you spare a look at this PR and maybe give us some feedback on the current proof interface?

…r by the name of the rule

gcarpio21 · 2025-03-24T12:24:22Z

@leventeBajczi could you spare a look at this PR and maybe give us some feedback on the current proof interface?

Definitely!

So far, I really like the relatively clean API for accessing the proofs, and I'm especially happy to see that the Z3 proofs are transformed to a 'simple' proof tree/DAG -- however, I'm uncertain how complete that transformation is based on the code, I think some information about that is missing (maybe as a comment?) to state how well Z3 proofs can be transformed into the common format.

Other than that, great work! I'm looking forward to integrating this with Theta. I'm really surprised at the number of solvers supporting proof generation, I only knew about MathSAT and Z3 beforehand. They will definitely be handy for us.

Have you maybe done some performance impact tests with the solvers when proof generation is enabled? I'd be interested to see how much performance is lost when it's active.

Right now, the Z3ToResoluteProofConverter class is still a work in progress. The goal is to transform Z3 proofs into a format similar to SMTInterpol’s (RESOLUTE), following the same proof rules.

Currently, the main functionality is to make Z3 proofs accessible through JavaSMT by simplifying Z3’s proof structures and implementing the ProofNode interface, which should capture all relevant proof information.

I haven’t run any performance tests yet. From what I know, enabling proof generation in a solver itself is usually quite costly. Hopefully, retrieving proofs through JavaSMT won’t introduce significant additional overhead.

I’ve also added more documentation in the code to clarify some of these points.

…esolutionProofDag`

…ion if proof generation is not enabled. The default method is now in `AbstractProver`instead of `BasicProverEnvironment`

…olProofNodeCreator`

…eritors

Fixed `Map`s in `ProofRuleResgistry` being empty

…en creating `Z3ProofNode`

… instances

…gain in interface `BasicProverEnvironment`

…evaluates to `unsat`

…evaluates to `unsat`.

…ublic

…roofs # Conflicts: # src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java

…f node for processing the proof terms. Renamed `getResAxiomRuleByName` to `getFromName` in `ResProofRule`

gcarpio21 added 16 commits February 3, 2025 19:26

Added multiple classes for supporting proof generation. Added method …

9f449e7

…getProof() in BasicProverEnvironment.java

Added GENERATE_PROOFS to ProverOptions

b2bc9eb

Added implementation of getProof for SMTInterpol. Changed default beh…

766e665

…aviour of getProof to return unsupported operation.

Merge remote-tracking branch 'refs/remotes/origin/master' into develo…

9c07f08

…p_a_common_proof_format_and_export_proofs

Z3: context now able to be created with proof generation.

955c1af

Option requireProofs must be set to true through Configuration. Added a class for testing the proof generation of Z3. SMTInterpol: some documentation.

Merge branch 'master' into develop_a_common_proof_format_and_export_p…

375937d

…roofs

Z3: Proof ast given by Z3 is now parsed to DAG made out of Z3ProofNode.

af4f670

Various changes to the ProofDAG interface and all classes inheriting it.

Z3: Corrections to the parsing of the proof ast.

c2139ad

Various changes to the ProofDAG interface and all classes inheriting it.

Mathsat5: The Native API now includes the methods for proof processing

e05451c

Merge branch 'master' into develop_a_common_proof_format_and_export_p…

e69d1e0

…roofs

Z3: The transitivity proof step from Z3 is now able to be converted t…

a6a3efd

…o multiple resolution steps.

Z3: Small correction when converting the transitivity proof rule to r…

2015b46

…esolution steps.

Z3: True, Asserted, Goal, MP, Reflexivity and Symmetry proof rules ca…

a4bbe62

…n now be converted to resolution proof rules.

Renamed some classes

e7940f1

gcarpio21 requested a review from baierd March 19, 2025 12:29

gcarpio21 self-assigned this Mar 20, 2025

gcarpio21 added 7 commits March 20, 2025 18:22

Renaming some classes for clarity

f988d6a

Method getFormula() in the ProofRule interface has default implem…

fcdf44f

…entation for when no formula is available.

Added Mathsat5ProofRule class

1d9ab98

Added Mathsat5ProofProcessor class for processing the proofs straight…

2fec458

… from Mathsat5

Added Mathsat5ProofNode class for storing the proofs in JavaSMT

7c20761

Mathsat5: proofs are enabled by setting ProverOptions.GENERATE_PROOFS

3d89810

Mathsat5: method getProof() now can be called to get a ProofNode …

d88ecb2

…object.

gcarpio21 commented Mar 20, 2025

View reviewed changes

src/org/sosy_lab/java_smt/solvers/z3/Z3NonRecursiveProofProcessor.java Show resolved Hide resolved

baierd requested changes Mar 21, 2025

View reviewed changes

gcarpio21 added 2 commits March 21, 2025 19:43

Checkstyle

e87f469

Class ProofRuleRegistry now allows to get a proof rule from any solve…

018d857

…r by the name of the rule

Z3: Changed the way the proof rule that Z3 gives back is processed

c5ea9bb

gcarpio21 added 28 commits March 24, 2025 19:37

ResolutionProofNode and SourceProofNode have been moved inside `R…

e2268ba

…esolutionProofDag`

getProof now checks if the state of the solver and throws an except…

e0d116d

…ion if proof generation is not enabled. The default method is now in `AbstractProver`instead of `BasicProverEnvironment`

Added documentation.

23e79a8

SMTInterpol: added basic traversal for retrieved proofs in `SmtInterp…

99f682e

…olProofNodeCreator`

Documentation

f0d19ac

getProof implementation was missing in some ProverEnvironment inh…

3debfe2

…eritors

Z3: added some tests for proofs

85f8e11

Refactoring of some methods and classes, name changes and modifiers.

44e6ce8

CVC5: fixed unending loop in getProof.

f7da393

Fixed `Map`s in `ProofRuleResgistry` being empty

Z3: Added tests for proof methods, fixed rule not properly created wh…

dc6d5b3

…en creating `Z3ProofNode`

CVC5: Corrected incorrect cast at getProof

12e4ccb

CVC5: proof dag now gets completely generated.

9bc37ca

Fixed incorrect generation of IDs for AbstractProofNode inheritors'…

78e5431

… instances

Documentation

9617048

AbstractProofNode now is an internal class of AbstractProofDag

95ee755

getProof no longer overridden in AbstractProver. default method a…

036a563

…gain in interface `BasicProverEnvironment`

getProof no longer overridden in AbstractProver. default method a…

fd2230a

…gain in interface `BasicProverEnvironment`

Mathsat5: getProof now checks if the state is closed and the stack …

7fcd878

…evaluates to `unsat`

Mathsat5: getProof now checks if the state is closed and the stack …

4dbc7ec

…evaluates to `unsat`.

Checkstyle

2aa8f25

Delete useless test in SmtInterpolProofsTest

07e5866

ProofRuleRegistry and method ProofRule.fromName no longer used

912e315

ProofRuleRegistry deleted ProofRule inheritor classes no longer p…

e942121

…ublic

Removed unwanted test

a888646

Merge branch 'master' into develop_a_common_proof_format_and_export_p…

2dce339

…roofs # Conflicts: # src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java

Checkstyle

9fc4a22

Removed duplicates

a268761

SMTInterpol: SmtInterpolProofNodeCreator creates a provitional proo…

fd5ae78

…f node for processing the proof terms. Renamed `getResAxiomRuleByName` to `getFromName` in `ResProofRule`

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Develop a common proof format and export proofs #458

Develop a common proof format and export proofs #458

gcarpio21 commented Mar 19, 2025 •

edited

Loading

baierd left a comment

baierd Mar 21, 2025

gcarpio21 Mar 24, 2025

baierd Mar 21, 2025

gcarpio21 Mar 24, 2025

baierd Mar 21, 2025

gcarpio21 Mar 25, 2025 •

edited

Loading

baierd Mar 21, 2025

gcarpio21 Mar 25, 2025

baierd Mar 21, 2025

gcarpio21 Mar 24, 2025

baierd Mar 21, 2025

baierd Mar 21, 2025

baierd Mar 21, 2025

baierd Mar 21, 2025

baierd Mar 21, 2025

gcarpio21 Mar 24, 2025

baierd commented Mar 21, 2025

gcarpio21 commented Mar 24, 2025



		//String proofStr = proof.toString();
		System.out.println(invokeGetProofMode(smtinterpol).toString());

Develop a common proof format and export proofs #458

Are you sure you want to change the base?

Develop a common proof format and export proofs #458

Conversation

gcarpio21 commented Mar 19, 2025 • edited Loading

Objective

Key Changes

Proof Format Conversion

Task List

Next Steps

baierd left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gcarpio21 Mar 25, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

baierd commented Mar 21, 2025

gcarpio21 commented Mar 24, 2025

gcarpio21 commented Mar 19, 2025 •

edited

Loading

gcarpio21 Mar 25, 2025 •

edited

Loading