diff options
author | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-03-26 16:47:47 -0400 |
---|---|---|
committer | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-03-26 16:47:47 -0400 |
commit | e586b8cdbed537bd2a6cba01f68eb3b34ecf08d8 (patch) | |
tree | ca7be72bdc2c95dd196885d97f029da6e3c2ee13 /src/theory | |
parent | e0cee0f58e1f542a598f2543231c5a8417761d1f (diff) |
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
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 3 | ||||
-rw-r--r-- | src/theory/theory.h | 5 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 6 | ||||
-rw-r--r-- | src/theory/valuation.cpp | 5 | ||||
-rw-r--r-- | src/theory/valuation.h | 5 |
7 files changed, 32 insertions, 1 deletions
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 @@ -516,6 +516,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. * * An implementation of check() is required to either: 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 @@ -97,6 +97,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 * is a Node that can be queried via getSatValue(). |