summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml2
-rw-r--r--config/bindings.m42
-rw-r--r--src/api/cvc4cpp.h4
-rw-r--r--src/base/exception.h4
-rw-r--r--src/base/listener.h9
-rw-r--r--src/context/cdhashmap.h6
-rw-r--r--src/context/cdhashset.h4
-rw-r--r--src/context/cdinsert_hashmap.h2
-rw-r--r--src/context/cdlist.h2
-rw-r--r--src/context/cdo.h2
-rw-r--r--src/context/context.h8
-rw-r--r--src/expr/expr_manager_template.h4
-rw-r--r--src/expr/node_manager.h4
-rw-r--r--src/include/cvc4_public.h16
-rw-r--r--src/main/portfolio_util.h4
-rw-r--r--src/options/options.h4
-rw-r--r--src/parser/antlr_input.h5
-rw-r--r--src/parser/input.h4
-rw-r--r--src/printer/printer.h4
-rw-r--r--src/prop/bvminisat/bvminisat.h2
-rw-r--r--src/smt/smt_engine.h4
-rw-r--r--src/smt_util/boolean_simplification.h4
-rw-r--r--src/smt_util/lemma_channels.h4
-rw-r--r--src/theory/rewriter.h4
-rw-r--r--src/theory/theory.h6
-rw-r--r--src/util/bin_heap.h4
-rw-r--r--src/util/resource_manager.h4
-rw-r--r--src/util/statistics_registry.h10
28 files changed, 57 insertions, 75 deletions
diff --git a/.travis.yml b/.travis.yml
index d1f72f955..27cb2915b 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -32,7 +32,7 @@ addons:
- libgmp-dev
- libboost-dev
- libboost-thread-dev
- - swig
+ - swig3.0
- libcln-dev
- openjdk-7-jdk
- antlr3
diff --git a/config/bindings.m4 b/config/bindings.m4
index 7174934c1..5941d81cd 100644
--- a/config/bindings.m4
+++ b/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
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index c3c429009..0d05c9b19 100644
--- a/src/api/cvc4cpp.h
+++ b/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 */
diff --git a/src/base/exception.h b/src/base/exception.h
index c6619ddd6..983a59572 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -158,8 +158,8 @@ public:
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;
diff --git a/src/base/listener.h b/src/base/listener.h
index 7e8d00039..88bcee742 100644
--- a/src/base/listener.h
+++ b/src/base/listener.h
@@ -125,14 +125,14 @@ private:
* 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 */
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 94b507a7e..958c48e22 100644
--- a/src/context/cdhashmap.h
+++ b/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)
diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h
index 0dc1f087d..b907d9823 100644
--- a/src/context/cdhashset.h
+++ b/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:
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
index 62268b471..d59bf584d 100644
--- a/src/context/cdinsert_hashmap.h
+++ b/src/context/cdinsert_hashmap.h
@@ -214,7 +214,7 @@ private:
<< " 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
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 8fcc977af..834e363f9 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -113,7 +113,7 @@ protected:
<< " from " << &l
<< " size " << d_size << std::endl;
}
- CDList& operator=(const CDList& l) CVC4_UNDEFINED;
+ CDList& operator=(const CDList& l) = delete;
private:
/**
diff --git a/src/context/cdo.h b/src/context/cdo.h
index 3cb646d6c..da6c8d338 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -50,7 +50,7 @@ protected:
/**
* 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
diff --git a/src/context/context.h b/src/context/context.h
index acff2b5c2..04da9c25d 100644
--- a/src/context/context.h
+++ b/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 @@ public:
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 */
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index a9cdfc587..bce1c8940 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -83,8 +83,8 @@ private:
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;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 71082ef9d..f7f3fb144 100644
--- a/src/expr/node_manager.h
+++ b/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();
diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h
index e1d406b03..7950a5af6 100644
--- a/src/include/cvc4_public.h
+++ b/src/include/cvc4_public.h
@@ -31,28 +31,12 @@
# 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__))
# define CVC4_CONST_FUNCTION __attribute__ ((__const__))
diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h
index ab65cbaf0..6ebd97d3d 100644
--- a/src/main/portfolio_util.h
+++ b/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;
};
diff --git a/src/options/options.h b/src/options/options.h
index 8ca713642..16210e1a3 100644
--- a/src/options/options.h
+++ b/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);
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 3a0c0fdfe..5598dd359 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -69,11 +69,10 @@ private:
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:
diff --git a/src/parser/input.h b/src/parser/input.h
index 4f1a0f7da..02d92749d 100644
--- a/src/parser/input.h
+++ b/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.
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 29d4f5598..6b34094e7 100644
--- a/src/printer/printer.h
+++ b/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);
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 6578b5ee8..728d26bd4 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -121,7 +121,7 @@ public:
private:
/* Disable the default constructor. */
- BVMinisatSatSolver() CVC4_UNDEFINED;
+ BVMinisatSatSolver() = delete;
class Statistics {
public:
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index e4bd7d77d..dc5a5e703 100644
--- a/src/smt/smt_engine.h
+++ b/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,
diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h
index 6274d0dbd..8e4d8aa25 100644
--- a/src/smt_util/boolean_simplification.h
+++ b/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)
diff --git a/src/smt_util/lemma_channels.h b/src/smt_util/lemma_channels.h
index 67de37ed8..b2af0dfe4 100644
--- a/src/smt_util/lemma_channels.h
+++ b/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;
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index eda5dcf26..cc948ae7c 100644
--- a/src/theory/rewriter.h
+++ b/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.
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 2c3c727cb..5d176a36b 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -83,9 +83,9 @@ private:
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;
diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h
index 7d733829b..d547530b1 100644
--- a/src/util/bin_heap.h
+++ b/src/util/bin_heap.h
@@ -60,8 +60,8 @@ private:
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())
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 2fa7a6bb4..3ca2babcf 100644
--- a/src/util/resource_manager.h
+++ b/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:
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index b000e91e8..d7f105b65 100644
--- a/src/util/statistics_registry.h
+++ b/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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback