| 2020-12-10 |
Gereon Kremer | Fixed a bunch of clang warnings. (#5637) |
blob | commitdiff | raw |
| 2020-09-22 |
Mathias Preiner | Update copyright header script to support CMake and... |
blob | commitdiff | raw | diff to current |
| 2020-06-16 |
Aina Niemetz | Update copyright headers. |
blob | commitdiff | raw | diff to current |
| 2020-02-26 |
Andrew Reynolds | Fix node arity issue in reduction of int2bv (#3777) |
blob | commitdiff | raw | diff to current |
| 2020-01-28 |
Andrew Reynolds | Avoid PLUS with one child for bv2nat elimination (... |
blob | commitdiff | raw | diff to current |
| 2019-10-30 |
Mathias Preiner | Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... |
blob | commitdiff | raw | diff to current |
| 2019-03-26 |
Aina Niemetz | Update copyright headers. |
blob | commitdiff | raw | diff to current |
| 2018-09-11 |
Andrew Reynolds | Support model cores via option --produce-model-cores... |
blob | commitdiff | raw | diff to current |
| 2018-08-04 |
Aina Niemetz | Add rewrite for BITVECTOR_ITE with const children.... |
blob | commitdiff | raw | diff to current |
| 2018-02-20 |
Aina Niemetz | Improve documentation of bv::utils::isCoreTerm (#1617) |
blob | commitdiff | raw | diff to current |
| 2018-02-20 |
Aina Niemetz | Unrecursified and merged bv::utils::is(Core|Equality... |
blob | commitdiff | raw | diff to current |
| 2018-02-17 |
Aina Niemetz | bv::utils::mk(And|Or) Do not return true if size of... |
blob | commitdiff | raw | diff to current |
| 2018-02-16 |
Aina Niemetz | Removed bv::utils::mkConjunction (redundant). (#1610) |
blob | commitdiff | raw | diff to current |
| 2018-02-13 |
Aina Niemetz | Moved (unrecursified) bv::utils::collectVars. (#1602) |
blob | commitdiff | raw | diff to current |
| 2018-02-11 |
Aina Niemetz | Move (unrecursified) bv::utils::numNodes to lazy_bitbla... |
blob | commitdiff | raw | diff to current |
| 2018-02-10 |
Aina Niemetz | Move BitVector specific funs from bv::utils to util... |
blob | commitdiff | raw | diff to current |
| 2018-02-10 |
Aina Niemetz | Remove mkNode from bv::utils (#1587) |
blob | commitdiff | raw | diff to current |
| 2018-02-08 |
Aina Niemetz | Clean up bv utils (part one). (#1580) |
blob | commitdiff | raw | diff to current |
| 2018-02-08 |
Aina Niemetz | Simplify and cleanup bv::utils::mkConjunction. (#1571) |
blob | commitdiff | raw | diff to current |
| 2018-02-07 |
Aina Niemetz | Use template for bv::utils::mkOr. (#1570) |
blob | commitdiff | raw | diff to current |
| 2018-02-07 |
Aina Niemetz | Use template for bv::utils::mkAnd. (#1569) |
blob | commitdiff | raw | diff to current |
| 2018-02-07 |
Aina Niemetz | Renamed bv::utils::isBVGroundTerm to isBvConstTerm... |
blob | commitdiff | raw | diff to current |
| 2018-02-07 |
Aina Niemetz | Split and document theory_bv_utils. (#1566) |
blob | commitdiff | raw | diff to current |
| 2018-01-16 |
Tim King | Removing more miscellaneous throw specifiers. (#1509) |
blob | commitdiff | raw | diff to current |
| 2018-01-09 |
Aina Niemetz | Add bv util mkConst(unsigned, Integer&). (#1499) |
blob | commitdiff | raw | diff to current |
| 2018-01-06 |
Mathias Preiner | Add special {SGE,SGT,NE}_UDIV1 side conditions for... |
blob | commitdiff | raw | diff to current |
| 2018-01-02 |
Andrew Reynolds | Rewrites for BitVector multiplication (#1465) |
blob | commitdiff | raw | diff to current |
| 2017-12-21 |
Mathias Preiner | Add rewriting rule for ranking benchmarks. (#1448) |
blob | commitdiff | raw | diff to current |
| 2017-12-09 |
Mathias Preiner | Add CEGQI BV linearization of additions and equalities... |
blob | commitdiff | raw | diff to current |
| 2017-12-08 |
Aina Niemetz | Fixed side conditions for CBQI BV, added unit tests... |
blob | commitdiff | raw | diff to current |
| 2017-10-05 |
Aina Niemetz | Add mkZero, mkOne and mkUmulo to bv utils. (#1200) |
blob | commitdiff | raw | diff to current |
| 2017-07-21 |
Tim King | Merge branch 'master' into cleanup-regexp |
blob | commitdiff | raw | diff to current |
| 2017-07-21 |
Tim King | Moving from the gnu extensions for hash maps to the... |
blob | commitdiff | raw | diff to current |
| 2017-07-07 |
Mathias Preiner | Update copyright headers. |
blob | commitdiff | raw | diff to current |
| 2016-10-13 |
ajreynol | Merging bv parts of ajr/bvExt branch, minor additions... |
blob | commitdiff | raw | diff to current |
| 2016-04-20 |
PaulMeng | update from the master |
blob | commitdiff | raw | diff to current |
| 2016-04-09 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-04-04 |
Tim King | Updating the copyright headers and scripts. |
blob | commitdiff | raw | diff to current |
| 2016-01-27 |
Liana Hadarean | Merged bit-vector and uf proof branch. |
blob | commitdiff | raw | diff to current |
| 2015-09-02 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' |
blob | commitdiff | raw | diff to current |
| 2015-08-20 |
Liana Hadarean | fix to bug659 due to algebraic solver model building |
blob | commitdiff | raw | diff to current |
| 2015-07-28 |
Tianyi Liang | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2015-07-20 |
ajreynol | Squashed merge of SygusComp 2015 branch. |
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-06-26 |
Morgan Deters | Merge tag 'smtcomp2014-resubmission' |
blob | commitdiff | raw | diff to current |
| 2014-06-22 |
Morgan Deters | Merge tag 'smtcomp2014-application' |
blob | commitdiff | raw | diff to current |
| 2014-06-19 |
Morgan Deters | Fix compile errors with some versions of GCC. |
blob | commitdiff | raw | diff to current |
| 2014-06-17 |
Morgan Deters | Fix compile errors with some versions of GCC. |
blob | commitdiff | raw | diff to current |
| 2014-06-15 |
lianah | bv static learning and rewrites for power of 2 terms |
blob | commitdiff | raw | diff to current |
| 2014-06-10 |
lianah | Merging CAV14 paper bit-vector work. |
blob | commitdiff | raw | diff to current |
| 2014-04-28 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-04-28 |
Kshitij Bansal | Merge pull request #25 from kbansal/sets |
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-17 |
Kshitij Bansal | simplify mkSkolem naming system: don't use $$ |
blob | commitdiff | raw | diff to current |
| 2013-12-26 |
Tianyi Liang | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-12-24 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2013-12-24 |
Morgan Deters | Minor code cleanup. |
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-09-30 |
Liana Hadarean | merged golden |
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-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-04-30 |
lianah | fixed merge conflicts |
blob | commitdiff | raw | diff to current |
| 2013-04-30 |
lianah | added several rewrite rules (BitwiseSlicing, Ule/SleEli... |
blob | commitdiff | raw | diff to current |
| 2013-04-30 |
lianah | added several rewrite rules (BitwiseSlicing, Ule/SleEli... |
blob | commitdiff | raw | diff to current |
| 2013-04-29 |
Kshitij Bansal | Merge pull request #9 from kbansal/master |
blob | commitdiff | raw | diff to current |
| 2013-04-26 |
Kshitij Bansal | Merge experimental decisionweight branch |
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-03-29 |
Dejan Jovanović | Merge branch 'master' of github.com:CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-03-27 |
lianah | Merge branch 'master' into bv-core |
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 |
| 2013-03-23 |
lianah | fixed some explanation problems for the core theory... |
blob | commitdiff | raw | diff to current |
| 2013-03-22 |
lianah | Merge branch 'master' into bv-core |
blob | commitdiff | raw | diff to current |
| 2013-03-21 |
lianah | Merge branch 'master' into bv-core |
blob | commitdiff | raw | diff to current |
| 2013-03-21 |
lianah | Merge branch 'master' into bv-core |
blob | commitdiff | raw | diff to current |
| 2013-03-21 |
lianah | Merge branch 'master' into bv-core |
blob | commitdiff | raw | diff to current |
| 2013-03-20 |
Liana Hadarean | merged master with dejan's constant evaluating equality... |
blob | commitdiff | raw | diff to current |
| 2013-03-13 |
lianah | post failed attempts at getting the incremental solver... |
blob | commitdiff | raw | diff to current |
| 2013-02-26 |
lianah | Merge branch '1.0.x' of https://github.com/CVC4/CVC4... |
blob | commitdiff | raw | diff to current |
| 2013-02-15 |
Tim King | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-14 |
Tim King | Removing BVDebug and replacing with Debug. |
blob | commitdiff | raw | diff to current |
| 2013-02-02 |
lianah | merged master into branch |
blob | commitdiff | raw | diff to current |
| 2013-01-29 |
lianah | compiling implementation of new slicer finished; need... |
blob | commitdiff | raw | diff to current |
| 2013-01-25 |
lianah | minor changes trying to optimize the slicing code |
blob | commitdiff | raw | diff to current |
| 2012-12-11 |
Liana Hadarean | fixed some slicer bugs; set up bv theory to run bit... |
blob | commitdiff | raw | diff to current |
| 2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
blob | commitdiff | raw | diff to current |
| 2012-09-19 |
Morgan Deters | General subscriber infrastructure for NodeManager,... |
blob | commitdiff | raw | diff to current |
| 2012-08-24 |
Morgan Deters | * disallow internal uses of mkVar() (you have to mkSkol... |
blob | commitdiff | raw | diff to current |
| 2012-06-13 |
Clark Barrett | Fixes lots of problems in bv rewrite rules and adds... |
blob | commitdiff | raw | diff to current |
| 2012-06-06 |
Dejan Jovanović | Changes to the combination mechanism, lots of details... |
blob | commitdiff | raw | diff to current |
| 2012-05-28 |
Clark Barrett | Added some BV rewrites, fixed bugs in array theory... |
blob | commitdiff | raw | diff to current |
| 2012-05-08 |
Liana Hadarean | Merging in bvprop branch, with proper bit-vector propag... |
blob | commitdiff | raw | diff to current |
| 2012-04-11 |
Morgan Deters | merge from arrays-clark branch |
blob | commitdiff | raw | diff to current |
| 2012-04-04 |
Liana Hadarean | * added propagation as lemmas to TheoryBV: |
blob | commitdiff | raw | diff to current |
| 2012-03-22 |
Liana Hadarean | Merged updated version of the bitvector theory: |
blob | commitdiff | raw | diff to current |
| 2012-02-25 |
Liana Hadarean | Refactored CnfStream to work with the bv theory Bitblaster: |
blob | commitdiff | raw | diff to current |
| 2011-09-28 |
Morgan Deters | variety of visibility fixes (should clean up some of... |
blob | commitdiff | raw | diff to current |
| next |
projects / cvc5.git / history