| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").
|
|
Adds missing override keywords.
|
|
This commit adds unit tests for the BitVector class and adds some additional argument checks. Additionally, it fixes a minor issue in the ZeroExtendUltConst rule if the zero_extend was by 0 bits. In that case, the rule was calling BitVector::extract() with high < low.
|
|
|
|
Tested against the recursive implementation with a temporary assertion on regression tests
with --bv-eq-slicer=auto.
|
|
This unrecursifies and merges bv::utils::isCoreTerm and bv::utils::isEqualityTerm to avoid
code duplication.
In the best case, the recursive implementation visits less nodes. This can be achieved with
the non-recursive implementation, however, at the cost of increased code complexity.
In practice, on QF_BV the new implementation slightly improves performance.
Tested against the recursive implementation with a temporary assertion on regression
tests (bv::utils::isCoreTerm was tested with --bv-eq-slicer=auto).
Further tested on QF_BV with a TO of 300s (slight performance improvement).
|
|
|
|
|
|
|
|
|
|
|
|
This unrecursifies and moves bv::utils::numNodes to an unnamed namespace in lazy_bitblaster.cpp
(only place where it is used). Tested against the recursive implementation (with a temporary
Assertion) on regression tests.
|
|
|
|
|
|
|
|
This is part one of an effort to clean up bv utils. It addresses review comments not addressed in
#1566 (changes of moved code), removes unused functions and moves a helper to compute the
gcd over Index.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This moves the implementation from the header to the .cpp file. It further documents all functions in
the header file.
|
|
|
|
|
|
Removing more miscellaneous throw specifiers. Also fixing the spelling of amount in several places.
|
|
Removing more miscellaneous throw specifiers.
|
|
|
|
This commit further fixes some other issues with bit-vectors of size 1.
|
|
|
|
|
|
Adds support for linearizing additions w.r.t. to a variable.
For example,
a * x + b + c * d * -x = e + x
is rewritten to
x * (a - c * d - 1) = e - b.
This also adds an additional rewriting rule x * x = x --> x < 2.
|
|
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).
|
|
|
|
This adds Gaussian Elimination as a preprocessing pass for BV. Gaussian Elimination is only applied if the given bit-width guarantees that no overflows can occur.
|
|
|
|
|
|
If a newly introduced atom is not rewritten it can happen that the
literals of both the original atom and the rewritten atom end up in the CNF.
However, only the original atom has a BB definition and the literal of the
rewritten atom is unconstrained (no BB definition).
|
|
This adds several utility functions for the theory BV. Function mkUmulo encodes an unsigned multiplication overflow detection operation, which we need for CBQI BV. In the future, we will introduce a Umulo node kind (and a corresponding bit-blasting strategy based on the encoding implemented in mkUmulo).
|
|
|
|
* Fixing CID 1362895: Initializing d_bvp to nullptr. Miscellaneous cleanup.
|
|
Commit 546d795470ca7c30fc62fe9b6c7b8e5838e1eed4
caused our nightly builds to fail because it did
not replace CVC4_THREADLOCAL with
CVC4_THREAD_LOCAL in interactive_shell. This
commit fixes the issue and adds readline to
Travis, s.t. readline related code gets compiled
as part of our CI tests.
|
|
|
|
|
|
* Guard use of AigBitblaster with CVC4_USE_ABC.
This removes the Unreachable() implementation of AigBitblaster in case CVC4 is
not compiled with ABC support.
|
|
|
|
* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
|
|
|
