| 2014-08-18 |
ajreynol | Add support for quantifier-specific instantiation level... |
blob | commitdiff | raw |
| 2014-08-15 |
Kshitij Bansal | Update smt_engine.cpp |
blob | commitdiff | raw | diff to current |
| 2014-07-13 |
Morgan Deters | Fix a bug in Boolean terms and arrays. Thanks to Jean... |
blob | commitdiff | raw | diff to current |
| 2014-07-10 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' into segfa... |
blob | commitdiff | raw | diff to current |
| 2014-07-01 |
Morgan Deters | Update copyrights. |
blob | commitdiff | raw | diff to current |
| 2014-07-01 |
Morgan Deters | Merge pull request #44 from mdeters/prio-queue-updates |
blob | commitdiff | raw | diff to current |
| 2014-07-01 |
Morgan Deters | Merge pull request #45 from mdeters/turn-off-strings-exp |
blob | commitdiff | raw | diff to current |
| 2014-06-30 |
Kshitij Bansal | Merge pull request #47 from kbansal/sets |
blob | commitdiff | raw | diff to current |
| 2014-06-26 |
Morgan Deters | Merge tag 'smtcomp2014-resubmission' |
blob | commitdiff | raw | diff to current |
| 2014-06-25 |
Andrew Reynolds | Merge pull request #34 from mdeters/datatypes-kinds |
blob | commitdiff | raw | diff to current |
| 2014-06-25 |
Andrew Reynolds | Merge pull request #37 from mdeters/quants-kinds |
blob | commitdiff | raw | diff to current |
| 2014-06-25 |
Andrew Reynolds | Merge pull request #38 from mdeters/uf-kinds |
blob | commitdiff | raw | diff to current |
| 2014-06-25 |
Morgan Deters | Turn strings-exp off by default (for the release) |
blob | commitdiff | raw | diff to current |
| 2014-06-23 |
Morgan Deters | Fatal error if --unconstrained-simp and --produce-model... |
blob | commitdiff | raw | diff to current |
| 2014-06-22 |
Morgan Deters | Merge tag 'smtcomp2014-application' |
blob | commitdiff | raw | diff to current |
| 2014-06-19 |
lianah | fixed merge conflict |
blob | commitdiff | raw | diff to current |
| 2014-06-19 |
lianah | added model generation to eager bit-blasting and turned... |
blob | commitdiff | raw | diff to current |
| 2014-06-19 |
Morgan Deters | New translator features: expand define-funs and combine... |
blob | commitdiff | raw | diff to current |
| 2014-06-19 |
Morgan Deters | Fix for new CASC features, fixes Java builds. |
blob | commitdiff | raw | diff to current |
| 2014-06-19 |
ajreynol | For casc : print models of functions rewritten by sort... |
blob | commitdiff | raw | diff to current |
| 2014-06-17 |
Morgan Deters | New translator features: expand define-funs and combine... |
blob | commitdiff | raw | diff to current |
| 2014-06-17 |
Morgan Deters | Fix for new CASC features, fixes Java builds. |
blob | commitdiff | raw | diff to current |
| 2014-06-17 |
ajreynol | For casc : print models of functions rewritten by sort... |
blob | commitdiff | raw | diff to current |
| 2014-06-15 |
lianah | Evil bitvector preprocessing pass for simplifying power... |
blob | commitdiff | raw | diff to current |
| 2014-06-13 |
ajreynol | Fix handling of ALIA. |
blob | commitdiff | raw | diff to current |
| 2014-06-11 |
Morgan Deters | Some clean-up, post bv-merge. |
blob | commitdiff | raw | diff to current |
| 2014-06-10 |
Tim King | Merging Tim's pseudoboolean work from his fmcad14 branch. |
blob | commitdiff | raw | diff to current |
| 2014-06-10 |
lianah | Merging CAV14 paper bit-vector work. |
blob | commitdiff | raw | diff to current |
| 2014-06-06 |
Kshitij Bansal | Merge pull request #28 from kbansal/sets |
blob | commitdiff | raw | diff to current |
| 2014-06-06 |
Kshitij Bansal | Sets translate, and other short fixes |
blob | commitdiff | raw | diff to current |
| 2014-06-04 |
Morgan Deters | SmtEngine::checkModel() now checks that model values... |
blob | commitdiff | raw | diff to current |
| 2014-05-15 |
Andrew Reynolds | Minor fixes. Add SMTCOMP 2014 script. |
blob | commitdiff | raw | diff to current |
| 2014-05-14 |
Andrew Reynolds | Finish --dump-instantiations option. Update scripts. |
blob | commitdiff | raw | diff to current |
| 2014-05-13 |
ajreynol | Add lazy strategy for bounded integers to avoid non... |
blob | commitdiff | raw | diff to current |
| 2014-05-12 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-05-11 |
Andrew Reynolds | More preparation for CASC proofs. Minor fix for sort... |
blob | commitdiff | raw | diff to current |
| 2014-05-10 |
Andrew Reynolds | Bug fixes to CBQI. Add first draft of CASC j7 TFF... |
blob | commitdiff | raw | diff to current |
| 2014-05-09 |
Andrew Reynolds | Add variable ordering to ambqi. Bug fix to macros... |
blob | commitdiff | raw | diff to current |
| 2014-05-02 |
Andrew Reynolds | Add option --dt-stc-ind for strengthening skolemization... |
blob | commitdiff | raw | diff to current |
| 2014-05-01 |
Kshitij Bansal | Merge remote-tracking branch 'upstream/master' into... |
blob | commitdiff | raw | diff to current |
| 2014-04-30 |
Tim King | T-entailment work, and QCF (quant conflict find) work... |
blob | commitdiff | raw | diff to current |
| 2014-04-28 |
Kshitij Bansal | Merge remote-tracking branch 'upstream/master' into... |
blob | commitdiff | raw | diff to current |
| 2014-04-10 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-04-10 |
Andrew Reynolds | Add support for cardinality constraints logic UFC.... |
blob | commitdiff | raw | diff to current |
| 2014-04-09 |
Kshitij Bansal | Merge pull request #24 from kbansal/sets-model |
blob | commitdiff | raw | diff to current |
| 2014-04-09 |
Kshitij Bansal | fix get-info error-behavior |
blob | commitdiff | raw | diff to current |
| 2014-04-06 |
Tim King | Merge pull request #21 from pcc/ite-fix |
blob | commitdiff | raw | diff to current |
| 2014-04-03 |
Morgan Deters | Some incremental bugs for Boolean terms, fixed. Thanks... |
blob | commitdiff | raw | diff to current |
| 2014-04-01 |
Tim King | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-03-26 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-03-21 |
Kshitij Bansal | Merge pull request #22 from kbansal/sets-model |
blob | commitdiff | raw | diff to current |
| 2014-03-19 |
Martin Brain | Refactor the theory specific parts of definition expans... |
blob | commitdiff | raw | diff to current |
| 2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-03-11 |
Morgan Deters | Fix for (get-assignment), resolves bug 553. |
blob | commitdiff | raw | diff to current |
| 2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-03-11 |
Andrew Reynolds | Initial refactor of rewrite rules, make theory_rewriter... |
blob | commitdiff | raw | diff to current |
| 2014-03-10 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-03-08 |
Tim King | Merge remote-tracking branch 'CVC4root/master' |
blob | commitdiff | raw | diff to current |
| 2014-03-08 |
Morgan Deters | Remove --ite-remove-quant; support pulling ground ITEs... |
blob | commitdiff | raw | diff to current |
| 2014-03-08 |
Morgan Deters | Fix bug 554 (nominally). |
blob | commitdiff | raw | diff to current |
| 2014-03-07 |
Morgan Deters | Fix strings-exp setting. |
blob | commitdiff | raw | diff to current |
| 2014-03-07 |
Morgan Deters | Fix strings-exp setting. |
blob | commitdiff | raw | diff to current |
| 2014-03-01 |
Tianyi Liang | a new regular expression engine for solving both positi... |
blob | commitdiff | raw | diff to current |
| 2014-02-28 |
Tianyi Liang | a new regular expression engine for solving both positi... |
blob | commitdiff | raw | diff to current |
| 2014-02-21 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-02-21 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-02-21 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-02-21 |
Kshitij Bansal | portfolio: fix export of emptyset |
blob | commitdiff | raw | diff to current |
| 2014-02-20 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-02-20 |
Andrew Reynolds | Fix ite and iff handling in QCF. Add option for heuris... |
blob | commitdiff | raw | diff to current |
| 2014-02-19 |
Tim King | Merge branch 'master' of github.com:CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-02-19 |
Tim King | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-02-18 |
Tianyi Liang | switch to total function str.to.int: maps invalid and... |
blob | commitdiff | raw | diff to current |
| 2014-02-18 |
Tianyi Liang | bring back the commits which is lost accidentally. |
blob | commitdiff | raw | diff to current |
| 2014-02-18 |
Tianyi Liang | add str2int |
blob | commitdiff | raw | diff to current |
| 2014-02-17 |
Morgan Deters | Fix for strings-exp: enable quantifiers |
blob | commitdiff | raw | diff to current |
| 2014-02-17 |
Morgan Deters | Fix strings preprocessing for justification heuristic |
blob | commitdiff | raw | diff to current |
| 2014-02-17 |
Tianyi Liang | type conversion |
blob | commitdiff | raw | diff to current |
| 2014-02-17 |
Tianyi Liang | type conversion |
blob | commitdiff | raw | diff to current |
| 2014-02-14 |
Tianyi Liang | fix expanding def |
blob | commitdiff | raw | diff to current |
| 2014-01-28 |
Tianyi Liang | merge internal and user of charat & substr into one |
blob | commitdiff | raw | diff to current |
| 2014-01-27 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-22 |
Tianyi Liang | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-01-22 |
Morgan Deters | Some minor fixes to SmtEngine strings settings. |
blob | commitdiff | raw | diff to current |
| 2014-01-22 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-01-22 |
Tianyi Liang | add warning for using strings in ALL_SUPPORTED |
blob | commitdiff | raw | diff to current |
| 2014-01-22 |
Tianyi Liang | Smarter options, but still have a bug |
blob | commitdiff | raw | diff to current |
| 2014-01-21 |
Tianyi Liang | Smarter options, but still have a bug |
blob | commitdiff | raw | diff to current |
| 2014-01-18 |
Tianyi Liang | strings with new ideas |
blob | commitdiff | raw | diff to current |
| 2014-01-18 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-17 |
Tianyi Liang | strings with new ideas |
blob | commitdiff | raw | diff to current |
| 2014-01-17 |
Kshitij Bansal | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-16 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-01-16 |
Tianyi Liang | adds partial functions |
blob | commitdiff | raw | diff to current |
| 2014-01-10 |
Andrew Reynolds | Add new method --quant-cf for finding conflicts eagerly... |
blob | commitdiff | raw | diff to current |
| 2014-01-09 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-08 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-04 |
Andrew Reynolds | Removing and consolidating options for uf-ss and quanti... |
blob | commitdiff | raw | diff to current |
| 2014-01-03 |
Andrew Reynolds | Added support for proof production in Equality Engine... |
blob | commitdiff | raw | diff to current |
| 2014-01-02 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| next |
projects / cvc5.git / history