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

Age	Commit message (Collapse)	Author
2017-07-10	Disable tarball signing for now.	Mathias Preiner

2017-07-06	Fix passing antlr arguments to configure in contrib/cut-release	Mathias Preiner
	Also fixes passing of makeargs.
2017-07-06	cut-release: git co -> git checkout	Aina Niemetz

2017-07-06	cut-release: option handling, get-antlr	Aina Niemetz
	+ easier-to-maintain option handling + new option for compiling release with local antlr
2014-07-02	Fix cut-release script for new configure rules.	Morgan Deters

2013-04-03	Pre-release versioning	Morgan Deters

2013-04-03	Some final minor changes before cutting 1.1.	Morgan Deters
	* update documentation * update the cut-release script * spelling/wording updates * add a (previously-failing) fuzzer regression
2013-03-19	Remove PropositionalQuery class and all CUDD-related build stuff (and ↵	Morgan Deters
	references)
2012-12-01	Cutting release 1.0.1.0	Morgan Deters

2012-12-01	fix cut-release sanity checks	Morgan Deters

2012-11-30	minor fix to release script	Morgan Deters

2012-10-08	* Models' SubstitutionMaps are now attached to the user context	Morgan Deters
	(rather than SAT context) * Enable part of CVC3 system test (resolves bug 375) * Fix infinite recursion in beta reduction code (resolves bug 417) * Some model-building assertions have been added * Other minor changes (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-06	* Clean up some options documentation	Morgan Deters
	* Remove defunct --no-theory-registration option * Point people to Wiki tutorial * Modernize the cut-release script * Misc cleanup, documentation (this commit was certified error- and warning-free by the test-and-commit script.)
2012-06-16	updated build script for smt-comp submission	Morgan Deters

2011-11-01	Improvements to header installation on user machines. Internally, we can	Morgan Deters
	still write, for example: #include "expr/node.h" but public CVC4 headers, upon installation to /usr/include/cvc4 (or wherever), have such #includes rewritten automatically to: #include <cvc4/expr/node.h>
2011-09-02	Merge from my post-smtcomp branch. Includes:	Morgan Deters
	Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.