Age | Commit message (Expand) | Author |
2014-02-17 | type conversion | Tianyi Liang |
2014-02-14 | Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add supp... | Andrew Reynolds |
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 | Merge branch 'master' of github.com:tiliang/CVC4 | 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-11 | escaped characters, having an issue with smt-lib defintion, further repair is... | Tianyi Liang |
2014-02-10 | Fix build (some nonexistent files listed in Makefile) | Morgan Deters |
2014-02-09 | More complete guess instantiation strategy, cvc4 now typically times out inst... | Andrew Reynolds |
2014-02-06 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang |
2014-02-06 | minor cleanup for merge | Tianyi Liang |
2014-02-06 | minor fix for merge | Tianyi Liang |
2014-02-06 | minor cleanup for merge | Tianyi Liang |
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 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang |
2014-02-05 | minor fix for merge | Tianyi Liang |
2014-02-05 | minor fix for merge | Tianyi Liang |
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 | Merge branch '1.3.x' | Morgan Deters |
2014-01-27 | URL update | Morgan Deters |
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 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang |
2014-01-24 | rev diseq | Tianyi Liang |
2014-01-24 | rev const split | Tianyi Liang |