Delete functions instead of using CVC4_UNDEFINED (cvc5#1794)

C++11 supports explicitly deleting functions that should not be used
(explictly or implictly), e.g. copy or assignment constructors. We were
previously using the CVC4_UNDEFINED macro that used a compiler-specific
attribute. The C++11 feature should be more portable.

.travis.yml

@@ -32,7 +32,7 @@ addons:
   - libgmp-dev
   - libboost-dev
   - libboost-thread-dev
-  - swig
+  - swig3.0
   - libcln-dev
   - openjdk-7-jdk
   - antlr3

config/bindings.m4

@@ -47,7 +47,7 @@ if test "$noswig" = yes; then
   SWIG=
 else
   if test -z "$SWIG"; then
-    AC_CHECK_PROGS(SWIG, [swig swig2.0 swig-2], [], [])
+    AC_CHECK_PROGS(SWIG, [swig swig3.0 swig-3], [], [])
   else
     AC_CHECK_PROG(SWIG, "$SWIG", "$SWIG", [])
   fi

src/api/cvc4cpp.h

@@ -1303,8 +1303,8 @@ class CVC4_PUBLIC Solver
   /**
    * Disallow copy/assignment.
    */
-  Solver(const Solver&) CVC4_UNDEFINED;
-  Solver& operator=(const Solver&) CVC4_UNDEFINED;
+  Solver(const Solver&) = delete;
+  Solver& operator=(const Solver&) = delete;
 
   /* .................................................................... */
   /* Sorts Handling                                                       */

src/base/exception.h

@@ -158,8 +158,8 @@ class CVC4_PUBLIC LastExceptionBuffer {
 
 private:
   /* Disallow copies */
-  LastExceptionBuffer(const LastExceptionBuffer&) CVC4_UNDEFINED;
-  LastExceptionBuffer& operator=(const LastExceptionBuffer&) CVC4_UNDEFINED;
+  LastExceptionBuffer(const LastExceptionBuffer&) = delete;
+  LastExceptionBuffer& operator=(const LastExceptionBuffer&) = delete;
 
   char* d_contents;
 

src/base/listener.h

@@ -125,14 +125,14 @@ class CVC4_PUBLIC ListenerCollection {
    * The user of the class must be know to remove listeners on the collection.
    * Allowing copies will only cause confusion.
    */
-  ListenerCollection(const ListenerCollection& copy) CVC4_UNDEFINED;
+  ListenerCollection(const ListenerCollection& copy) = delete;
 
   /**
    * Disabling the assignment operator.
    * The user of the class must be know to remove listeners on the collection.
    * Allowing copies will only cause confusion.
    */
-  ListenerCollection& operator=(const ListenerCollection& copy) CVC4_UNDEFINED;
+  ListenerCollection& operator=(const ListenerCollection& copy) = delete;
 
   /** A list of the listeners in the collection.*/
   ListenerList d_listeners;
@@ -153,10 +153,9 @@ class ListenerRegistrationList {
 
  private:
   /** Disallow copying.*/
-  ListenerRegistrationList(const ListenerRegistrationList&) CVC4_UNDEFINED;
+  ListenerRegistrationList(const ListenerRegistrationList&) = delete;
   /** Disallow assignment.*/
-  ListenerRegistrationList operator=(const ListenerRegistrationList&)
-      CVC4_UNDEFINED;
+  ListenerRegistrationList operator=(const ListenerRegistrationList&) = delete;
   std::list<ListenerCollection::Registration*> d_registrations;
 };/* class CVC4::ListenerRegistrationList */
 

src/context/cdhashmap.h

@@ -177,7 +177,7 @@ class CDOhash_map : public ContextObj {
         d_next(NULL)
   {
   }
-  CDOhash_map& operator=(const CDOhash_map&) CVC4_UNDEFINED;
+  CDOhash_map& operator=(const CDOhash_map&) = delete;
 
  public:
   CDOhash_map(Context* context,
@@ -290,8 +290,8 @@ class CDHashMap : public ContextObj {
   void restore(ContextObj* data) override { Unreachable(); }
 
   // no copy or assignment
-  CDHashMap(const CDHashMap&) CVC4_UNDEFINED;
-  CDHashMap& operator=(const CDHashMap&) CVC4_UNDEFINED;
+  CDHashMap(const CDHashMap&) = delete;
+  CDHashMap& operator=(const CDHashMap&) = delete;
 
 public:
   CDHashMap(Context* context)

src/context/cdhashset.h

@@ -32,8 +32,8 @@ class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn> {
   typedef CDInsertHashMap<V, bool, HashFcn> super;
 
   // no copy or assignment
-  CDHashSet(const CDHashSet&) CVC4_UNDEFINED;
-  CDHashSet& operator=(const CDHashSet&) CVC4_UNDEFINED;
+  CDHashSet(const CDHashSet&) = delete;
+  CDHashSet& operator=(const CDHashSet&) = delete;
 
 public:
 

src/context/cdinsert_hashmap.h

@@ -214,7 +214,7 @@ class CDInsertHashMap : public ContextObj {
                     << " from " << &l
                     << " size " << d_size << std::endl;
   }
-  CDInsertHashMap& operator=(const CDInsertHashMap&) CVC4_UNDEFINED;
+  CDInsertHashMap& operator=(const CDInsertHashMap&) = delete;
 
   /**
    * Implementation of mandatory ContextObj method save: simply copies

src/context/cdlist.h

@@ -113,7 +113,7 @@ class CDList : public ContextObj {
                     << " from " << &l
                     << " size " << d_size << std::endl;
   }
-  CDList& operator=(const CDList& l) CVC4_UNDEFINED;
+  CDList& operator=(const CDList& l) = delete;
 
 private:
   /**

src/context/cdo.h

@@ -50,7 +50,7 @@ class CDO : public ContextObj {
   /**
    * operator= for CDO is private to ensure CDO object is not copied.
    */
-  CDO<T>& operator=(const CDO<T>& cdo) CVC4_UNDEFINED;
+  CDO<T>& operator=(const CDO<T>& cdo) = delete;
 
   /**
    * Implementation of mandatory ContextObj method save: simply copies the

src/context/context.h

@@ -94,8 +94,8 @@ class Context {
   friend std::ostream& operator<<(std::ostream&, const Context&);
 
   // disable copy, assignment
-  Context(const Context&) CVC4_UNDEFINED;
-  Context& operator=(const Context&) CVC4_UNDEFINED;
+  Context(const Context&) = delete;
+  Context& operator=(const Context&) = delete;
 
 public:
 
@@ -208,8 +208,8 @@ class Context {
 class UserContext : public Context {
 private:
   // disable copy, assignment
-  UserContext(const UserContext&) CVC4_UNDEFINED;
-  UserContext& operator=(const UserContext&) CVC4_UNDEFINED;
+  UserContext(const UserContext&) = delete;
+  UserContext& operator=(const UserContext&) = delete;
 public:
   UserContext() {}
 };/* class UserContext */

src/expr/expr_manager_template.h

@@ -83,8 +83,8 @@ class CVC4_PUBLIC ExprManager {
   friend class NodeManager;
 
   // undefined, private copy constructor and assignment op (disallow copy)
-  ExprManager(const ExprManager&) CVC4_UNDEFINED;
-  ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED;
+  ExprManager(const ExprManager&) = delete;
+  ExprManager& operator=(const ExprManager&) = delete;
 
   std::vector<DatatypeType> d_keep_dtt;
   std::vector<Datatype> d_keep_dt;

src/expr/node_manager.h

@@ -349,9 +349,9 @@ class NodeManager {
   // bool properlyContainsDecision(TNode); // all children are atomic
 
   // undefined private copy constructor (disallow copy)
-  NodeManager(const NodeManager&) CVC4_UNDEFINED;
+  NodeManager(const NodeManager&) = delete;
 
-  NodeManager& operator=(const NodeManager&) CVC4_UNDEFINED;
+  NodeManager& operator=(const NodeManager&) = delete;
 
   void init();
 

src/include/cvc4_public.h

@@ -31,27 +31,11 @@
 #  endif /* __GNUC__ >= 4 */
 #endif /* defined _WIN32 || defined __CYGWIN__ */
 
-// Can use CVC4_UNDEFINED for things like undefined, private
-// copy constructors.  The advantage is that with CVC4_UNDEFINED,
-// if something _does_ try to call the function, you get an error
-// at the point of the call (rather than a link error later).
-
 // CVC4_UNUSED is to mark something (e.g. local variable, function)
 // as being _possibly_ unused, so that the compiler generates no
 // warning about it.  This might be the case for e.g. a variable
 // only used in DEBUG builds.
 
-#ifdef __GNUC__
-#  if __GNUC__ > 4 || ( __GNUC__ == 4 && __GNUC_MINOR__ >= 3 )
-     /* error function attribute only exists in GCC >= 4.3.0 */
-#    define CVC4_UNDEFINED __attribute__((__error__("this function intentionally undefined")))
-#  else /* GCC < 4.3.0 */
-#    define CVC4_UNDEFINED
-#  endif /* GCC >= 4.3.0 */
-#else /* ! __GNUC__ */
-#  define CVC4_UNDEFINED
-#endif /* __GNUC__ */
-
 #ifdef __GNUC__
 #  define CVC4_UNUSED __attribute__((__unused__))
 #  define CVC4_NORETURN __attribute__ ((__noreturn__))

src/main/portfolio_util.h

@@ -86,8 +86,8 @@ class OptionsList {
 
   size_t size() const;
  private:
-  OptionsList(const OptionsList&) CVC4_UNDEFINED;
-  OptionsList& operator=(const OptionsList&) CVC4_UNDEFINED;
+  OptionsList(const OptionsList&) = delete;
+  OptionsList& operator=(const OptionsList&) = delete;
   std::vector<Options*> d_options;
 };
 

src/options/options.h

@@ -114,13 +114,13 @@ class CVC4_PUBLIC Options {
    * Options cannot be copied as they are given an explicit list of
    * Listeners to respond to.
    */
-  Options(const Options& options) CVC4_UNDEFINED;
+  Options(const Options& options) = delete;
 
   /**
    * Options cannot be assigned as they are given an explicit list of
    * Listeners to respond to.
    */
-  Options& operator=(const Options& options) CVC4_UNDEFINED;
+  Options& operator=(const Options& options) = delete;
 
   static std::string formatThreadOptionException(const std::string& option);
 

src/parser/antlr_input.h

@@ -69,11 +69,10 @@ class AntlrInputStream : public InputStream {
                    LineBuffer* line_buffer);
 
   /* This is private and unimplemented, because you should never use it. */
-  AntlrInputStream(const AntlrInputStream& inputStream) CVC4_UNDEFINED;
+  AntlrInputStream(const AntlrInputStream& inputStream) = delete;
 
   /* This is private and unimplemented, because you should never use it. */
-  AntlrInputStream& operator=(const AntlrInputStream& inputStream)
-    CVC4_UNDEFINED;
+  AntlrInputStream& operator=(const AntlrInputStream& inputStream) = delete;
 
 public:
 

src/parser/input.h

@@ -90,8 +90,8 @@ class CVC4_PUBLIC Input {
    * copy construction and assignment.  Mark them private and do not define
    * them.
    */
-  Input(const Input& input) CVC4_UNDEFINED;
-  Input& operator=(const Input& input) CVC4_UNDEFINED;
+  Input(const Input& input) = delete;
+  Input& operator=(const Input& input) = delete;
 
  public:
   /** Create an input for the given file.

src/printer/printer.h

@@ -100,8 +100,8 @@ class Printer
 
  private:
   /** Disallow copy, assignment  */
-  Printer(const Printer&) CVC4_UNDEFINED;
-  Printer& operator=(const Printer&) CVC4_UNDEFINED;
+  Printer(const Printer&) = delete;
+  Printer& operator=(const Printer&) = delete;
 
   /** Make a Printer for a given OutputLanguage */
   static std::unique_ptr<Printer> makePrinter(OutputLanguage lang);

src/prop/bvminisat/bvminisat.h

@@ -121,7 +121,7 @@ class BVMinisatSatSolver : public BVSatSolverInterface,
 
  private:
   /* Disable the default constructor. */
-  BVMinisatSatSolver() CVC4_UNDEFINED;
+  BVMinisatSatSolver() = delete;
 
   class Statistics {
   public:

src/smt/smt_engine.h

@@ -402,8 +402,8 @@ class CVC4_PUBLIC SmtEngine {
   void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations");
 
   // disallow copy/assignment
-  SmtEngine(const SmtEngine&) CVC4_UNDEFINED;
-  SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED;
+  SmtEngine(const SmtEngine&) = delete;
+  SmtEngine& operator=(const SmtEngine&) = delete;
 
   //check satisfiability (for query and check-sat)
   Result checkSatisfiability(const Expr& assumption,

src/smt_util/boolean_simplification.h

@@ -35,8 +35,8 @@ namespace CVC4 {
  */
 class BooleanSimplification {
   // cannot construct one of these
-  BooleanSimplification() CVC4_UNDEFINED;
-  BooleanSimplification(const BooleanSimplification&) CVC4_UNDEFINED;
+  BooleanSimplification() = delete;
+  BooleanSimplification(const BooleanSimplification&) = delete;
 
   static bool push_back_associative_commute_recursive(
       Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)

src/smt_util/lemma_channels.h

@@ -60,10 +60,10 @@ class CVC4_PUBLIC LemmaChannels {
 
  private:
   // Disable copy constructor.
-  LemmaChannels(const LemmaChannels&) CVC4_UNDEFINED;
+  LemmaChannels(const LemmaChannels&) = delete;
 
   // Disable assignment operator.
-  LemmaChannels& operator=(const LemmaChannels&) CVC4_UNDEFINED;
+  LemmaChannels& operator=(const LemmaChannels&) = delete;
 
   /** This captures the old options::lemmaInputChannel .*/
   LemmaInputChannel* d_lemmaInputChannel;

src/theory/rewriter.h

@@ -72,8 +72,8 @@ class Rewriter {
                                   TNode node, TNode cache);
 
   // disable construction of rewriters; all functionality is static
-  Rewriter() CVC4_UNDEFINED;
-  Rewriter(const Rewriter&) CVC4_UNDEFINED;
+  Rewriter() = delete;
+  Rewriter(const Rewriter&) = delete;
 
   /**
    * Rewrites the node using the given theory rewriter.

src/theory/theory.h

@@ -83,9 +83,9 @@ class Theory {
   friend class ::CVC4::TheoryEngine;
 
   // Disallow default construction, copy, assignment.
-  Theory() CVC4_UNDEFINED;
-  Theory(const Theory&) CVC4_UNDEFINED;
-  Theory& operator=(const Theory&) CVC4_UNDEFINED;
+  Theory() = delete;
+  Theory(const Theory&) = delete;
+  Theory& operator=(const Theory&) = delete;
 
   /** An integer identifying the type of the theory. */
   TheoryId d_id;

src/util/bin_heap.h

@@ -60,8 +60,8 @@ class BinaryHeap {
   CmpFcn d_cmp;
 
   // disallow copy and assignment
-  BinaryHeap(const BinaryHeap&) CVC4_UNDEFINED;
-  BinaryHeap& operator=(const BinaryHeap&) CVC4_UNDEFINED;
+  BinaryHeap(const BinaryHeap&) = delete;
+  BinaryHeap& operator=(const BinaryHeap&) = delete;
 
 public:
   BinaryHeap(const CmpFcn& c = CmpFcn())

src/util/resource_manager.h

@@ -120,13 +120,13 @@ class CVC4_PUBLIC ResourceManager {
    * ResourceManagers cannot be copied as they are given an explicit
    * list of Listeners to respond to.
    */
-  ResourceManager(const ResourceManager&) CVC4_UNDEFINED;
+  ResourceManager(const ResourceManager&) = delete;
 
   /**
    * ResourceManagers cannot be assigned as they are given an explicit
    * list of Listeners to respond to.
    */
-  ResourceManager& operator=(const ResourceManager&) CVC4_UNDEFINED;
+  ResourceManager& operator=(const ResourceManager&) = delete;
 
 public:
 

src/util/statistics_registry.h

@@ -392,9 +392,9 @@ class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> {
   const ReadOnlyDataStat<T>& d_stat;
 
   /** Private copy constructor undefined (no copy permitted). */
-  WrappedStat(const WrappedStat&) CVC4_UNDEFINED;
+  WrappedStat(const WrappedStat&) = delete;
   /** Private assignment operator undefined (no copy permitted). */
-  WrappedStat<T>& operator=(const WrappedStat&) CVC4_UNDEFINED;
+  WrappedStat<T>& operator=(const WrappedStat&) = delete;
 
 public:
 
@@ -653,7 +653,7 @@ class CVC4_PUBLIC StatisticsRegistry : public StatisticsBase, public Stat {
 private:
 
   /** Private copy constructor undefined (no copy permitted). */
-  StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED;
+  StatisticsRegistry(const StatisticsRegistry&) = delete;
 
 public:
 
@@ -760,9 +760,9 @@ class CodeTimer {
   bool d_reentrant;
 
   /** Private copy constructor undefined (no copy permitted). */
-  CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED;
+  CodeTimer(const CodeTimer& timer) = delete;
   /** Private assignment operator undefined (no copy permitted). */
-  CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED;
+  CodeTimer& operator=(const CodeTimer& timer) = delete;
 
 public:
   CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) {