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

Age	Commit message (Collapse)	Author
2019-04-24	Do not use __ prefix for header guards. (#2974)	Mathias Preiner
	Fixes 2887.
2019-03-26	Update copyright headers.	Aina Niemetz

2018-09-22	cmake: Remove unused CMakeLists.txt	Mathias Preiner

2018-09-22	cmake: Added initial build infrastructure.	Aina Niemetz

2018-09-19	Decision strategy: incorporate arrays. (#2495)	Andrew Reynolds

2018-08-16	Move node algorithms to separate file (#2311)	Andres Noetzli

2018-08-15	Remove unused tuple classes (#2313)	Andres Noetzli
	Since we are using C++11, we can replace the triple and quad classes with std::tuple.
2018-06-25	Updated copyright headers.	Aina Niemetz

2018-06-04	Move assertion. (#2051)	Andrew Reynolds

2018-05-30	Fix for issue #2002 (#2012)	Andres Noetzli

2018-03-06	Make statistics output consistent. (#1647)	Mathias Preiner
	* Fixes --hide-zero-stats (and really skips the 0 values) * Removes the additional newline after each statistic * Introduces theory::getStatsPrefix(TheoryId) to generate consistent prefixes for statistics based on the theory id (e.g., THEORY_BV -> "theory::bv").
2018-03-05	Enable -Wsuggest-override by default. (#1643)	Mathias Preiner
	Adds missing override keywords.
2018-02-06	Resolving warnings from -Winconsistent-missing-override on clang. (#1563)	Tim King

2018-01-10	Removing throw specifiers for TypeRules. (#1501)	Tim King

2018-01-10	Removing throw specifiers from type enumerators. (#1502)	Tim King

2018-01-08	Removing more miscellaneous throw specifiers. (#1488)	Tim King
	Removing more miscellaneous throw specifiers.
2017-12-08	Make collect model info return a Bool (#1421)	Andrew Reynolds

2017-11-15	Adding garbage collection for Proof objects. (#1294)	Tim King

2017-10-25	Switching EqProof to use shared_ptr everywhere. (#1217)	Tim King
	This clarifies the memory ownership of EqProofs.
2017-10-11	Cleaning up ProofArray class. (#1208)	Tim King

2017-07-20	Moving from the gnu extensions for hash maps to the c++11 hash maps	Tim King
	* Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes.
2017-07-12	Make type rules more strict for operators whose type rules involve subtypes. ↵	ajreynol
	Disable support for subrange and predicate subtypes (which were only partially supported previously).
2017-07-07	Update copyright headers.	Mathias Preiner

2017-06-30	Minor change to trigger selection, fixes related to subtypes (in macros, ↵	ajreynol
	cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
2017-06-15	Fix for bug 639.	Clark Barrett

2017-04-28	Partial fix for bug 717.experiment	Clark Barrett

2017-04-21	Fix for bug 681 (now gives reasonable error message about using constant	Clark Barrett
	arrays).
2017-04-18	Fix for bug 639.	Clark Barrett

2017-04-04	Simplify Theory::collectModelInfo interface to not take deprecated fullModel ↵	ajreynol
	argument.
2017-03-27	Remove throw qualifiers in type enumerators	Andres Notzli
	This addresses Coverity issues: - 1172154 - 1172156 - 1172157 - 1172158 - 1172159 - 1379612 - 1379612 - 1421430 - 1172166 - 1172144 - 1362709 - 1362696 - 1172145 - 1172147 - 1172148 - 1379610 - 1362772 - 1362676 - 1362704 - 1362749 - 1362876 - 1362843 - 1362837 - 1362881 - 1172223 - 1172155
2017-03-18	Fix to help with bug 717	Clark Barrett

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-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.
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-09-16	In a ROW guard proof, if the transitivity proof does not have a disequality, ↵	guykatzz
	we can deduce that it is a constant-disequality proof and process it accordingly
2016-09-16	Handling a corner case where a ROW's guard is a constant disequality.	Guy
	If this is a simple proof (e.g., just 1 != 2), change the d_id from Transitivity to ConstantDisequality
2016-07-06	A few proof bugs fixed	Guy

2016-06-01	Merge from proof branch	Guy

2016-06-01	Revert "Merging proof branch"	Guy
	This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
2016-06-01	Merging proof branch	Guy

2016-04-15	Rolling back the rewrite code	Guy

2016-04-14	Remove some no-longer-required rewrites of array lemmas	Guy

2016-04-03	Updating the copyright headers and scripts.	Tim King

2016-04-03	Removed the theory-specific merge reason types. Instead, added a mechanism ↵	Guy
	for dynamically allocating these tags upon request.
2016-03-24	Refactored the equality engine in order to remove theory-specific logic from ↵	Guy
	equality path reconstruction
2016-03-23	squash-merge from proof branch	Guy

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-04	Fixed two more memory leaks in array_info.cpp	Clark Barrett

2016-02-02	Moving dump., command., model., and ite_removal. from smt_util/ to smt/. ↵	Tim King
	Breaking an edge between the sat solver and command.h.
2016-02-01	Fixing a memory leak in array info.	Tim King