added model generation for bv subtheories and bv-inequality solver option

1 files changed, 12 insertions, 0 deletions

diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index 3dfeba140..6d2ed0cf6 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -458,3 +458,15 @@ BitVector InequalityGraph::getValueInModel(TNode node) const {
   Assert (hasModelValue(id));
   return getValue(id); 
 }
+
+void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) {
+  for (ModelValues::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
+    TermId id = (*it).first;
+    BitVector value = (*it).second.value;
+    TNode var = getTermNode(id);
+    Node constant = utils::mkConst(value);
+    Node assignment = utils::mkNode(kind::EQUAL, var, constant);
+    assignments.push_back(assignment); 
+    Debug("bitvector-model") << "   " << var <<" => " << constant << "\n"; 
+  }
+}