Merge from my post-smtcomp branch. Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.

1 files changed, 9 insertions, 9 deletions

diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 5002c8a59..9375998f9 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -2,8 +2,8 @@
 /*! \file valuation.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: taking
+ ** Minor contributors (to current version): barrett, dejan
  ** 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
@@ -31,16 +31,12 @@ bool Valuation::isSatLiteral(TNode n) const {
   return d_engine->getPropEngine()->isSatLiteral(n);
 }
 
-bool Valuation::hasSatValue(TNode n, bool& value) const {
-  return d_engine->getPropEngine()->hasValue(n, value);
-}
-
-Node Valuation::getSatValue(TNode n) const{
+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){
+    if(atomRes.getKind() == kind::CONST_BOOLEAN) {
       return NodeManager::currentNM()->mkConst(!atomRes.getConst<bool>());
-    }else{
+    } else {
       Assert(atomRes.isNull());
       return atomRes;
     }
@@ -49,5 +45,9 @@ Node Valuation::getSatValue(TNode n) const{
   }
 }
 
+bool Valuation::hasSatValue(TNode n, bool& value) const {
+  return d_engine->getPropEngine()->hasValue(n, value);
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */