work on propositional layer, expression builder support for large expressions, output classes, and minisat

8 files changed, 172 insertions, 66 deletions

diff --git a/src/util/assert.h b/src/util/Assert.h
index 8fd970c6c..8fd970c6c 100644
--- a/src/util/assert.h
+++ b/src/util/Assert.h
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index c70553c3e..8baf872d2 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -5,4 +5,6 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libutil.la
 
 libutil_la_SOURCES = \
-	command.cpp
+	command.cpp \
+	decision_engine.cpp \
+	output.cpp
diff --git a/src/util/command.cpp b/src/util/command.cpp
index 190f794da..c78fbc089 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -31,7 +31,7 @@ AssertCommand::AssertCommand(const Expr& e) :
 }
 
 void AssertCommand::invoke(SmtEngine* smt_engine) {
-  smt_engine->assert(d_expr);
+  smt_engine->assertFormula(d_expr);
 }
 
 CheckSatCommand::CheckSatCommand() {
diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp
new file mode 100644
index 000000000..ae79f920d
--- /dev/null
+++ b/src/util/decision_engine.cpp
@@ -0,0 +1,29 @@
+/*********************                                           -*- C++ -*-  */
+/** decision_engine.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/decision_engine.h"
+#include "util/Assert.h"
+#include "util/literal.h"
+
+namespace CVC4 {
+
+DecisionEngine::~DecisionEngine() {
+}
+
+/**
+ * Only here to permit compilation and linkage.  This may be pure
+ * virtual in the final design (?)
+ */
+Literal DecisionEngine::nextDecision() {
+  Unreachable();
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h
index a6f8596dd..3a093211c 100644
--- a/src/util/decision_engine.h
+++ b/src/util/decision_engine.h
@@ -12,6 +12,7 @@
 #ifndef __CVC4__DECISION_ENGINE_H
 #define __CVC4__DECISION_ENGINE_H
 
+#include "cvc4_config.h"
 #include "util/literal.h"
 
 namespace CVC4 {
@@ -22,12 +23,17 @@ namespace CVC4 {
 /**
  * A decision mechanism for the next decision.
  */
-class DecisionEngine {
+class CVC4_PUBLIC DecisionEngine {
 public:
   /**
+   * Destructor.
+   */
+  virtual ~DecisionEngine();
+
+  /**
    * Get the next decision.
    */
-  virtual Literal nextDecision() = 0;
+  virtual Literal nextDecision();// = 0
 
   // TODO: design decision: decision engine should be notified of
   // propagated lits, and also why(?) (so that it can make decisions
diff --git a/src/util/literal.h b/src/util/literal.h
index 7af9826bb..3ec216a6a 100644
--- a/src/util/literal.h
+++ b/src/util/literal.h
@@ -14,7 +14,8 @@
 
 namespace CVC4 {
 
-class Literal;
+class Literal {
+};
 
 }/* CVC4 namespace */
 
diff --git a/src/util/output.cpp b/src/util/output.cpp
new file mode 100644
index 000000000..e07f32a66
--- /dev/null
+++ b/src/util/output.cpp
@@ -0,0 +1,29 @@
+/*********************                                           -*- C++ -*-  */
+/** output.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.
+ **
+ ** Output utility classes and functions.
+ **/
+
+#include "cvc4_config.h"
+
+#include <iostream>
+#include "util/output.h"
+
+namespace CVC4 {
+
+null_streambuf null_sb;
+std::ostream null_os(&null_sb);
+
+DebugC   Debug  (&std::cout);
+WarningC Warning(&std::cerr);
+NoticeC  Notice (&std::cout);
+ChatC    Chat   (&std::cout);
+TraceC   Trace  (&std::cout);
+
+}/* CVC4 namespace */
diff --git a/src/util/output.h b/src/util/output.h
index 21b7b6e4c..b6532b93a 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -13,125 +13,164 @@
 #ifndef __CVC4__OUTPUT_H
 #define __CVC4__OUTPUT_H
 
+#include "cvc4_config.h"
+
 #include <iostream>
 #include <string>
+#include <cstdio>
+#include <cstdarg>
 #include <set>
+
 #include "util/exception.h"
 
 namespace CVC4 {
 
-class Debug {
+class null_streambuf : public std::streambuf {
+public:
+  int overflow(int c) { return c; }
+};/* class null_streambuf */
+
+extern null_streambuf null_sb;
+extern std::ostream null_os CVC4_PUBLIC;
+
+class CVC4_PUBLIC DebugC {
   std::set<std::string> d_tags;
-  std::ostream &d_out;
+  std::ostream *d_os;
 
 public:
-  static void operator()(const char* tag, const char*);
-  static void operator()(const char* tag, std::string);
-  static void operator()(string tag, const char*);
-  static void operator()(string tag, std::string);
-  static void operator()(const char*);// Yeting option
-  static void operator()(std::string);// Yeting option
+  DebugC(std::ostream* os) : d_os(os) {}
+
+  void operator()(const char* tag, const char*);
+  void operator()(const char* tag, std::string);
+  void operator()(std::string tag, const char*);
+  void operator()(std::string tag, std::string);
+  //void operator()(const char*);// Yeting option
+  //void operator()(std::string);// Yeting option
 
   static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
-  static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
   static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
-  static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
   // Yeting option not possible here
 
-  static std::ostream& operator()(const char* tag);
-  static std::ostream& operator()(std::string tag);
-  static std::ostream& operator()();// Yeting option
+  std::ostream& operator()(const char* tag) {
+    if(d_tags.find(tag) != d_tags.end())
+      return *d_os;
+    else return null_os;
+  }
+  std::ostream& operator()(std::string tag) {
+    if(d_tags.find(tag) != d_tags.end())
+      return *d_os;
+    else return null_os;
+  }
+  std::ostream& operator()();// Yeting option
 
-  static void on (const char* tag) { d_tags.insert(std::string(tag)); }
-  static void on (std::string tag) { d_tags.insert(tag);              }
-  static void off(const char* tag) { d_tags.erase (std::string(tag)); }
-  static void off(std::string tag) { d_tags.erase (tag);              }
+  void on (const char* tag) { d_tags.insert(std::string(tag)); }
+  void on (std::string tag) { d_tags.insert(tag);              }
+  void off(const char* tag) { d_tags.erase (std::string(tag)); }
+  void off(std::string tag) { d_tags.erase (tag);              }
 
-  static void setStream(std::ostream& os) { d_out = os; }
+  void setStream(std::ostream& os) { d_os = &os; }
 };/* class Debug */
 
+extern DebugC Debug CVC4_PUBLIC;
 
-class Warning {
-  std::ostream &d_out;
+class CVC4_PUBLIC WarningC {
+  std::ostream *d_os;
 
 public:
-  static void operator()(const char*);
-  static void operator()(std::string);
+  WarningC(std::ostream* os) : d_os(os) {}
 
-  static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
-  static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  void operator()(const char* s) { *d_os << s; }
+  void operator()(std::string s) { *d_os << s; }
 
-  static std::ostream& operator()();
+  void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
-  static void setStream(std::ostream& os) { d_out = os; }
+  std::ostream& operator()() { return *d_os; }
+
+  void setStream(std::ostream& os) { d_os = &os; }
 };/* class Warning */
 
+extern WarningC Warning CVC4_PUBLIC;
 
-class Notice {
-  std::ostream &d_os;
+class CVC4_PUBLIC NoticeC {
+  std::ostream *d_os;
 
 public:
-  static void operator()(const char*);
-  static void operator()(std::string);
+  NoticeC(std::ostream* os) : d_os(os) {}
+
+  void operator()(const char*);
+  void operator()(std::string);
 
-  static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
-  static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
-  static std::ostream& operator()();
+  std::ostream& operator()() { return *d_os; }
 
-  static void setStream(std::ostream& os) { d_out = os; }
+  void setStream(std::ostream& os) { d_os = &os; }
 };/* class Notice */
 
+extern NoticeC Notice CVC4_PUBLIC;
 
-class Chat {
-  std::ostream &d_os;
+class CVC4_PUBLIC ChatC {
+  std::ostream *d_os;
 
 public:
-  static void operator()(const char*);
-  static void operator()(std::string);
+  ChatC(std::ostream* os) : d_os(os) {}
 
-  static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
-  static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  void operator()(const char*);
+  void operator()(std::string);
 
-  static std::ostream& operator()();
+  void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
-  static void setStream(std::ostream& os) { d_out = os; }
+  std::ostream& operator()() { return *d_os; }
+
+  void setStream(std::ostream& os) { d_os = &os; }
 };/* class Chat */
 
+extern ChatC Chat CVC4_PUBLIC;
 
-class Trace {
-  std::ostream &d_os;
+class CVC4_PUBLIC TraceC {
+  std::ostream *d_os;
+  std::set<std::string> d_tags;
 
 public:
-  static void operator()(const char* tag, const char*);
-  static void operator()(const char* tag, std::string);
-  static void operator()(string tag, const char*);
-  static void operator()(string tag, std::string);
+  TraceC(std::ostream* os) : d_os(os) {}
 
-  static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+  void operator()(const char* tag, const char*);
+  void operator()(const char* tag, std::string);
+  void operator()(std::string tag, const char*);
+  void operator()(std::string tag, std::string);
+
+  void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {
+    char buf[1024];
     va_list vl;
     va_start(vl, fmt);
-    vfprintf(buf, 1024, fmt, vl);
+    vsnprintf(buf, sizeof(buf), fmt, vl);
     va_end(vl);
+    *d_os << buf;
   }
-  static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) {
-  }
-  static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+  void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {
   }
-  static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+
+  std::ostream& operator()(const char* tag) {
+    if(d_tags.find(tag) != d_tags.end())
+      return *d_os;
+    else return null_os;
   }
 
-  static std::ostream& operator()(const char* tag);
-  static std::ostream& operator()(std::string tag);
+  std::ostream& operator()(std::string tag) {
+    if(d_tags.find(tag) != d_tags.end())
+      return *d_os;
+    else return null_os;
+  }
 
-  static void on (const char* tag) { d_tags.insert(std::string(tag)); };
-  static void on (std::string tag) { d_tags.insert(tag);              };
-  static void off(const char* tag) { d_tags.erase (std::string(tag)); };
-  static void off(std::string tag) { d_tags.erase (tag);              };
+  void on (const char* tag) { d_tags.insert(std::string(tag)); };
+  void on (std::string tag) { d_tags.insert(tag);              };
+  void off(const char* tag) { d_tags.erase (std::string(tag)); };
+  void off(std::string tag) { d_tags.erase (tag);              };
 
-  static void setStream(std::ostream& os) { d_out = os; }
+  void setStream(std::ostream& os) { d_os = &os; }
 };/* class Trace */
 
+extern TraceC Trace CVC4_PUBLIC;
 
 }/* CVC4 namespace */