Age | Commit message (Expand) | Author |
2014-02-14 | partial function charat | Tianyi Liang |
2014-02-13 | fix expanding def | Tianyi Liang |
2014-02-12 | bug fix for reverse check | Tianyi Liang |
2014-02-11 | lexer fix: disable smt-lib conversion for string literals | Tianyi Liang |
2014-02-11 | minor fix for recognizing the tail backslash, still have smt-lib compliance i... | Tianyi Liang |
2014-02-11 | resolve merge conflicts | Tianyi Liang |
2014-02-11 | escaped characters, having an issue with smt-lib defintion, further repair is... | Tianyi Liang |
2014-02-11 | minor fix for merge | Tianyi Liang |
2014-02-11 | minor cleanup for merge | Tianyi Liang |
2014-02-11 | minor fix for merge | Tianyi Liang |
2014-02-09 | More complete guess instantiation strategy, cvc4 now typically times out inst... | Andrew Reynolds |
2014-02-06 | Minor fix for previous commit | Morgan Deters |
2014-02-06 | Oops.. premature push on lexer fix (remove debugging output) | Morgan Deters |
2014-02-06 | Fixes for escape-handling for string literals in SMT-LIBv2 lexer | Morgan Deters |
2014-02-05 | Bug fix for theory strings related to old cycle detection code (was leading t... | Andrew Reynolds |
2014-02-04 | Do not use transitive closure module for cycle detection in datatypes (was bo... | Andrew Reynolds |
2014-02-04 | Add variable ordering for QCF to accelerate matching procedure. Preparing fo... | Andrew Reynolds |
2014-02-03 | Handle nested (universal) quantifiers in QCF algorithm. Make relevant domain... | Andrew Reynolds |
2014-01-31 | Substr fix: (= (str.substr "" 0 3) "xxx") should be SAT in the defintion of S... | Tianyi Liang |
2014-01-30 | Refactor QCF slightly. Bug fix for relevant domain (non-ground terms were ad... | Andrew Reynolds |
2014-01-30 | stats for eq/diseq splits | Tianyi Liang |
2014-01-30 | another name change | Tianyi Liang |
2014-01-30 | change string stats text names | Tianyi Liang |
2014-01-30 | adds stats | Tianyi Liang |
2014-01-29 | roll back to uf implementation for substr and charat | Tianyi Liang |
2014-01-29 | add prefixof, suffixof | Tianyi Liang |
2014-01-28 | merge internal and user of charat & substr into one | Tianyi Liang |
2014-01-28 | More optimizations of quantifier instantiation data structures. | Andrew Reynolds |
2014-01-27 | More optimization of QCF and instantiation caching. Fix CDInstMatchTrie. | Andrew Reynolds |
2014-01-26 | More optimization of QCF. Fixed InstMatchTrie for caching instantiations. U... | Andrew Reynolds |
2014-01-25 | replace charat uf with internal one | Tianyi Liang |
2014-01-24 | minor fix, indexof rewriter opt | Tianyi Liang |
2014-01-24 | fix: indexof, replace rewriting | Tianyi Liang |
2014-01-24 | rev diseq | Tianyi Liang |
2014-01-24 | rev const split | Tianyi Liang |
2014-01-24 | optimize for the reverse direction | Tianyi Liang |
2014-01-24 | Simplify the QCF algorithm by more aggressive flattening, removes EqRegistry ... | Andrew Reynolds |
2014-01-23 | fix: constants are inferred to be the same | Tianyi Liang |
2014-01-23 | minor fix | Tianyi Liang |
2014-01-22 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Tianyi Liang |
2014-01-22 | Some minor fixes to SmtEngine strings settings. | Morgan Deters |
2014-01-22 | commented out all_supported in strings for now, it has a bug here. | Tianyi Liang |
2014-01-22 | solve string exp issue for regexp | Tianyi Liang |
2014-01-22 | add warning for using strings in ALL_SUPPORTED | Tianyi Liang |
2014-01-22 | Smarter options, but still have a bug | Tianyi Liang |
2014-01-22 | Delay QuantifiersEngine and UF strong solver initialization until after final... | Morgan Deters |
2014-01-20 | improve string contains | Tianyi Liang |
2014-01-20 | improve string contains | Tianyi Liang |
2014-01-18 | Fixed non-termination issue in bounded integers. | Andrew Reynolds |
2014-01-18 | Performance optimization for E-matching, working on using QCF module for prop... | Andrew Reynolds |