src/expr/kind.h is now automatically generated.

Build src/expr before src/util.

Moved CVC4::Command to the expr package.

Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).

Added file-level documentation to Antlr sources

When built for debug, spin on SEGV instead of aborting.  Really useful
for debugging problems that crop up only on long runs.  Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.

Updated src/main/about.h for 2010.

1 files changed, 74 insertions, 0 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
new file mode 100644
index 000000000..2f8dd789e
--- /dev/null
+++ b/src/expr/command.cpp
@@ -0,0 +1,74 @@
+/*********************                                           -*- C++ -*-  */
+/** command.cpp
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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.
+ **
+ ** Implementation of command objects.
+ **/
+
+#include "expr/command.h"
+#include "smt/smt_engine.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+ostream& operator<<(ostream& out, const Command* c) {
+  if (c == NULL) {
+    out << "null";
+  } else {
+    c->toStream(out);
+  }
+  return out;
+}
+
+CommandSequence::~CommandSequence() {
+  for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+    delete d_commandSequence[i];
+  }
+}
+
+void CommandSequence::invoke(SmtEngine* smtEngine) {
+  for(; d_index < d_commandSequence.size(); ++d_index) {
+    d_commandSequence[d_index]->invoke(smtEngine);
+    delete d_commandSequence[d_index];
+  }
+}
+
+void CheckSatCommand::toStream(ostream& out) const {
+  if(d_expr.isNull()) {
+    out << "CheckSat()";
+  } else {
+    out << "CheckSat(" << d_expr << ")";
+  }
+}
+
+void CommandSequence::toStream(ostream& out) const {
+  out << "CommandSequence[" << endl;
+  for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+    out << *d_commandSequence[i] << endl;
+  }
+  out << "]";
+}
+
+void DeclarationCommand::toStream(std::ostream& out) const {
+  out << "Declare(";
+  bool first = true;
+  for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) {
+    if(!first) {
+      out << ", ";
+    }
+    out << d_declaredSymbols[i];
+    first = false;
+  }
+  out << ")";
+}
+
+}/* CVC4 namespace */