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

Age	Commit message (Collapse)	Author
2012-10-24	Includes many fixes to build system for Solaris (thanks Tim!), and also	Morgan Deters
	just in general, and some documentation adjustments.
2012-10-23	The contrib/get-antlr-3.4 script:	Tim King
	- Has no outdated reference to /usr/share/java/stringtemplate.jar (as discussed on the mailing list). - Attempts to determine if the computer is 64 or 32 bit and configure antlr appropriately. - Warns the user about it's guess. - Tells the user how to correct an incorrect guess.
2012-09-26	Fix a handful of things for Mac, and Java bindings.	Morgan Deters
	Also add a "mac-build" script that sets up prerequisites for Mac.
2012-06-13	Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow ↵	Morgan Deters
	condition when reading from stdin. This should completely resolve bug #319. However, on large inputs especially (like the stp/testcase benchmarks), this inlining feature can speed parsing by 5-10%, at the cost of not supporting interactive sessions on stdin (like in the SMT-COMP application track). So I updated the submission script and competition build so that * a competition build with antlr-inlining is built for the main and parallel tracks * a competition build without antlr-inlining is built for the application track Again, the effect is only when reading the stdin stream (but that's how SMT-COMP works). For normal (non-competition) builds, we need to support interactive sessions (from e.g. KIND) on stdin, so this inlining is off for all builds except main- and parallel-track competition builds. Also added a "get-antlr-3.4" script that automatically downloads and locally installs a copy of libantlr3c and the antlr parser generator inside the CVC4 source tree. Closing bug #319.