From e586b8cdbed537bd2a6cba01f68eb3b34ecf08d8 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan@cs.nyu.edu>
Date: Tue, 26 Mar 2013 16:47:47 -0400
Subject: 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
---
 src/theory/theory_engine.h | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/theory/theory_engine.h')

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index a3779f0e8..a8fe52498 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -709,6 +709,12 @@ public:
    */
   theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
 
+  /**
+   * Retruns the value that a theory that owns the type of var currently
+   * has (or null if none);
+   */
+  Node getModelValue(TNode var);
+
 private:
 
   /** Default visitor for pre-registration */
-- 
cgit v1.2.3