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/bv | |
| 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/bv')
| -rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 4 | ||||
| -rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 3 |
2 files changed, 6 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); }; } |