diff options
| author | Tim King <taking@cs.nyu.edu> | 2011-04-07 19:28:25 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2011-04-07 19:28:25 +0000 |
| commit | f2696072837541f16932b1fd5f5740d45b4341b9 (patch) | |
| tree | 79eddf644995df24338f75d645981bba3a9cce42 /src | |
| parent | eca82ddc05ff6e81592f7cceec60b0d3269bab5c (diff) | |
Made Valuation::getValue() and Valuation::getSatValue() const.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/valuation.cpp | 4 | ||||
| -rw-r--r-- | src/theory/valuation.h | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 9f33c2c4f..536255c2d 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -23,11 +23,11 @@ namespace CVC4 { namespace theory { -Node Valuation::getValue(TNode n) { +Node Valuation::getValue(TNode n) const { return d_engine->getValue(n); } -Node Valuation::getSatValue(TNode n) { +Node Valuation::getSatValue(TNode n) const{ if(n.getKind() == kind::NOT) { Node atomRes = d_engine->getPropEngine()->getValue(n[0]); if(atomRes.getKind() == kind::CONST_BOOLEAN){ diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 94c2bc12f..0c60ec5ea 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -38,7 +38,7 @@ public: d_engine(engine) { } - Node getValue(TNode n); + Node getValue(TNode n) const; /** * Get the current SAT assignment to the node n. @@ -48,7 +48,7 @@ public: * * @return Node::null() if no current assignment; otherwise true or false. */ - Node getSatValue(TNode n); + Node getSatValue(TNode n) const; };/* class Valuation */ |