From: Tim King <taking@google.com>
Date: Mon, 27 Mar 2017 16:40:30 +0000 (-0700)
Subject: Moving the theory::Assertion struct into its own file.
X-Git-Tag: cvc5-1.0.0~5870
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7b89724488085d7eed3e37520ca11d8cd1e18120;p=cvc5.git

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

diff --git a/src/Makefile.am b/src/Makefile.am
index 6283a8002..1d43b4ec2 100644
--- 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
index 000000000..99ddbc6e9
--- /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
index 000000000..2a5e71adc
--- /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 fd8cffa9f..0bea566b1 100644
--- 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();