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

Age	Commit message (Collapse)	Author
2011-10-17	Sharing work	Dejan Jovanović

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-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.
2011-07-11	Clark's work on array theory - can now solve all QF_AX problems	Clark Barrett

2011-07-09	surprize surprize	Dejan Jovanović

2011-07-05	updated preprocessing and rewriting input equalities into inequalities for LRA	Dejan Jovanović

2011-05-05	Merge from nonclausal-simplification-v2 branch:	Morgan Deters
	* Preprocessing-time, non-clausal, Boolean simplification round to support "quasi-non-linear rewrites" as discussed at last few meetings. * --simplification=none is the default for now, but we'll probably change that to --simplification=incremental. --simplification=batch is also a possibility. See --simplification=help for details. * RecursionBreaker<T> now uses a hash set for the seen trail. * Fixes to TLS stuff to support that. * Fixes to theory and SmtEngine documentation. * Fixes to stream indentation. * Other miscellaneous stuff.
2011-04-07	Made Valuation::getValue() and Valuation::getSatValue() const.	Tim King

2011-03-31	Fixes to Valuation.	Tim King

2011-03-30	Add Valuation::getSatValue() so that theories can access the current	Morgan Deters
	(propositional) assignment for theory atoms. Fixed Debug/Trace as discussed in bug ticket #252 and on the mailing list. This implementation leads to some compiler warnings in production builds, but these will be corrected in coming days. There appears to be a small speedup in the parser as a result of this fix: http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1902&reference_id=1886&p=5 Cleaned up a few CD Boolean attribute things. Various small fixes to coding guidelines / test coverage. This commit: * Resolves bug 252 (tracing not disabled in production builds) * Resolves bug 254 (implement CDAttrHash<>::BitIterator::find())
2011-02-26	Merge from theory-break-dependences branch to break Theory and TheoryEngine ↵	Morgan Deters
	dependences; now, if you touch theory_engine.h, only a few things in theory need be recompiled (TheoryEngine, SharedTermManager, .... but no theory implementations), along with the PropEngine and SmtEngine. If you touch a specific theory's .h file, only that theory must be recompiled (along with the TheoryEngine, since it uses traits, and SmtEngine, since it tells the TheoryEngine which theory implementations to use).