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

Age	Commit message (Collapse)	Author
2013-12-05	Update copyrights, add missing file-level documentation; fix perms.	Morgan Deters

2013-11-27	General pre-release cleanup commit	Morgan Deters
	* Rename {model,util_model}.{h,cpp} files to match class names * Fix alreadyVisited() issue in TheoryEngine * Remove spurious Message that causes compliance issues * Update copyrights, fix public/private markings in headers * minor comment fixes * remove EXTRACT_OP as a special-case in typechecker * note about rewriters in theoryskel readme * Clean up some compiler warnings * Code typos and spacing
2013-11-26	Bug fix for E-matching select terms, minor fix for bounded integers, bug fix ↵	Andrew Reynolds
	to improve performance of quantifiers rewriter
2013-11-10	Flatten libcvc4 build structure; remove some #include interdependences	Morgan Deters

2013-11-06	Bug fixes for bounded integer quantification. Current best strategy is to ↵	Andrew Reynolds
	turn off MBQI. Disable relevant triggers by default.
2013-10-07	Multiple fixes for datatypes theory solver: add support for parametric ↵	Andrew Reynolds
	datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup.
2013-09-30	Bug fixes and improvements for symmetry breaking, it now supports multiple ↵	Andrew Reynolds
	sorts. Working on monotonicity inference.
2013-09-27	Add new symmetry breaking technique for finite model finding. Improvements ↵	Andrew Reynolds
	to bounded integer quantifier instantiation.
2013-09-15	Change default option of simple ite lifting within quantifier bodies. add ↵	Andrew Reynolds
	some debug messages.
2013-09-13	Documentation fixes, some code typo fixes, file perms, other minor things.	Morgan Deters

2013-08-13	Minor cleanup.	Morgan Deters

2013-08-13	Minor fixes for --fmf-fmc for quantifiers containing datatypes	Andrew Reynolds

2013-08-13	initial modifications for per-ic cbqi	Andrew Reynolds

2013-07-29	Fix numerous compiler warnings on various platforms	Morgan Deters

2013-07-22	Add option --cbqi-recurse.	Andrew Reynolds

2013-07-22	Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added ↵	Andrew Reynolds
	infrastructure to BV collectModelInfo in preparation for bug fix.
2013-07-18	Fix quantifier instantiation bug in cbqi, add default priorities in rewrite ↵	Andrew Reynolds
	engine.
2013-07-09	add relevant domain computation	Andrew Reynolds

2013-07-02	Minor fixes for bounded integers, rewrite engine.	Andrew Reynolds

2013-06-28	More bug fixes for interval models.	Andrew Reynolds

2013-06-26	Add support for interval models in bounded integers MBQI (in progress).	Andrew Reynolds

2013-06-25	Refactoring of model engine to separate individual implementations of model ↵	Andrew Reynolds
	builder. Begin work on interval models for integers. 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-06-05	Fix bug in --fmf-fmc for producing models of functions not appearing in ↵	Andrew Reynolds
	quantified formulas.
2013-06-04	Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant ↵	Andrew Reynolds
	bounds for bounded integers.
2013-05-23	Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.	Andrew Reynolds

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-14	Refactoring to separate old and new model building/checking code.	Andrew Reynolds

2013-05-11	Preliminary version of finite model finding over bounded integer ↵	Andrew Reynolds
	quantification. Minor update to casc script.
2013-05-10	Add documentation for --disable-fmf-inst-gen, which removes a warning	Morgan Deters

2013-05-09	Add simplification option --fo-prop-quant. Add model support for new ↵	Andrew Reynolds
	model-checking procedure. Add run script for casc24-fnt.
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-30	Add option in quantifiers for clause splitting	Andrew Reynolds

2013-04-26	FCSimplex branch merge	Tim King

2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

2013-04-01	Merging some cleanup work:	Morgan Deters
	* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed
2013-03-30	do simple ite rewriting within quantifiers	Andrew Reynolds

2013-03-15	changed default option for quantifier instantiation	Andrew Reynolds

2013-03-14	Merge branch '1.0.x'	Morgan Deters

2013-03-14	fix to build system: #include the proper file when they are in both builds ↵	Morgan Deters
	and src
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-24	added option --model-u-dt-enum for outputting uninterpreted sorts as ↵	Andrew Reynolds
	datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts
2013-02-16	Some cleanup and copyright updating	Morgan Deters
	* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-07	Merge branch '1.0.x'	Morgan Deters
	Conflicts: src/theory/quantifiers/theory_quantifiers.cpp
2013-02-07	Only put quantifier assertions in model equality engine if fullModel==true	Morgan Deters

2013-02-07	Significant work on bug #491 (not yet closed).	Morgan Deters

2013-02-05	dos2unix conversion for a number of files; this avoids spurious conflicts ↵	Morgan Deters
	when merging to master