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

Age	Commit message (Collapse)	Author
2018-09-04	Remove CVC3 compatibility layer (#2418)	Andres Noetzli

2014-06-06	Sets translate, and other short fixes	Kshitij Bansal
	- $ is a simple symbol is smt2. - ever found yourself counting in kind.h? no longer. - expose parser "logic is set" state for smt/smt2 (any better way?) - a more helpful assertion message in smt_engine
2014-06-05	Add --default-dag-thresh to translator, build translator with other examples.	Morgan Deters

2012-11-28	Adding the helloworld.cpp example.	Tim King

2012-11-27	Adding an example to show how to use arithmetic.	Tim King

2012-10-03	better documentation, allow examples to be installed, etc	Morgan Deters

2012-07-14	an example that uses bitvectors to simulate sha1 computation and dumps an ↵	Dejan Jovanović
	smt problem corresponding to the hash-inversion problem
2012-07-10	* fixing the simple_vc_cxx.cpp compile issue (no more Integer constants)	Dejan Jovanović
	* adding as examples the programs i used to translate nonlinear smt2 problems to other formats
2011-11-22	fix module name for CVC4 jar file; part of the fix for the Debian package ↵	Morgan Deters
	build failure last night
2011-11-22	More language bindings work:	Morgan Deters
	* with a patched SWIG, the ocaml bindings build correctly. ** I will provide my patch to the SWIG dev team. * fixed some class interfaces to play more nicely with SWIG. * php, perl, tcl now work; examples added. * improved binding module building and installation. Also: Stop #defining NULL ((void) 0). This has been in cvc4_public.h for a long, long time, I forget why I added it in the first place, and it's a very, very bad idea. In C++, certain things are permitted for NULL that aren't permitted for ((void) 0), like for instance implicit conversion to any pointer type. We didn't see an issue here (until now, when interfacing with SWIG), because GCC is usually pretty smart at working around such a broken #definition of NULL. But that's fragile. New exception-free Command architecture. Previously, some command invocations were wrapped in a try {} catch() {} and printed out an error. This is much more consistent now. Each Command invocation results in a CommandStatus. The status can be "unsupported", "error", or "success" (these are each derived classes, though, not strings, so that they can be easily printed in a language-specific way... e.g., in SMT-LIBv2, they are printed in a manner consistent with the spec, and "success" is not printed if the print-success option is off.) All Command functionality are now no-throw functions, which @cconway reports is a Good Thing for Google (where all C++ exceptions are suspect), and also I think is much cleaner than the old way in this instance. Added an --smtlib2 option that enables an "SMT-LIBv2 compliance mode"---really it just sets a few other options like strictParsing, inputLanguage, and printSuccess. In the future we might put other options into a compliance mode, or we might choose to make it the default.
2011-11-15	Bindings work (ocaml bindings are now sort of working); also minor cleanup	Morgan Deters

2011-11-15	fixes for python language binding, added python example	Morgan Deters

2011-09-30	forgot to put some things in the distro	Morgan Deters

2011-09-30	interfaces fixes and cleanups...and examples of each interface!	Morgan Deters