| 2013-12-11 |
Morgan Deters | Whitespace. |
blob | commitdiff | raw |
| 2013-12-10 |
Morgan Deters | Remove "NodeValue width" output |
blob | commitdiff | raw | diff to current |
| 2013-12-05 |
Morgan Deters | Update copyrights, add missing file-level documentation... |
blob | commitdiff | raw | diff to current |
| 2013-12-04 |
Morgan Deters | Partial kind branch merge, including new --rewrite... |
blob | commitdiff | raw | diff to current |
| 2013-12-04 |
Morgan Deters | Don't put define-funs in model output; bug 411 testcase... |
blob | commitdiff | raw | diff to current |
| 2013-12-03 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-11-29 |
Morgan Deters | Fix proofs build. |
blob | commitdiff | raw | diff to current |
| 2013-11-27 |
Morgan Deters | General pre-release cleanup commit |
blob | commitdiff | raw | diff to current |
| 2013-11-26 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-11-25 |
Tim King | Merge remote-tracking branch 'CVC4root/master' |
blob | commitdiff | raw | diff to current |
| 2013-11-25 |
Tim King | Substantial Changes: |
blob | commitdiff | raw | diff to current |
| 2013-11-21 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-11-20 |
Tim King | Changing the number of bits allocated per field in... |
blob | commitdiff | raw | diff to current |
| 2013-11-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-11-06 |
lianah | fixed proof regression script and added a new uf test... |
blob | commitdiff | raw | diff to current |
| 2013-11-04 |
lianah | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-10-28 |
Clark Barrett | Turn off model-based arrays (causing crashes in portfolio) |
blob | commitdiff | raw | diff to current |
| 2013-10-09 |
lianah | fixed options::proof() segfault |
blob | commitdiff | raw | diff to current |
| 2013-10-09 |
lianah | cleaned up proof code |
blob | commitdiff | raw | diff to current |
| 2013-10-09 |
lianah | fixed uf proof bug: now storing deleted theory lemmas |
blob | commitdiff | raw | diff to current |
| 2013-10-08 |
lianah | added currying for uf proofs; still needs debugging |
blob | commitdiff | raw | diff to current |
| 2013-10-07 |
Liana Hadarean | merged golden |
blob | commitdiff | raw | diff to current |
| 2013-10-07 |
Andrew Reynolds | Multiple fixes for datatypes theory solver: add support... |
blob | commitdiff | raw | diff to current |
| 2013-10-03 |
Andrew Reynolds | Added support for converting unsorted problems to multi... |
blob | commitdiff | raw | diff to current |
| 2013-10-02 |
Andrew Reynolds | Added support for converting unsorted problems to multi... |
blob | commitdiff | raw | diff to current |
| 2013-10-01 |
Tianyi Liang | replace with a new method for disequality, move to... |
blob | commitdiff | raw | diff to current |
| 2013-09-30 |
Liana Hadarean | merged golden |
blob | commitdiff | raw | diff to current |
| 2013-09-27 |
Morgan Deters | Some fixes to recent strings commits. |
blob | commitdiff | raw | diff to current |
| 2013-09-27 |
Morgan Deters | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-09-27 |
Tianyi Liang | adds communication with arith engine |
blob | commitdiff | raw | diff to current |
| 2013-09-27 |
Andrew Reynolds | Add new symmetry breaking technique for finite model... |
blob | commitdiff | raw | diff to current |
| 2013-09-27 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-09-27 |
Tianyi Liang | removes unsound cases, adds unrolling |
blob | commitdiff | raw | diff to current |
| 2013-09-27 |
Tianyi Liang | removes unsound cases, adds unrolling |
blob | commitdiff | raw | diff to current |
| 2013-09-24 |
Clark Barrett | Better fix for bug 528 |
blob | commitdiff | raw | diff to current |
| 2013-09-23 |
Morgan Deters | Revert Clark's last commit, at his request; there are... |
blob | commitdiff | raw | diff to current |
| 2013-09-23 |
Clark Barrett | Cleaner version of bug-fix for 528, also moved substitu... |
blob | commitdiff | raw | diff to current |
| 2013-09-19 |
Clark Barrett | Fix for bug 528 |
blob | commitdiff | raw | diff to current |
| 2013-09-18 |
Morgan Deters | Fixes to theoryof-mode; no longer static in Theory... |
blob | commitdiff | raw | diff to current |
| 2013-09-13 |
Morgan Deters | Documentation fixes, some code typo fixes, file perms... |
blob | commitdiff | raw | diff to current |
| 2013-09-09 |
Morgan Deters | Fix declare-datatypes dumping bug (bug 385). |
blob | commitdiff | raw | diff to current |
| 2013-09-09 |
Morgan Deters | Support per-command verbosity settings. |
blob | commitdiff | raw | diff to current |
| 2013-09-05 |
Morgan Deters | Fix declare-fun/define-fun in dumps; resolves bugs... |
blob | commitdiff | raw | diff to current |
| 2013-08-26 |
Kshitij Bansal | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
| 2013-08-20 |
Morgan Deters | Change recursive expandDefinitions() to an interative... |
blob | commitdiff | raw | diff to current |
| 2013-08-08 |
Morgan Deters | Fix a serious bug in the preprocessor; problem inputs... |
blob | commitdiff | raw | diff to current |
| 2013-07-24 |
Morgan Deters | Regressions now checking models on unknown too. But... |
blob | commitdiff | raw | diff to current |
| 2013-07-23 |
Morgan Deters | (get-info :all-options) to get option values; also... |
blob | commitdiff | raw | diff to current |
| 2013-07-17 |
Morgan Deters | Fix bug 516; include some bug testcases. |
blob | commitdiff | raw | diff to current |
| 2013-07-11 |
Morgan Deters | Support for TPTP's TFF0 (with arithmetic) |
blob | commitdiff | raw | diff to current |
| 2013-07-07 |
Morgan Deters | Model output is now const; this related to bug 519 |
blob | commitdiff | raw | diff to current |
| 2013-06-25 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
| 2013-06-25 |
Morgan Deters | Support for abs, to_int, is_int, divisible in SMT-LIB... |
blob | commitdiff | raw | diff to current |
| 2013-06-21 |
Morgan Deters | Fix failure in non-assertion builds on incorrect SmtEng... |
blob | commitdiff | raw | diff to current |
| 2013-06-19 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
| 2013-06-04 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
| 2013-06-03 |
Morgan Deters | Merge tag 'casc24' |
blob | commitdiff | raw | diff to current |
| 2013-05-29 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
| 2013-05-22 |
Andrew Reynolds | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-05-21 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
| 2013-05-21 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
| 2013-05-20 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
| 2013-05-20 |
Morgan Deters | Fix error reporting on use of (nonlinear) div,mod,... |
blob | commitdiff | raw | diff to current |
| 2013-05-20 |
Morgan Deters | Don't allow get-model & co after a user push/pop |
blob | commitdiff | raw | diff to current |
| 2013-05-20 |
Morgan Deters | Better error on invalid logic strings. |
blob | commitdiff | raw | diff to current |
| 2013-05-20 |
Morgan Deters | Fix to empty response to (get-assignment). |
blob | commitdiff | raw | diff to current |
| 2013-05-17 |
Morgan Deters | Better error on invalid logic strings. |
blob | commitdiff | raw | diff to current |
| 2013-05-17 |
Morgan Deters | Fix to empty response to (get-assignment). |
blob | commitdiff | raw | diff to current |
| 2013-05-10 |
Andrew Reynolds | Add simplification option --fo-prop-quant. Add model... |
blob | commitdiff | raw | diff to current |
| 2013-05-09 |
Kshitij Bansal | Merge branch 'master' of ssh://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-05-09 |
Andrew Reynolds | Add new method for checking candidate models, --fmf... |
blob | commitdiff | raw | diff to current |
| 2013-05-08 |
Morgan Deters | final updates for smt-eval script |
blob | commitdiff | raw | diff to current |
| 2013-05-06 |
Tim King | Disables justification stop only for LRA if the problem... |
blob | commitdiff | raw | diff to current |
| 2013-05-03 |
Tim King | Merging branch 'soiquickexplain'. |
blob | commitdiff | raw | diff to current |
| 2013-05-03 |
Tim King | Merge branch 'fcexplanations' |
blob | commitdiff | raw | diff to current |
| 2013-05-02 |
lianah | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-05-01 |
Morgan Deters | Fix to dumping re: boolean terms, datatypes |
blob | commitdiff | raw | diff to current |
| 2013-05-01 |
lianah | added back BitwiseEq rule |
blob | commitdiff | raw | diff to current |
| 2013-04-30 |
lianah | fixed merge conflicts |
blob | commitdiff | raw | diff to current |
| 2013-04-30 |
lianah | innd examples are solved fast, but destruction assertio... |
blob | commitdiff | raw | diff to current |
| 2013-04-30 |
lianah | uncompiling new bv to bool lifting |
blob | commitdiff | raw | diff to current |
| 2013-04-30 |
lianah | finished implementing bv to bool lifting and added... |
blob | commitdiff | raw | diff to current |
| 2013-04-24 |
Morgan Deters | Theory "alternates" support |
blob | commitdiff | raw | diff to current |
| 2013-04-18 |
lianah | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-04-18 |
lianah | making sure sat context is zero when user context is... |
blob | commitdiff | raw | diff to current |
| 2013-04-18 |
lianah | fixing destruction order in SmtEngine |
blob | commitdiff | raw | diff to current |
| 2013-04-17 |
lianah | innd examples are solved fast, but destruction assertio... |
blob | commitdiff | raw | diff to current |
| 2013-04-16 |
lianah | uncompiling new bv to bool lifting |
blob | commitdiff | raw | diff to current |
| 2013-04-12 |
lianah | finished implementing bv to bool lifting and added... |
blob | commitdiff | raw | diff to current |
| 2013-04-03 |
Dejan Jovanović | * changing the bitblast-eager to bitblast on pre-register |
blob | commitdiff | raw | diff to current |
| 2013-04-02 |
Morgan Deters | Regenerated copyrights: canonicalized names, no emails |
blob | commitdiff | raw | diff to current |
| 2013-04-02 |
Morgan Deters | update copyrights |
blob | commitdiff | raw | diff to current |
| 2013-04-02 |
Clark Barrett | Fix regression error by turning off model-based solver... |
blob | commitdiff | raw | diff to current |
| 2013-04-02 |
Clark Barrett | Turning on model based array solver for QF_AX |
blob | commitdiff | raw | diff to current |
| 2013-04-02 |
Clark Barrett | Made eager lemmas an option, enabled for QF_AX |
blob | commitdiff | raw | diff to current |
| 2013-04-02 |
Clark Barrett | Disabling eager array index splitting for QF_AX |
blob | commitdiff | raw | diff to current |
| 2013-04-01 |
Morgan Deters | Merging some cleanup work: |
blob | commitdiff | raw | diff to current |
| 2013-04-01 |
Morgan Deters | Fix bug 491 and related issues with checkModel() and... |
blob | commitdiff | raw | diff to current |
| 2013-03-31 |
Clark Barrett | Disabling eager array index splitting for QF_AUFLIA |
blob | commitdiff | raw | diff to current |
| 2013-03-27 |
lianah | added model generation for bv subtheories and bv-inequa... |
blob | commitdiff | raw | diff to current |
| next |
projects / cvc5.git / history