| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2012-08-07 | Some items from the CVC4 public interface review: | Morgan Deters |
| 2012-08-04 | isConst() rule for datatypes | Morgan Deters |
| 2012-08-03 | the array-store "construle" for isConst | Morgan Deters |
| 2012-08-03 | Comparisons for LogicInfos, and associated tests | Morgan Deters |
| 2012-08-03 | ArrayStoreAll infrastructure | 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 | some fixes for Mac OS | Morgan Deters |
| 2012-07-31 | fixes for portfolio | Morgan Deters |
| 2012-07-31 | Moving some instantiation-related stuff from src/theory to src/theory/quantif... | Morgan Deters |
| 2012-07-31 | fix some file documentation | Morgan Deters |
| 2012-07-31 | Options merge. This commit: | Morgan Deters |
| 2012-07-27 | Minor cleanup after today's commits: | Morgan Deters |
| 2012-07-27 | removing unecessary files | Andrew Reynolds |
| 2012-07-27 | merging fmf-devel branch, includes refactored datatype theory, updates to mod... | Andrew Reynolds |
| 2012-07-27 | Merge quantifiers2-trunk: | François Bobot |
| 2012-07-26 | Datatype enumerator work. This version is not a "fair" enumerator, but I got... | Morgan Deters |
| 2012-07-18 | small change to model-generation function, after discussion w/ Andy | Morgan Deters |
| 2012-07-18 | removing an obsolete assertion in model-generation framework, per Andy's request | Morgan Deters |
| 2012-07-17 | minor fix to prevent getValue from returning null | Andrew Reynolds |
| 2012-07-16 | found a bug in the initialization order of UF, EqualityEngine, and the UF str... | Morgan Deters |
| 2012-07-14 | Type enumerator infrastructure and uninterpreted constant support. No suppor... | Morgan Deters |
