Age | Commit message (Collapse) | Author |
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
Renamed operator CHOICE to WITNESS, and removed it from the front end
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
BV. (#1447)
This refactors solveBvLit to support explicit handling of disequalities (and, in the next step, inequalities) when generating side conditions.
|
|
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).
|
|
* 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
|
|
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.
|
|
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.
|
|
Make eliminateSkolemFunctions(...) iterative and some more minor fixes.
|
|
|