getModelValue implementation in bitvectors

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 57a77c0d25268c96c887ce3ca55d4ff88836dc83..e28ef3ddf16dfadde9e6e7445e9a642fed0c0793 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -137,6 +137,12 @@ void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
   
 }
 
+Node TheoryBV::getModelValue(TNode var) {
+  Assert(!inConflict());
+  return d_bitblastSolver.getModelValue(var);
+}
+
+
 void TheoryBV::propagate(Effort e) {
   Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index e38f3568cdb451a09bdb35e831c9c4e485f10fe7..ffb043bb60de72a9ee23c7c50a46c24f1bb68fe3 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -117,6 +117,8 @@ private:
 
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
+  Node getModelValue(TNode var);
+
   inline std::string indent()
   {
     std::string indentStr(getSatContext()->getLevel(), ' ');