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

Age	Commit message (Collapse)	Author
2014-07-01	Update copyrights.	Morgan Deters

2014-06-03	Support E-matching/QCF for Set operators.	ajreynol

2014-02-14	Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add ↵	Andrew Reynolds
	support for ITE terms. Add full-delay inst-when mode. Make strings come before quantifiers in check. Minor cleanup.
2014-01-28	More optimizations of quantifier instantiation data structures.	Andrew Reynolds

2013-05-08	Add new method for checking candidate models, --fmf-fmc. Add infrastructure ↵	Andrew Reynolds
	for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp). Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model. Add option for relational triggers such as x = f(y), --relational-trigger.
2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

2013-03-11	ite removal option for quantifiers --ite-remove-quant, e-matching for ↵	Andrew Reynolds
	boolean terms, improvement for pre skolemization
2013-02-04	Model no longer adds subterms of quantifiers to equality engine, this fixed ↵	Andrew Reynolds
	bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.
2012-11-14	replaced all static member data from rewrite rule triggers, added ↵	Andrew Reynolds
	infrastructure for recognizing quantifier macros
2012-10-23	more major cleanup of quantifiers code, separating rewrite-rules-specific ↵	Andrew Reynolds
	code from quantifiers-specific code
2012-10-11	Standardizing copyright notice. Touches ALL sources, guys, sorry.. it's	Morgan Deters
	just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-10	cleanup up some static data members in the quantifiers code	Andrew Reynolds

2012-07-31	Moving some instantiation-related stuff from src/theory to ↵	Morgan Deters
	src/theory/quantifiers and src/theory/rewriterules. This unclutters the src/theory directory somewhat. The namespaces weren't changed, only the file locations.