summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2012-09-26Fix type checking for define-funs (resolves bug 398).Morgan Deters
2012-09-26The Tuesday Afternoon Catch-All Commit (TACAC):Morgan Deters
2012-09-24some api changesDejan Jovanović
2012-09-24Fix the memout issue seen in recent nightly regressions (was due to aMorgan Deters
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
2012-09-21SMT-LIBv2 compliance updates:Morgan Deters
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-09-15minor interface improvements, compliance fixesMorgan Deters
2012-09-14Fix a soundness bug reported by Matthias Weiler (had to do with expired TNodes).Morgan Deters
2012-09-14Fix a few minor issues in options processing, improving usability, consistenc...Morgan Deters
2012-09-13ensure that get-value and get-model are consistent, rewrite function value bo...Andrew Reynolds
2012-09-12Adding model assertions after SAT responses.Morgan Deters
2012-09-11Partially reverting the changes made in 4308. There is now both an Expr and N...Tim King
2012-09-10modified getValue to return Expr instead of NodeAndrew Reynolds
2012-09-06Remove SmtEngine::getStackLevel(), which exposed implementation details and w...Morgan Deters
2012-08-31merge 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-28Improved compatibility layer, now supports quantifiers. Also incorporatesMorgan Deters
2012-08-27fix a destruction-order issue that was (1) causing valgrind to complain loudl...Morgan Deters
2012-08-16The SmtEngine now ensures that setLogicInternal() is called even if there is ...Morgan Deters
2012-08-08Public interface review items:Morgan Deters
2012-08-07Fix SmtEngine::setInfo() handling for certain keys. This fixes the "unsuppor...Morgan Deters
2012-08-06Support setting :regular-output-channel and :diagnostic-output-channel.Morgan Deters
2012-08-03fix uses of getMetaKind() from outside the expr package. (they now use isCon...Morgan Deters
2012-08-01add isFinished() to type enumerators (so we don't rely on exception-throwing ...Morgan Deters
2012-08-01a couple fixes to SmtEngine::setOption(). thanks Andy for the report!Morgan Deters
2012-08-01fix for the SmtEngine::beforeSearch() option predicateMorgan Deters
2012-07-31fixes for portfolioMorgan Deters
2012-07-31fix some file documentationMorgan Deters
2012-07-31Options merge. This commit:Morgan Deters
2012-07-17SMT-LIBv2 compliance updates:Morgan Deters
2012-07-17fix for --produce-models with CVC4 presentation languageMorgan Deters
2012-07-16Support for having two SmtEngines with the same ExprManager.Morgan Deters
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-07-08minor SMT-LIBv2 compliance issuesMorgan Deters
2012-07-08Bugs resolved by this commit: #314, #322, #359, #364, #365.Morgan Deters
2012-06-18bugfix, enable only QF_LRA, not other arithKshitij Bansal
2012-06-18QF_LRA, Quantifiers: enable use decision for (only for) stopping searchKshitij Bansal
2012-06-17QF_AUFLIA: enable use decision for (only for) stopping searchKshitij Bansal
2012-06-17enabling theoryof=term for quantifiers with sharingDejan Jovanović
2012-06-17Removed assertion that can failClark Barrett
2012-06-16This is an attempt to fix the bug in the justification heuristic. TheKshitij Bansal
2012-06-16changing theoryOf in shared mode with arrays to move equalities to arraysDejan Jovanović
2012-06-16Fixing if condition for trivial equalities in arithmetic. Also some whitespac...Tim King
2012-06-15Fixes some assertion failuresClark Barrett
2012-06-15Fix for incompleteness bug with decision engine: repeated simplificationClark Barrett
2012-06-15one bug fixedKshitij Bansal
2012-06-14WIPKshitij Bansal
2012-06-14add failing regression, move error upKshitij Bansal
2012-06-14New substitutions implementation - fixes performance issue seen in nonclausalClark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback