diff options
-rw-r--r-- | src/expr/kind_epilogue.h | 3 | ||||
-rw-r--r-- | src/expr/kind_middle.h | 3 | ||||
-rw-r--r-- | src/expr/kind_prologue.h | 2 | ||||
-rwxr-xr-x | src/expr/mkkind | 1 | ||||
-rw-r--r-- | src/main/main.cpp | 14 | ||||
-rw-r--r-- | src/util/result.h | 8 |
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; |