Support for set compliment and universe set. Simplify approach for sep.nil nodes.

3 files changed, 0 insertions, 103 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 9dcbc3b4b..c04de4421 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -40,8 +40,6 @@ libexpr_la_SOURCES = \
 	pickle_data.h \
 	pickler.cpp \
 	pickler.h \
-	sepconst.cpp \
-	sepconst.h \
 	symbol_table.cpp \
 	symbol_table.h \
 	type.cpp \
diff --git a/src/expr/sepconst.cpp b/src/expr/sepconst.cpp
deleted file mode 100644
index 7646b90d3..000000000
--- a/src/expr/sepconst.cpp
+++ /dev/null
@@ -1,29 +0,0 @@
-/*********************                                                        */
-/*! \file sepconst.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "expr/sepconst.h"
-#include <iostream>
-
-using namespace std;
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, const NilRef& asa) {
-  return out << "(nil " << asa.getType() << ")";
-}
-
-}/* CVC4 namespace */
diff --git a/src/expr/sepconst.h b/src/expr/sepconst.h
deleted file mode 100644
index 9f86c7efc..000000000
--- a/src/expr/sepconst.h
+++ /dev/null
@@ -1,72 +0,0 @@
-/*********************                                                        */
-/*! \file sepconst.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_public.h"
-
-#pragma once
-
-namespace CVC4 {
-  // messy; Expr needs NilRef (because it's the payload of a
-  // CONSTANT-kinded expression), and NilRef needs Expr.
-  class CVC4_PUBLIC NilRef;
-  //class CVC4_PUBLIC EmpStar;
-}/* CVC4 namespace */
-
-#include "expr/expr.h"
-#include "expr/type.h"
-#include <iostream>
-
-namespace CVC4 {
-
-class CVC4_PUBLIC NilRef {
-  const Type d_type;
-  NilRef() { }
-public:
-  NilRef(Type refType):d_type(refType) { }
-
-  ~NilRef() throw() {
-  }
-  Type getType() const { return d_type; }
-  bool operator==(const NilRef& es) const throw() {
-    return d_type == es.d_type;
-  }
-  bool operator!=(const NilRef& es) const throw() {
-    return !(*this == es);
-  }
-  bool operator<(const NilRef& es) const throw() {
-    return d_type < es.d_type;
-  }
-  bool operator<=(const NilRef& es) const throw() {
-    return d_type <= es.d_type;
-  }
-  bool operator>(const NilRef& es) const throw() {
-    return !(*this <= es);
-  }
-  bool operator>=(const NilRef& es) const throw() {
-    return !(*this < es);
-  }
-};/* class NilRef */
-
-std::ostream& operator<<(std::ostream& out, const NilRef& es) CVC4_PUBLIC;
-
-struct CVC4_PUBLIC NilRefHashFunction {
-  inline size_t operator()(const NilRef& es) const {
-    return TypeHashFunction()(es.getType());
-  }
-};/* struct NilRefHashFunction */
-
-}/* CVC4 namespace */