diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-11 13:08:00 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-11 11:08:00 -0700 |
commit | 64c48c4d3b4c26b0ba28ab1ab11ef2314ca0cbee (patch) | |
tree | ece6319150e855d2b0850f7508d9e3ee080b7f03 /src/theory/bv | |
parent | 2fb903ed7309fd97c848b03f6587c9d0604efd24 (diff) |
Support model cores via option --produce-model-cores. (#2407)
This adds support for model cores, fixes #1233.
It includes some minor cleanup and additions to utility functions.
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); |