Add SmtGlobals Class

- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.

4 files changed, 0 insertions, 558 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 63f31ed67..d4964f56a 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -70,8 +70,6 @@ libexpr_la_SOURCES = \
 	predicate.cpp \
 	record.cpp \
 	record.h \
-	result.cpp \
-	result.h \
 	uninterpreted_constant.cpp \
 	uninterpreted_constant.h
 
@@ -113,7 +111,6 @@ EXTRA_DIST = \
 	resource_manager.i \
 	sexpr.i \
 	record.i \
-	result.i \
 	predicate.i \
 	variable_type_map.i \
 	uninterpreted_constant.i
diff --git a/src/expr/result.cpp b/src/expr/result.cpp
deleted file mode 100644
index aeb62b0c3..000000000
--- a/src/expr/result.cpp
+++ /dev/null
@@ -1,358 +0,0 @@
-/*********************                                                        */
-/*! \file result.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Encapsulation of the result of a query.
- **
- ** Encapsulation of the result of a query.
- **/
-#include "expr/result.h"
-
-#include <algorithm>
-#include <cctype>
-#include <iostream>
-#include <string>
-
-#include "base/cvc4_assert.h"
-#include "expr/node.h"
-
-using namespace std;
-
-#warning "TODO: Move Node::setLanguage out of Node and into util/. Then move Result back into util/."
-
-namespace CVC4 {
-
-Result::Result()
-    : d_sat(SAT_UNKNOWN)
-    , d_validity(VALIDITY_UNKNOWN)
-    , d_which(TYPE_NONE)
-    , d_unknownExplanation(UNKNOWN_REASON)
-    , d_inputName("")
-{ }
-
-
-Result::Result(enum Sat s, std::string inputName)
-    : d_sat(s)
-    , d_validity(VALIDITY_UNKNOWN)
-    , d_which(TYPE_SAT)
-    , d_unknownExplanation(UNKNOWN_REASON)
-    , d_inputName(inputName)
-{
-  PrettyCheckArgument(s != SAT_UNKNOWN,
-                      "Must provide a reason for satisfiability being unknown");
-}
-
-Result::Result(enum Validity v, std::string inputName)
-    : d_sat(SAT_UNKNOWN)
-    , d_validity(v)
-    , d_which(TYPE_VALIDITY)
-    , d_unknownExplanation(UNKNOWN_REASON)
-    , d_inputName(inputName)
-{
-  PrettyCheckArgument(v != VALIDITY_UNKNOWN,
-                      "Must provide a reason for validity being unknown");
-}
-
-
-Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation,
-               std::string inputName)
-    : d_sat(s)
-    , d_validity(VALIDITY_UNKNOWN)
-    , d_which(TYPE_SAT)
-    , d_unknownExplanation(unknownExplanation)
-    , d_inputName(inputName)
-{
-  PrettyCheckArgument(s == SAT_UNKNOWN,
-                      "improper use of unknown-result constructor");
-}
-
-Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation,
-               std::string inputName)
-    : d_sat(SAT_UNKNOWN)
-    , d_validity(v)
-    , d_which(TYPE_VALIDITY)
-    , d_unknownExplanation(unknownExplanation)
-    , d_inputName(inputName)
-{
-  PrettyCheckArgument(v == VALIDITY_UNKNOWN,
-                      "improper use of unknown-result constructor");
-}
-
-Result::Result(const std::string& instr, std::string inputName) :
-  d_sat(SAT_UNKNOWN),
-  d_validity(VALIDITY_UNKNOWN),
-  d_which(TYPE_NONE),
-  d_unknownExplanation(UNKNOWN_REASON),
-  d_inputName(inputName) {
-  string s = instr;
-  transform(s.begin(), s.end(), s.begin(), ::tolower);
-  if(s == "sat" || s == "satisfiable") {
-    d_which = TYPE_SAT;
-    d_sat = SAT;
-  } else if(s == "unsat" || s == "unsatisfiable") {
-    d_which = TYPE_SAT;
-    d_sat = UNSAT;
-  } else if(s == "valid") {
-    d_which = TYPE_VALIDITY;
-    d_validity = VALID;
-  } else if(s == "invalid") {
-    d_which = TYPE_VALIDITY;
-    d_validity = INVALID;
-  } else if(s == "incomplete") {
-    d_which = TYPE_SAT;
-    d_sat = SAT_UNKNOWN;
-    d_unknownExplanation = INCOMPLETE;
-  } else if(s == "timeout") {
-    d_which = TYPE_SAT;
-    d_sat = SAT_UNKNOWN;
-    d_unknownExplanation = TIMEOUT;
-  } else if(s == "resourceout") {
-    d_which = TYPE_SAT;
-    d_sat = SAT_UNKNOWN;
-    d_unknownExplanation = RESOURCEOUT;
-  } else if(s == "memout") {
-    d_which = TYPE_SAT;
-    d_sat = SAT_UNKNOWN;
-    d_unknownExplanation = MEMOUT;
-  } else if(s == "interrupted") {
-    d_which = TYPE_SAT;
-    d_sat = SAT_UNKNOWN;
-    d_unknownExplanation = INTERRUPTED;
-  } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
-    d_which = TYPE_SAT;
-    d_sat = SAT_UNKNOWN;
-  } else {
-    IllegalArgument(s, "expected satisfiability/validity result, "
-                    "instead got `%s'", s.c_str());
-  }
-}
-
-Result::UnknownExplanation Result::whyUnknown() const {
-  PrettyCheckArgument( isUnknown(), this,
-                       "This result is not unknown, so the reason for "
-                       "being unknown cannot be inquired of it" );
-  return d_unknownExplanation;
-}
-
-bool Result::operator==(const Result& r) const throw() {
-  if(d_which != r.d_which) {
-    return false;
-  }
-  if(d_which == TYPE_SAT) {
-    return d_sat == r.d_sat &&
-      ( d_sat != SAT_UNKNOWN ||
-        d_unknownExplanation == r.d_unknownExplanation );
-  }
-  if(d_which == TYPE_VALIDITY) {
-    return d_validity == r.d_validity &&
-      ( d_validity != VALIDITY_UNKNOWN ||
-        d_unknownExplanation == r.d_unknownExplanation );
-  }
-  return false;
-}
-
-bool operator==(enum Result::Sat sr, const Result& r) throw() {
-  return r == sr;
-}
-
-bool operator==(enum Result::Validity vr, const Result& r) throw() {
-  return r == vr;
-}
-bool operator!=(enum Result::Sat s, const Result& r) throw(){
-  return !(s == r);
-}
-bool operator!=(enum Result::Validity v, const Result& r) throw(){
-  return !(v == r);
-}
-
-Result Result::asSatisfiabilityResult() const throw() {
-  if(d_which == TYPE_SAT) {
-    return *this;
-  }
-
-  if(d_which == TYPE_VALIDITY) {
-    switch(d_validity) {
-
-    case INVALID:
-      return Result(SAT, d_inputName);
-
-    case VALID:
-      return Result(UNSAT, d_inputName);
-
-    case VALIDITY_UNKNOWN:
-      return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
-
-    default:
-      Unhandled(d_validity);
-    }
-  }
-
-  // TYPE_NONE
-  return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
-}
-
-Result Result::asValidityResult() const throw() {
-  if(d_which == TYPE_VALIDITY) {
-    return *this;
-  }
-
-  if(d_which == TYPE_SAT) {
-    switch(d_sat) {
-
-    case SAT:
-      return Result(INVALID, d_inputName);
-
-    case UNSAT:
-      return Result(VALID, d_inputName);
-
-    case SAT_UNKNOWN:
-      return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
-
-    default:
-      Unhandled(d_sat);
-    }
-  }
-
-  // TYPE_NONE
-  return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName);
-}
-
-string Result::toString() const {
-  stringstream ss;
-  ss << *this;
-  return ss.str();
-}
-
-ostream& operator<<(ostream& out, enum Result::Sat s) {
-  switch(s) {
-  case Result::UNSAT: out << "UNSAT"; break;
-  case Result::SAT: out << "SAT"; break;
-  case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break;
-  default: Unhandled(s);
-  }
-  return out;
-}
-
-ostream& operator<<(ostream& out, enum Result::Validity v) {
-  switch(v) {
-  case Result::INVALID: out << "INVALID"; break;
-  case Result::VALID: out << "VALID"; break;
-  case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break;
-  default: Unhandled(v);
-  }
-  return out;
-}
-
-ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) {
-  switch(e) {
-  case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break;
-  case Result::INCOMPLETE: out << "INCOMPLETE"; break;
-  case Result::TIMEOUT: out << "TIMEOUT"; break;
-  case Result::RESOURCEOUT: out << "RESOURCEOUT"; break;
-  case Result::MEMOUT: out << "MEMOUT"; break;
-  case Result::INTERRUPTED: out << "INTERRUPTED"; break;
-  case Result::NO_STATUS: out << "NO_STATUS"; break;
-  case Result::UNSUPPORTED: out << "UNSUPPORTED"; break;
-  case Result::OTHER: out << "OTHER"; break;
-  case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
-  default: Unhandled(e);
-  }
-  return out;
-}
-
-ostream& operator<<(ostream& out, const Result& r) {
-  r.toStream(out, Node::setlanguage::getLanguage(out));
-  return out;
-}/* operator<<(ostream&, const Result&) */
-
-
-void Result::toStreamDefault(std::ostream& out) const throw() {
-  if(getType() == Result::TYPE_SAT) {
-    switch(isSat()) {
-    case Result::UNSAT:
-      out << "unsat";
-      break;
-    case Result::SAT:
-      out << "sat";
-      break;
-    case Result::SAT_UNKNOWN:
-      out << "unknown";
-      if(whyUnknown() != Result::UNKNOWN_REASON) {
-        out << " (" << whyUnknown() << ")";
-      }
-      break;
-    }
-  } else {
-    switch(isValid()) {
-    case Result::INVALID:
-      out << "invalid";
-      break;
-    case Result::VALID:
-      out << "valid";
-      break;
-    case Result::VALIDITY_UNKNOWN:
-      out << "unknown";
-      if(whyUnknown() != Result::UNKNOWN_REASON) {
-        out << " (" << whyUnknown() << ")";
-      }
-      break;
-    }
-  }
-}/* Result::toStreamDefault() */
-
-
-void Result::toStreamSmt2(ostream& out) const throw(){
-  if(getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) {
-    out << "unknown";
-  } else {
-    toStreamDefault(out);
-  }
-}
-
-void Result::toStreamTptp(std::ostream& out) const throw() {
-  out << "% SZS status ";
-  if(isSat() == Result::SAT) {
-    out << "Satisfiable";
-  } else if(isSat() == Result::UNSAT) {
-    out << "Unsatisfiable";
-  } else if(isValid() == Result::VALID) {
-    out << "Theorem";
-  } else if(isValid() == Result::INVALID) {
-    out << "CounterSatisfiable";
-  } else {
-    out << "GaveUp";
-  }
-  out << " for " << getInputName();
-}
-
-void Result::toStream(std::ostream& out, OutputLanguage language) const throw() {
-  switch(language) {
-  case language::output::LANG_SMTLIB_V2_0:
-  case language::output::LANG_SMTLIB_V2_5:
-  case language::output::LANG_SYGUS:
-  case language::output::LANG_Z3STR:
-    toStreamSmt2(out);
-    break;
-  case language::output::LANG_TPTP:
-    toStreamTptp(out);
-    break;
-  case language::output::LANG_AST:
-  case language::output::LANG_AUTO:
-  case language::output::LANG_CVC3:
-  case language::output::LANG_CVC4:
-  case language::output::LANG_MAX:
-  case language::output::LANG_SMTLIB_V1:
-  default:
-    toStreamDefault(out);
-    break;
-  };
-}
-
-}/* CVC4 namespace */
diff --git a/src/expr/result.h b/src/expr/result.h
deleted file mode 100644
index 8069f7ef9..000000000
--- a/src/expr/result.h
+++ /dev/null
@@ -1,177 +0,0 @@
-/*********************                                                        */
-/*! \file result.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Encapsulation of the result of a query.
- **
- ** Encapsulation of the result of a query.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__RESULT_H
-#define __CVC4__RESULT_H
-
-#include <iostream>
-#include <string>
-
-#include "base/exception.h"
-#include "options/language.h"
-
-namespace CVC4 {
-
-class Result;
-
-std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC;
-
-/**
- * Three-valued SMT result, with optional explanation.
- */
-class CVC4_PUBLIC Result {
-public:
-  enum Sat {
-    UNSAT = 0,
-    SAT = 1,
-    SAT_UNKNOWN = 2
-  };
-
-  enum Validity {
-    INVALID = 0,
-    VALID = 1,
-    VALIDITY_UNKNOWN = 2
-  };
-
-  enum Type {
-    TYPE_SAT,
-    TYPE_VALIDITY,
-    TYPE_NONE
-  };
-
-  enum UnknownExplanation {
-    REQUIRES_FULL_CHECK,
-    INCOMPLETE,
-    TIMEOUT,
-    RESOURCEOUT,
-    MEMOUT,
-    INTERRUPTED,
-    NO_STATUS,
-    UNSUPPORTED,
-    OTHER,
-    UNKNOWN_REASON
-  };
-
-private:
-  enum Sat d_sat;
-  enum Validity d_validity;
-  enum Type d_which;
-  enum UnknownExplanation d_unknownExplanation;
-  std::string d_inputName;
-
-public:
-
-  Result();
-
-  Result(enum Sat s, std::string inputName = "");
-
-  Result(enum Validity v, std::string inputName = "");
-
-  Result(enum Sat s,
-         enum UnknownExplanation unknownExplanation,
-         std::string inputName = "");
-
-  Result(enum Validity v, enum UnknownExplanation unknownExplanation,
-         std::string inputName = "");
-
-  Result(const std::string& s, std::string inputName = "");
-
-  Result(const Result& r, std::string inputName) {
-    *this = r;
-    d_inputName = inputName;
-  }
-
-  enum Sat isSat() const {
-    return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
-  }
-
-  enum Validity isValid() const {
-    return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
-  }
-
-  bool isUnknown() const {
-    return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
-  }
-
-  Type getType() const {
-    return d_which;
-  }
-
-  bool isNull() const {
-    return d_which == TYPE_NONE;
-  }
-
-  enum UnknownExplanation whyUnknown() const;
-
-  bool operator==(const Result& r) const throw();
-  inline bool operator!=(const Result& r) const throw();
-  Result asSatisfiabilityResult() const throw();
-  Result asValidityResult() const throw();
-
-  std::string toString() const;
-
-  std::string getInputName() const { return d_inputName; }
-
-  /**
-   * Write a Result out to a stream in this language.
-   */
-  void toStream(std::ostream& out, OutputLanguage language) const throw();
-
-  /**
-   * This is mostly the same the default
-   * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN,
-   *
-   */
-  void toStreamSmt2(std::ostream& out) const throw();
-
-  /**
-   * Write a Result out to a stream in the Tptp format
-   */
-  void toStreamTptp(std::ostream& out) const throw();
-
-  /**
-   * Write a Result out to a stream.
-   *
-   * The default implementation writes a reasonable string in lowercase
-   * for sat, unsat, valid, invalid, or unknown results.  This behavior
-   * is overridable by each Printer, since sometimes an output language
-   * has a particular preference for how results should appear.
-   */
-  void toStreamDefault(std::ostream& out) const throw();
-};/* class Result */
-
-inline bool Result::operator!=(const Result& r) const throw() {
-  return !(*this == r);
-}
-
-std::ostream& operator<<(std::ostream& out,
-                         enum Result::Sat s) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& out,
-                         enum Result::Validity v) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& out,
-                         enum Result::UnknownExplanation e) CVC4_PUBLIC;
-
-bool operator==(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC;
-bool operator==(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
-
-bool operator!=(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC;
-bool operator!=(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__RESULT_H */
diff --git a/src/expr/result.i b/src/expr/result.i
deleted file mode 100644
index becbe9aa9..000000000
--- a/src/expr/result.i
+++ /dev/null
@@ -1,20 +0,0 @@
-%{
-#include "expr/result.h"
-%}
-
-%ignore CVC4::operator<<(std::ostream&, const Result& r);
-
-%rename(equals) CVC4::Result::operator==(const Result& r) const;
-%ignore CVC4::Result::operator!=(const Result& r) const;
-
-%ignore CVC4::operator<<(std::ostream&, enum Result::Sat);
-%ignore CVC4::operator<<(std::ostream&, enum Result::Validity);
-%ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation);
-
-%ignore CVC4::operator==(enum Result::Sat, const Result&);
-%ignore CVC4::operator!=(enum Result::Sat, const Result&);
-
-%ignore CVC4::operator==(enum Result::Validity, const Result&);
-%ignore CVC4::operator!=(enum Result::Validity, const Result&);
-
-%include "expr/result.h"