cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2021-04-05	New C++ Api: Rename and move headers. (#6292)	Aina Niemetz

2021-04-01	Rename namespace CVC5 to cvc5. (#6258)	Aina Niemetz

2021-03-31	Rename namespace CVC4 to CVC5. (#6249)	Aina Niemetz

2021-03-16	cmake: Generate cvc4_export.h and set visibility to hidden. (#6139)	Mathias Preiner
	The build system (cmake) will automatically generate an export header cvc4_export.h, which makes sure that the correct export features are defined depending on the compiler and target platform. The macro CVC4_EXPORT replaces CVC4_PUBLIC and its usage is reduced by 2/3. Co-authored-by: Gereon Kremer <nafur42@gmail.com>
2021-03-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2020-09-22	Update copyright header script to support CMake and Python files (#5067)	Mathias Preiner
	This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-06-16	Update copyright headers.	Aina Niemetz

2020-03-05	Migrate a majority of the functionality in parsers to the new API (#3838)	Andrew Reynolds
	This PR migrates a majority of the functionality of the parsers (cvc, tptp, smt2/sygus) to the new API. The main omitted functionality not addressed in this PR is the datatypes. Largely, the Expr-level Datatype is still used throughout. Remaining tasks: Migrate the Datatypes to the new API in cvc/smt2. Eliminate the use of ExprManager::mkVar (with flags for DEFINED/GLOBAL). For the latter, I have made a utility function in Parser::mkVar that captures all calls to this function. Notice that the existing mkVar/mkBoundVar/mkDefinedFun have been renamed to the more fitting names bindVar/bindBoundVar/bindDefinedFun etc. Note: this PR contains no major code changes, each line of code should roughly correspond one-to-one with the changed version. This fixes CVC4/cvc4-projects#77, fixes CVC4/cvc4-projects#78, fixes CVC4/cvc4-projects#80, fixes CVC4/cvc4-projects#85.
2020-02-26	Minor improvement to ParseOp (#3808)	Andrew Reynolds

2020-02-17	Using ParseOp in TPTP (#3764)	Haniel Barbosa

2020-02-13	Update sygus v1 parser to use ParseOp utility (#3756)	Andrew Reynolds