Age | Commit message (Expand) | Author |
2012-09-29 | This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and ... | Tim King |
2012-09-28 | rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak... | Morgan Deters |
2012-09-28 | Public interface review items: | Morgan Deters |
2012-09-26 | updates to model generation : do not modify equality engine during getValue, ... | Andrew Reynolds |
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-25 | some buggy examples for incrementality, and make bug326 run as part of make r... | 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-22 | another fix for the equality class iterator | Dejan Jovanović |
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-19 | fix for bug 370. | Dejan Jovanović |
2012-09-19 | Changing the equality engines's euivalence class iterator. Andy please check ... | Dejan Jovanović |
2012-09-17 | minor fix for models, added simple cliques option for uf strong solver | Andrew Reynolds |
2012-09-16 | store values returned by get-value in TheoryModel::d_reps if necessary, fixes... | Andrew Reynolds |
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 | added getCardinality to model | Andrew Reynolds |
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-10 | Fixed an error in the rewriter Pascal pointed out. This was in effectively de... | Tim King |
2012-09-03 | minor cleanup leftover from fmf-devel | Andrew Reynolds |
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 | * Reversing commit r4258 (which disabled failing regressions). Fixed the pro... | Morgan Deters |
2012-08-26 | Array constants finished and working. Unit tests for array constants. | Clark Barrett |
2012-08-24 | * disallow internal uses of mkVar() (you have to mkSkolem()) | Morgan Deters |
2012-08-24 | disallow assertions to inactive theories. | Morgan Deters |
2012-08-24 | fix TheoryEngine::collectModelInfo() to only call collectModelInfo() on activ... | Morgan Deters |
2012-08-24 | fix warning in arrays rewriter | Morgan Deters |
2012-08-24 | fix get-value output in a couple ways; this fixes bug #378 | Morgan Deters |
2012-08-23 | attribute stuff for Clark's array constants | Morgan Deters |
2012-08-23 | Array constant coding done except for the attributes needed | Clark Barrett |
2012-08-22 | More progress on array constants. | Clark Barrett |
2012-08-21 | add some incremental in-tree regressions | Morgan Deters |
2012-08-21 | rewriterules: fix a correction bug with --simplification=batch | François Bobot |
2012-08-20 | remove duplicate function TheoryEngine::getTheory(TheoryId). It was a duplic... | Morgan Deters |
2012-08-20 | minor cleanup | Morgan Deters |
2012-08-19 | 1. Fix for inst_match.cpp to allow compilation on fedora | Clark Barrett |
2012-08-16 | The SmtEngine now ensures that setLogicInternal() is called even if there is ... | Morgan Deters |
2012-08-16 | Replace propagateAsDecision() with Theory::getNextDecisionRequest(): | Morgan Deters |
2012-08-14 | Implements TheoryArith::collectModelInfo(). The current implementation is qu... | Tim King |
2012-08-14 | Adds substituteDelta() to DeltaRational which given a value for delta returns... | Tim King |
2012-08-14 | Switched TheoryModel assertEqualityEngine to use const Equality Engine pointers. | Tim King |
2012-08-14 | Switched a number of EqClassIterator operations to const as well as the inter... | Tim King |
2012-08-13 | Make a few functions in TheoryEngine (like theoryOf()) const. | Morgan Deters |
2012-08-13 | Minor cleanup. No performance difference expected. | Morgan Deters |