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

Age	Commit message (Collapse)	Author
2017-03-28	Refactor the standard effort of relational solver	Paul Meng

2017-03-28	Fix bug 787.	ajreynol

2017-03-28	Fix for bug 733	Clark Barrett

2017-03-24	Add some regressions. Minor.	ajreynol

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

2017-03-20	fixed cvc4 parser for set complement	Paul Meng

2017-03-17	better support for proof production when encountering bool terms: handle the ↵	guykatzz
	new proof constructs generated by the equality engine. proof production for bool-array.smt2 passes
2017-03-16	More fixes, features to examples.	ajreynol

2017-03-16	Minor fixes, always expand applications of lambdas at preprocess.	ajreynol

2017-03-16	Support for SMT LIB 2.6 syntax declare-datatype and match.	ajreynol

2017-03-16	Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for ↵	ajreynol
	mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
2017-03-15	Fix regress1 Makefile for rewriterules, fixes bug 783.	ajreynol

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

2017-03-09	better proof support for bools and formulas	guykatzz

2017-03-07	More fixes for printing/parsing sets, fix kind name.	ajreynol

2017-03-07	Fix cvc parser for set compliment.	ajreynol

2017-03-06	Support for set compliment and universe set. Simplify approach for sep.nil ↵	ajreynol
	nodes.
2017-03-03	Fix for collectModelInfo related to finite types + preregistration. ↵	ajreynol
	Generalize previous fix for sets, minor changes to Datatypes.
2017-03-03	Another minor fix for sets related to sharing + finite element types.	ajreynol

2017-03-02	Fixes related to sets.	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-30	Fix regexp cache issue in strings, add regression.	ajreynol

2017-01-18	Fix non-idempotent rewrite in Array rewriter	Andres Noetzli
	This commit fixes bug 637 ( http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=637 ) as proposed in Bugzilla and adds the minified test case to the regression tests.
2017-01-11	Merge pull request #129 from timothy-king/regression-scrubber	Clark Barrett
	Adding regression test scrubbing.
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-10	Adding regression test scrubbing.	Tim King

2017-01-05	Disabling a regression test that assumes CVC4 is configured with proofs on. ↵	Tim King
	Modifying the travis rules so there are instances with proofs disabled.
2017-01-04	Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor ↵	ajreynol
	changes.
2017-01-04	Marking regression test files as non-executable.	Tim King

2017-01-04	Reverting two files encoding with DOS linebreaks back into using unix ↵	Tim King
	linebreaks.
2016-12-16	Fix dependency tracing for fewerPreprocessingHoles	Andres Notzli
	Previously, dependency tracing in `ite_removal.cpp` was only done with the `unsatCores` option but `fewerPreprocessingHoles` requires dependencies, too. This lead to errors during proof construction when `fewerPreprocessingHoles` was active. This commit fixes the condition and includes a test case that previously failed. Additionally, it fixes a similar issue in the theory engine. NOTE: this commit might not fix all instances of this problem. `smt_engine.cpp` turns certain flags off with `unsatCores`. Compatibility between those flags and `fewerPreprocessingHoles` needs to be checked separately.
2016-12-12	Fix split-find-unsat-w-emp test	Andres Notzli
	Commit 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa did not update the split-find-unsat-w-emp test, this commit fixes that.
2016-12-08	Fix (inactive) `MultSlice` rewrite	Andres Notzli
	The `MultSlice` rewrite was previously accepting multiplications of three and more variables even though it was designed for multiplications of two variables only. Fortunately, the rewrite was not actively used in the bitvector solver. This commit strengthens the condition in `applies()` and adds a unit test that checks that x * y * z and x * y do not get rewritten to the same term.
2016-12-08	Enable remaining cardinality benchmarks	ajreynol

2016-12-07	Add missing regression	ajreynol

2016-12-07	Add sets regression, fixes bug 754. Minor fix to regexp in strings.	ajreynol

2016-12-07	Added cardinality to cvc language, fixes bug 753. Throw logic exception when ↵	ajreynol
	using cardinality on sets with finite element type.
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-07	Fix nf exp tracking for non-linear string equalities, fixes bug 768.	ajreynol

2016-12-02	Fix for bug 734	Clark Barrett

2016-12-02	Merge pull request #113 from 4tXJ7f/remove_extract_rule	Clark Barrett
	Remove wrong `ExtractMultLeadingBit` rule
2016-12-02	Bug fixes and refactoring of parametric datatypes, add some regressions.	ajreynol

2016-12-02	Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and ↵	ajreynol
	--fmf-fun-rlv, fixes bug 723.
2016-12-01	Fix quantifiers dynamic splitting module for incremental mode, fixes bug 765 ↵	ajreynol
	and 763.
2016-12-01	Improvement and bug fix for str.indexof reduction, add regression. Other ↵	ajreynol
	minor changes.
2016-11-30	Remove wrong `ExtractMultLeadingBit` rule	Andres Notzli
	The rule `ExtractMultLeadingBit` estimated the number of leading zeros wrong: when there were ones in the leading constant parts of the factors, it was using the length of the non-zero part instead of the length of the zero part. This commit includes an example for which the previous version of the rule would cause a wrong answer.
2016-11-30	Merge pull request #115 from 4tXJ7f/bug766	Clark Barrett
	Fix parsing of BVROTR by CVC parser
2016-11-30	Fix parsing of BVROTR by CVC parser	Andres Notzli
	This commit fixes Bugzilla bug 766 as proposed by jacobly.alt@gmail.com.