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

diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 501aafb291d8da6109b9e19068c12e7ed56e03df..f48a03975167ec6ae5b3aac3e15b92c511613fed 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -127,3 +127,7 @@ EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
 void BitblastSolver::collectModelInfo(TheoryModel* m) {
   return d_bitblaster->collectModelInfo(m); 
 }
+
+Node BitblastSolver::getModelValue(TNode node) {
+  return d_bitblaster->getVarValue(node);
+}

diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 3396d813b290cbd26c9ef6ec2f5221f268f975e8..5100067107aea7ff1e40dbe9f4fa046e95dbad1d 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -45,7 +45,8 @@ public:
   bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
-  void collectModelInfo(TheoryModel* m); 
+  void collectModelInfo(TheoryModel* m);
+  Node getModelValue(TNode node);
 };
 
 }

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 5b20324303938ff0bf9d1fc62df6ca022c0302c7..94cf9accd75c2d930626d57880ddf68d7ef377a9 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -515,6 +515,11 @@ public:
    */
   virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; }
 
+  /**
+   * Return the model value of the give shared term (or null if not avalilable.
+   */
+  virtual Node getModelValue(TNode var) { return Node::null(); }
+
   /**
    * Check the current assignment's consistency.
    *

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f7f68985041ced855f143433993340c31bd19e77..b89ca8fa43e2e112ea8f23775c206bfecdb1540f 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1129,6 +1129,11 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
 }
 
+Node TheoryEngine::getModelValue(TNode var) {
+  Assert(d_sharedTerms.isShared(var));
+  return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
+}
+
 static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
 
   std::set<TNode> all;

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index a3779f0e888ac5e2f1c3c443cebac027ea545d26..a8fe52498384b6f2f28297d20b3a41496ede07d8 100644 (file)
--- 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 */

diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 389a1746111c2b84fcacfa14574b4279ed7fe661..c5d2845bdcb70d125fa7ac36277153165de0ca6c 100644 (file)
--- 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);

diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index f69bacc19fcadee83525d2d55f88e1ce6ef97b20..36e62a402233895ea04c3035141f5fa842d68d30 100644 (file)
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -96,6 +96,11 @@ public:
    */
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
+  /**
+   * Returns the model value of the shared term (or null if not available).
+   */
+  Node getModelValue(TNode var);
+
   /**
    * Ensure that the given node will have a designated SAT literal
    * that is definitionally equal to it.  The result of this function