2019-12-09 |
Andres Noetzli | Make theory rewriters non-static (#3547) |
blob | commitdiff | raw |
2019-05-18 |
Andres Noetzli | Fix BV ITE rewrite (#3004) |
blob | commitdiff | raw | diff to current |
2019-04-01 |
Andres Noetzli | Fix RewriteITEBv to ensure rewrite to fixpoint (#2878) |
blob | commitdiff | raw | diff to current |
2019-03-26 |
Aina Niemetz | Update copyright headers. |
blob | commitdiff | raw | diff to current |
2018-10-20 |
Aina Niemetz | BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_X... |
blob | commitdiff | raw | diff to current |
2018-10-17 |
Aina Niemetz | BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_O... |
blob | commitdiff | raw | diff to current |
2018-10-16 |
Aina Niemetz | BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_A... |
blob | commitdiff | raw | diff to current |
2018-08-08 |
Andres Noetzli | Require Swig 3 (#2283) |
blob | commitdiff | raw | diff to current |
2018-08-07 |
Aina Niemetz | Add rewrite for nested BITVECTOR_ITE that can be merged... |
blob | commitdiff | raw | diff to current |
2018-08-04 |
Aina Niemetz | Add rewrite for nested BITVECTOR_ITE with cond_outer... |
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-08-03 |
Aina Niemetz | Add rewrite for BITVECTOR_ITE with term_then == term_el... |
blob | commitdiff | raw | diff to current |
2018-08-02 |
Aina Niemetz | Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with... |
blob | commitdiff | raw | diff to current |
2018-06-25 |
Aina Niemetz | Updated copyright headers. |
blob | commitdiff | raw | diff to current |
2018-04-05 |
Mathias Preiner | Add more general SignExtendUltConst rewriting. (#1385) |
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-10-21 |
Mathias Preiner | Add rewriting rules for Eq/Ult with sign_extend and... |
blob | commitdiff | raw | diff to current |
2017-09-01 |
Andres Noetzli | Replace CVC4_THREADLOCAL in interactive_shell (#1065) |
blob | commitdiff | raw | diff to current |
2017-07-07 |
Mathias Preiner | Update copyright headers. |
blob | commitdiff | raw | diff to current |
2017-06-21 |
Andrew Reynolds | Merge pull request #175 from CVC4/fix_uninit |
blob | commitdiff | raw | diff to current |
2017-06-15 |
Clark Barrett | Merge pull request #167 from CVC4/fix_div |
blob | commitdiff | raw | diff to current |
2017-06-14 |
Andres Noetzli | Remove UdivSelf rewrite, add UdivZero rewrite |
blob | commitdiff | raw | diff to current |
2017-03-06 |
Clark Barrett | Adding support for bool-to-bv |
blob | commitdiff | raw | diff to current |
2016-11-10 |
ajreynol | Add option for enabling/disabling lazy extended functio... |
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-09 |
Tim King | Removing StatisticsRegistry's static functions current... |
blob | commitdiff | raw | diff to current |
2015-12-15 |
Tim King | Refactoring Options Handler & Library Cycle Breaking |
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-11-27 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
2014-11-17 |
lianah | added command line option for extractArith bv rewrite |
blob | commitdiff | raw | diff to current |
2014-11-10 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
2014-11-05 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
2014-10-23 |
lianah | Fixed inefficiency in bit-vector rewrite rule. |
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-11 |
lianah | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
2014-06-11 |
lianah | switched bv equality order |
blob | commitdiff | raw | diff to current |
2014-06-10 |
lianah | Merging CAV14 paper bit-vector work. |
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-11-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
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-09 |
lianah | fixed options::proof() segfault |
blob | commitdiff | raw | diff to current |
2013-09-30 |
Liana Hadarean | merged golden |
blob | commitdiff | raw | diff to current |
2013-09-18 |
Morgan Deters | Support for bv2nat/int2bv in parser and BV rewriter. |
blob | commitdiff | raw | diff to current |
2013-08-26 |
Kshitij Bansal | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
2013-07-16 |
Morgan Deters | Minor bugfixes to model-building |
blob | commitdiff | raw | diff to current |
2013-05-07 |
lianah | one more fix for rewrites |
blob | commitdiff | raw | diff to current |
2013-05-07 |
lianah | fixed bv rewrite blow-up |
blob | commitdiff | raw | diff to current |
2013-05-07 |
Liana Hadarean | fixed bv rewrite rule bug |
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 | merged master |
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 |
lianah | removed tracing code causing slowdown; cleaned up some... |
blob | commitdiff | raw | diff to current |
2013-04-30 |
lianah | fixed merge conflicts |
blob | commitdiff | raw | diff to current |
2013-04-30 |
lianah | merged cvc4 master |
blob | commitdiff | raw | diff to current |
2013-04-30 |
lianah | updated the author name |
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 bvule, bvsle operator elimination rulesl; added... |
blob | commitdiff | raw | diff to current |
2013-04-30 |
lianah | added some bv rewrite rules |
blob | commitdiff | raw | diff to current |
2013-04-30 |
lianah | updated the author name |
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-25 |
lianah | added bvule, bvsle operator elimination rulesl; added... |
blob | commitdiff | raw | diff to current |
2013-04-21 |
lianah | added some bv rewrite rules |
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 |
2012-11-13 |
Liana Hadarean | fixed failed bv regressions by refactoring out some... |
blob | commitdiff | raw | diff to current |
2012-11-13 |
Liana Hadarean | added support for division by zero for bit-vector divis... |
blob | commitdiff | raw | diff to current |
2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
blob | commitdiff | raw | diff to current |
2012-10-09 |
Liana Hadarean | fixed bv rewriter to evaluate bvurem over constants |
blob | commitdiff | raw | diff to current |
2012-06-13 |
Clark Barrett | Fixes more problems in bv rewrites |
blob | commitdiff | raw | diff to current |
2012-06-12 |
Clark Barrett | Changed bitvector theory rewriter so that equalities... |
blob | commitdiff | raw | diff to current |
2012-06-11 |
Clark Barrett | OK, now the rewrite issues are fixed |
blob | commitdiff | raw | diff to current |
2012-06-11 |
Clark Barrett | Fix for array bug with decision heuristic |
blob | commitdiff | raw | diff to current |
2012-06-10 |
Clark Barrett | Added a very fruitful assertion to the rewriter: checks... |
blob | commitdiff | raw | diff to current |
2012-05-30 |
Clark Barrett | Added BitwiseEq bitvector rewrite |
blob | commitdiff | raw | diff to current |
2012-05-29 |
Clark Barrett | Enabled SolveEq bv rewrite |
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-04-04 |
Liana Hadarean | * added propagation as lemmas to TheoryBV: |
blob | commitdiff | raw | diff to current |
2012-03-29 |
Tim King | Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is... |
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 |
2012-02-20 |
Morgan Deters | portfolio merge |
blob | commitdiff | raw | diff to current |
2011-09-02 |
Morgan Deters | Merge from my post-smtcomp branch. Includes: |
blob | commitdiff | raw | diff to current |
2011-03-22 |
Dejan Jovanović | updating debug output usage to eliviate impact of bug 252 |
blob | commitdiff | raw | diff to current |
2011-03-20 |
Dejan Jovanović | commit for the version of bitvectors that passes all... |
blob | commitdiff | raw | diff to current |
2011-02-26 |
Morgan Deters | Commit to fix bug 241 (improper "using namespace std... |
blob | commitdiff | raw | diff to current |
2011-02-16 |
Dejan Jovanović | updates for the rewriter, added some statistics |
blob | commitdiff | raw | diff to current |
2011-01-05 |
Dejan Jovanović | Commit for the theory engine and rewriter changes.... |
blob | commitdiff | raw | diff to current |
|