adding

* getModelValue to valuation
* getModelValue to theory engine
* getModelValue to theory
implemented getModelValue in bitvector

the purpose of getModelValue is to ask for a concrete value of a shared term

1 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 389a17461..c5d2845bd 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -83,6 +83,11 @@ EqualityStatus Valuation::getEqualityStatus(TNode a, TNode b) {
   return d_engine->getEqualityStatus(a, b);
 }
 
+Node Valuation::getModelValue(TNode var) {
+  return d_engine->getModelValue(var);
+}
+
+
 Node Valuation::ensureLiteral(TNode n) {
   Debug("ensureLiteral") << "rewriting: " << n << std::endl;
   Node rewritten = Rewriter::rewrite(n);