summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv_utils.cpp
AgeCommit message (Expand)Author
2019-03-26Update copyright headers.Aina Niemetz
2018-09-11Support model cores via option --produce-model-cores. (#2407)Andrew Reynolds
2018-08-03Add rewrite for BITVECTOR_ITE with const children. (#2271)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-03-09Some minor cleanup in bv::utils. (#1663)Aina Niemetz
2018-02-20Moved and simplified bv::utils::intersect. (#1614)Aina Niemetz
2018-02-20Unrecursified and merged bv::utils::is(Core|Equality)Term. (#1605)Aina Niemetz
2018-02-15Removed bv::utils::mkConjunction (redundant). (#1610)Aina Niemetz
2018-02-13Moved (unrecursified) bv::utils::collectVars. (#1602)Aina Niemetz
2018-02-11Move (unrecursified) bv::utils::numNodes to lazy_bitblaster.cpp. (#1594)Aina Niemetz
2018-02-09Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589)Aina Niemetz
2018-02-09Remove mkNode from bv::utils (#1587)Aina Niemetz
2018-02-08Clean up bv utils (part one). (#1580)Aina Niemetz
2018-02-08Simplify and cleanup bv::utils::mkConjunction. (#1571)Aina Niemetz
2018-02-07Use template for bv::utils::mkOr. (#1570)Aina Niemetz
2018-02-07Use template for bv::utils::mkAnd. (#1569)Aina Niemetz
2018-02-06Renamed bv::utils::isBVGroundTerm to isBvConstTerm. (#1568)Aina Niemetz
2018-02-06Split and document theory_bv_utils. (#1566)Aina Niemetz
2017-12-08Add CEGQI BV linearization of additions and equalities over additions. (#1417)Mathias Preiner
2017-12-08Fixed side conditions for CBQI BV, added unit tests. (#1434)Aina Niemetz
2017-10-04Add mkZero, mkOne and mkUmulo to bv utils. (#1200)Aina Niemetz
2017-07-07Update copyright headers.Mathias Preiner
2016-04-20update from the masterPaulMeng
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-08-20fix to bug659 due to algebraic solver model buildingLiana Hadarean
2014-07-01Update copyrights.Morgan Deters
2014-06-10Merging CAV14 paper bit-vector work.lianah
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback