Age | Commit message (Expand) | Author |
2014-11-17 | New, uniform checkTime statistic for all theories (as discussed in meeting). | Morgan Deters |
2014-11-17 | Resource-limiting work. | Liana Hadarean |
2014-11-16 | Add term db mode. Minor changes to quantifiers rewriter: split ITE's where e... | ajreynol |
2014-11-14 | Be lazier to consider EQC in UF+cardinality solver. Minor cleanup. | ajreynol |
2014-11-13 | Remove two obsolete versions of MBQI. | ajreynol |
2014-11-13 | More preparation for filtering relevant terms in TermDb. | ajreynol |
2014-11-12 | BV inequality graph TNode fix. | Morgan Deters |
2014-11-12 | Fix BV inequality solver caching. | Morgan Deters |
2014-11-11 | Merge pull request #64 from mdeters/theorysets-hashset-iteration | Kshitij Bansal |
2014-11-11 | Work on synchronizing decision=justification and E-matching. | ajreynol |
2014-11-10 | Merge pull request #63 from mdeters/theorystrings-hashset-iteration | Tianyi Liang |
2014-11-10 | Bug 593 fix: if the type is finite, it is now considered for detecting theori... | Dejan Jovanović |
2014-11-10 | Do not eliminate variables only occurring in patterns. Minor improvements to... | ajreynol |
2014-11-09 | Update TheorySets to use CDHashSet<>::key_begin() / key_end(). | Morgan Deters |
2014-11-09 | Update TheoryStrings to use CDHashSet<>::key_begin() / key_end(). | Morgan Deters |
2014-11-09 | Fix dt shared terms issue, reenable regression. | ajreynol |
2014-11-08 | Fix bug with incremental+datatypes. Minor cleanup. Disable regression bug48... | ajreynol |
2014-11-07 | Remove some unused variables. | Morgan Deters |
2014-11-07 | Fixed bug in model builder with subtypes | Clark Barrett |
2014-11-07 | Fix memory issues in bitvector theory, which is now valgrind-clean (mostly re... | Morgan Deters |
2014-11-07 | Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor impr... | ajreynol |
2014-11-07 | Properly distinguish which EQC to assign values in datatypes, use assertRepre... | ajreynol |
2014-11-06 | Minor fix for getInstCons | ajreynol |
2014-11-06 | Reenable regression. Add (for now, disabled) changes to datatypes theory com... | ajreynol |
2014-11-05 | Fix model bug in --mbqi=fmc. Minor cleanup in datatypes. | ajreynol |
2014-11-05 | More work on datatypes theory combination: fix bug in care graph, do not assi... | ajreynol |
2014-11-01 | Added cache to getModelValue | Clark Barrett |
2014-11-01 | Fix cegqi for synthesis without syntax. | ajreynol |
2014-11-01 | Simplify which lemmas to communicate in dt. | ajreynol |
2014-11-01 | Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in lemma... | ajreynol |
2014-11-01 | Fix some mistakes in datatypes theory combination, disable two regressions. ... | ajreynol |
2014-10-31 | Do not allow duplication of function definitions. Set incomplete flag in mod... | ajreynol |
2014-10-30 | Be more lazy about generating array lemmas | Clark Barrett |
2014-10-29 | Added new, much faster, care graph computation for arrays | Clark Barrett |
2014-10-28 | Preprocessing step for finding finite runs of well-defined function definitio... | ajreynol |
2014-10-28 | Initial infrastructure for function definition quantifiers, internal parsing ... | ajreynol |
2014-10-28 | Improve stats in conjecture generator, minor cleanup. | ajreynol |
2014-10-25 | Minor fix for --user-pat=resort | ajreynol |
2014-10-24 | Fix typo. | Morgan Deters |
2014-10-24 | Add --user-pat=resort. Minor cleanup of options. | ajreynol |
2014-10-23 | Fixed inefficiency in bit-vector rewrite rule. | lianah |
2014-10-21 | Fixed bug 589 | Tianyi Liang |
2014-10-21 | Fixed bug 590, added regression test | Clark Barrett |
2014-10-20 | Minor cleanup in datatypes. | ajreynol |
2014-10-19 | Finish sets type enumerator implementation. | Kshitij Bansal |
2014-10-18 | Fix assertion. | ajreynol |
2014-10-18 | Add dt lemma: zero size implies nullary constructor. | ajreynol |
2014-10-18 | Fix for bounded integers when incremental, fixes bug 588. Add option --dt-bi... | ajreynol |
2014-10-17 | Minor change for performance according to Andy's suggestion. | Tianyi Liang |
2014-10-16 | Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ch... | ajreynol |