| 2014-02-21 |
Morgan Deters | Fix makefile dependence for system tests. |
commit | commitdiff | tree |
| 2014-02-21 |
Kshitij Bansal | disable test cvc3_main, attempt to fix dist_check |
commit | commitdiff | tree |
| 2014-02-21 |
Kshitij Bansal | Merge pull request #10 from kbansal/sets-for-merge |
commit | commitdiff | tree |
| 2014-02-21 |
Kshitij Bansal | option to print stats after every satisfiability or... |
commit | commitdiff | tree |
| 2014-02-21 |
Kshitij Bansal | add new theory (sets) |
commit | commitdiff | tree |
| 2014-02-21 |
Kshitij Bansal | fix a -Wunused |
commit | commitdiff | tree |
| 2014-02-21 |
Tianyi Liang | fix makefile |
commit | commitdiff | tree |
| 2014-02-21 |
Tianyi Liang | add more tests, and define int.to.str(NEGATIVE)="" |
commit | commitdiff | tree |
| 2014-02-20 |
Tianyi Liang | add two cases to the regression test |
commit | commitdiff | tree |
| 2014-02-20 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-02-20 |
Tianyi Liang | hot fix for str2int/int2str |
commit | commitdiff | tree |
| 2014-02-20 |
Tianyi Liang | add negative int2str |
commit | commitdiff | tree |
| 2014-02-20 |
Morgan Deters | String parsing example in CVC parser |
commit | commitdiff | tree |
| 2014-02-20 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-02-20 |
Tianyi Liang | hot fix for str2int/int2str |
commit | commitdiff | tree |
| 2014-02-20 |
Tianyi Liang | add negative int2str |
commit | commitdiff | tree |
| 2014-02-20 |
Morgan Deters | String parsing example in CVC parser |
commit | commitdiff | tree |
| 2014-02-20 |
Andrew Reynolds | Fix ite and iff handling in QCF. Add option for heuris... |
commit | commitdiff | tree |
| 2014-02-20 |
Kshitij Bansal | portfolio: add stat to track time spent waiting for... |
commit | commitdiff | tree |
| 2014-02-19 |
Tim King | Merge branch 'master' of github.com:CVC4/CVC4 |
commit | commitdiff | tree |
| 2014-02-19 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-02-19 |
Tim King | Merge branch '1.3.x' |
commit | commitdiff | tree |
| 2014-02-19 |
Tim King | Stopping non-linear terms from entering the dio solver... |
commit | commitdiff | tree |
| 2014-02-19 |
Tianyi Liang | add negative int2str |
commit | commitdiff | tree |
| 2014-02-19 |
Morgan Deters | String parsing example in CVC parser |
commit | commitdiff | tree |
| 2014-02-18 |
Tianyi Liang | missed files for the latter commit |
commit | commitdiff | tree |
| 2014-02-18 |
Tianyi Liang | str.to.int(INVALID) = -1 |
commit | commitdiff | tree |
| 2014-02-18 |
Tianyi Liang | switch to total function str.to.int: maps invalid and... |
commit | commitdiff | tree |
| 2014-02-18 |
Tianyi Liang | bring back the commits which is lost accidentally. |
commit | commitdiff | tree |
| 2014-02-18 |
Tianyi Liang | add str2int |
commit | commitdiff | tree |
| 2014-02-17 |
Morgan Deters | Fix for strings-exp: enable quantifiers |
commit | commitdiff | tree |
| 2014-02-17 |
Morgan Deters | Fix strings preprocessing for justification heuristic |
commit | commitdiff | tree |
| 2014-02-17 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-02-17 |
Tianyi Liang | type conversion |
commit | commitdiff | tree |
| 2014-02-17 |
Tianyi Liang | type conversion |
commit | commitdiff | tree |
| 2014-02-14 |
Andrew Reynolds | Make QCF more incremental. Fix bug in QCF handling... |
commit | commitdiff | tree |
| 2014-02-14 |
Tianyi Liang | partial function charat |
commit | commitdiff | tree |
| 2014-02-14 |
Tianyi Liang | fix expanding def |
commit | commitdiff | tree |
| 2014-02-12 |
Tianyi Liang | bug fix for reverse check |
commit | commitdiff | tree |
| 2014-02-12 |
Tianyi Liang | lexer fix: disable smt-lib conversion for string literals |
commit | commitdiff | tree |
| 2014-02-12 |
Tianyi Liang | minor fix for recognizing the tail backslash, still... |
commit | commitdiff | tree |
| 2014-02-11 |
Tianyi Liang | resolve merge conflicts |
commit | commitdiff | tree |
| 2014-02-11 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-02-11 |
Tianyi Liang | escaped characters, having an issue with smt-lib defint... |
commit | commitdiff | tree |
| 2014-02-11 |
Tianyi Liang | minor fix for merge |
commit | commitdiff | tree |
| 2014-02-11 |
Tianyi Liang | minor cleanup for merge |
commit | commitdiff | tree |
| 2014-02-11 |
Tianyi Liang | minor fix for merge |
commit | commitdiff | tree |
| 2014-02-11 |
Tianyi Liang | escaped characters, having an issue with smt-lib defint... |
commit | commitdiff | tree |
| 2014-02-11 |
Morgan Deters | Fix build (some nonexistent files listed in Makefile) |
commit | commitdiff | tree |
| 2014-02-09 |
Andrew Reynolds | More complete guess instantiation strategy, cvc4 now... |
commit | commitdiff | tree |
| 2014-02-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-02-06 |
Tianyi Liang | minor cleanup for merge |
commit | commitdiff | tree |
| 2014-02-06 |
Tianyi Liang | minor fix for merge |
commit | commitdiff | tree |
| 2014-02-06 |
Tianyi Liang | minor cleanup for merge |
commit | commitdiff | tree |
| 2014-02-06 |
Morgan Deters | Minor fix for previous commit |
commit | commitdiff | tree |
| 2014-02-06 |
Morgan Deters | Oops.. premature push on lexer fix (remove debugging... |
commit | commitdiff | tree |
| 2014-02-06 |
Morgan Deters | Fixes for escape-handling for string literals in SMT... |
commit | commitdiff | tree |
| 2014-02-05 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-02-05 |
Tianyi Liang | minor fix for merge |
commit | commitdiff | tree |
| 2014-02-05 |
Tianyi Liang | minor fix for merge |
commit | commitdiff | tree |
| 2014-02-05 |
Andrew Reynolds | Bug fix for theory strings related to old cycle detecti... |
commit | commitdiff | tree |
| 2014-02-04 |
Andrew Reynolds | Do not use transitive closure module for cycle detectio... |
commit | commitdiff | tree |
| 2014-02-04 |
Andrew Reynolds | Add variable ordering for QCF to accelerate matching... |
commit | commitdiff | tree |
| 2014-02-03 |
Andrew Reynolds | Handle nested (universal) quantifiers in QCF algorithm... |
commit | commitdiff | tree |
| 2014-01-31 |
Tianyi Liang | Substr fix: (= (str.substr "" 0 3) "xxx") should be... |
commit | commitdiff | tree |
| 2014-01-30 |
Andrew Reynolds | Refactor QCF slightly. Bug fix for relevant domain... |
commit | commitdiff | tree |
| 2014-01-30 |
Tianyi Liang | stats for eq/diseq splits |
commit | commitdiff | tree |
| 2014-01-30 |
Tianyi Liang | another name change |
commit | commitdiff | tree |
| 2014-01-30 |
Tianyi Liang | change string stats text names |
commit | commitdiff | tree |
| 2014-01-30 |
Tianyi Liang | adds stats |
commit | commitdiff | tree |
| 2014-01-29 |
Tianyi Liang | roll back to uf implementation for substr and charat |
commit | commitdiff | tree |
| 2014-01-29 |
Tianyi Liang | add prefixof, suffixof |
commit | commitdiff | tree |
| 2014-01-28 |
Tianyi Liang | merge internal and user of charat & substr into one |
commit | commitdiff | tree |
| 2014-01-28 |
Andrew Reynolds | More optimizations of quantifier instantiation data... |
commit | commitdiff | tree |
| 2014-01-27 |
Morgan Deters | Merge branch '1.3.x' |
commit | commitdiff | tree |
| 2014-01-27 |
Morgan Deters | URL update |
commit | commitdiff | tree |
| 2014-01-27 |
Andrew Reynolds | More optimization of QCF and instantiation caching... |
commit | commitdiff | tree |
| 2014-01-26 |
Andrew Reynolds | More optimization of QCF. Fixed InstMatchTrie for... |
commit | commitdiff | tree |
| 2014-01-25 |
Tianyi Liang | replace charat uf with internal one |
commit | commitdiff | tree |
| 2014-01-25 |
Tianyi Liang | minor fix, indexof rewriter opt |
commit | commitdiff | tree |
| 2014-01-24 |
Tianyi Liang | fix: indexof, replace rewriting |
commit | commitdiff | tree |
| 2014-01-24 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-01-24 |
Tianyi Liang | rev diseq |
commit | commitdiff | tree |
| 2014-01-24 |
Tianyi Liang | rev const split |
commit | commitdiff | tree |
| 2014-01-24 |
Tianyi Liang | optimize for the reverse direction |
commit | commitdiff | tree |
| 2014-01-24 |
Tianyi Liang | rev diseq |
commit | commitdiff | tree |
| 2014-01-24 |
Tianyi Liang | rev const split |
commit | commitdiff | tree |
| 2014-01-24 |
Andrew Reynolds | Simplify the QCF algorithm by more aggressive flattenin... |
commit | commitdiff | tree |
| 2014-01-24 |
Tianyi Liang | optimize for the reverse direction |
commit | commitdiff | tree |
| 2014-01-23 |
Tianyi Liang | fix: constants are inferred to be the same |
commit | commitdiff | tree |
| 2014-01-23 |
Tianyi Liang | minor fix |
commit | commitdiff | tree |
| 2014-01-22 |
Tianyi Liang | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2014-01-22 |
Morgan Deters | Some minor fixes to SmtEngine strings settings. |
commit | commitdiff | tree |
| 2014-01-22 |
Tianyi Liang | commented out all_supported in strings for now, it... |
commit | commitdiff | tree |
| 2014-01-22 |
Tianyi Liang | solve string exp issue for regexp |
commit | commitdiff | tree |
| 2014-01-22 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-01-22 |
Tianyi Liang | add warning for using strings in ALL_SUPPORTED |
commit | commitdiff | tree |
| 2014-01-22 |
Tianyi Liang | Smarter options, but still have a bug |
commit | commitdiff | tree |
| 2014-01-22 |
Morgan Deters | Delay QuantifiersEngine and UF strong solver initializa... |
commit | commitdiff | tree |
| 2014-01-21 |
Tianyi Liang | Smarter options, but still have a bug |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog