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

diff --git a/src/util/command.h b/src/util/command.h
deleted file mode 100644
index 81af801d1..000000000
--- a/src/util/command.h
+++ /dev/null
@@ -1,301 +0,0 @@
-/*********************                                           -*- 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();
-  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() {
-}
-
-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 */