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

Age	Commit message (Collapse)	Author
2012-07-27	removing unecessary files	Andrew Reynolds

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.
2010-10-04	remove/shuffle some #include dependencies; fix some documentation; apply ↵	Morgan Deters
	coding standards
2010-08-17	Merge from "cc" branch:	Morgan Deters
	CongruenceClosure implementation; CongruenceClosure white-box test. New UF theory implementation based on new CC module. This one supports predicates. The two UF implementations exist in parallel (they can be selected at runtime via the new command line option "--uf"). Added type infrastructure for TUPLE. Fixes to unit tests that failed in 16-August-2010 regressions. Needed to instantiate TheoryEngine with an Options structure, and explicitly call ->shutdown() on it before destruction (like the SMTEngine does). Fixed test makefiles to (1) perform all tests even in the presence of failures, (2) give proper summaries of subdirectory tests (e.g. regress0/uf and regress0/precedence) Other minor changes.