8 Commits

Author SHA1 Message Date
Aina Niemetz
0647c4c107 Update copyright headers. (#11561)
Co-authored-by: Daniel Larraz <daniel-larraz@users.noreply.github.com>
2025-01-23 17:54:20 +00:00
Hans-Jörg
bd2d37404b Change author name from "Hans-Jörg" to "Hans-Joerg" (#11155)
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
2024-08-13 09:24:21 +00:00
Aina Niemetz
5a31718ffd c api: Add support for proofs. (#10877) 2024-06-26 17:58:07 +00:00
Aina Niemetz
434cdead90 test: Add tests for uncovered API coverage. (#10725) 2024-05-06 08:27:49 -05:00
Abdalrhman Mohamed
9d1e1a15a4 Expose DSL Proof Rules. (#10568)
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.
2024-04-18 15:09:59 +00:00
Andrew Reynolds
7af25ed764 Fix uncovered API errors due to skolem ids (#10561)
Fixes the nightlies.
2024-03-28 16:15:21 +00:00
Aina Niemetz
fdf9ce7138 Update copyright headers. (#10459) 2024-03-12 09:35:09 -07:00
Hans-Jörg
0a35879fc1 Make Proof Rule enum a part of the API (#9925)
This pull requests makes the enum that lists all proof rules a part of the API.

It also renames the enum from PfRule to ProofRule. It also renames some unrelated types and function names that share the PfRule name (such as DslPfRule).
This rename unfortunately touches many files since PfRule is not an uncommon type. (second to last commit)
2023-09-27 00:58:03 +00:00