| 2014-03-19 |
Morgan Deters | Minor usability fixes related to SMT-LIB compliance. |
commit | commitdiff | tree |
| 2014-03-19 |
Morgan Deters | Fix proof signatures makefile |
commit | commitdiff | tree |
| 2014-03-19 |
Morgan Deters | Minor documentation fixups. |
commit | commitdiff | tree |
| 2014-03-19 |
Andrew Reynolds | Fix a memory leak in LFSC proof checker. Largest QF_UF... |
commit | commitdiff | tree |
| 2014-03-17 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-03-17 |
Tianyi Liang | hot fix for pre-reg term caching in strings |
commit | commitdiff | tree |
| 2014-03-17 |
Tianyi Liang | hot fix for pre-reg term caching in strings |
commit | commitdiff | tree |
| 2014-03-14 |
Morgan Deters | SMT-LIB compliance: allow bin/hex set-info, e.g. (set... |
commit | commitdiff | tree |
| 2014-03-14 |
Morgan Deters | dos2unix on the proof signatures, and fix the makefile. |
commit | commitdiff | tree |
| 2014-03-14 |
Andrew Reynolds | Add ability to provide theory-specific proof rules... |
commit | commitdiff | tree |
| 2014-03-13 |
Andrew Reynolds | Add working example of LFSC proof with quantifiers... |
commit | commitdiff | tree |
| 2014-03-12 |
Andrew Reynolds | Work on array pf signature, add working example. Add... |
commit | commitdiff | tree |
| 2014-03-12 |
Andrew Reynolds | Minor fixes post-merge of RR. |
commit | commitdiff | tree |
| 2014-03-12 |
Morgan Deters | Fix LogicInfo unit test. |
commit | commitdiff | tree |
| 2014-03-12 |
Morgan Deters | Some standardization of regression Makefiles that got... |
commit | commitdiff | tree |
| 2014-03-12 |
Morgan Deters | Draft contrib/get-abc script for bitvectors libabc... |
commit | commitdiff | tree |
| 2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
commit | commitdiff | tree |
| 2014-03-11 |
Morgan Deters | Fix for rewriterules build breakage. |
commit | commitdiff | tree |
| 2014-03-11 |
Morgan Deters | Fix for random-seed option. |
commit | commitdiff | tree |
| 2014-03-11 |
Morgan Deters | Fix for portfolio. |
commit | commitdiff | tree |
| 2014-03-11 |
Morgan Deters | Minor cleanup. |
commit | commitdiff | tree |
| 2014-03-11 |
Morgan Deters | Fix for (get-assignment), resolves bug 553. |
commit | commitdiff | tree |
| 2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
commit | commitdiff | tree |
| 2014-03-11 |
Morgan Deters | Fix some Win32 and SMT-LIB compliance bugs discovered... |
commit | commitdiff | tree |
| 2014-03-11 |
Andrew Reynolds | Initial refactor of rewrite rules, make theory_rewriter... |
commit | commitdiff | tree |
| 2014-03-10 |
Tianyi Liang | adds intro vars length cache |
commit | commitdiff | tree |
| 2014-03-10 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-03-10 |
Tianyi Liang | minor change for strings-fmf |
commit | commitdiff | tree |
| 2014-03-10 |
Tianyi Liang | minor change for strings-fmf |
commit | commitdiff | tree |
| 2014-03-08 |
Morgan Deters | Re-fix bug 551 by adding a check to the arith ITE simpl... |
commit | commitdiff | tree |
| 2014-03-08 |
Tim King | Merge pull request #18 from timothy-king/master |
commit | commitdiff | tree |
| 2014-03-08 |
Tim King | Fixing name changes that cam in from the merge. |
commit | commitdiff | tree |
| 2014-03-08 |
Tim King | Merge remote-tracking branch 'CVC4root/master' |
commit | commitdiff | tree |
| 2014-03-08 |
Morgan Deters | Remove --ite-remove-quant; support pulling ground ITEs... |
commit | commitdiff | tree |
| 2014-03-08 |
Morgan Deters | Fix run_regression on Mac. |
commit | commitdiff | tree |
| 2014-03-08 |
Morgan Deters | Fix bug 554 (nominally). |
commit | commitdiff | tree |
| 2014-03-08 |
Tim King | Fixing a SWIG problem for RationalFromDoubleException. |
commit | commitdiff | tree |
| 2014-03-07 |
Tim King | Merging a squash of the branch timothy-king/CVC4/glpkne... |
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 |
| next |
projects / cvc5.git / shortlog