- libgmp-dev
- libboost-dev
- libboost-thread-dev
- - swig
+ - swig3.0
- libcln-dev
- openjdk-7-jdk
- antlr3
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
/**
* 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 */
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;
* 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;
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 */
d_next(NULL)
{
}
- CDOhash_map& operator=(const CDOhash_map&) CVC4_UNDEFINED;
+ CDOhash_map& operator=(const CDOhash_map&) = delete;
public:
CDOhash_map(Context* context,
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)
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:
<< " 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
<< " from " << &l
<< " size " << d_size << std::endl;
}
- CDList& operator=(const CDList& l) CVC4_UNDEFINED;
+ CDList& operator=(const CDList& l) = delete;
private:
/**
/**
* 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
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:
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 */
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;
// 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();
# 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__))
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;
};
* 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);
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:
* 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.
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);
private:
/* Disable the default constructor. */
- BVMinisatSatSolver() CVC4_UNDEFINED;
+ BVMinisatSatSolver() = delete;
class Statistics {
public:
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,
*/
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)
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;
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.
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;
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())
* 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:
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:
private:
/** Private copy constructor undefined (no copy permitted). */
- StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED;
+ StatisticsRegistry(const StatisticsRegistry&) = delete;
public:
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) {
projects / cvc5.git / commitdiff