2014-11-18 |
lianah | All Minisat solve calls now return lbool (fixes bug... |
commit | commitdiff | tree |
2014-11-18 |
ajreynol | Compute model basis only for fmf. Add another co-datat... |
commit | commitdiff | tree |
2014-11-18 |
ajreynol | Add local theory extensions instantiation strategy... |
commit | commitdiff | tree |
2014-11-17 |
lianah | added command line option for extractArith bv rewrite |
commit | commitdiff | tree |
2014-11-17 |
Morgan Deters | Short-circuit in TheoryArithPrivate::check(), care... |
commit | commitdiff | tree |
2014-11-17 |
Morgan Deters | New, uniform checkTime statistic for all theories ... |
commit | commitdiff | tree |
2014-11-17 |
Liana Hadarean | Resource-limiting work. |
commit | commitdiff | tree |
2014-11-16 |
ajreynol | Add term db mode. Minor changes to quantifiers rewrite... |
commit | commitdiff | tree |
2014-11-14 |
ajreynol | Be lazier to consider EQC in UF+cardinality solver... |
commit | commitdiff | tree |
2014-11-13 |
Clark Barrett | Minor changes to AUTHORS and COPYING |
commit | commitdiff | tree |
2014-11-13 |
Morgan Deters | Minor adjustments to wording. |
commit | commitdiff | tree |
2014-11-13 |
Morgan Deters | Copyright text fixes. |
commit | commitdiff | tree |
2014-11-13 |
Morgan Deters | Merge pull request #69 from mdeters/bug594 |
commit | commitdiff | tree |
2014-11-13 |
ajreynol | Remove two obsolete versions of MBQI. |
commit | commitdiff | tree |
2014-11-13 |
ajreynol | More preparation for filtering relevant terms in TermDb. |
commit | commitdiff | tree |
2014-11-13 |
Morgan Deters | Possible fix for bug594 |
commit | commitdiff | tree |
2014-11-13 |
Morgan Deters | Merge pull request #65 from mdeters/bv-ineq-cachefix |
commit | commitdiff | tree |
2014-11-13 |
Morgan Deters | BV inequality graph TNode fix. |
commit | commitdiff | tree |
2014-11-13 |
Morgan Deters | Fix BV inequality solver caching. |
commit | commitdiff | tree |
2014-11-12 |
Morgan Deters | Fix tokenization of "reset" in SMT-LIB v2.0. It's... |
commit | commitdiff | tree |
2014-11-11 |
Morgan Deters | Minor cleanup. |
commit | commitdiff | tree |
2014-11-11 |
Kshitij Bansal | Merge pull request #64 from mdeters/theorysets-hashset... |
commit | commitdiff | tree |
2014-11-11 |
ajreynol | Work on synchronizing decision=justification and E... |
commit | commitdiff | tree |
2014-11-10 |
Tianyi Liang | Merge pull request #63 from mdeters/theorystrings-hashs... |
commit | commitdiff | tree |
2014-11-10 |
Dejan Jovanović | Bug 593 fix: if the type is finite, it is now considere... |
commit | commitdiff | tree |
2014-11-10 |
ajreynol | Do not eliminate variables only occurring in patterns... |
commit | commitdiff | tree |
2014-11-10 |
Morgan Deters | Merge branch '1.4.x' |
commit | commitdiff | tree |
2014-11-10 |
Morgan Deters | Update TheorySets to use CDHashSet<>::key_begin() ... |
commit | commitdiff | tree |
2014-11-09 |
Morgan Deters | Update TheoryStrings to use CDHashSet<>::key_begin... |
commit | commitdiff | tree |
2014-11-09 |
Morgan Deters | Work around an apparent bug in libc++ that was causing... |
commit | commitdiff | tree |
2014-11-09 |
Morgan Deters | Fix a deterministic assignment-ordering for get-assignm... |
commit | commitdiff | tree |
2014-11-09 |
Morgan Deters | Increase stack size when running regressions (fixes... |
commit | commitdiff | tree |
2014-11-09 |
ajreynol | Fix dt shared terms issue, reenable regression. |
commit | commitdiff | tree |
2014-11-08 |
ajreynol | Fix bug with incremental+datatypes. Minor cleanup... |
commit | commitdiff | tree |
2014-11-08 |
Morgan Deters | Merge pull request #62 from mdeters/bv-cleanup |
commit | commitdiff | tree |
2014-11-08 |
Morgan Deters | Remove some unused variables. |
commit | commitdiff | tree |
2014-11-08 |
Clark Barrett | Fixed bug in model builder with subtypes |
commit | commitdiff | tree |
2014-11-07 |
Morgan Deters | Remove some dead code. |
commit | commitdiff | tree |
2014-11-07 |
Morgan Deters | Fix a memory leak in SatSolverRegistry (re: bug #594). |
commit | commitdiff | tree |
2014-11-07 |
Morgan Deters | Fix memory issues in bitvector theory, which is now... |
commit | commitdiff | tree |
2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
commit | commitdiff | tree |
2014-11-07 |
Morgan Deters | Fix missing case in Boolean terms rewriting. (Resolves... |
commit | commitdiff | tree |
2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
commit | commitdiff | tree |
2014-11-07 |
Morgan Deters | Corrected fix for missing case in model postprocessor... |
commit | commitdiff | tree |
2014-11-07 |
ajreynol | Enable --quant-cf by default. Fix bug in qcf for mixed... |
commit | commitdiff | tree |
2014-11-07 |
Morgan Deters | Revert "Fix missing case in model postprocessor (resolv... |
commit | commitdiff | tree |
2014-11-07 |
Morgan Deters | Revert "Fix missing case in model postprocessor (resolv... |
commit | commitdiff | tree |
2014-11-07 |
Morgan Deters | Update competition build rules. |
commit | commitdiff | tree |
2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
commit | commitdiff | tree |
2014-11-07 |
Morgan Deters | Fix missing case in model postprocessor (resolves bug... |
commit | commitdiff | tree |
2014-11-07 |
ajreynol | Properly distinguish which EQC to assign values in... |
commit | commitdiff | tree |
2014-11-06 |
ajreynol | Minor fix for getInstCons |
commit | commitdiff | tree |
2014-11-06 |
ajreynol | Reenable regression. Add (for now, disabled) changes... |
commit | commitdiff | tree |
2014-11-05 |
ajreynol | Fix model bug in --mbqi=fmc. Minor cleanup in datatypes. |
commit | commitdiff | tree |
2014-11-05 |
Morgan Deters | Merge branch '1.4.x' |
commit | commitdiff | tree |
2014-11-05 |
Morgan Deters | Fix get-bug-attachments script. |
commit | commitdiff | tree |
2014-11-05 |
ajreynol | More work on datatypes theory combination: fix bug... |
commit | commitdiff | tree |
2014-11-02 |
Clark Barrett | Added cache to getModelValue |
commit | commitdiff | tree |
2014-11-01 |
ajreynol | Fix cegqi for synthesis without syntax. |
commit | commitdiff | tree |
2014-11-01 |
ajreynol | Simplify which lemmas to communicate in dt. |
commit | commitdiff | tree |
2014-11-01 |
ajreynol | Fix bug 592: introduce skolem for dt instantiate lemma... |
commit | commitdiff | tree |
2014-11-01 |
ajreynol | Fix some mistakes in datatypes theory combination,... |
commit | commitdiff | tree |
2014-10-31 |
ajreynol | Do not allow duplication of function definitions. ... |
commit | commitdiff | tree |
2014-10-30 |
Clark Barrett | Be more lazy about generating array lemmas |
commit | commitdiff | tree |
2014-10-30 |
Clark Barrett | Added new, much faster, care graph computation for... |
commit | commitdiff | tree |
2014-10-28 |
ajreynol | Preprocessing step for finding finite runs of well... |
commit | commitdiff | tree |
2014-10-28 |
ajreynol | Initial infrastructure for function definition quantifi... |
commit | commitdiff | tree |
2014-10-28 |
ajreynol | Improve stats in conjecture generator, minor cleanup. |
commit | commitdiff | tree |
2014-10-25 |
ajreynol | Minor fix for --user-pat=resort |
commit | commitdiff | tree |
2014-10-24 |
Morgan Deters | Fix typo. |
commit | commitdiff | tree |
2014-10-24 |
Morgan Deters | Minor parser performance fix. |
commit | commitdiff | tree |
2014-10-24 |
ajreynol | Add --user-pat=resort. Minor cleanup of options. |
commit | commitdiff | tree |
2014-10-23 |
Morgan Deters | Parsing and infrastructure support for SMT-LIBv2.5... |
commit | commitdiff | tree |
2014-10-23 |
lianah | Fixed inefficiency in bit-vector rewrite rule. |
commit | commitdiff | tree |
2014-10-22 |
Morgan Deters | Fix bug590 regression distcheck failure from last night. |
commit | commitdiff | tree |
2014-10-22 |
Tianyi Liang | Fixed bug 589 |
commit | commitdiff | tree |
2014-10-21 |
Clark Barrett | Fixed bug 590, added regression test |
commit | commitdiff | tree |
2014-10-20 |
ajreynol | Minor cleanup in datatypes. |
commit | commitdiff | tree |
2014-10-20 |
Kshitij Bansal | Merge pull request #59 from kbansal/sets3 |
commit | commitdiff | tree |
2014-10-20 |
Kshitij Bansal | Finish sets type enumerator implementation. |
commit | commitdiff | tree |
2014-10-20 |
Kshitij Bansal | fix statistic in decision engine |
commit | commitdiff | tree |
2014-10-18 |
ajreynol | Fix assertion. |
commit | commitdiff | tree |
2014-10-18 |
ajreynol | Add dt lemma: zero size implies nullary constructor. |
commit | commitdiff | tree |
2014-10-18 |
ajreynol | Fix for bounded integers when incremental, fixes bug... |
commit | commitdiff | tree |
2014-10-17 |
Morgan Deters | Merge branch '1.4.x' |
commit | commitdiff | tree |
2014-10-17 |
Morgan Deters | Remove a bad (unstable, timing-dependent) test. |
commit | commitdiff | tree |
2014-10-17 |
Tianyi Liang | Minor change for performance according to Andy's sugges... |
commit | commitdiff | tree |
2014-10-16 |
Morgan Deters | Fix clang warnings |
commit | commitdiff | tree |
2014-10-16 |
ajreynol | Make --user-pat=trust default. Fix a few warnings... |
commit | commitdiff | tree |
2014-10-16 |
Morgan Deters | Merge branch '1.4.x' |
commit | commitdiff | tree |
2014-10-16 |
Morgan Deters | Add Thomas Hunger to THANKS file (for having submitted... |
commit | commitdiff | tree |
2014-10-16 |
ajreynol | Use n-ary splits instead of binary splits in theory... |
commit | commitdiff | tree |
2014-10-16 |
ajreynol | Add dt.size to datatypes theory. Add option for fairne... |
commit | commitdiff | tree |
2014-10-14 |
lianah | fix for memory leak in BVQuickCheck |
commit | commitdiff | tree |
2014-10-14 |
Morgan Deters | Merge pull request #58 from mdeters/smt-attributes |
commit | commitdiff | tree |
2014-10-14 |
Morgan Deters | Context-dependent expr attributes are now attached... |
commit | commitdiff | tree |
2014-10-14 |
Kshitij Bansal | amend prvs commit |
commit | commitdiff | tree |
2014-10-14 |
Kshitij Bansal | trace decision-node |
commit | commitdiff | tree |
2014-10-13 |
ajreynol | CEGQI uses model. Enforce fairness in CEGQI natively. |
commit | commitdiff | tree |
2014-10-13 |
ajreynol | Model building into quantifiers engine. Simplify axiom... |
commit | commitdiff | tree |
next |