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

Age	Commit message (Collapse)	Author
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-18	Merge pull request #128 from 4tXJ7f/fix_lfsc_perf	Andrew Reynolds
	[LFSC] Fix performance issues, more determinism
2017-01-18	Minor fix in relations.	ajreynol

2017-01-16	[LFSC] Fix performance issues, more determinism	Andres Notzli
	For certain proofs, the performance was drastically different on different OSes. The cause for this difference was a pointer comparison in the deduplication in `Expr::defeq()`. Depending on how the OS allocated the memory, an expression `a` would get replaced with an equivalent expression `b` or vice versa, which in turn affected performance of `Expr::free_in()` dramatically (sub-second vs. >5 min running times). This commit makes the process more deterministic by using a heuristic that favors symbolic expressions and greedily tries to make small refcounts smaller when replacing, and changes `Expr::free_in()` to not repeatedly explore the same subexpressions.
2017-01-13	Fix call to SExpr constructor for greater portability.	Clark Barrett

2017-01-13	Merge pull request #130 from chadbrewbaker/master	Clark Barrett
	Fixing memory leak
2017-01-13	Do not rewrite explanations in strings.	ajreynol

2017-01-11	Merge pull request #129 from timothy-king/regression-scrubber	Clark Barrett
	Adding regression test scrubbing.
2017-01-11	Merge pull request #131 from makaimann/fix_702	Clark Barrett
	Proposed fix for bug 702
2017-01-11	Proposed fix for bug 702. Checks to make sure the Expr's operator is not of ↵	makaimann
	kind BUILTIN before passing to prefixPrintGetValue()
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-11	Merge pull request #127 from cristian-mattarei/issue_679	Clark Barrett
	Bug 679 fix
2017-01-10	revert	Chad Brewbaker

2017-01-10	Quashing memory leak	Chad Brewbaker

2017-01-10	Adding regression test scrubbing.	Tim King

2017-01-08	With reference to Bug 679, this commit integrates part of the patch ↵	Cristian Mattarei
	proposed, and it fixes the correct float parsing of an std::istringstream. The compilation issue in Bug 679 does not apply anymore with gcc6.3.1
2017-01-06	quashing debug memory leak	Chad Brewbaker

2017-01-06	Minor fix for sets.	ajreynol

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	Marking the proof signature files as non-executable.	Tim King

2017-01-04	Setting the executable bit for the newer run scripts in contrib.	Tim King

2017-01-04	Reverting two files encoding with DOS linebreaks back into using unix ↵	Tim King
	linebreaks.
2017-01-04	Merge pull request #122 from 4tXJ7f/fix_lfsc_str	Andrew Reynolds
	[LFSC] Minor fixes/improvements
2017-01-04	Merge pull request #120 from 4tXJ7f/fix_f_pp_holes	guykatzz
	Fix dependency tracing for fewerPreprocessingHoles
2017-01-04	Merge pull request #121 from 4tXJ7f/fix_lfsc_mem_leaks	Andrew Reynolds
	[LFSC] Fix memory leaks when creating CExprs
2016-12-29	Changing a set of TNodes to a set of Nodes in the BV inequality solver. The ↵	Tim King
	ref count of the TNodes in the set can become 0. Set operations containing garbage collected TNodes could then fail.
2016-12-29	Eliminating a signed vs. unsigned comparison.	Tim King

2016-12-29	Changing getTearDownIncremental() to return the type of ↵	Tim King
	options::tearDownIncremental.
2016-12-29	Adding a destructor to InstantiationNotify.	Tim King

2016-12-29	Adding a destructor to RepBoundExt.	Tim King

2016-12-29	Reordering sep and sets in Makefile.theories.	Tim King

2016-12-28	[LFSC] Minor fixes/improvements	Andres Notzli
	- Avoid mixing new/delete with malloc/free - Remove reimplementation of strcmp - Add assertions
2016-12-28	[LFSC] Fix memory leaks when creating CExprsfix_lfsc_mem_leaks	Andres Notzli
	In certain cases, LFSC was creating CExprs with the single-argument constructor, which allocates an array of one child, only to immediately replace it with a new array (without deleting the old one). Additionally, this commit fixes the construction of TYPE/KIND/MPZ/MPQ expressions (the null pointer is appended automatically by the single argument constructor, an array with two null pointer entries should not be necessary).
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-14	Merge pull request #119 from 4tXJ7f/smt_v2_5	Clark Barrett
	Switch from SMT-LIB v2.0 to v2.5 for smt2 files
2016-12-14	Switch from SMT-LIB v2.0 to v2.5 for smt2 files	Andres Notzli
	As mentioned in bug 741, CVC4 was parsing `.smt2` files using the SMT-LIB v2.0 standard by default. This commit switches to v2.5.
2016-12-14	Made tear-down-incremental more like it used to be: when tear-down value	Clark Barrett
	is 1, it does not automatically enable incremental mode.
2016-12-13	Merge pull request #118 from 4tXJ7f/fix_emp	Andrew Reynolds
	Fix split-find-unsat-w-emp test
2016-12-12	Merge pull request #117 from 4tXJ7f/fix_order	Clark Barrett
	Fix initialization order
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-11	Merge branch 'master' into fix_order	Clark Barrett

2016-12-11	Merge pull request #116 from 4tXJ7f/fix_mult	Clark Barrett
	Fix (inactive) `MultSlice` rewrite
2016-12-09	Fixing a use after free bug in Polynomial::denominatorLCM.	Tim King

2016-12-08	Fix initialization order	Andres Notzli
	This commit addresses the following warning: ``` warning: field 'd_negOne' will be initialized after field 'd_pivots' [-Wreorder] ```
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