summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv_rewriter.cpp
AgeCommit message (Expand)Author
2021-06-11Remove support for lazy BV extended function reductions and inferences (#6728)Andrew Reynolds
2021-06-10Ensure bv2nat and int2bv are not rewritten when using solve-bv-as-int (#6725)Andrew Reynolds
2021-05-27Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)Andres Noetzli
2021-05-21BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)Aina Niemetz
2021-05-06Use constant folding for evaluating BV eager atom (#6494)Andrew Reynolds
2021-04-22Move expand definition from Theory to TheoryRewriter (#6408)Andrew Reynolds
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-05Remove partial UDIV/UREM operators. (#6069)Mathias Preiner
2020-12-15Remove bv divide by zero option (#5672)Andrew Reynolds
2020-09-22Add simple BV solver (#5065)Mathias Preiner
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-03Added a new rule to simplify (bvugt (bvurem T x) x) (#4993)Gereon Kremer
2020-06-16Update copyright headers.Aina Niemetz
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2019-12-09Make theory rewriters non-static (#3547)Andres Noetzli
2019-05-17Fix BV ITE rewrite (#3004)Andres Noetzli
2019-04-01Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)Andres Noetzli
2019-03-26Update copyright headers.Aina Niemetz
2018-10-19BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special const...Aina Niemetz
2018-10-16BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special const....Aina Niemetz
2018-10-16BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_AND) with 0 (#2596).Aina Niemetz
2018-08-07Require Swig 3 (#2283)Andres Noetzli
2018-08-07Add rewrite for nested BITVECTOR_ITE that can be merged. (#2273)Aina Niemetz
2018-08-03 Add rewrite for nested BITVECTOR_ITE with cond_outer == cond_inner. (#2272)Aina Niemetz
2018-08-03Add rewrite for BITVECTOR_ITE with const children. (#2271)Aina Niemetz
2018-08-03Add rewrite for BITVECTOR_ITE with term_then == term_else. (#2268)Aina Niemetz
2018-08-02Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with const condition/child....Aina Niemetz
2018-06-25Updated copyright headers.Aina Niemetz
2018-04-05Add more general SignExtendUltConst rewriting. (#1385)Mathias Preiner
2017-12-20Add rewriting rule for ranking benchmarks. (#1448)Mathias Preiner
2017-10-20Add rewriting rules for Eq/Ult with sign_extend and constants. (#1258)Mathias Preiner
2017-08-31Replace CVC4_THREADLOCAL in interactive_shell (#1065)Andres Noetzli
2017-07-07Update copyright headers.Mathias Preiner
2017-06-14Remove UdivSelf rewrite, add UdivZero rewriteAndres Noetzli
2017-03-06Adding support for bool-to-bvClark Barrett
2016-11-10Add option for enabling/disabling lazy extended function reduction in bitvect...ajreynol
2016-10-13Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.ajreynol
2016-04-20update from the masterPaulMeng
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2014-11-17added command line option for extractArith bv rewritelianah
2014-10-23Fixed inefficiency in bit-vector rewrite rule.lianah
2014-07-01Update copyrights.Morgan Deters
2014-06-11switched bv equality orderlianah
2014-06-10Merging CAV14 paper bit-vector work.lianah
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback