From: Dejan Jovanović <dejan@cs.nyu.edu>
Date: Tue, 26 Mar 2013 20:47:47 +0000 (-0400)
Subject: adding
X-Git-Tag: cvc5-1.0.0~7366
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e586b8cdbed537bd2a6cba01f68eb3b34ecf08d8;p=cvc5.git

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 501aafb29..f48a03975 100644
--- 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 3396d813b..510006710 100644
--- 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 5b2032430..94cf9accd 100644
--- 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 f7f689850..b89ca8fa4 100644
--- 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 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 */
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);
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index f69bacc19..36e62a402 100644
--- 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