diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv_utils.cpp | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 3 |
2 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 470f9ac7f..9ccaa58e9 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -57,6 +57,12 @@ unsigned getSignExtendAmount(TNode node) /* ------------------------------------------------------------------------- */ +bool isOnes(TNode node) +{ + if (!node.isConst()) return false; + return node == mkOnes(getSize(node)); +} + bool isZero(TNode node) { if (!node.isConst()) return false; diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 9fccf92a7..2ece472e4 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -52,6 +52,9 @@ unsigned getExtractLow(TNode node); /* Get the number of bits by which a given node is extended. */ unsigned getSignExtendAmount(TNode node); +/* Returns true if given node represents a bit-vector comprised of ones. */ +bool isOnes(TNode node); + /* Returns true if given node represents a zero bit-vector. */ bool isZero(TNode node); |