summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-02-17type conversionTianyi Liang
2014-02-14Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add supp...Andrew Reynolds
2014-02-14partial function charatTianyi Liang
2014-02-13fix expanding defTianyi Liang
2014-02-12bug fix for reverse checkTianyi Liang
2014-02-11lexer fix: disable smt-lib conversion for string literalsTianyi Liang
2014-02-11minor fix for recognizing the tail backslash, still have smt-lib compliance i...Tianyi Liang
2014-02-11resolve merge conflictsTianyi Liang
2014-02-11Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-02-11escaped characters, having an issue with smt-lib defintion, further repair is...Tianyi Liang
2014-02-11minor fix for mergeTianyi Liang
2014-02-11minor cleanup for mergeTianyi Liang
2014-02-11minor fix for mergeTianyi Liang
2014-02-11escaped characters, having an issue with smt-lib defintion, further repair is...Tianyi Liang
2014-02-10Fix build (some nonexistent files listed in Makefile)Morgan Deters
2014-02-09More complete guess instantiation strategy, cvc4 now typically times out inst...Andrew Reynolds
2014-02-06Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-02-06minor cleanup for mergeTianyi Liang
2014-02-06minor fix for mergeTianyi Liang
2014-02-06minor cleanup for mergeTianyi Liang
2014-02-06Minor fix for previous commitMorgan Deters
2014-02-06Oops.. premature push on lexer fix (remove debugging output)Morgan Deters
2014-02-06Fixes for escape-handling for string literals in SMT-LIBv2 lexerMorgan Deters
2014-02-05Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-02-05minor fix for mergeTianyi Liang
2014-02-05minor fix for mergeTianyi Liang
2014-02-05Bug fix for theory strings related to old cycle detection code (was leading t...Andrew Reynolds
2014-02-04Do not use transitive closure module for cycle detection in datatypes (was bo...Andrew Reynolds
2014-02-04Add variable ordering for QCF to accelerate matching procedure. Preparing fo...Andrew Reynolds
2014-02-03Handle nested (universal) quantifiers in QCF algorithm. Make relevant domain...Andrew Reynolds
2014-01-31Substr fix: (= (str.substr "" 0 3) "xxx") should be SAT in the defintion of S...Tianyi Liang
2014-01-30Refactor QCF slightly. Bug fix for relevant domain (non-ground terms were ad...Andrew Reynolds
2014-01-30stats for eq/diseq splitsTianyi Liang
2014-01-30another name changeTianyi Liang
2014-01-30change string stats text namesTianyi Liang
2014-01-30adds statsTianyi Liang
2014-01-29roll back to uf implementation for substr and charatTianyi Liang
2014-01-29add prefixof, suffixofTianyi Liang
2014-01-28merge internal and user of charat & substr into oneTianyi Liang
2014-01-28More optimizations of quantifier instantiation data structures.Andrew Reynolds
2014-01-27Merge branch '1.3.x'Morgan Deters
2014-01-27URL updateMorgan Deters
2014-01-27More optimization of QCF and instantiation caching. Fix CDInstMatchTrie.Andrew Reynolds
2014-01-26More optimization of QCF. Fixed InstMatchTrie for caching instantiations. U...Andrew Reynolds
2014-01-25replace charat uf with internal oneTianyi Liang
2014-01-24minor fix, indexof rewriter optTianyi Liang
2014-01-24fix: indexof, replace rewritingTianyi Liang
2014-01-24Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-01-24rev diseqTianyi Liang
2014-01-24rev const splitTianyi Liang
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback