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

diff --git a/src/expr/kind_epilogue.h b/src/expr/kind_epilogue.h
index 0db7038d83f218911d26b3a8a51f6bb0881c8afe..06f92261b83173a2aae96ba42415b5880c881a97 100644 (file)
--- 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 6c352c3c94ecb8cabecc3c5f37c4cd76be9c9ede..7dee408537fee40112f2a026e4daaab0066cc309 100644 (file)
--- 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 cf9d2e3beec5370cf7624647b79bd6b41c09147c..bdc0ff5995abf862f31b111809572a4a10c23fae 100644 (file)
--- 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 c8ad61571c1dc8a22c39620d3f7f58e2ed3e2978..b0a8f4565594c40a2cd178f73668667a3013b335 100755 (executable)
--- 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 de179edb8c093191a5e956cc0cbac824fd91bc69..d4b40c12df09bdad6af255b85de42202fb56419c 100644 (file)
--- 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 cac72aba780e79a2b777fec91c02c9a01a5b7d52..8cfac4d090cf3a65e4bb963ba6bf82fde3f86b73 100644 (file)
--- 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;