4 files changed, 48 insertions, 10 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 787323495..b773a84ee 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -2,10 +2,10 @@
 /*! \file theory_engine.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: dejan, taking
+ ** Major contributors: taking, dejan
  ** Minor contributors (to current version): cconway, barrett
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -191,6 +191,13 @@ public:
   }
 
   /**
+   * Get a pointer to the underlying propositional engine.
+   */
+  prop::PropEngine* getPropEngine() const {
+    return d_propEngine;
+  }
+
+  /**
    * Return whether or not we are incomplete (in the current context).
    */
   bool isIncomplete() {
diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h
index 067fe55d0..c6541dbea 100644
--- a/src/theory/theory_traits_template.h
+++ b/src/theory/theory_traits_template.h
@@ -1,12 +1,25 @@
-/*
- * theory_traits_template.h
- *
- *  Created on: Dec 23, 2010
- *      Author: dejan
- */
+/*********************                                                        */
+/*! \file theory_traits_template.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #pragma once
 
+#include "cvc4_private.h"
 #include "theory/theory.h"
 
 ${theory_includes}
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 20d339b52..1f82f1404 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -27,5 +27,13 @@ Node Valuation::getValue(TNode n) {
   return d_engine->getValue(n);
 }
 
+Node Valuation::getSatValue(TNode n) {
+  if(n.getKind() == kind::NOT) {
+    return NodeManager::currentNM()->mkConst(! d_engine->getPropEngine()->getValue(n[0]).getConst<bool>());
+  } else {
+    return d_engine->getPropEngine()->getValue(n);
+  }
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 2d38c29cd..94c2bc12f 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -40,6 +40,16 @@ public:
 
   Node getValue(TNode n);
 
+  /**
+   * Get the current SAT assignment to the node n.
+   *
+   * This is only permitted if n is a theory atom that has an associated
+   * SAT literal (or its negation).
+   *
+   * @return Node::null() if no current assignment; otherwise true or false.
+   */
+  Node getSatValue(TNode n);
+
 };/* class Valuation */
 
 }/* CVC4::theory namespace */