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

Age	Commit message (Collapse)	Author
2017-04-05	Caching for fun def process, add regression.	ajreynol

2017-03-22	Minor fix for bounded integers.	ajreynol

2017-03-15	Allow 0 argument recursive functions. Fixes bug 782.	ajreynol

2017-03-02	Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵	ajreynol
	Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
2017-02-07	Generalize finite bound inference to unifiable variables in set membership ↵	ajreynol
	literals.
2017-01-11	Fix for when variables are (partially) bound in multiple ways, add ↵	ajreynol
	regression. Improve printing for bound int module. Track when relations are enabled in sets, set incomplete if card+rels are both enabled since model construction is not guaranteed to succeed.
2017-01-04	Marking regression test files as non-executable.	Tim King

2016-12-07	Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.	ajreynol

2016-12-07	Refactoring, generalization of bounded inference module. Simplification of ↵	ajreynol
	rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
2016-12-02	Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and ↵	ajreynol
	--fmf-fun-rlv, fixes bug 723.
2016-11-17	Fix Makefiles in test	Andres Notzli
	With the recent changes to the regress tests, some of the Makefiles were not in sync anymore. This commit fixes that.
2016-10-21	Move slow regress0 benchmarks to regress1, increment regress1 through regress3.	ajreynol

2016-06-01	Initial infrastructure for bounded set quantification (disabled). ↵	ajreynol
	Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.
2016-05-23	Fix related to parametric sorts whose interpretation is finite due to ↵	ajreynol
	uninterpreted sorts + FMF. Generalizes previous fix in term registration visitor.
2016-04-11	Minor fixes for inst match generators. Updates to qip.google	ajreynol

2016-04-10	More work on instantiation propagation. Enable external filtering of ↵	ajreynol
	instantiations. All quantifiers strategies terminate when a conflict can be established.
2016-03-07	Minor change to F-Length inference in strings. No internal tracking of ↵	ajreynol
	cardinality assertions in uf. Change fullModel false array collectModelInfo to assign constants.
2016-02-23	Fix term database for non-equal, congruent terms in master equality engine. ↵	ajreynol
	Disable ITE terms in quant conflict find.
2016-02-19	Fixes and improvements for datatypes properties and splitting.	ajreynol

2016-02-18	Implement dynamic splitting for quantified formulas. Minor refactoring of ↵	ajreynol
	reductions in quantifiers engine.
2016-02-09	Fix regression, minor change to output.	ajreynol

2016-02-08	Updates related to finite model finding and (co)datatypes. Bug fix ↵	ajreynol
	enumerator and codatatype rewriter, further simplify fmc.
2016-02-01	Simplify fmc model construction, add regression. Improve FMF debug assertions.	ajreynol

2016-01-20	Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant ↵	ajreynol
	values. Add regression.
2016-01-19	Bug fixes for model construction with codatatypes, add regressions.	ajreynol

2016-01-18	Bug fix rewriter for fun defs.	ajreynol

2016-01-15	Ensure model construction for parametric sorts involving uninterpreted sorts ↵	ajreynol
	respect cardinality bounds on when finite model finding is enabled.
2015-12-22	Always split on constructor types for datatypes involving uninterpreted ↵	ajreynol
	sorts when finite model finding is enabled, add regressions.
2015-12-22	Bug fix for cbqi, do not use model values for terms involving non-enumerable ↵	ajreynol
	sorts.
2015-11-06	Changing file permissions to add or remove executable tag as appropriate.	Tim King

2015-11-04	Better combination of UF with cbqi, refactor quantifiers intialization.	ajreynol

2015-06-27	Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by ↵	ajreynol
	default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.
2015-04-27	Disambiguate namespaces in options, fix permissions	Clark Barrett

2015-04-26	Bug fixes and improvements for mbqi with theory symbols, TheoryModel ↵	ajreynol
	fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.
2015-04-23	Merge branch 'master' into google	Clark Barrett

2015-04-23	A few more minor updates to match google repository with CVC4 repository	Clark Barrett
	(mostly whitespace differences).
2015-04-23	Added option for --check-unsat-cores and various core bug fixes (merge of ↵	Liana Hadarean
	Morgan's proof branch).
2015-04-21	Fix file permissions	Clark Barrett

2014-11-07	Properly distinguish which EQC to assign values in datatypes, use ↵	ajreynol
	assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure.
2014-11-06	Reenable regression. Add (for now, disabled) changes to datatypes theory ↵	ajreynol
	combination. Relax communication of dt facts.
2014-11-05	More work on datatypes theory combination: fix bug in care graph, do not ↵	ajreynol
	assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes.
2014-04-14	Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ↵	Andrew Reynolds
	Improve datatypes rewrite, make option for previous dt semantics.
2014-04-10	Add support for cardinality constraints logic UFC. Add regressions in fmf/. ↵	Andrew Reynolds
	Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.
2014-03-07	Remove --ite-remove-quant; support pulling ground ITEs out of quantifier ↵	Morgan Deters
	bodies; fix bug 551, improper ITE removal under quantifiers.
2013-12-23	Proof-checking code; fixups of segfaults and missing functionality in proof ↵	Morgan Deters
	generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but not --check-proofs, since LFSC code uses globals) * proofs are not yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-11-11	Change exit status to be more consistent with other command-line tools: 0 ↵	Morgan Deters
	success, nonzero error
2013-10-24	Fix for bug515	Clark Barrett

2013-09-18	Support a personal build configuration and make rules.	Morgan Deters

2013-09-13	Documentation fixes, some code typo fixes, file perms, other minor things.	Morgan Deters

2013-09-09	Another minor fix for datatypes to repair my previous commit.	Andrew Reynolds