ada/cvc5

Fork 0

mirror of https://github.com/AdaCore/cvc5.git synced 2026-02-12 12:32:16 -08:00

Commit Graph

Author	SHA1	Message	Date
mudathirmahgoub	944db35aa1	Fix cpp api coverage check (#10193 )	2023-12-04 08:32:52 -06:00
Hans-Jörg	14fc6f88bb	Fix behaviour and API tests for proofs (#10137 ) Add a test for '<<' for the proof format mode Add this test to the uncovered functions for Python and Java Return placeholder value if Proof object is empty Add tests for this (and add them to uncovered functions)	2023-11-07 17:29:44 +00:00
Hans-Jörg	ce64f348d3	Add API for Proofs (#9895 ) This pull requests adds support to get Proofs as proper objects from the API. To do so it adds an object Proof that encapsulates a ProofNode. Furthermore, it adds a function proofsToString to the Solver object that prints (a vector of) proofs. Finally, it modifies the getProof function of the Solver object to return proofs. Proof rules are returned as strings. One thing I don't quite like is that the proof component configuration must be given to both the getProof and proofsToString method and must be the same.	2023-10-12 12:05:01 -05:00

Author

SHA1

Message

Date

mudathirmahgoub

944db35aa1

Fix cpp api coverage check (#10193 )

2023-12-04 08:32:52 -06:00

Hans-Jörg

14fc6f88bb

Fix behaviour and API tests for proofs (#10137 )

Add a test for '<<' for the proof format mode
Add this test to the uncovered functions for Python and Java
Return placeholder value if Proof object is empty
Add tests for this (and add them to uncovered functions)

2023-11-07 17:29:44 +00:00

Hans-Jörg

ce64f348d3

Add API for Proofs (#9895 )

This pull requests adds support to get Proofs as proper objects from the API.

To do so it adds an object Proof that encapsulates a ProofNode. Furthermore, it adds a function proofsToString to the Solver object that prints (a vector of) proofs. Finally, it modifies the getProof function of the Solver object to return proofs.

Proof rules are returned as strings.

One thing I don't quite like is that the proof component configuration must be given to both the getProof and proofsToString method and must be the same.

2023-10-12 12:05:01 -05:00

3 Commits