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

Age	Commit message (Collapse)	Author
2016-11-13	Switching a large allocation to be heap allocated.	Tim King

2016-11-13	Deleting a parsed Command in the interactive_shell_black test.	Tim King

2016-11-12	Merge pull request #106 from timothy-king/cvc-parser-exception-leaks	Clark Barrett
	Adding garbage collection for the CVC Parser for Commands when except…
2016-11-12	Fixed a bug in cdhashmap in which doubly-linked list was not properly ↵	Clark Barrett
	cleaned up on a call to obliterate. Also, removed some experimental code and a unit test from cdmap_black that used it. This test created a CDList in context memory which seems like a very bad idea (and it was improperly implemented resulting in a memory leak).
2016-11-11	Adding garbage collection for the CVC Parser for Commands when exceptions ↵	Tim King
	are thrown.
2016-11-11	Merge pull request #105 from timothy-king/delete-maxed-out	Tim King
	Adding garbage collection of nodes with maxed out reference counts.
2016-11-11	Deleting successfully parsed commands in the parser_black unit test.	Tim King

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-10	Fixing a delete vs free mismatch in parser_builder_black.h.	Tim King

2016-11-10	Adding garbage collection of nodes with maxed out reference counts.	Tim King

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-07	Disabling out of memory tests unit tests when ASAN is enabled. ASAN failures ↵	Tim King
	are too hard for the unit testing framework.
2016-11-07	Changing ArrayStoreAll's constructor to delay allocation until it is done ↵	Tim King
	checking error conditions. This prevents a memory leak in exception throwing branches.
2016-11-07	Fixing a memory leak in the CnfStream unit tests.	Tim King

2016-11-04	Fix three leaks in unit tests	Andres Notzli
	The `testMultipleCollection` test case was allocating a ListenerCollection without deleting it. The helper function `countCommands` was not deleting the `Command`s returned from `InteractiveShell::readCommand`. In the `testEmptyFileInput` and `testSimpleFileInput` tests, the `filename` string was not deleted. This commit fixes all issues.
2016-11-04	Fix memory leak in node_black unit test.	Clark Barrett

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	Fix back() of empty deque in context_mm_black test	Andres Notzli
	The `testPushPop()` test case does a pop out of scope at the end that lead to UB in `ContextManager::pop()` because it did a `deque::back()` on an empty deque without checking. This commit adds an assertion in the `ContextManager` and checks that the test case triggers the assertion.
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.
2016-08-10	Improvements to strings: work on propagations for reverse normal form ↵	ajreynol
	processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring.
2016-08-09	Fixes for sep star rewrite.	ajreynol

2016-07-28	Fix bug 749.	ajreynol

2016-07-21	Fixes for strings, explanations for constant split propagations, substr ↵	ajreynol
	under concat rewrite. Avoid duplicate re.range length lemmas.
2016-07-20	Infer conflicts in strings based on abstracting equality as contains. Minor ↵	ajreynol
	cleanup.
2016-07-19	Add infrastructure for tracking instantiation lemmas (for proofs, and ↵	ajreynol
	minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.
2016-07-08	Minor fix to last commit.	ajreynol

2016-07-07	Simplifications for strings normal forms, fix case for concat reps in normal ↵	ajreynol
	forms.
2016-07-07	Ensure heap disjointness in sep refinements.	ajreynol