Made Valuation::getValue() and Valuation::getSatValue() const.

diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 9f33c2c4f365aa4ba6409e484a61eaca197f9fc6..536255c2ddbc57aed11c92a56405d3efc024a8d8 100644 (file)
--- 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 94c2bc12f683949dad05372e0ba8fe1b46473196..0c60ec5eaad81daf9c3b732cf2871319ac83b123 100644 (file)
--- 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 */