additional work on parser hookup, configuration + build

5 files changed, 86 insertions, 21 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 4fe483c98..c70553c3e 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -4,4 +4,5 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libutil.la
 
-libutil_la_SOURCES =
+libutil_la_SOURCES = \
+	command.cpp
diff --git a/src/util/assert.h b/src/util/assert.h
index 6691c1b04..4a164716c 100644
--- a/src/util/assert.h
+++ b/src/util/assert.h
@@ -20,20 +20,27 @@
 
 namespace CVC4 {
 
-class AssertionException : public Exception {
+class CVC4_PUBLIC AssertionException : public Exception {
 public:
   AssertionException() : Exception() {}
   AssertionException(std::string msg) : Exception(msg) {}
   AssertionException(const char* msg) : Exception(msg) {}
 };/* class AssertionException */
 
-class UnreachableCodeException : public AssertionException {
+class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
 public:
   UnreachableCodeException() : AssertionException() {}
   UnreachableCodeException(std::string msg) : AssertionException(msg) {}
   UnreachableCodeException(const char* msg) : AssertionException(msg) {}
 };/* class UnreachableCodeException */
 
+class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
+public:
+  UnhandledCaseException() : UnreachableCodeException() {}
+  UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {}
+  UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {}
+};/* class UnhandledCaseException */
+
 #ifdef CVC4_ASSERTIONS
 #  define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ":  " #cond, __builtin_expect((cond), 1), ## msg)
 #else /* ! CVC4_ASSERTIONS */
@@ -41,10 +48,12 @@ public:
 #endif /* CVC4_ASSERTIONS */
 
 #define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ":  " #cond, __builtin_expect((cond), 1), ## msg)
-#define Unreachable(cond, msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, __builtin_expect((cond), 1), ## msg)
+#define Unreachable(msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, ## msg)
+#define Unhandled(msg...) __CVC4_UNHANDLEDGLUE("Hit an unhandled case at " __FILE__ ":", __LINE__, ## msg)
 
 #define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg)
-#define __CVC4_UNREACHABLEGLUE(str, line, cond, msg...) AssertImpl(str #line, cond, ## msg)
+#define __CVC4_UNREACHABLEGLUE(str, line, msg...) UnreachableImpl(str #line, ## msg)
+#define __CVC4_UNHANDLEDGLUE(str, line, msg...) UnhandledImpl(str #line, ## msg)
 
 inline void AssertImpl(const char* info, bool cond, std::string msg) {
   if(EXPECT_FALSE( ! cond ))
@@ -79,6 +88,24 @@ inline void UnreachableImpl(const char* info) {
   throw new UnreachableCodeException(info);
 }
 
+#ifdef __GNUC__
+inline void UnhandledImpl(const char* info, std::string msg) __attribute__ ((noreturn));
+inline void UnhandledImpl(const char* info, const char* msg) __attribute__ ((noreturn));
+inline void UnhandledImpl(const char* info) __attribute__ ((noreturn));
+#endif /* __GNUC__ */
+
+inline void UnhandledImpl(const char* info, std::string msg) {
+  throw new UnhandledCaseException(std::string(info) + "\n" + msg);
+}
+
+inline void UnhandledImpl(const char* info, const char* msg) {
+  throw new UnhandledCaseException(std::string(info) + "\n" + msg);
+}
+
+inline void UnhandledImpl(const char* info) {
+  throw new UnhandledCaseException(info);
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__ASSERT_H */
diff --git a/src/util/command.cpp b/src/util/command.cpp
new file mode 100644
index 000000000..db03a9189
--- /dev/null
+++ b/src/util/command.cpp
@@ -0,0 +1,18 @@
+/*********************                                           -*- C++ -*-  */
+/** command.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ **/
+
+#include "util/command.h"
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+
+}/* CVC4 namespace */
diff --git a/src/util/command.h b/src/util/command.h
index 976e2b3d7..6de87c9f2 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -13,39 +13,48 @@
 #define __CVC4__COMMAND_H
 
 #include "expr/expr.h"
+#include "smt/smt_engine.h"
 
 namespace CVC4 {
 
-class SmtEngine;
-
 class Command {
+protected:
   SmtEngine* d_smt;
 
 public:
   Command(CVC4::SmtEngine* smt) : d_smt(smt) {}
+  SmtEngine* getSmtEngine() { return d_smt; }
   virtual void invoke() = 0;
 };
 
 class AssertCommand : public Command {
+protected:
+  Expr d_expr;
+
 public:
-  AssertCommand(const Expr&);
-  void invoke() { }
+  AssertCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {}
+  void invoke() { d_smt->assert(d_expr); }
 };
 
 class CheckSatCommand : public Command {
+protected:
+  Expr d_expr;
+
 public:
-  CheckSatCommand(void);
-  CheckSatCommand(const Expr&);
-  void invoke() { }
+  CheckSatCommand(CVC4::SmtEngine* smt) : Command(smt), d_expr(Expr::null()) {}
+  CheckSatCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {}
+  void invoke() { d_smt->checkSat(d_expr); }
 };
 
 class QueryCommand : public Command {
+protected:
+  Expr d_expr;
+
 public:
-  QueryCommand(const Expr&);
-  void invoke() { }
+  QueryCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {}
+  void invoke() { d_smt->query(d_expr); }
 };
 
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__COMMAND_H */
diff --git a/src/util/exception.h b/src/util/exception.h
index e3b8f2293..76eabe67e 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -15,19 +15,20 @@
 
 #include <string>
 #include <iostream>
+#include "cvc4_config.h"
 
 namespace CVC4 {
 
-class Exception {
+class CVC4_PUBLIC Exception {
 protected:
   std::string d_msg;
 public:
   // Constructors
-  Exception(): d_msg("Unknown exception") { }
-  Exception(const std::string& msg): d_msg(msg) { }
-  Exception(const char* msg): d_msg(msg) { }
+  Exception() : d_msg("Unknown exception") {}
+  Exception(const std::string& msg) : d_msg(msg) {}
+  Exception(const char* msg) : d_msg(msg) {}
   // Destructor
-  virtual ~Exception() { }
+  virtual ~Exception() {}
   // NON-VIRTUAL METHODs for setting and printing the error message
   void setMessage(const std::string& msg) { d_msg = msg; }
   // Printing: feel free to redefine toString().  When inherited,
@@ -36,13 +37,22 @@ public:
   virtual std::string toString() const { return d_msg; }
   // No need to overload operator<< for the inherited classes
   friend std::ostream& operator<<(std::ostream& os, const Exception& e);
+};/* class Exception */
+
+
+class CVC4_PUBLIC IllegalArgumentException : public Exception {
+public:
+  IllegalArgumentException() : Exception("Illegal argument to method or function") {}
+  IllegalArgumentException(const std::string& msg) : Exception(msg) {}
+  IllegalArgumentException(const char* msg) : Exception(msg) {}
+};/* class IllegalArgumentException */
 
-}; // end of class Exception
 
 inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
   return os << e.toString();
 }
 
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXCEPTION_H */