minor cleanup; give the main driver a different exit code for SAT-INVALID/UNSAT-VALID

6 files changed, 23 insertions, 8 deletions

diff --git a/src/expr/kind_epilogue.h b/src/expr/kind_epilogue.h
index 0db7038d8..06f92261b 100644
--- a/src/expr/kind_epilogue.h
+++ b/src/expr/kind_epilogue.h
@@ -10,7 +10,8 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Kinds of Nodes.
+ ** Epilogue for the Node kind header.  This file finishes off the
+ ** pretty-printing function for the Kind enum.
  **/
 
   case LAST_KIND: out << "LAST_KIND"; break;
diff --git a/src/expr/kind_middle.h b/src/expr/kind_middle.h
index 6c352c3c9..7dee40853 100644
--- a/src/expr/kind_middle.h
+++ b/src/expr/kind_middle.h
@@ -10,7 +10,8 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Kinds of Nodes.
+ ** Middle section of the Node kind header.  This file finishes off the
+ ** Kind enum and starts the pretty-printing function definition.
  **/
 
   LAST_KIND
diff --git a/src/expr/kind_prologue.h b/src/expr/kind_prologue.h
index cf9d2e3be..bdc0ff599 100644
--- a/src/expr/kind_prologue.h
+++ b/src/expr/kind_prologue.h
@@ -10,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Kinds of Nodes.
+ ** Prologue of the Node kind header.  This file starts the Kind enumeration.
  **/
 
 #ifndef __CVC4__KIND_H
diff --git a/src/expr/mkkind b/src/expr/mkkind
index c8ad61571..b0a8f4565 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -24,7 +24,6 @@ cat <<EOF
  **     $0 $@
  **
  ** for the CVC4 project.
- **
  **/
 
 EOF
diff --git a/src/main/main.cpp b/src/main/main.cpp
index de179edb8..d4b40c12d 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -148,8 +148,18 @@ int main(int argc, char *argv[]) {
     abort();
   }
 
-  // TODO: adjust return value based on lastResult
-  return 0;
+  switch(lastResult.asSatisfiabilityResult().isSAT()) {
+
+  case Result::SAT:
+    return 10;
+
+  case Result::UNSAT:
+    return 20;
+
+  default:
+    return 0;
+
+  }
 }
 
 void doCommand(SmtEngine& smt, Command* cmd) {
diff --git a/src/util/result.h b/src/util/result.h
index cac72aba7..8cfac4d09 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -75,8 +75,12 @@ public:
     d_which(TYPE_VALIDITY) {
   }
 
-  enum SAT isSAT();
-  enum Validity isValid();
+  enum SAT isSAT() {
+    return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
+  }
+  enum Validity isValid() {
+    return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
+  }
   enum UnknownExplanation whyUnknown();
 
   inline Result asSatisfiabilityResult() const;