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

Age	Commit message (Collapse)	Author
2011-11-02	Only print a shortlist of most-commonly-used options on option processing ↵	Morgan Deters
	errors; reduces clutter, increases usability
2011-11-02	give an option error if the user specifies --proof in a non-proof-enabled build	Morgan Deters

2011-11-02	fully implement the always-check-again-after-the-output-channel-is-used fix ↵	Morgan Deters
	for bug #275. will finally close #275.
2011-11-02	Sometimes antlr decides to generate lexers and parsers in a different ↵	Morgan Deters
	directory than specified by "-o dir" ?! Fix that by specifying "-fo dir".
2011-11-02	better Integer asserts when there's overflow on conversion to unsigned long ↵	Morgan Deters
	/ long
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-10-31	fixes to assertions in GMP to match CLN behavior	Morgan Deters

2011-10-31	Added assertions to the CLN implementation of Integer for getLong() and ↵	Tim King
	getUnsignedLong().
2011-10-31	fix to "make install"	Morgan Deters

2011-10-29	fix some doxygen warnings	Morgan Deters

2011-10-29	fix unit tests	Morgan Deters

2011-10-29	Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, ↵	Morgan Deters
	SmtEngine::getProof(), a few other things..
2011-10-28	* ability to output NodeBuilders without first converting them to ↵	Morgan Deters
	Nodes---useful for debugging. * language-dependent Node::toString() * some minor proof-related cleanup
2011-10-28	merged the proofgen3 branch into trunk:	Liana Hadarean
	- can now output LFSC checkable resolution proofs - added configuration option --enable-proof - added command line argument --proof To turn proofs on build with proofs enabled and run with --proof.
2011-10-28	Adding a check in Polynomial::parsePolynomial to better enforce the ↵	Tim King
	arithmetic normal form when assertions are enabled.
2011-10-25	Initialize resource limit and millisecond limit options	Kshitij Bansal

2011-10-23	Implement changes from yesterday morning's meeting (10/21/2011):	Morgan Deters
	* OutputChannel::lemma() now returns an unsigned int. This facility isn't functional yet, but the signature is there. For now, it always returns the current user level (which is "correct" from the interface point of view, but not what we want). * Pseudobooleans disabled. This should fix some quantifier benchmarks Andy's been working with on the quantifiers2 branch. * --limit / --time-limit options renamed --rlimit and --tlimit. There may be slowdown from disabling pseudobooleans.
2011-10-21	some printing and parser fixes for problems recently uncovered	Morgan Deters

2011-10-21	add gcc version information to Configuration, and warn when building with ↵	Morgan Deters
	v4.5.1 which has a buggy optimizer (resolves bug #266)
2011-10-20	add support for QF_AUFLIA and QF_AUFLIRA logic strings in SMT inputs, for ↵	Morgan Deters
	testing
2011-10-19	fix bug #264: competition / other static library builds when readline isn't ↵	Morgan Deters
	available
2011-10-19	Adding support for QF_UFLIA to the smt2 parser.	Tim King

2011-10-19	Merging the branch branches/arithmetic/push-pop-support from r2247 to r2256 ↵	Tim King
	into trunk. Arithmetic should now be closer to being able to support push and pop.
2011-10-17	Sharing work	Dejan Jovanović

2011-10-13	fix make dist	Morgan Deters

2011-10-13	Interruption, time-out, and deterministic time-out ("resource-out") features.	Morgan Deters
	Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API This will need more work, but it's a start. Also implemented TheoryEngine::properPropagation(). Other minor things.
2011-10-07	Some new Datatype public functionality, as per Chris Conway's suggestions on ↵	Morgan Deters
	the dev mailing list.
2011-10-06	don't build language bindings unless expressly requested with ↵	Morgan Deters
	--enable-language-bindings
2011-10-05	Reverting a fix from earlier today that fixed a Mac OS warning but ↵	Morgan Deters
	completely broke Linux. :-(
2011-10-05	ensureLiteral() in CNF stream to support Andy's quantifiers work; an update ↵	Morgan Deters
	to model gen on booleans; and a little cleanup
2011-10-05	minor visibility fixes	Morgan Deters

2011-10-05	remove some debugging code that slowed down last night's regressions	Morgan Deters

2011-10-04	Disabling the variable removal hueristic by default.	Tim King

2011-10-04	fixes to context-dependent caching substitutions	Morgan Deters

2011-10-04	add a guard for history saving, to enable building without GNU history library	Morgan Deters

2011-10-04	compatibility, bindings	Morgan Deters

2011-10-04	cvc3 compatibility layer; and another libantlr3c v3.4 incompatibility fix	Morgan Deters

2011-10-04	compat layer cleanup	Morgan Deters

2011-10-04	oops, one more fix, hopefully the last	Morgan Deters

2011-10-04	Yet Another Antlr3 Mod---this time, all my fault: for configuration ↵	Morgan Deters
	auto-detection of libantlr3c, I chose an innocent-looking function that was present in both versions. But it's signature had changed, breaking source compatibility in both directions. Just like the other function that started the whole mess. Silly me.
2011-10-04	Oh, here's another cute compatibility fix for libantlr3c 3.4-beta4. They ↵	Morgan Deters
	#define true and false to their own ANTLR3_TRUE and ANTLR3_FALSE, wreaking havoc on our parsers. I'm really fed up with this package.
2011-10-04	mimicking Chris's recent contribution to QueryResult in CVC3 in the ↵	Morgan Deters
	compatibility layer
2011-10-04	more fixes for libantlr3c v3.4	Morgan Deters

2011-10-03	user push/pop support in minisat and simplification; also bindings work	Morgan Deters

2011-10-03	Importing Chris's recent changes to CVC3's ValidityChecker into the ↵	Morgan Deters
	compatibility layer
2011-09-30	fix to CNF undoTranslate(), to support incrementality	Morgan Deters

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

2011-09-30	more push/pop infrastructure, some SAT stuff	Morgan Deters

2011-09-30	fixes to incremental simplification, cnf routines, other stuff in ↵	Morgan Deters
	preparation of user push/pop in SAT solver
2011-09-29	compatibility work, documentation	Morgan Deters