more refactoring

4 files changed, 68 insertions, 43 deletions

diff --git a/configure.ac b/configure.ac
index b321fef6b..ffa8092df 100644
--- a/configure.ac
+++ b/configure.ac
@@ -870,6 +870,8 @@ CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
+CVC4_CXX_OPTION([-fuse-ld=gold], [FUSE_LD_GOLD])
+CVC4_C_OPTION([-fuse-ld=gold], [C_FUSE_LD_GOLD])
 AC_SUBST([WERROR])
 AC_SUBST([WNO_CONVERSION_NULL])
 AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
@@ -1151,8 +1153,8 @@ cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
-CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED"
-CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions"
+CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED $FUSE_LD_GOLD"
+CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED $C_FUSE_LD_GOLD -fexceptions"
 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 CVC4_CHECK_FOR_READLINE
 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
@@ -1292,8 +1294,8 @@ AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion co
 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
 
 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
-CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
-CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
+CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated $FUSE_LD_GOLD"
+CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions $C_FUSE_LD_GOLD"
 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 
 # visibility flag not supported for Windows builds
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 0c844f92d..251b3b58c 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -131,9 +131,56 @@ bool NodeTemplate<ref_count>::hasBoundVar() {
   return getAttribute(HasBoundVarAttr());
 }
 
+template <bool ref_count>
+void NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
+  assertTNodeNotExpired();
+  d_nv->printAst(out, indent);
+}
+
+std::ostream& operator<<(std::ostream& out, TNode n) {
+  n.toStream(out, Node::setdepth::getDepth(out),
+             Node::printtypes::getPrintTypes(out), Node::dag::getDag(out),
+             Node::setlanguage::getLanguage(out));
+  return out;
+}
+
+template <bool ref_count>
+std::ostream& operator<<(std::ostream& out,
+                         const std::vector<NodeTemplate<ref_count> >& ns) {
+  for (typename std::vector<NodeTemplate<ref_count> >::const_iterator
+           i = ns.begin(),
+           end = ns.end();
+       i != end; ++i) {
+    out << *i;
+  }
+  return out;
+}
+
+template <bool ref_count>
+void NodeTemplate<ref_count>::toStream(std::ostream& out, int toDepth,
+                                       bool types, size_t dag,
+                                       OutputLanguage language) const {
+  assertTNodeNotExpired();
+  d_nv->toStream(out, toDepth, types, dag, language);
+}
+
 template bool NodeTemplate<true>::isConst() const;
 template bool NodeTemplate<false>::isConst() const;
 template bool NodeTemplate<true>::hasBoundVar();
 template bool NodeTemplate<false>::hasBoundVar();
+template void NodeTemplate<true>::printAst(std::ostream& out, int indent) const;
+template void NodeTemplate<false>::printAst(std::ostream& out,
+                                            int indent) const;
+template void NodeTemplate<true>::toStream(std::ostream& out, int toDepth,
+                                           bool types, size_t dag,
+                                           OutputLanguage language) const;
+template void NodeTemplate<false>::toStream(std::ostream& out, int toDepth,
+                                            bool types, size_t dag,
+                                            OutputLanguage language) const;
+template std::ostream& operator<<(std::ostream& out,
+                                  const std::vector<NodeTemplate<true> >& ns);
+
+template std::ostream& operator<<(std::ostream& out,
+                                  const std::vector<NodeTemplate<false> >& ns);
 
 }/* CVC4 namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index 69bb98f95..ef5b81594 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -22,18 +22,17 @@
 #ifndef __CVC4__NODE_H
 #define __CVC4__NODE_H
 
-#include <vector>
-#include <string>
-#include <iostream>
-#include <utility>
 #include <algorithm>
+#include <cstdint>
 #include <functional>
-#include <stdint.h>
+#include <iosfwd>
+#include <string>
+#include <utility>
+#include <vector>
 
 #include "base/configuration.h"
 #include "base/cvc4_assert.h"
 #include "base/exception.h"
-#include "base/output.h"
 #include "expr/type.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
@@ -832,11 +831,9 @@ public:
    * (might break language compliance, but good for debugging expressions)
    * @param language the language in which to output
    */
-  inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
-                       OutputLanguage language = language::output::LANG_AUTO) const {
-    assertTNodeNotExpired();
-    d_nv->toStream(out, toDepth, types, dag, language);
-  }
+  void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+                size_t dag = 1,
+                OutputLanguage language = language::output::LANG_AUTO) const;
 
   /**
    * IOStream manipulator to set the maximum depth of Nodes when
@@ -880,7 +877,7 @@ public:
    * @param out output stream to print to.
    * @param indent number of spaces to indent the formula by.
    */
-  inline void printAst(std::ostream& out, int indent = 0) const;
+  void printAst(std::ostream& out, int indent = 0) const;
 
   /**
    * Check if the node has a subterm t.
@@ -913,14 +910,7 @@ public:
  * @param n the node to output to the stream
  * @return the stream
  */
-inline std::ostream& operator<<(std::ostream& out, TNode n) {
-  n.toStream(out,
-             Node::setdepth::getDepth(out),
-             Node::printtypes::getPrintTypes(out),
-             Node::dag::getDag(out),
-             Node::setlanguage::getLanguage(out));
-  return out;
-}
+std::ostream& operator<<(std::ostream& out, TNode n);
 
 /**
  * Serializes a vector of node to the given stream.
@@ -929,17 +919,9 @@ inline std::ostream& operator<<(std::ostream& out, TNode n) {
  * @param ns the vector of nodes to output to the stream
  * @return the stream
  */
-template<bool ref_count>
-inline std::ostream& operator<<(std::ostream& out,
-                                const std::vector< NodeTemplate<ref_count> > & ns) {
-  for(typename std::vector< NodeTemplate<ref_count> >::const_iterator
-        i=ns.begin(), end=ns.end();
-      i != end; ++i){
-    out << *i;
-  }
-  return out;
-}
-
+template <bool ref_count>
+std::ostream& operator<<(std::ostream& out,
+                         const std::vector<NodeTemplate<ref_count> >& ns);
 
 }/* CVC4 namespace */
 
@@ -1221,13 +1203,6 @@ NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count2>& right) const {
   return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
 }
 
-template <bool ref_count>
-inline void
-NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
-  assertTNodeNotExpired();
-  d_nv->printAst(out, indent);
-}
-
 /**
  * Returns a node representing the operator of this expression.
  * If this is an APPLY, then the operator will be a functional term.
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 44c116558..58bf6ad30 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -32,12 +32,13 @@
 #include <string>
 #include <ext/hash_set>
 
+#include "base/output.h"
 #include "base/tls.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node_value.h"
-#include "util/subrange_bound.h"
 #include "options/options.h"
+#include "util/subrange_bound.h"
 
 namespace CVC4 {