Age | Commit message (Expand) | Author |
2012-09-26 | Finish off SEXPR kind work. | Morgan Deters |
2012-09-26 | Fix type checking for define-funs (resolves bug 398). | Morgan Deters |
2012-09-26 | The Tuesday Afternoon Catch-All Commit (TACAC): | Morgan Deters |
2012-09-24 | some api changes | Dejan Jovanović |
2012-09-24 | Fix the memout issue seen in recent nightly regressions (was due to a | Morgan Deters |
2012-09-22 | Separate public-facing and internal-facing interfaces to Statistics. | Morgan Deters |
2012-09-21 | SMT-LIBv2 compliance updates: | Morgan Deters |
2012-09-19 | General subscriber infrastructure for NodeManager, as discussed in the | Morgan Deters |
2012-09-15 | minor interface improvements, compliance fixes | Morgan Deters |
2012-09-14 | Fix a soundness bug reported by Matthias Weiler (had to do with expired TNodes). | Morgan Deters |
2012-09-14 | Fix a few minor issues in options processing, improving usability, consistenc... | Morgan Deters |
2012-09-13 | ensure that get-value and get-model are consistent, rewrite function value bo... | Andrew Reynolds |
2012-09-12 | Adding model assertions after SAT responses. | Morgan Deters |
2012-09-11 | Partially reverting the changes made in 4308. There is now both an Expr and N... | Tim King |
2012-09-10 | modified getValue to return Expr instead of Node | Andrew Reynolds |
2012-09-06 | Remove SmtEngine::getStackLevel(), which exposed implementation details and w... | Morgan Deters |
2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
2012-08-29 | * Numerous documentation fixes (fix doxygen warnings, add missing documentati... | Morgan Deters |
2012-08-28 | Improved compatibility layer, now supports quantifiers. Also incorporates | Morgan Deters |
2012-08-27 | fix a destruction-order issue that was (1) causing valgrind to complain loudl... | Morgan Deters |
2012-08-16 | The SmtEngine now ensures that setLogicInternal() is called even if there is ... | Morgan Deters |
2012-08-08 | Public interface review items: | Morgan Deters |
2012-08-07 | Fix SmtEngine::setInfo() handling for certain keys. This fixes the "unsuppor... | Morgan Deters |
2012-08-06 | Support setting :regular-output-channel and :diagnostic-output-channel. | Morgan Deters |
2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use isCon... | Morgan Deters |
2012-08-01 | add isFinished() to type enumerators (so we don't rely on exception-throwing ... | Morgan Deters |
2012-08-01 | a couple fixes to SmtEngine::setOption(). thanks Andy for the report! | Morgan Deters |
2012-08-01 | fix for the SmtEngine::beforeSearch() option predicate | Morgan Deters |
2012-07-31 | fixes for portfolio | Morgan Deters |
2012-07-31 | fix some file documentation | Morgan Deters |
2012-07-31 | Options merge. This commit: | Morgan Deters |
2012-07-17 | SMT-LIBv2 compliance updates: | Morgan Deters |
2012-07-17 | fix for --produce-models with CVC4 presentation language | Morgan Deters |
2012-07-16 | Support for having two SmtEngines with the same ExprManager. | Morgan Deters |
2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
2012-07-08 | minor SMT-LIBv2 compliance issues | Morgan Deters |
2012-07-08 | Bugs resolved by this commit: #314, #322, #359, #364, #365. | Morgan Deters |
2012-06-18 | bugfix, enable only QF_LRA, not other arith | Kshitij Bansal |
2012-06-18 | QF_LRA, Quantifiers: enable use decision for (only for) stopping search | Kshitij Bansal |
2012-06-17 | QF_AUFLIA: enable use decision for (only for) stopping search | Kshitij Bansal |
2012-06-17 | enabling theoryof=term for quantifiers with sharing | Dejan Jovanović |
2012-06-17 | Removed assertion that can fail | Clark Barrett |
2012-06-16 | This is an attempt to fix the bug in the justification heuristic. The | Kshitij Bansal |
2012-06-16 | changing theoryOf in shared mode with arrays to move equalities to arrays | Dejan Jovanović |
2012-06-16 | Fixing if condition for trivial equalities in arithmetic. Also some whitespac... | Tim King |
2012-06-15 | Fixes some assertion failures | Clark Barrett |
2012-06-15 | Fix for incompleteness bug with decision engine: repeated simplification | Clark Barrett |
2012-06-15 | one bug fixed | Kshitij Bansal |
2012-06-14 | WIP | Kshitij Bansal |
2012-06-14 | add failing regression, move error up | Kshitij Bansal |