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, 297 insertions, 0 deletions

diff --git a/src/expr/command.h b/src/expr/command.h
new file mode 100644
index 000000000..dedefb782
--- /dev/null
+++ b/src/expr/command.h
@@ -0,0 +1,297 @@
+/*********************                                           -*- C++ -*-  */
+/** command.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): cconway
+ ** 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 the command pattern on SmtEngines.  Command
+ ** objects are generated by the parser (typically) to implement the
+ ** commands in parsed input (see Parser::parseNextCommand()), or by
+ ** client code.
+ **/
+
+#ifndef __CVC4__COMMAND_H
+#define __CVC4__COMMAND_H
+
+#include <iostream>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "cvc4_config.h"
+#include "expr/expr.h"
+#include "util/result.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+class Command;
+
+inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
+
+class CVC4_PUBLIC Command {
+public:
+  virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
+  virtual ~Command() {};
+  virtual void toStream(std::ostream&) const = 0;
+  std::string toString() const;
+};/* class Command */
+
+class CVC4_PUBLIC EmptyCommand : public Command {
+public:
+  EmptyCommand(std::string name = "");
+  void invoke(CVC4::SmtEngine* smt_engine);
+  void toStream(std::ostream& out) const;
+private:
+  std::string d_name;
+};/* class EmptyCommand */
+
+class CVC4_PUBLIC AssertCommand : public Command {
+public:
+  AssertCommand(const BoolExpr& e);
+  void invoke(CVC4::SmtEngine* smt_engine);
+  void toStream(std::ostream& out) const;
+protected:
+  BoolExpr d_expr;
+};/* class AssertCommand */
+
+class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
+public:
+  DeclarationCommand(const std::vector<std::string>& ids);
+  void toStream(std::ostream& out) const;
+protected:
+  std::vector<std::string> d_declaredSymbols;
+};
+
+class CVC4_PUBLIC CheckSatCommand : public Command {
+public:
+  CheckSatCommand(const BoolExpr& e);
+  void invoke(SmtEngine* smt);
+  Result getResult();
+  void toStream(std::ostream& out) const;
+protected:
+  BoolExpr d_expr;
+  Result d_result;
+};/* class CheckSatCommand */
+
+class CVC4_PUBLIC QueryCommand : public Command {
+public:
+  QueryCommand(const BoolExpr& e);
+  void invoke(SmtEngine* smt);
+  Result getResult();
+  void toStream(std::ostream& out) const;
+protected:
+  BoolExpr d_expr;
+  Result d_result;
+};/* class QueryCommand */
+
+class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
+public:
+  /** The status an SMT benchmark can have */
+  enum BenchmarkStatus {
+    /** Benchmark is satisfiable */
+    SMT_SATISFIABLE,
+    /** Benchmark is unsatisfiable */
+    SMT_UNSATISFIABLE,
+    /** The status of the benchmark is unknown */
+    SMT_UNKNOWN
+  };
+  SetBenchmarkStatusCommand(BenchmarkStatus status);
+  void invoke(SmtEngine* smt);
+  void toStream(std::ostream& out) const;
+protected:
+  BenchmarkStatus d_status;
+};/* class SetBenchmarkStatusCommand */
+
+inline std::ostream& operator<<(std::ostream& out,
+                                SetBenchmarkStatusCommand::BenchmarkStatus bs)
+  CVC4_PUBLIC;
+
+class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
+public:
+  SetBenchmarkLogicCommand(std::string logic);
+  void invoke(SmtEngine* smt);
+  void toStream(std::ostream& out) const;
+protected:
+  std::string d_logic;
+};/* class SetBenchmarkLogicCommand */
+
+class CVC4_PUBLIC CommandSequence : public Command {
+public:
+  CommandSequence();
+  ~CommandSequence();
+  void invoke(SmtEngine* smt);
+  void addCommand(Command* cmd);
+  void toStream(std::ostream& out) const;
+
+  typedef std::vector<Command*>::iterator iterator;
+  typedef std::vector<Command*>::const_iterator const_iterator;
+
+  const_iterator begin() const { return d_commandSequence.begin(); }
+  const_iterator end() const { return d_commandSequence.end(); }
+
+  iterator begin() { return d_commandSequence.begin(); }
+  iterator end() { return d_commandSequence.end(); }
+
+private:
+  /** All the commands to be executed (in sequence) */
+  std::vector<Command*> d_commandSequence;
+  /** Next command to be executed */
+  unsigned int d_index;
+};/* class CommandSequence */
+
+}/* CVC4 namespace */
+
+/* =========== inline function definitions =========== */
+
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+inline std::ostream& operator<<(std::ostream& out, const Command& c) {
+  c.toStream(out);
+  return out;
+}
+
+/* class Command */
+
+inline std::string Command::toString() const {
+  std::stringstream ss;
+  toStream(ss);
+  return ss.str();
+}
+
+/* class EmptyCommand */
+
+inline EmptyCommand::EmptyCommand(std::string name) :
+  d_name(name) {
+}
+
+inline void EmptyCommand::invoke(SmtEngine* smt_engine) {
+}
+
+inline void EmptyCommand::toStream(std::ostream& out) const {
+  out << "EmptyCommand(" << d_name << ")";
+}
+
+/* class AssertCommand */
+
+inline AssertCommand::AssertCommand(const BoolExpr& e) :
+  d_expr(e) {
+}
+
+inline void AssertCommand::invoke(SmtEngine* smt_engine) {
+  smt_engine->assertFormula(d_expr);
+}
+
+inline void AssertCommand::toStream(std::ostream& out) const {
+  out << "Assert(" << d_expr << ")";
+}
+
+/* class CheckSatCommand */
+
+inline CheckSatCommand::CheckSatCommand(const BoolExpr& e) :
+  d_expr(e) {
+}
+
+inline void CheckSatCommand::invoke(SmtEngine* smt_engine) {
+  d_result = smt_engine->checkSat(d_expr);
+}
+
+inline Result CheckSatCommand::getResult() {
+  return d_result;
+}
+
+/* class QueryCommand */
+
+inline QueryCommand::QueryCommand(const BoolExpr& e) :
+  d_expr(e) {
+}
+
+inline void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) {
+  d_result = smt_engine->query(d_expr);
+}
+
+inline Result QueryCommand::getResult() {
+  return d_result;
+}
+
+inline void QueryCommand::toStream(std::ostream& out) const {
+  out << "Query(";
+  d_expr.printAst(out, 0);
+  out << ")";
+}
+
+/* class CommandSequence */
+
+inline CommandSequence::CommandSequence() :
+  d_index(0) {
+}
+
+inline void CommandSequence::addCommand(Command* cmd) {
+  d_commandSequence.push_back(cmd);
+}
+
+/* class DeclarationCommand */
+
+inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) :
+  d_declaredSymbols(ids) {
+}
+
+/* class SetBenchmarkStatusCommand */
+
+inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus s) :
+  d_status(s) {
+}
+
+inline void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) {
+  // FIXME: TODO: something to be done with the status
+}
+
+inline void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
+  out << "SetBenchmarkStatus(" << d_status << ")";
+}
+
+/* class SetBenchmarkLogicCommand */
+
+inline SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string l) :
+  d_logic(l) {
+}
+
+inline void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) {
+  // FIXME: TODO: something to be done with the logic
+}
+
+inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
+  out << "SetBenchmarkLogic(" << d_logic << ")";
+}
+
+/* output stream insertion operator for benchmark statuses */
+inline std::ostream& operator<<(std::ostream& out,
+                                SetBenchmarkStatusCommand::BenchmarkStatus bs) {
+  switch(bs) {
+
+  case SetBenchmarkStatusCommand::SMT_SATISFIABLE:
+    return out << "sat";
+
+  case SetBenchmarkStatusCommand::SMT_UNSATISFIABLE:
+    return out << "unsat";
+
+  case SetBenchmarkStatusCommand::SMT_UNKNOWN:
+    return out << "unknown";
+
+  default:
+    return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]";
+  }
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__COMMAND_H */