From: Dejan Jovanović <dejan@cs.nyu.edu>
Date: Tue, 26 Mar 2013 20:52:21 +0000 (-0400)
Subject: getModelValue implementation in bitvectors
X-Git-Tag: cvc5-1.0.0~7365
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=70d1a0171840cd62b5c1d89b875ffb50da216793;p=cvc5.git

getModelValue implementation in bitvectors
---

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 57a77c0d2..e28ef3ddf 100644
--- 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 e38f3568c..ffb043bb6 100644
--- 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(), ' ');