summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/bv_inverter.h
AgeCommit message (Collapse)Author
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)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
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-06-16Update copyright headers.Aina Niemetz
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
Renamed operator CHOICE to WITNESS, and removed it from the front end
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-15Disable solving non-linear BV literals by default (#2070)Andrew Reynolds
2018-02-08Adding virtual destructors on classes with virtual functions. (#1583)Tim King
2018-02-06Updated copyright header for bv_inverter.(cpp|h).Aina Niemetz
2018-01-08Improvements to quant+BV/Bool variable elimination (#1495)Andrew Reynolds
2017-12-20Add explicit disequality handling when generating side condition for CBQI ↵Aina Niemetz
BV. (#1447) This refactors solveBvLit to support explicit handling of disequalities (and, in the next step, inequalities) when generating side conditions.
2017-12-08Fixed side conditions for CBQI BV, added unit tests. (#1434)Aina Niemetz
This fixes the side conditions for BITVECTOR_UREM_TOTAL, BITVECTOR_UDIV_TOTAL, BITVECTOR_LSHR, BITVECTOR_ASHR, BITVECTOR_SHL. It refactors side condition generation for better readability and unit testing. It further adds unit tests for all side conditions we generate in order to check if they too weak or to restrictive (which may result in unsound behavior). This is achieved by checking the following two implications: not (exists x. s * x = t => SC) ... if sat, SC is too restrictive not (SC => exists x. s * x = t) ... if sat SC is too weak This simplifies to checking not (SC <=> exists x. s * x = t).
2017-11-01CBQI BV choice expressions (#1296)Andrew Reynolds
* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently. * Minor * Make unique bound variables for choice functions in BvInstantor, clean up. * Incorporate missing optimizations * Clang format * Unused field. * Minor * Fix, add regression. * Fix regression. * Fix bug that led to incorrect cleanup of instantiations. * Add missing regression * Improve handling of choice rewriting. * Fix * Clang format * Use canonical variables for choice functions in cbqi bv. * Add regression * Clang format. * Address review. * Clang format
2017-10-25CBQI BV: Add handling for missing operators. (#1274)Aina Niemetz
This adds inverse handling for BITVECTOR_XOR, BITVECTOR_SIGN_EXTENDS, BITVECTOR_COMP, BITVECTOR_ASHR. Function isInvertible() now corresponds to exactly the operators (plus index) for which we can determine an inverse, which avoids traversing along non-invertible paths. This further enables a test case that I missed to enable in PR #1268.
2017-10-23CBQI BV: Add ULT/SLT inverse handling. (#1268)Aina Niemetz
This adds inverse handling for ULT(BV), SLT(BV) and disequalities. Rewriting of inequalities and disequalities to equalities with slack can now be disabled with an option (--cbqi-bv-inv-in-dis-eq). Function solve_bv_constraint is now merged into solve_bv_lit.
2017-10-02Address comments from PR #1164. (#1174)Mathias Preiner
Make eliminateSkolemFunctions(...) iterative and some more minor fixes.
2017-09-29Move BvInverter class into separate file. (#1173)Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback