Cython `cdef` classes without an explicit `__init__` constructor have an
implicit `__init__` that accepts any number of arguments. (Python
classes, by contrast, default to an `__init__` that takes no arguments.)
This can lead to confusing situations where arguments appear to be
accepted but are discarded. This PR fixes the issue by adding explicit
`__init__` methods to the Cython classes.
Additionally, this PR removes some unnecessary field initializations in
the Cython classes.
The helper method `create_rewrite_proof` no longer generates rewrite
rule holes on my dev branch, since the given rewrite is handled by
ARITH_POLY_NORM now.
The later uses only ASCII letters instead of Unicode characters. This
currently leads to a build issue with the Java headers on FreeBSD:
https://github.com/cvc5/cvc5/issues/11145
This PR exposes hashing and equality of proofs in the API to avoid
reconstructing the same proof step multiple times from the Lean side.
Notes:
- Proof equality in this PR is referential, not syntactical. However,
this is still useful for caching (and better than nothing).
- A default constructor, `Proof()`, is added to the Java API to mirror
the C++ and Python APIs and the `Term()` constructor in the Java API.
This PR implements one approach to exposing DSL Proof rules to the user: by making the DSL rule enum public.
Notes:
The safe toString method is not included in safe_print.h because it's generated by the RARE parser.
To test the hash and toString, for all enum values, a "last" enum value is needed. However, the current last enum value (DISTINCT_BINARY_ELIM) used in the test is generated by the RARE parser and may change in the future. Potential fixes include: adding LAST enum value, moving NONE to the end, or defining a LAST whose value is generated by the RARE parser.
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.
