Make Proof Rule enum a part of the API #9925
Conversation
|
Oh I noticed that I broke something with my last commit. Will investigate. |
hansjoergschurr
force-pushed
the
devel/public-rule-type
branch
from
938e806 to
a25ac49
Compare
hansjoergschurr
force-pushed
the
devel/public-rule-type
branch
4 times, most recently
from
b22fd2a to
3d9487e
Compare
hansjoergschurr
added
the
do not merge
hansjoergschurr
changed the title
|
Is this PR ready to go? I assume this is the first PR to go in for the proof API? |
hansjoergschurr
force-pushed
the
devel/public-rule-type
branch
from
33bab9b to
1a5eeb4
Compare
hansjoergschurr
removed
the
do not merge
hansjoergschurr
changed the title
|
If it passes the CI it should be ready to go. I just added Mathjax support. I am not 100% happy with including the config in the Javadoc CMake file. It seems fragile and somewhat repetitious, but I am not sure if there is a much better place. |
There was a problem hiding this comment.
A few requests. Also, I believe you will need to add the print function for ProofRule to the unit tests here:
https://github.com/cvc5/cvc5/blob/main/test/unit/api/python/test_uncovered.cpp
https://github.com/cvc5/cvc5/blob/main/test/unit/api/java/UncoveredTest.cpp
Also a cpp unit test for printing proof rules needs to be added I think, similar to:
https://github.com/cvc5/cvc5/blob/main/test/unit/api/cpp/api_kind_black.cpp
This moves the header file that contains the proof rule enum to the public headers and also moves the associated cpp file. Furthermore, it removes the `internal` namespace from those files.
This also renames some internal funtions and types that contain PfRule. This ensures consistency.
This uses a Regex to first split the comment at the two types of math tags and then skips thoes during replacements.
The old code to translate RST lists was very specific to the types of list that occured the enum docs. The new one should be more general. It can handle abritrarily nested lists.
The translator sees closing parentheses as part of a funtion
refrerence and would incorrectly move them inside an `{@ link ..}`
Co-authored-by: Aina Niemetz <[email protected]>
hansjoergschurr
force-pushed
the
devel/public-rule-type
branch
from
649662c to
c5bb767
Compare
|
I think I added the appropriate unit tests. |
This pull requests makes the enum that lists all proof rules a part of the API.
It also renames the enum from
PfRuletoProofRule. It also renames some unrelated types and function names that share thePfRulename (such asDslPfRule).This rename unfortunately touches many files since
PfRuleis not an uncommon type. (second to last commit)I also added the enum to the Java and Python API, but I am not sure I got this right. It is in the last commit.