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

Age	Commit message (Collapse)	Author
2012-06-14	New substitutions implementation - fixes performance issue seen in nonclausal	Clark Barrett
	simplification for some benchmarks
2012-06-14	The "no-tears-in-competition-mode" commit. Change all (non-driver, ↵	Morgan Deters
	non-SAT-solver) uses of std::cout to the Message stream, and all uses of std::cerr to the Warning stream.
2012-06-12	Adding constant propagation code - needs more testing - off by default	Clark Barrett

2012-06-06	disabling a super-expensive assertions to speed up debug runs	Dejan Jovanović

2012-06-05	Fixed a performance issue with unconstrained simplifier	Clark Barrett

2012-06-04	Added preprocessing pass that propagates unconstrained values - solves all of	Clark Barrett
	the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help generally on at least BV and maybe others. Off by default for now - results are mixed and it's hard to evaluate with so many existing assertion failures and segfaults - will re-evaluate once those are fixed
2012-03-01	Partial merge from kind-backend branch, including Minisat and CNF work to	Morgan Deters
	support incrementality. Some clean-up work will likely follow, but the CNF/Minisat stuff should be left pretty much untouched. Expected performance change negligible; slightly better on memory: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5 Note that there are crashes, but that these are exhibited in the nightly regression run too!
2011-10-05	remove some debugging code that slowed down last night's regressions	Morgan Deters

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

2011-09-29	Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵	Morgan Deters
	and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
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-09-02	Partial merge of integers work; this is simple B&B and some pseudoboolean	Morgan Deters
	infrastructure, and takes care not to affect CVC4's performance on LRA benchmarks.
2011-07-05	updated preprocessing and rewriting input equalities into inequalities for LRA	Dejan Jovanović