| 2014-03-20 |
Kshitij Bansal | fix for sets/mar2014/..317minimized.. |
commit | commitdiff | tree |
| 2014-03-20 |
Kshitij Bansal | Fix for registration issues of term appearing in a... |
commit | commitdiff | tree |
| 2014-03-20 |
Kshitij Bansal | rewriter fix, weaken an assertion |
commit | commitdiff | tree |
| 2014-03-20 |
Kshitij Bansal | constant normal form and rewrite |
commit | commitdiff | tree |
| 2014-03-20 |
Kshitij Bansal | fix a sharing issues with sets |
commit | commitdiff | tree |
| 2014-03-20 |
Kshitij Bansal | push subtyping for sets to the element type |
commit | commitdiff | tree |
| 2014-03-20 |
Kshitij Bansal | enable check-models for sets/ regressions |
commit | commitdiff | tree |
| 2014-03-20 |
Kshitij Bansal | work on set model |
commit | commitdiff | tree |
| 2014-03-20 |
Kshitij Bansal | testlemma regressions |
commit | commitdiff | tree |
| 2014-03-07 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-03-07 |
Tianyi Liang | remove unrolling depth |
commit | commitdiff | tree |
| 2014-03-07 |
Tianyi Liang | bring back D-Norm |
commit | commitdiff | tree |
| 2014-03-07 |
Morgan Deters | Fix strings-exp setting. |
commit | commitdiff | tree |
| 2014-03-07 |
Tianyi Liang | remove unrolling depth |
commit | commitdiff | tree |
| 2014-03-07 |
Tianyi Liang | bring back D-Norm |
commit | commitdiff | tree |
| 2014-03-07 |
Morgan Deters | Fix strings-exp setting. |
commit | commitdiff | tree |
| 2014-03-07 |
Thomas Hunger | Add swig renames for new Z3STR language. |
commit | commitdiff | tree |
| 2014-03-07 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-03-07 |
Tianyi Liang | adds incremental for strings; clean-up codes |
commit | commitdiff | tree |
| 2014-03-07 |
Tianyi Liang | adds incremental for strings; clean-up codes |
commit | commitdiff | tree |
| 2014-03-05 |
Kshitij Bansal | Merge pull request #14 from kbansal/sets-parserchanges |
commit | commitdiff | tree |
| 2014-03-05 |
Kshitij Bansal | Array smtlib compliance tests |
commit | commitdiff | tree |
| 2014-03-05 |
Kshitij Bansal | Revert "fix naming conflicts in benchmarks" |
commit | commitdiff | tree |
| 2014-03-05 |
Kshitij Bansal | Don't tokenize SET_THEORY operators in smt2 parser |
commit | commitdiff | tree |
| 2014-03-05 |
Tim King | Improving support for POW in arithmetic. Resolves bug... |
commit | commitdiff | tree |
| 2014-03-04 |
Thomas Hunger | Guard java-specific swig code with SWIGJAVA. |
commit | commitdiff | tree |
| 2014-03-04 |
Morgan Deters | Don't theory-preprocess under quantifiers; but DO theor... |
commit | commitdiff | tree |
| 2014-03-04 |
Morgan Deters | More useful error message when someone tries mkExpr... |
commit | commitdiff | tree |
| 2014-03-01 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-03-01 |
Tianyi Liang | add re.nostr for the empty regular expression; add... |
commit | commitdiff | tree |
| 2014-03-01 |
Tianyi Liang | minor clean-up, bring back derivatives |
commit | commitdiff | tree |
| 2014-03-01 |
Tianyi Liang | a new regular expression engine for solving both positi... |
commit | commitdiff | tree |
| 2014-03-01 |
Tianyi Liang | add re.nostr for the empty regular expression; add... |
commit | commitdiff | tree |
| 2014-02-28 |
Tianyi Liang | minor clean-up, bring back derivatives |
commit | commitdiff | tree |
| 2014-02-28 |
Tianyi Liang | a new regular expression engine for solving both positi... |
commit | commitdiff | tree |
| 2014-02-28 |
Kshitij Bansal | Merge pull request #12 from kbansal/in-to-member |
commit | commitdiff | tree |
| 2014-02-28 |
Kshitij Bansal | theory/sets: cleanup |
commit | commitdiff | tree |
| 2014-02-28 |
Kshitij Bansal | rename kind::IN to kind::MEMBER (fixes some windows... |
commit | commitdiff | tree |
| 2014-02-28 |
Kshitij Bansal | Merge pull request #11 from kbansal/improve-stats-every... |
commit | commitdiff | tree |
| 2014-02-27 |
Kshitij Bansal | --stats-every-query option: print increment in addition... |
commit | commitdiff | tree |
| 2014-02-27 |
Andrew Reynolds | Bug fix for QCF algorithm, was missing instantiations... |
commit | commitdiff | tree |
| 2014-02-26 |
Tianyi Liang | sorry for the missing file |
commit | commitdiff | tree |
| 2014-02-26 |
Tianyi Liang | bug fix (caused by merge), move cardinality option... |
commit | commitdiff | tree |
| 2014-02-26 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-02-26 |
Tianyi Liang | add a new file |
commit | commitdiff | tree |
| 2014-02-26 |
Tianyi Liang | for merging |
commit | commitdiff | tree |
| 2014-02-26 |
Tianyi Liang | smt-lib syntax change: str.contain -> str.contains... |
commit | commitdiff | tree |
| 2014-02-26 |
Tianyi Liang | for merging |
commit | commitdiff | tree |
| 2014-02-25 |
Morgan Deters | Minor code clean up in parser. |
commit | commitdiff | tree |
| 2014-02-25 |
Morgan Deters | New translation work, support Z3-str-style string const... |
commit | commitdiff | tree |
| 2014-02-25 |
Morgan Deters | Fix quotes in string constants. |
commit | commitdiff | tree |
| 2014-02-25 |
Andrew Reynolds | Add options --full-saturate-quant and --mbqi=trust... |
commit | commitdiff | tree |
| 2014-02-24 |
Tianyi Liang | smt-lib syntax change: str.contain -> str.contains... |
commit | commitdiff | tree |
| 2014-02-24 |
Tianyi Liang | bug fix: strings preprocess for the orignal term, causi... |
commit | commitdiff | tree |
| 2014-02-21 |
Morgan Deters | Merge branch '1.3.x' |
commit | commitdiff | tree |
| 2014-02-21 |
Morgan Deters | No diamond-breaking under quantifiers (resolves bug... |
commit | commitdiff | tree |
| 2014-02-21 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-02-21 |
Tianyi Liang | reorganize substr, fix some potential bugs, adds cache... |
commit | commitdiff | tree |
| 2014-02-21 |
Tianyi Liang | reorganize substr, fix some potential bugs, adds cache... |
commit | commitdiff | tree |
| 2014-02-21 |
Morgan Deters | Merge branch '1.3.x' |
commit | commitdiff | tree |
| 2014-02-21 |
Morgan Deters | Fix two variants of Node::substitute(). |
commit | commitdiff | tree |
| 2014-02-21 |
Kshitij Bansal | portfolio: fix export of emptyset |
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / shortlog