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

Age	Commit message (Collapse)	Author
2017-03-31	Add option multi-trigger-linear, minor optimization to E-matching.	ajreynol

2017-03-30	Merge pull request #139 from 4tXJ7f/remove_throw	Clark Barrett
	[Coverity] Remove throw qualifiers in src/smt
2017-03-30	[Coverity] Remove throw qualifiers in src/smtremove_throw	Andres Notzli
	Addresses coverity issues: 1172167 1172174 1172176 1172183 1172185 1172186 1172188 1172189 1172191 1172192 1172193 1172194 1172197 1172197 1172198 1172434 1172437 1172438 1172443 1172445 1172446 1172447 1172448 1362695 1362700 1362717 1362736 1362768 1362786 1362811 1379599 1421404 1421405 1421406 1421407 1421408 1421409 1421410 1421411 1421412 1421413
2017-03-30	Minor fixes for trigger selection max.	ajreynol

2017-03-29	Add quantifiers options related to model and master equality engine.	ajreynol

2017-03-29	Merge pull request #138 from PaulMeng/master	PaulMeng
	Refactor the standard effort of relational solver
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-28	Minor refactoring sygus.	ajreynol

2017-03-28	More work on sygus. Add regress4 to Makefile.	ajreynol

2017-03-27	Fixing a bug for checking whether a node was visited.	Tim King

2017-03-27	Minor cleanups to ExtTheory.	Tim King

2017-03-27	Removing the friend class modifier from ExtTheory to Theory.	Tim King

2017-03-27	Merge pull request #137 from 4tXJ7f/throw_quals	Clark Barrett
	Remove throw qualifiers in type enumerators
2017-03-27	Making the ExtTheory object a private member of Theory.	Tim King

2017-03-27	Making ppNotifyAssertions take a const vector.	Tim King

2017-03-27	Moving the CareGraph into its own file.	Tim King

2017-03-27	Moving the theory::Assertion struct into its own file.	Tim King

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-26	Alphabetizing libcvc4_la_SOURCES.	Tim King

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

2017-03-24	Refactor model building for quantifiers to be a single pass, simplification. ↵	ajreynol
	Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.
2017-03-23	Fixing warning message.	Clark Barrett

2017-03-23	support incremental unsat cores	guykatzz

2017-03-22	Fix more cases of rewritten explanations in strings for bug 784. Minor.	ajreynol

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

2017-03-22	Work on new approach for sygus involving conditional solutions. Refactoring ↵	ajreynol
	of sygus solver. Bug fix for sygus solution reconstruction.
2017-03-21	Improve computeCareGraph functions to check shared term equality status once ↵	ajreynol
	per equivalence class pair.
2017-03-20	Merge pull request #135 from PaulMeng/master	Andrew Reynolds
	fixed cvc4 parser for set complement
2017-03-20	fixed cvc4 parser for set complement	Paul Meng

2017-03-18	Fix for bug 707.	Clark Barrett

2017-03-18	Fix to help with bug 717	Clark Barrett

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	Fixes bug 781. Copy constructor for Expr needed to set the NodeManagerScope.	Tim King

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	Merge pull request #134 from 4tXJ7f/fix_host	Clark Barrett
	Fix win-build script to use MinGW-w64 by default
2017-03-15	Allow 0 argument recursive functions. Fixes bug 782.	ajreynol

2017-03-15	Fix win-build script to use MinGW-w64 by default	Andres Notzli
	Previous changes to the win-build script left the script in an inconsistent state: the script was updated to refer to MinGW-w64 but the default host was still referring to MinGW.
2017-03-14	Merge pull request #133 from 4tXJ7f/fix_uninitialized	guykatzz
	Fix uninitialized variable
2017-03-14	fix uninitialized variable	Andres Notzli

2017-03-14	Merge pull request #132 from 4tXJ7f/fix_mingw64	Clark Barrett
	Fix MinGW-w64 build
2017-03-10	Minor fix for cbqi-all.	ajreynol

2017-03-09	bug fix	guykatzz

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

2017-03-08	Fix MinGW-w64 build	Andres Notzli
	This commit fixes configure.ac to try to get clock_gettime() from pthread. Without it, clock_gettime() is detected as missing at configuration time for MinGW-w64 but exists at compile time, which causes conflicts. Additionally, this commit updates the helper script for Windows to use MinGW-w64 by default instead of MinGW.