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

Age	Commit message (Collapse)	Author
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.
2017-03-07	More fixes for printing/parsing sets, fix kind name.	ajreynol

2017-03-07	Fix cvc parser for set compliment.	ajreynol

2017-03-06	Do not eagerly construct explanations in relation solver.	ajreynol

2017-03-06	Support for set compliment and universe set. Simplify approach for sep.nil ↵	ajreynol
	nodes.
2017-03-06	Adding support for bool-to-bv	Clark Barrett
	Squashed commit of the following: commit 5197a663eb262afbeb7740f53b5bd27479dccea0 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Mar 6 00:16:16 2017 -0800 Remove IFF case commit 2119b25a30ed42eca54f632e7232c9f76ae5755a Author: guykatzz <katz911@gmail.com> Date: Mon Feb 20 12:37:06 2017 -0800 proof support for bvcomp commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 21:09:04 2017 -0800 Added missing cases to operator<< for bv rewrite rules. commit 0ed797c31d0e66cadc35b2397716c841d1aff270 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 11:43:51 2017 -0800 Added rewrite rules for new bitvector kinds. commit 3b23dffb317de5559f8a95118fef633f711c114a Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Feb 13 14:41:49 2017 -0800 First draft of bool-to-bv pass.
2017-03-03	Fix for collectModelInfo related to finite types + preregistration. ↵	ajreynol
	Generalize previous fix for sets, minor changes to Datatypes.
2017-03-03	Another minor fix for sets related to sharing + finite element types.	ajreynol

2017-03-02	Fixes related to sets.	ajreynol

2017-03-02	Minor cleanup and reorganization related to last commit.	ajreynol

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-02-16	Minor fixes for relations, quantifiers dsplit.	ajreynol

2017-02-16	Fixes for sets+rels check. Minor.	ajreynol

2017-02-15	Minimization modes for fmf bound.	ajreynol

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.