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

Age	Commit message (Collapse)	Author
2014-04-10	Expand definitions in theory datatypes, now has the expected semantics for ↵	Andrew Reynolds
	incorrectly applied selector terms.
2014-01-28	More optimizations of quantifier instantiation data structures.	Andrew Reynolds

2014-01-10	Add new method --quant-cf for finding conflicts eagerly for quantified ↵	Andrew Reynolds
	formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup.
2013-06-24	Add options for symmetry breaking in uf+ss totality axiom approach, option ↵	Andrew Reynolds
	for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
2013-06-17	Make --var-elim-quant true by default. Add rewrite engine to quantifiers ↵	Andrew Reynolds
	module.
2013-05-22	Significant work on bounded integer quantification to handle non-trivial ↵	Andrew Reynolds
	bounds. Refactoring of InstConstantAttribute to be internal to TermDb.
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-03-06	fixed two bugs for the new E-matching implementation, added aggressive ↵	Andrew Reynolds
	miniscoping option --ag-miniscope-quant, minor cleanup
2013-02-05	More improvements for E-matching	Andrew Reynolds

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-12-01	drastic simplification of quantifiers code regarding equality queries, ↵	Andrew Reynolds
	instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine
2012-11-30	quantifiers now uses master equality engine, preparation work to cleanup code	Andrew Reynolds

2012-11-14	replaced all static member data from rewrite rule triggers, added ↵	Andrew Reynolds
	infrastructure for recognizing quantifier macros
2012-11-13	refactoring of quantifiers rewriter based on code review from yesterday, ↵	Andrew Reynolds
	refactoring code out of instantiators in preparation for quantifiers equality engine
2012-11-12	minor bug fixes for quantifiers, added sort inference module (not ready to ↵	Andrew Reynolds
	be used yet), added new totality lemma option for uf strong solver
2012-11-02	more minor updates to inst gen and representative selection, clean up of ↵	Andrew Reynolds
	equality query
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-10-01	initial draft of skolemization during pre-processing, made simple cliques ↵	Andrew Reynolds
	the default option for uf strong solver
2012-08-20	remove duplicate function TheoryEngine::getTheory(TheoryId). It was a ↵	Morgan Deters
	duplicate of TheoryEngine::theoryOf(TheoryId)
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.