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

Age	Commit message (Collapse)	Author
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	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	Fix parsing of BVROTR by CVC parser	Andres Notzli
	This commit fixes Bugzilla bug 766 as proposed by jacobly.alt@gmail.com.
2016-11-18	Merge pull request #110 from 4tXJ7f/fix_makefiles	Clark Barrett
	Fix Makefiles in test
2016-11-18	Modified a couple of regressoins to use ALL/QF_ALL instead of ↵	Clark Barrett
	ALL_SUPPORTED/QF_ALL_SUPPORTED
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-11-11	Add simple inferences for extended bitvector functions, add a few related ↵	ajreynol
	options. Use bv2nat, int2bv as triggers. Add regressions.
2016-11-08	Add a few options to separation logic and sets. Minor changes to separation ↵	ajreynol
	logic, change syntax for empty heap constraint.
2016-11-03	Add priorities to getNextDecision. Properly handle case for finite types + ↵	ajreynol
	unbounded heaps in sep logic. Fix another simple memory leak in sygus.
2016-11-02	Add missing regression.	ajreynol

2016-11-02	Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ↵	ajreynol
	Fix a few more memory leaks.
2016-10-26	Enable bv2nat regressions	ajreynol

2016-10-26	Merge pull request #98 from 4tXJ7f/fix_dist_build	Andrew Reynolds
	Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build
2016-10-26	New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵	ajreynol
	as extension of sets solver, add regressions.
2016-10-23	Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build	Andres Notzli
	This commit adds regress4 to the `test/regress/Makefile.am`.
2016-10-21	Fix/add missing makefiles.	ajreynol

2016-10-21	Move slow regress0 benchmarks to regress1, increment regress1 through regress3.	ajreynol

2016-10-13	Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.	ajreynol

2016-10-13	Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"	Tim King
	This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing changes made to 5f415d4585134612bc24e9a823289fee35541a01.
2016-10-11	Merge branch 'origin' of https://github.com/CVC4/CVC4.git	Paul Meng
	Conflicts: src/options/quantifiers_options
2016-09-28	Fix the merge of kbansal/card branch (2039eab).	Kshitij Bansal
	A bug was introduced in the cleanup process as preparation for the merge (theory_sets_private.cpp, lines 2502-2508 in this commit).
2016-09-20	More refactoring of cbqi. Add a few regressions. Add option for qcf.	ajreynol

2016-09-13	refactored the code, added more benchmarks and minor fixes	Paul Meng

2016-09-12	fixed capitalized "kind"	Paul Meng

2016-09-12	Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry ↵	ajreynol
	breaking in theory sep.
2016-09-09	Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.	ajreynol

2016-09-09	Support for separation logic + EPR. Refactor preprocessing of sep.nil, only ↵	ajreynol
	allow sep disequal card constants when type is monotonic. Update logics on sep regressions.
2016-08-30	added more benchmarks	Paul Meng

2016-08-24	Merge remote-tracking branch 'origin/master'	PaulMeng

2016-08-15	Enable bounded set membership with --fmf-bound. Map to term models for ↵	ajreynol
	bounded set membership.
2016-08-12	Add a few more regressions.	ajreynol

2016-08-12	Minor fixes to model construction to take singleton equivalence classes into ↵	ajreynol
	account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.