summaryrefslogtreecommitdiff
path: root/src/api/cpp/cvc5_checks.h
AgeCommit message (Collapse)Author
2021-11-06Print `unsupported` for unrecognized flags. (#7384)Abdalrhman Mohamed
Fixes #7374.
2021-10-28Add a `define-fun` command for each `:named` term. (#7308)Abdalrhman Mohamed
This PR is step towards enabling -o raw-benchmark for regressions. It creates a define-fun command for each named term. This allows us to reparse dumped benchmarks containing named terms, but we still lose track of those terms and do not print them in response to (get-assignment) and (get-unsat-core) commands. This PR also simplifies the interface for DefineFunCommand interface and removes support for (define ...) command.
2021-04-21Goodbye CVC4, hello cvc5! (#6371)Mathias Preiner
This commits changes the build system to cvc5 and removes the remaining occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
2021-04-15Rename occurrences of CVC4 to CVC5. (#6351)Aina Niemetz
This renames everything but GitHub links and build system related macros. Switching the build system to cvc5 will be the last step in the renaming process.
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4_ macros to CVC5_. (#6327)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-07New C++ Api: Rename and move checks.h. (#6306)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback