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.

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);