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

Age	Commit message (Collapse)	Author
2021-05-26	Add more examples to the documentation (#6569)	Gereon Kremer
	This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details: - for consistency, all cpp examples are moved from examples/api to examples/api/cpp - add capabilities for SMT-LIB examples, and two simple smt2 examples - more docs/examples/*.rst files - two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)
2021-04-20	Remove support for CVC3 language. (#6369)	Aina Niemetz

2021-04-12	Refactor and update copyright headers. (#6316)	Aina Niemetz

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-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2020-12-02	Update copyright headers.	Aina Niemetz

2020-11-20	Updates to API in preparation for using symbol manager for model (#5481)	Andrew Reynolds
	printModel no longer makes sense if the list of declared symbols is managed outside the solver. Also, mkConst needs a variant to distinguish a provided name of "" vs. a name that is not provided.
2020-10-29	Add mkInteger to the API (#5274)	mudathirmahgoub
	This PR adds mkInteger to the API and update mkReal to ensure that the returned term has real sort. The parsers are modified to parse numbers like "0" "5" as integers and "0.0" and "15.0" as reals. This means subtyping is effectively eliminated from all theories except arithmetic. Other changes: Term::isValue is removed which was introduced to support parsing for constant arrays. It is no longer needed after this PR. Benchmarks are updated to match the changes in the parsers Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
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-23	New C++ API: Remove examples for old API. (#4650)	Aina Niemetz
	This removes obsolete examples for the old API in preparation of making the old API private. Examples for the new API are renamed from -new.cpp to .cpp.
2020-06-16	Update copyright headers.	Aina Niemetz

2020-04-15	Change option names --default-dag-thresh and --default-expr-depth (#4309)	Andrew Reynolds

2020-03-31	Rename checkValid/query to checkEntailed. (#4191)	Aina Niemetz
	This renames api::Solver::checkValidAssuming to checkEntailed and removes api::Solver::checkValid. Internally, SmtEngine::query is renamed to SmtEngine::checkEntailed, and these changes are further propagated to the Result class.
2019-09-25	Use separate CMake project for CVC4 examples. (#3196)	Mathias Preiner

2019-03-26	Update copyright headers.	Aina Niemetz

2018-06-25	Updated copyright headers.	Aina Niemetz

2017-07-07	Update copyright headers.	Mathias Preiner

2017-01-11	Proposed fix for bug 702. Checks to make sure the Expr's operator is not of ↵	makaimann
	kind BUILTIN before passing to prefixPrintGetValue()
2016-04-20	update from the master	PaulMeng

2014-12-09	Cleanup.	Morgan Deters

2014-07-01	Update copyrights.	Morgan Deters

2013-11-27	Incremental is now on by default when using from API, off for command-line ↵	Morgan Deters
	driver except in interactive mode.
2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

2012-12-01	Polishing API examples.	Tim King

2012-11-30	all API examples now have java versions too; bitvectors gets built; also ↵	Morgan Deters
	updated old-style copyrights in the examples
2012-11-30	Updating the combination.cpp example.	Tim King

2012-11-30	Changes to SExpr to accept autoconversion from bool and const char*. Adding ↵	Tim King
	an example for combination.