Moving the theory::Assertion struct into its own file.

diff --git a/src/Makefile.am b/src/Makefile.am
index 6283a800208884f39891427438e70d293dfa11a7..1d43b4ec2e39b571b7da0a33f59697b59498dc29 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -142,6 +142,8 @@ libcvc4_la_SOURCES = \
        smt/term_formula_removal.cpp \
        smt/term_formula_removal.h \
        smt/update_ostream.h \
+       theory/assertion.cpp \
+       theory/assertion.h \
        theory/atom_requests.cpp \
        theory/atom_requests.h \
        theory/interrupted.h \

diff --git a/src/theory/assertion.cpp b/src/theory/assertion.cpp
new file mode 100644 (file)
index 0000000..99ddbc6
--- /dev/null
+++ b/src/theory/assertion.cpp
@@ -0,0 +1,27 @@
+/*********************                                                        */
+/*! \file assertion.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Theory assertions.
+ **
+ ** Theory assertions.
+ **/
+
+#include "theory/assertion.h"
+
+namespace CVC4 {
+namespace theory {
+
+std::ostream& operator<<(std::ostream& out, const Assertion& a) {
+  return out << a.assertion;
+}
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */

diff --git a/src/theory/assertion.h b/src/theory/assertion.h
new file mode 100644 (file)
index 0000000..2a5e71a
--- /dev/null
+++ b/src/theory/assertion.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file assertion.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The representation of the assertions sent to theories.
+ **
+ ** The representation of the assertions sent to theories.
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ASSERTION_H
+#define __CVC4__THEORY__ASSERTION_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+
+/** Information about an assertion for the theories. */
+struct Assertion {
+  /** The assertion expression. */
+  const Node assertion;
+
+  /** Has this assertion been preregistered with this theory. */
+  const bool isPreregistered;
+
+  Assertion(TNode assertion, bool isPreregistered)
+      : assertion(assertion), isPreregistered(isPreregistered) {}
+
+  /** Convert the assertion to a TNode. */
+  operator TNode() const { return assertion; }
+
+  /** Convert the assertion to a Node. */
+  operator Node() const { return assertion; }
+
+}; /* struct Assertion */
+
+std::ostream& operator<<(std::ostream& out, const Assertion& a);
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ASSERTION_H */

diff --git a/src/theory/theory.h b/src/theory/theory.h
index fd8cffa9feff15b7bf379e9b8b28a44bce8bebc3..0bea566b18c2674337a107b218bf520a239daf96 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -35,6 +35,7 @@
 #include "smt/command.h"
 #include "smt/dump.h"
 #include "smt/logic_request.h"
+#include "theory/assertion.h"
 #include "theory/logic_info.h"
 #include "theory/output_channel.h"
 #include "theory/valuation.h"
@@ -62,53 +63,23 @@ namespace eq {
   class EqualityEngine;
 }/* CVC4::theory::eq namespace */
 
-/**
- * Information about an assertion for the theories.
- */
-struct Assertion {
-
-  /** The assertion */
-  Node assertion;
-  /** Has this assertion been preregistered with this theory */
-  bool isPreregistered;
-
-  Assertion(TNode assertion, bool isPreregistered)
-  : assertion(assertion), isPreregistered(isPreregistered) {}
-
-  /**
-   * Convert the assertion to a TNode.
-   */
-  operator TNode () const {
-    return assertion;
-  }
-
-  /**
-   * Convert the assertion to a Node.
-   */
-  operator Node () const {
-    return assertion;
-  }
-
-};/* struct Assertion */
 
 /**
- * A (oredered) pair of terms a theory cares about.
+ * A (ordered) pair of terms a theory cares about.
  */
 struct CarePair {
-
-  TNode a, b;
-  TheoryId theory;
-
-public:
+ public:
+  const TNode a, b;
+  const TheoryId theory;
 
   CarePair(TNode a, TNode b, TheoryId theory)
-  : a(a < b ? a : b), b(a < b ? b : a), theory(theory) {}
+      : a(a < b ? a : b), b(a < b ? b : a), theory(theory) {}
 
-  bool operator == (const CarePair& other) const {
+  bool operator==(const CarePair& other) const {
     return (theory == other.theory) && (a == other.a) && (b == other.b);
   }
 
-  bool operator < (const CarePair& other) const {
+  bool operator<(const CarePair& other) const {
     if (theory < other.theory) return true;
     if (theory > other.theory) return false;
     if (a < other.a) return true;
@@ -116,7 +87,7 @@ public:
     return b < other.b;
   }
 
-};/* struct CarePair */
+}; /* struct CarePair */
 
 /**
  * A set of care pairs.
@@ -924,7 +895,7 @@ public:
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
-inline std::ostream& operator<<(std::ostream& out, const theory::Assertion& a);
+
 
 inline theory::Assertion Theory::get() {
   Assert( !done(), "Theory::get() called with assertion queue empty!" );
@@ -942,10 +913,6 @@ inline theory::Assertion Theory::get() {
   return fact;
 }
 
-inline std::ostream& operator<<(std::ostream& out, const theory::Assertion& a) {
-  return out << a.assertion;
-}
-
 inline std::ostream& operator<<(std::ostream& out,
                                 const CVC4::theory::Theory& theory) {
   return out << theory.identify();