Age | Commit message (Expand) | Author |
2014-12-06 | Added C++/Java api examples; | Tianyi Liang |
2014-12-06 | Fix dt.size care graph. | ajreynol |
2014-12-04 | Relaxed the constant requirement for regular expression loop; | Tianyi Liang |
2014-12-04 | clean up and improve intersection | Tianyi Liang |
2014-12-03 | Floating point infrastructure. | Martin Brain |
2014-12-03 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Kshitij Bansal |
2014-12-03 | Revert "Disable constants sharing in eq engine, disable hack in theory engine." | Kshitij Bansal |
2014-12-02 | disable inter cache | Tianyi Liang |
2014-11-28 | Synchronize conjecture generation with E-matching. Minor fix to --full-satur... | ajreynol |
2014-11-26 | add intersection rewriting | Tianyi Liang |
2014-11-26 | add more regexp rewriting | Tianyi Liang |
2014-11-26 | add more functions for regular expressions | Tianyi Liang |
2014-11-25 | Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos... | ajreynol |
2014-11-21 | Throw error when pattern is not list of terms. | ajreynol |
2014-11-21 | Change default option to --inst-when=full-last-call (interleave instantiation... | ajreynol |
2014-11-20 | Disable constants sharing in eq engine, disable hack in theory engine. Chang... | ajreynol |
2014-11-19 | Making construction of trigger sets not use the global engine state. | Dejan Jovanović |
2014-11-18 | Merge pull request #70 from kbansal/sets-for-merge-squashed | Kshitij Bansal |
2014-11-18 | Set Constant's normal form and other short fixes | Kshitij Bansal |
2014-11-18 | clear model cache in BVQuickCheck clearSolver() (fixes bug 587) | Liana Hadarean |
2014-11-18 | Compute model basis only for fmf. Add another co-datatype regression. | ajreynol |
2014-11-18 | Add local theory extensions instantiation strategy (incomplete). Refactor ho... | ajreynol |
2014-11-17 | added command line option for extractArith bv rewrite | lianah |
2014-11-17 | Short-circuit in TheoryArithPrivate::check(), care of Tim. | Morgan Deters |
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 |