diff options
author | Tim King <taking@google.com> | 2017-07-17 10:51:09 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2017-07-17 10:51:09 -0700 |
commit | 7366c27f348adfe919fad3a16ee769e9215405c0 (patch) | |
tree | 310649dd7b726b0f309de144366814296b06771f | |
parent | a94318b0b1f0c4b8a2a4d6757b073626af06deea (diff) | |
parent | 53a226a753e509e028c386072c87d94c0a1316be (diff) |
Merge branch 'master' into cleanup-regexp
28 files changed, 464 insertions, 618 deletions
diff --git a/.travis.yml b/.travis.yml index 1ca15d50e..f474cb47d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -16,7 +16,6 @@ env: # via the "travis encrypt" command using the project repo's public key - secure: "fRfdzYwV10VeW5tVSvy5qpR8ZlkXepR7XWzCulzlHs9SRI2YY20BpzWRjyMBiGu2t7IeJKT7qdjq/CJOQEM8WS76ON7QJ1iymKaRDewDs3OhyPJ71fsFKEGgLky9blk7I9qZh23hnRVECj1oJAVry9IK04bc2zyIEjUYpjRkUAQ=" matrix: - - TRAVIS_CVC4=yes CXXFLAGS='-std=gnu++11' TRAVIS_CVC4_CONFIG='--enable-proof' - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c --enable-proof --with-portfolio' - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio' - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='--disable-proof' diff --git a/config/is_sorted.m4 b/config/is_sorted.m4 deleted file mode 100644 index 52b062d7e..000000000 --- a/config/is_sorted.m4 +++ /dev/null @@ -1,20 +0,0 @@ -# CHECK_FOR_IS_SORTED -# ------------------- -# Look for is_sorted in std:: and __gnu_cxx:: and define -# some things to make it easy to find later. -AC_DEFUN([CHECK_FOR_IS_SORTED], [ -AC_MSG_CHECKING([where we can find is_sorted]) -AC_LANG_PUSH([C++]) -is_sorted_result= -AC_COMPILE_IFELSE([AC_LANG_PROGRAM([#include <algorithm>], - [std::is_sorted((int*)0L, (int*)0L);])], - [is_sorted_result=std], - [AC_COMPILE_IFELSE([AC_LANG_PROGRAM([#include <ext/algorithm>], - [__gnu_cxx::is_sorted((int*)0L, (int*)0L);])], - [is_sorted_result=__gnu_cxx], - [AC_MSG_FAILURE([cannot find std::is_sorted() or __gnu_cxx::is_sorted()])])]) -AC_LANG_POP([C++]) -AC_MSG_RESULT($is_sorted_result) -if test "$is_sorted_result" = __gnu_cxx; then is_sorted_result=1; else is_sorted_result=0; fi -AC_DEFINE_UNQUOTED([IS_SORTED_IN_GNUCXX_NAMESPACE], $is_sorted_result, [Define to 1 if __gnu_cxx::is_sorted() exists]) -])# CHECK_FOR_IS_SORTED diff --git a/configure.ac b/configure.ac index b321fef6b..c0cec382f 100644 --- a/configure.ac +++ b/configure.ac @@ -1073,9 +1073,6 @@ AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>]) # check with which standard strerror_r() complies AC_FUNC_STRERROR_R -# is is_sorted() in std or __gnu_cxx? -CHECK_FOR_IS_SORTED - # require boost library BOOST_REQUIRE() diff --git a/examples/hashsmt/sha1.hpp b/examples/hashsmt/sha1.hpp index 4bfee50fc..72c560dff 100644 --- a/examples/hashsmt/sha1.hpp +++ b/examples/hashsmt/sha1.hpp @@ -30,9 +30,9 @@ // Note: this implementation does not handle message longer than // 2^32 bytes. -#pragma once +#ifndef __CVC4__EXAMPLES__HASHSMT__SHA1_H +#define __CVC4__EXAMPLES__HASHSMT__SHA1_H -#include <boost/static_assert.hpp> #include <cstddef> #include "word.h" @@ -45,8 +45,10 @@ namespace std { namespace hashsmt { -BOOST_STATIC_ASSERT(sizeof(unsigned char)*8 == 8); -BOOST_STATIC_ASSERT(sizeof(unsigned int)*8 == 32); +static_assert(sizeof(unsigned char)*8 == 8, + "Unexpected size for unsigned char"); +static_assert(sizeof(unsigned int)*8 == 32, + "Unexpected size for unsigned int"); inline cvc4_uint32 left_rotate(cvc4_uint32 x, std::size_t n) { @@ -224,3 +226,4 @@ inline void sha1::get_digest(digest_type digest) } // namespace hashsmt +#endif /* __CVC4__EXAMPLES__HASHSMT__SHA1_H */ diff --git a/src/base/Makefile.am b/src/base/Makefile.am index bf919cd81..491baaa90 100644 --- a/src/base/Makefile.am +++ b/src/base/Makefile.am @@ -26,9 +26,7 @@ libbase_la_SOURCES = \ listener.h \ modal_exception.h \ output.cpp \ - output.h \ - ptr_closer.h - + output.h BUILT_SOURCES = \ diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index f989e40e5..93133be24 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -151,7 +151,7 @@ compiled with " + ::CVC4::Configuration::getCompiler() + "\n\ on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\ Copyright (c) 2009-2017\n\ by the authors and their institutional affiliations listed at \n\ -http:\/\/cvc4.cs.stanford.edu/authors\n\n" + \ +http://cvc4.cs.stanford.edu/authors\n\n" + \ ( IS_GPL_BUILD ? "\ This build of CVC4 uses GPLed libraries, and is thus covered by the GNU\n\ General Public License (GPL) version 3. Versions of CVC4 are available\n\ diff --git a/src/base/ptr_closer.h b/src/base/ptr_closer.h deleted file mode 100644 index cd0c707b1..000000000 --- a/src/base/ptr_closer.h +++ /dev/null @@ -1,73 +0,0 @@ -/********************* */ -/*! \file ptr_closer.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A class to close owned pointers in the destructor. - ** - ** A class to close owned pointers in the destructor. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__PTR_CLOSER_H -#define __CVC4__PTR_CLOSER_H - -namespace CVC4 { - -/** - * A class to close owned pointers in the destructor. This plays a similar role - * to unique_ptr, but without move semantics. This is designed to overcome the - * lack of having unique_ptr in C++05. - * - * This is a variant of unique_ptr that is not designed for move semantics. - * These are appropriate to own pointer allocations on the stack that should be - * deleted when an exception is thrown. These should be used with care within - * heap based data structures, and never as the return value of a function. - */ -template <class T> -class PtrCloser { - public: - PtrCloser() : d_pointer(NULL) {} - explicit PtrCloser(T* pointer) : d_pointer(pointer) {} - ~PtrCloser() { delete d_pointer; } - - /** Deletes the currently owned copy and takes ownership of pointer. */ - void reset(T* pointer = NULL) { - delete d_pointer; - d_pointer = pointer; - } - - /** Gives up ownership of the pointer to the caller. */ - T* release() { - T* copy = d_pointer; - d_pointer = NULL; - return copy; - } - - /** Returns the pointer. */ - T* get() const { return d_pointer; } - - /** Returns the pointer. Undefined if the pointer is null. */ - T* operator->() const { return d_pointer; } - - /** Returns true if the pointer is not-null. */ - operator bool() const { return d_pointer != NULL; } - - private: - PtrCloser(const PtrCloser*) CVC4_UNDEFINED; - PtrCloser& operator=(const PtrCloser&) CVC4_UNDEFINED; - - /** An owned pointer object allocated by `new`. Or NULL. */ - T* d_pointer; -}; /* class PtrCloser */ - -} /* CVC4 namespace */ - -#endif /* __CVC4__PTR_CLOSER_H */ diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h index f53d60cf9..ef8f661fa 100644 --- a/src/context/cdinsert_hashmap.h +++ b/src/context/cdinsert_hashmap.h @@ -33,7 +33,6 @@ #include "cvc4_private.h" -#include <boost/static_assert.hpp> #include <deque> #include <ext/hash_map> #include <utility> @@ -383,9 +382,8 @@ public: } };/* class CDInsertHashMap<> */ - template <class Data, class HashFcn> -class CDInsertHashMap <TNode, Data, HashFcn > : public ContextObj { +class CDInsertHashMap<TNode, Data, HashFcn> : public ContextObj { /* CDInsertHashMap is challenging to get working with TNode. * Consider using CDHashMap<TNode,...> instead. * @@ -397,7 +395,8 @@ class CDInsertHashMap <TNode, Data, HashFcn > : public ContextObj { * hashed. Getting the order right with a guarantee is too hard. */ - BOOST_STATIC_ASSERT(sizeof(Data) == 0); + static_assert(sizeof(Data) == 0, + "Cannot create a CDInsertHashMap with TNode keys"); }; }/* CVC4::context namespace */ diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 7cee41b91..3dab675c3 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -20,7 +20,6 @@ #ifndef __CVC4__CONTEXT__CDLIST_H #define __CVC4__CONTEXT__CDLIST_H -#include <boost/static_assert.hpp> #include <iterator> #include <memory> #include <string> @@ -417,21 +416,21 @@ public: } };/* class CDList<> */ - template <class T, class CleanUp> -class CDList <T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj { +class CDList<T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj { /* CDList is incompatible for use with a ContextMemoryAllocator. * Consider using CDChunkList<T> instead. * * Explanation: - * If ContextMemoryAllocator is used and d_list grows at a deeper context level - * the reallocated will be reallocated in a context memory region that can be - * destroyed on pop. To support this, a full copy of d_list would have to be made. - * As this is unacceptable for performance in other situations, we do not do - * this. + * If ContextMemoryAllocator is used and d_list grows at a deeper context + * level the reallocated will be reallocated in a context memory region that + * can be destroyed on pop. To support this, a full copy of d_list would have + * to be made. As this is unacceptable for performance in other situations, we + * do not do this. */ - BOOST_STATIC_ASSERT(sizeof(T) == 0); + static_assert(sizeof(T) == 0, + "Cannot create a CDList with a ContextMemoryAllocator."); }; }/* CVC4::context namespace */ diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h index 9f364eac5..0d265271d 100644 --- a/src/context/cdtrail_hashmap.h +++ b/src/context/cdtrail_hashmap.h @@ -44,7 +44,6 @@ #pragma once -#include <boost/static_assert.hpp> #include <ext/hash_map> #include <deque> #include <utility> @@ -551,7 +550,7 @@ public: };/* class CDTrailHashMap<> */ template <class Data, class HashFcn> -class CDTrailHashMap <TNode, Data, HashFcn > : public ContextObj { +class CDTrailHashMap<TNode, Data, HashFcn> : public ContextObj { /* CDTrailHashMap is challenging to get working with TNode. * Consider using CDHashMap<TNode,...> instead. * @@ -563,7 +562,8 @@ class CDTrailHashMap <TNode, Data, HashFcn > : public ContextObj { * hashed. Getting the order right with a guarantee is too hard. */ - BOOST_STATIC_ASSERT(sizeof(Data) == 0); + static_assert(sizeof(Data) == 0, + "Cannot create a CDTrailHashMap with TNode keys"); }; }/* CVC4::context namespace */ diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 8d8fba43c..57cfa0221 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -155,10 +155,11 @@ #ifndef __CVC4__NODE_BUILDER_H #define __CVC4__NODE_BUILDER_H -#include <iostream> -#include <vector> #include <cstdlib> +#include <iostream> +#include <memory> #include <stdint.h> +#include <vector> namespace CVC4 { static const unsigned default_nchild_thresh = 10; @@ -171,7 +172,6 @@ namespace CVC4 { #include "base/cvc4_assert.h" #include "base/output.h" -#include "base/ptr_closer.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" @@ -890,14 +890,14 @@ template <unsigned nchild_thresh> Node* NodeBuilder<nchild_thresh>::constructNodePtr() { // maybeCheckType() can throw an exception. Make sure to call the destructor // on the exception branch. - PtrCloser<Node> np(new Node(constructNV())); + std::unique_ptr<Node> np(new Node(constructNV())); maybeCheckType(*np.get()); return np.release(); } template <unsigned nchild_thresh> Node* NodeBuilder<nchild_thresh>::constructNodePtr() const { - PtrCloser<Node> np(new Node(constructNV())); + std::unique_ptr<Node> np(new Node(constructNV())); maybeCheckType(*np.get()); return np.release(); } diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index 8cccd9bfe..6d655e1fe 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -27,7 +27,7 @@ namespace CVC4 { namespace expr { -class NodeSelfIterator : std::iterator<std::input_iterator_tag, Node> { +class NodeSelfIterator : public std::iterator<std::input_iterator_tag, Node> { Node d_node; Node::const_iterator d_child; diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 8b79e046c..697ce6642 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -20,6 +20,7 @@ #include <cstring> #include <fstream> #include <iostream> +#include <memory> #include <new> // This must come before PORTFOLIO_BUILD. @@ -27,7 +28,6 @@ #include "base/configuration.h" #include "base/output.h" -#include "base/ptr_closer.h" #include "expr/expr_iomanip.h" #include "expr/expr_manager.h" #include "main/command_executor.h" @@ -249,7 +249,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } # endif - PtrCloser<Parser> replayParser; + std::unique_ptr<Parser> replayParser; if( opts.getReplayInputFilename() != "" ) { std::string replayFilename = opts.getReplayInputFilename(); ParserBuilder replayParserBuilder(exprMgr, replayFilename, opts); @@ -357,7 +357,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { vector< vector<Command*> > allCommands; allCommands.push_back(vector<Command*>()); - PtrCloser<Parser> parser(parserBuilder.build()); + std::unique_ptr<Parser> parser(parserBuilder.build()); if(replayParser) { // have the replay parser use the file's declarations replayParser->useDeclarationsFrom(parser.get()); @@ -512,7 +512,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ } - PtrCloser<Parser> parser(parserBuilder.build()); + std::unique_ptr<Parser> parser(parserBuilder.build()); if(replayParser) { // have the replay parser use the file's declarations replayParser->useDeclarationsFrom(parser.get()); diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp index ff5d7f7b5..76578b6c4 100644 --- a/src/options/didyoumean_test.cpp +++ b/src/options/didyoumean_test.cpp @@ -21,28 +21,28 @@ #include "didyoumean.h" #include <iostream> -#include <boost/foreach.hpp> + using namespace std; using namespace CVC4; set<string> getDebugTags(); set<string> getOptionStrings(); -int main() -{ +int main() { string a, b; cin >> a; cout << "Matches with debug tags:" << endl; - vector<string> ret = DidYouMean(getDebugTags()).getMatch(a); - BOOST_FOREACH(string s, ret) cout << s << endl; + for (const string& s : DidYouMean(getDebugTags()).getMatch(a)) { + cout << s << endl; + } cout << "Matches with option strings:" << endl; - ret = DidYouMean(getOptionStrings()).getMatch(a); - BOOST_FOREACH(string s, ret) cout << s << endl; + for (const string& s : DidYouMean(getOptionStrings()).getMatch(a)) { + cout << s << endl; + } } -set<string> getDebugTags() -{ +set<string> getDebugTags() { set<string> a; a.insert("CDInsertHashMap"); a.insert("CDTrailHashMap"); @@ -426,340 +426,339 @@ set<string> getDebugTags() return a; } -set<string> getOptionStrings() -{ +set<string> getOptionStrings() { const char* cmdlineOptions[] = { - "lang", - "output-lang", - "language", - "output-language", - "verbose", - "quiet", - "stats", - "no-stats", - "statistics", - "no-statistics", - "stats-every-query", - "no-stats-every-query", - "statistics-every-query", - "no-statistics-every-query", - "parse-only", - "no-parse-only", - "preprocess-only", - "no-preprocess-only", - "trace", - "debug", - "print-success", - "no-print-success", - "smtlib-strict", - "default-expr-depth", - "default-dag-thresh", - "print-expr-types", - "eager-type-checking", - "lazy-type-checking", - "no-type-checking", - "biased-ites", - "no-biased-ites", - "boolean-term-conversion-mode", - "theoryof-mode", - "use-theory", - "bitblast-eager", - "no-bitblast-eager", - "bitblast-share-lemmas", - "no-bitblast-share-lemmas", - "bitblast-eager-fullcheck", - "no-bitblast-eager-fullcheck", - "bv-inequality-solver", - "no-bv-inequality-solver", - "bv-core-solver", - "no-bv-core-solver", - "bv-to-bool", - "no-bv-to-bool", - "bv-propagate", - "no-bv-propagate", - "bv-eq", - "no-bv-eq", - "dt-rewrite-error-sel", - "no-dt-rewrite-error-sel", - "dt-force-assignment", - "unate-lemmas", - "arith-prop", - "heuristic-pivots", - "standard-effort-variable-order-pivots", - "error-selection-rule", - "simplex-check-period", - "pivot-threshold", - "prop-row-length", - "disable-dio-solver", - "enable-arith-rewrite-equalities", - "disable-arith-rewrite-equalities", - "enable-miplib-trick", - "disable-miplib-trick", - "miplib-trick-subs", - "cut-all-bounded", - "no-cut-all-bounded", - "maxCutsInContext", - "revert-arith-models-on-unsat", - "no-revert-arith-models-on-unsat", - "fc-penalties", - "no-fc-penalties", - "use-fcsimplex", - "no-use-fcsimplex", - "use-soi", - "no-use-soi", - "restrict-pivots", - "no-restrict-pivots", - "collect-pivot-stats", - "no-collect-pivot-stats", - "use-approx", - "no-use-approx", - "approx-branch-depth", - "dio-decomps", - "no-dio-decomps", - "new-prop", - "no-new-prop", - "arith-prop-clauses", - "soi-qe", - "no-soi-qe", - "rewrite-divk", - "no-rewrite-divk", - "se-solve-int", - "no-se-solve-int", - "lemmas-on-replay-failure", - "no-lemmas-on-replay-failure", - "dio-turns", - "rr-turns", - "dio-repeat", - "no-dio-repeat", - "replay-early-close-depth", - "replay-failure-penalty", - "replay-num-err-penalty", - "replay-reject-cut", - "replay-lemma-reject-cut", - "replay-soi-major-threshold", - "replay-soi-major-threshold-pen", - "replay-soi-minor-threshold", - "replay-soi-minor-threshold-pen", - "symmetry-breaker", - "no-symmetry-breaker", - "condense-function-values", - "no-condense-function-values", - "disable-uf-ss-regions", - "uf-ss-eager-split", - "no-uf-ss-eager-split", - "uf-ss-totality", - "no-uf-ss-totality", - "uf-ss-totality-limited", - "uf-ss-totality-sym-break", - "no-uf-ss-totality-sym-break", - "uf-ss-abort-card", - "uf-ss-explained-cliques", - "no-uf-ss-explained-cliques", - "uf-ss-simple-cliques", - "no-uf-ss-simple-cliques", - "uf-ss-deq-prop", - "no-uf-ss-deq-prop", - "disable-uf-ss-min-model", - "uf-ss-clique-splits", - "no-uf-ss-clique-splits", - "uf-ss-sym-break", - "no-uf-ss-sym-break", - "uf-ss-fair", - "no-uf-ss-fair", - "arrays-optimize-linear", - "no-arrays-optimize-linear", - "arrays-lazy-rintro1", - "no-arrays-lazy-rintro1", - "arrays-model-based", - "no-arrays-model-based", - "arrays-eager-index", - "no-arrays-eager-index", - "arrays-eager-lemmas", - "no-arrays-eager-lemmas", - "disable-miniscope-quant", - "disable-miniscope-quant-fv", - "disable-prenex-quant", - "disable-var-elim-quant", - "disable-ite-lift-quant", - "cnf-quant", - "no-cnf-quant", - "clause-split", - "no-clause-split", - "pre-skolem-quant", - "no-pre-skolem-quant", - "ag-miniscope-quant", - "no-ag-miniscope-quant", - "macros-quant", - "no-macros-quant", - "fo-prop-quant", - "no-fo-prop-quant", - "disable-smart-triggers", - "relevant-triggers", - "no-relevant-triggers", - "relational-triggers", - "no-relational-triggers", - "register-quant-body-terms", - "no-register-quant-body-terms", - "inst-when", - "eager-inst-quant", - "no-eager-inst-quant", - "full-saturate-quant", - "no-full-saturate-quant", - "literal-matching", - "enable-cbqi", - "no-enable-cbqi", - "cbqi-recurse", - "no-cbqi-recurse", - "user-pat", - "flip-decision", - "disable-quant-internal-reps", - "finite-model-find", - "no-finite-model-find", - "mbqi", - "mbqi-one-inst-per-round", - "no-mbqi-one-inst-per-round", - "mbqi-one-quant-per-round", - "no-mbqi-one-quant-per-round", - "fmf-inst-engine", - "no-fmf-inst-engine", - "disable-fmf-inst-gen", - "fmf-inst-gen-one-quant-per-round", - "no-fmf-inst-gen-one-quant-per-round", - "fmf-fresh-dc", - "no-fmf-fresh-dc", - "disable-fmf-fmc-simple", - "fmf-bound-int", - "no-fmf-bound-int", - "axiom-inst", - "quant-cf", - "no-quant-cf", - "quant-cf-mode", - "quant-cf-when", - "rewrite-rules", - "no-rewrite-rules", - "rr-one-inst-per-round", - "no-rr-one-inst-per-round", - "strings-exp", - "no-strings-exp", - "strings-lb", - "strings-fmf", - "no-strings-fmf", - "strings-eit", - "no-strings-eit", - "strings-alphabet-card", - "show-sat-solvers", - "random-freq", - "random-seed", - "restart-int-base", - "restart-int-inc", - "refine-conflicts", - "no-refine-conflicts", - "minisat-elimination", - "no-minisat-elimination", - "minisat-dump-dimacs", - "no-minisat-dump-dimacs", - "model-format", - "dump", - "dump-to", - "force-logic", - "simplification", - "no-simplification", - "static-learning", - "no-static-learning", - "produce-models", - "no-produce-models", - "check-models", - "no-check-models", - "dump-models", - "no-dump-models", - "proof", - "no-proof", - "check-proofs", - "no-check-proofs", - "dump-proofs", - "no-dump-proofs", - "produce-unsat-cores", - "no-produce-unsat-cores", - "produce-assignments", - "no-produce-assignments", - "interactive", - "no-interactive", - "ite-simp", - "no-ite-simp", - "on-repeat-ite-simp", - "no-on-repeat-ite-simp", - "simp-with-care", - "no-simp-with-care", - "simp-ite-compress", - "no-simp-ite-compress", - "unconstrained-simp", - "no-unconstrained-simp", - "repeat-simp", - "no-repeat-simp", - "simp-ite-hunt-zombies", - "sort-inference", - "no-sort-inference", - "incremental", - "no-incremental", - "abstract-values", - "no-abstract-values", - "model-u-dt-enum", - "no-model-u-dt-enum", - "tlimit", - "tlimit-per", - "rlimit", - "rlimit-per", - "rewrite-apply-to-const", - "no-rewrite-apply-to-const", - "replay", - "replay-log", - "decision", - "decision-threshold", - "decision-use-weight", - "no-decision-use-weight", - "decision-random-weight", - "decision-weight-internal", - "version", - "license", - "help", - "show-config", - "show-debug-tags", - "show-trace-tags", - "early-exit", - "no-early-exit", - "threads", - "threadN", - "filter-lemma-length", - "fallback-sequential", - "no-fallback-sequential", - "incremental-parallel", - "no-incremental-parallel", - "no-interactive-prompt", - "continued-execution", - "immediate-exit", - "segv-spin", - "no-segv-spin", - "segv-nospin", - "wait-to-join", - "no-wait-to-join", - "strict-parsing", - "no-strict-parsing", - "mmap", - "no-mmap", - "no-checking", - "no-filesystem-access", - "no-include-file", - "enable-idl-rewrite-equalities", - "disable-idl-rewrite-equalities", - "sets-propagate", - "no-sets-propagate", - "sets-eager-lemmas", - "no-sets-eager-lemmas", - NULL, - };/* cmdlineOptions */ + "lang", + "output-lang", + "language", + "output-language", + "verbose", + "quiet", + "stats", + "no-stats", + "statistics", + "no-statistics", + "stats-every-query", + "no-stats-every-query", + "statistics-every-query", + "no-statistics-every-query", + "parse-only", + "no-parse-only", + "preprocess-only", + "no-preprocess-only", + "trace", + "debug", + "print-success", + "no-print-success", + "smtlib-strict", + "default-expr-depth", + "default-dag-thresh", + "print-expr-types", + "eager-type-checking", + "lazy-type-checking", + "no-type-checking", + "biased-ites", + "no-biased-ites", + "boolean-term-conversion-mode", + "theoryof-mode", + "use-theory", + "bitblast-eager", + "no-bitblast-eager", + "bitblast-share-lemmas", + "no-bitblast-share-lemmas", + "bitblast-eager-fullcheck", + "no-bitblast-eager-fullcheck", + "bv-inequality-solver", + "no-bv-inequality-solver", + "bv-core-solver", + "no-bv-core-solver", + "bv-to-bool", + "no-bv-to-bool", + "bv-propagate", + "no-bv-propagate", + "bv-eq", + "no-bv-eq", + "dt-rewrite-error-sel", + "no-dt-rewrite-error-sel", + "dt-force-assignment", + "unate-lemmas", + "arith-prop", + "heuristic-pivots", + "standard-effort-variable-order-pivots", + "error-selection-rule", + "simplex-check-period", + "pivot-threshold", + "prop-row-length", + "disable-dio-solver", + "enable-arith-rewrite-equalities", + "disable-arith-rewrite-equalities", + "enable-miplib-trick", + "disable-miplib-trick", + "miplib-trick-subs", + "cut-all-bounded", + "no-cut-all-bounded", + "maxCutsInContext", + "revert-arith-models-on-unsat", + "no-revert-arith-models-on-unsat", + "fc-penalties", + "no-fc-penalties", + "use-fcsimplex", + "no-use-fcsimplex", + "use-soi", + "no-use-soi", + "restrict-pivots", + "no-restrict-pivots", + "collect-pivot-stats", + "no-collect-pivot-stats", + "use-approx", + "no-use-approx", + "approx-branch-depth", + "dio-decomps", + "no-dio-decomps", + "new-prop", + "no-new-prop", + "arith-prop-clauses", + "soi-qe", + "no-soi-qe", + "rewrite-divk", + "no-rewrite-divk", + "se-solve-int", + "no-se-solve-int", + "lemmas-on-replay-failure", + "no-lemmas-on-replay-failure", + "dio-turns", + "rr-turns", + "dio-repeat", + "no-dio-repeat", + "replay-early-close-depth", + "replay-failure-penalty", + "replay-num-err-penalty", + "replay-reject-cut", + "replay-lemma-reject-cut", + "replay-soi-major-threshold", + "replay-soi-major-threshold-pen", + "replay-soi-minor-threshold", + "replay-soi-minor-threshold-pen", + "symmetry-breaker", + "no-symmetry-breaker", + "condense-function-values", + "no-condense-function-values", + "disable-uf-ss-regions", + "uf-ss-eager-split", + "no-uf-ss-eager-split", + "uf-ss-totality", + "no-uf-ss-totality", + "uf-ss-totality-limited", + "uf-ss-totality-sym-break", + "no-uf-ss-totality-sym-break", + "uf-ss-abort-card", + "uf-ss-explained-cliques", + "no-uf-ss-explained-cliques", + "uf-ss-simple-cliques", + "no-uf-ss-simple-cliques", + "uf-ss-deq-prop", + "no-uf-ss-deq-prop", + "disable-uf-ss-min-model", + "uf-ss-clique-splits", + "no-uf-ss-clique-splits", + "uf-ss-sym-break", + "no-uf-ss-sym-break", + "uf-ss-fair", + "no-uf-ss-fair", + "arrays-optimize-linear", + "no-arrays-optimize-linear", + "arrays-lazy-rintro1", + "no-arrays-lazy-rintro1", + "arrays-model-based", + "no-arrays-model-based", + "arrays-eager-index", + "no-arrays-eager-index", + "arrays-eager-lemmas", + "no-arrays-eager-lemmas", + "disable-miniscope-quant", + "disable-miniscope-quant-fv", + "disable-prenex-quant", + "disable-var-elim-quant", + "disable-ite-lift-quant", + "cnf-quant", + "no-cnf-quant", + "clause-split", + "no-clause-split", + "pre-skolem-quant", + "no-pre-skolem-quant", + "ag-miniscope-quant", + "no-ag-miniscope-quant", + "macros-quant", + "no-macros-quant", + "fo-prop-quant", + "no-fo-prop-quant", + "disable-smart-triggers", + "relevant-triggers", + "no-relevant-triggers", + "relational-triggers", + "no-relational-triggers", + "register-quant-body-terms", + "no-register-quant-body-terms", + "inst-when", + "eager-inst-quant", + "no-eager-inst-quant", + "full-saturate-quant", + "no-full-saturate-quant", + "literal-matching", + "enable-cbqi", + "no-enable-cbqi", + "cbqi-recurse", + "no-cbqi-recurse", + "user-pat", + "flip-decision", + "disable-quant-internal-reps", + "finite-model-find", + "no-finite-model-find", + "mbqi", + "mbqi-one-inst-per-round", + "no-mbqi-one-inst-per-round", + "mbqi-one-quant-per-round", + "no-mbqi-one-quant-per-round", + "fmf-inst-engine", + "no-fmf-inst-engine", + "disable-fmf-inst-gen", + "fmf-inst-gen-one-quant-per-round", + "no-fmf-inst-gen-one-quant-per-round", + "fmf-fresh-dc", + "no-fmf-fresh-dc", + "disable-fmf-fmc-simple", + "fmf-bound-int", + "no-fmf-bound-int", + "axiom-inst", + "quant-cf", + "no-quant-cf", + "quant-cf-mode", + "quant-cf-when", + "rewrite-rules", + "no-rewrite-rules", + "rr-one-inst-per-round", + "no-rr-one-inst-per-round", + "strings-exp", + "no-strings-exp", + "strings-lb", + "strings-fmf", + "no-strings-fmf", + "strings-eit", + "no-strings-eit", + "strings-alphabet-card", + "show-sat-solvers", + "random-freq", + "random-seed", + "restart-int-base", + "restart-int-inc", + "refine-conflicts", + "no-refine-conflicts", + "minisat-elimination", + "no-minisat-elimination", + "minisat-dump-dimacs", + "no-minisat-dump-dimacs", + "model-format", + "dump", + "dump-to", + "force-logic", + "simplification", + "no-simplification", + "static-learning", + "no-static-learning", + "produce-models", + "no-produce-models", + "check-models", + "no-check-models", + "dump-models", + "no-dump-models", + "proof", + "no-proof", + "check-proofs", + "no-check-proofs", + "dump-proofs", + "no-dump-proofs", + "produce-unsat-cores", + "no-produce-unsat-cores", + "produce-assignments", + "no-produce-assignments", + "interactive", + "no-interactive", + "ite-simp", + "no-ite-simp", + "on-repeat-ite-simp", + "no-on-repeat-ite-simp", + "simp-with-care", + "no-simp-with-care", + "simp-ite-compress", + "no-simp-ite-compress", + "unconstrained-simp", + "no-unconstrained-simp", + "repeat-simp", + "no-repeat-simp", + "simp-ite-hunt-zombies", + "sort-inference", + "no-sort-inference", + "incremental", + "no-incremental", + "abstract-values", + "no-abstract-values", + "model-u-dt-enum", + "no-model-u-dt-enum", + "tlimit", + "tlimit-per", + "rlimit", + "rlimit-per", + "rewrite-apply-to-const", + "no-rewrite-apply-to-const", + "replay", + "replay-log", + "decision", + "decision-threshold", + "decision-use-weight", + "no-decision-use-weight", + "decision-random-weight", + "decision-weight-internal", + "version", + "license", + "help", + "show-config", + "show-debug-tags", + "show-trace-tags", + "early-exit", + "no-early-exit", + "threads", + "threadN", + "filter-lemma-length", + "fallback-sequential", + "no-fallback-sequential", + "incremental-parallel", + "no-incremental-parallel", + "no-interactive-prompt", + "continued-execution", + "immediate-exit", + "segv-spin", + "no-segv-spin", + "segv-nospin", + "wait-to-join", + "no-wait-to-join", + "strict-parsing", + "no-strict-parsing", + "mmap", + "no-mmap", + "no-checking", + "no-filesystem-access", + "no-include-file", + "enable-idl-rewrite-equalities", + "disable-idl-rewrite-equalities", + "sets-propagate", + "no-sets-propagate", + "sets-eager-lemmas", + "no-sets-eager-lemmas", + NULL, + }; /* cmdlineOptions */ int i = 0; set<string> ret; - while(cmdlineOptions[i] != NULL) { + while (cmdlineOptions[i] != NULL) { ret.insert(cmdlineOptions[i]); i++; } diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 171c6cab0..a2e9e6f47 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -531,10 +531,10 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { // files. See the documentation in "parser/antlr_undefines.h" for more details. #include "parser/antlr_undefines.h" -#include <stdint.h> #include <cassert> +#include <memory> +#include <stdint.h> -#include "base/ptr_closer.h" #include "options/set_language.h" #include "parser/antlr_tracing.h" #include "parser/parser.h" @@ -595,7 +595,6 @@ namespace CVC4 { #include <vector> #include "base/output.h" -#include "base/ptr_closer.h" #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" @@ -659,7 +658,7 @@ parseExpr returns [CVC4::Expr expr = CVC4::Expr()] */ parseCommand returns [CVC4::Command* cmd_return = NULL] @declarations { - CVC4::PtrCloser<CVC4::Command> cmd; + std::unique_ptr<CVC4::Command> cmd; } @after { cmd_return = cmd.release(); @@ -689,7 +688,7 @@ parseCommand returns [CVC4::Command* cmd_return = NULL] * Matches a command of the input. If a declaration, it will return an empty * command. */ -command [CVC4::PtrCloser<CVC4::Command>* cmd] +command [std::unique_ptr<CVC4::Command>* cmd] : ( mainCommand[cmd] SEMICOLON | SEMICOLON | LET_TOK { PARSER_STATE->pushScope(); } @@ -716,7 +715,7 @@ options { backtrack = true; } : letDecl | typeLetDecl[check] ; -mainCommand[CVC4::PtrCloser<CVC4::Command>* cmd] +mainCommand[std::unique_ptr<CVC4::Command>* cmd] @init { Expr f; SExpr sexpr; @@ -934,7 +933,7 @@ symbolicExpr[CVC4::SExpr& sexpr] /** * Match a top-level declaration. */ -toplevelDeclaration[CVC4::PtrCloser<CVC4::Command>* cmd] +toplevelDeclaration[std::unique_ptr<CVC4::Command>* cmd] @init { std::vector<std::string> ids; Type t; @@ -951,7 +950,7 @@ toplevelDeclaration[CVC4::PtrCloser<CVC4::Command>* cmd] */ boundVarDecl[std::vector<std::string>& ids, CVC4::Type& t] @init { - CVC4::PtrCloser<Command> local_cmd; + std::unique_ptr<Command> local_cmd; } : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[&local_cmd,t,ids,false] @@ -1002,14 +1001,14 @@ boundVarDeclReturn[std::vector<CVC4::Expr>& terms, * because type declarations are always top-level, except for * type-lets, which don't use this rule. */ -declareTypes[CVC4::PtrCloser<CVC4::Command>* cmd, +declareTypes[std::unique_ptr<CVC4::Command>* cmd, const std::vector<std::string>& idList] @init { Type t; } /* A sort declaration (e.g., "T : TYPE") */ : TYPE_TOK - { CVC4::PtrCloser<DeclarationSequence> seq(new DeclarationSequence()); + { std::unique_ptr<DeclarationSequence> seq(new DeclarationSequence()); for(std::vector<std::string>::const_iterator i = idList.begin(); i != idList.end(); ++i) { // Don't allow a type variable to clash with a previously @@ -1044,7 +1043,7 @@ declareTypes[CVC4::PtrCloser<CVC4::Command>* cmd, * permitted and "cmd" is output. If topLevel is false, bound vars * are created */ -declareVariables[CVC4::PtrCloser<CVC4::Command>* cmd, CVC4::Type& t, +declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::Type& t, const std::vector<std::string>& idList, bool topLevel] @init { Expr f; @@ -1052,7 +1051,7 @@ declareVariables[CVC4::PtrCloser<CVC4::Command>* cmd, CVC4::Type& t, } /* A variable declaration (or definition) */ : type[t,CHECK_DECLARED] ( EQUAL_TOK formula[f] )? - { CVC4::PtrCloser<DeclarationSequence> seq; + { std::unique_ptr<DeclarationSequence> seq; if(topLevel) { seq.reset(new DeclarationSequence()); } @@ -2260,7 +2259,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes] constructorDef[CVC4::Datatype& type] @init { std::string id; - CVC4::PtrCloser<CVC4::DatatypeConstructor> ctor; + std::unique_ptr<CVC4::DatatypeConstructor> ctor; } : identifier[id,CHECK_UNDECLARED,SYM_SORT] { // make the tester @@ -2280,7 +2279,7 @@ constructorDef[CVC4::Datatype& type] } ; -selector[CVC4::PtrCloser<CVC4::DatatypeConstructor>* ctor] +selector[std::unique_ptr<CVC4::DatatypeConstructor>* ctor] @init { std::string id; Type t, t2; diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index 8f084ba34..ff3308d89 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -4,8 +4,9 @@ AM_CPPFLAGS = \ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable $(WNO_UNINITIALIZED) $(WNO_CONVERSION_NULL) # Compile generated C files using C++ compiler -CC=$(CXX) AM_CFLAGS = $(AM_CXXFLAGS) +CFLAGS=$(CXXFLAGS) +CC=$(CXX) ANTLR_OPTS = diff --git a/src/parser/smt1/Makefile.am b/src/parser/smt1/Makefile.am index ae49d0659..f5320002d 100644 --- a/src/parser/smt1/Makefile.am +++ b/src/parser/smt1/Makefile.am @@ -5,6 +5,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTH # Compile generated C files using C++ compiler AM_CFLAGS = $(AM_CXXFLAGS) +CFLAGS=$(CXXFLAGS) CC=$(CXX) ANTLR_OPTS = diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index 315ded475..b30922d58 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -71,9 +71,9 @@ options { // files. See the documentation in "parser/antlr_undefines.h" for more details. #include "parser/antlr_undefines.h" +#include <memory> #include <stdint.h> -#include "base/ptr_closer.h" #include "smt/command.h" #include "parser/parser.h" #include "parser/antlr_tracing.h" @@ -115,7 +115,6 @@ namespace CVC4 { #include <vector> #include "base/output.h" -#include "base/ptr_closer.h" #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" @@ -157,7 +156,7 @@ parseExpr returns [CVC4::parser::smt1::myExpr expr] */ parseCommand returns [CVC4::Command* cmd_return = NULL] @declarations { - CVC4::PtrCloser<CVC4::Command> cmd; + std::unique_ptr<CVC4::Command> cmd; } @after { cmd_return = cmd.release(); @@ -177,7 +176,7 @@ parseCommand returns [CVC4::Command* cmd_return = NULL] * Matches the whole SMT-LIB benchmark. * @return the sequence command containing the whole problem */ -benchmark [CVC4::PtrCloser<CVC4::Command>* cmd] +benchmark [std::unique_ptr<CVC4::Command>* cmd] : LPAREN_TOK BENCHMARK_TOK IDENTIFIER benchAttributes[cmd] RPAREN_TOK | EOF ; @@ -187,10 +186,10 @@ benchmark [CVC4::PtrCloser<CVC4::Command>* cmd] * command sequence. * @return the command sequence */ -benchAttributes [CVC4::PtrCloser<CVC4::Command>* cmd] +benchAttributes [std::unique_ptr<CVC4::Command>* cmd] @init { - CVC4::PtrCloser<CVC4::CommandSequence> cmd_seq(new CommandSequence()); - CVC4::PtrCloser<CVC4::Command> attribute; + std::unique_ptr<CVC4::CommandSequence> cmd_seq(new CommandSequence()); + std::unique_ptr<CVC4::Command> attribute; } @after { cmd->reset(cmd_seq.release()); @@ -205,13 +204,13 @@ benchAttributes [CVC4::PtrCloser<CVC4::Command>* cmd] * a corresponding command * @return a command corresponding to the attribute */ -benchAttribute [CVC4::PtrCloser<CVC4::Command>* smt_command] +benchAttribute [std::unique_ptr<CVC4::Command>* smt_command] @declarations { std::string name; BenchmarkStatus b_status; Expr expr; - CVC4::PtrCloser<CVC4::CommandSequence> command_seq; - CVC4::PtrCloser<CVC4::Command> declaration_command; + std::unique_ptr<CVC4::CommandSequence> command_seq; + std::unique_ptr<CVC4::Command> declaration_command; } : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->preemptCommand(new SetBenchmarkLogicCommand(name)); @@ -495,7 +494,7 @@ attribute[std::string& s] { s = AntlrInput::tokenText($ATTR_IDENTIFIER); } ; -functionDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command] +functionDeclaration[std::unique_ptr<CVC4::Command>* smt_command] @declarations { std::string name; std::vector<Type> sorts; @@ -517,7 +516,7 @@ functionDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command] /** * Matches the declaration of a predicate and declares it */ -predicateDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command] +predicateDeclaration[std::unique_ptr<CVC4::Command>* smt_command] @declarations { std::string name; std::vector<Type> p_sorts; @@ -534,7 +533,7 @@ predicateDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command] } ; -sortDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command] +sortDeclaration[std::unique_ptr<CVC4::Command>* smt_command] @declarations { std::string name; } @@ -590,7 +589,7 @@ status[ CVC4::BenchmarkStatus& status ] * Matches an annotation, which is an attribute name, with an optional user * value. */ -annotation[CVC4::PtrCloser<CVC4::Command>* smt_command] +annotation[std::unique_ptr<CVC4::Command>* smt_command] @init { std::string key, value; std::vector<Expr> pats; diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am index fece5e5e8..995e442e6 100644 --- a/src/parser/smt2/Makefile.am +++ b/src/parser/smt2/Makefile.am @@ -5,6 +5,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTH # Compile generated C files using C++ compiler AM_CFLAGS = $(AM_CXXFLAGS) +CFLAGS=$(CXXFLAGS) CC=$(CXX) ANTLR_OPTS = diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5d24ec024..88709c29a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -85,7 +85,8 @@ using namespace CVC4::parser; // files. See the documentation in "parser/antlr_undefines.h" for more details. #include "parser/antlr_undefines.h" -#include "base/ptr_closer.h" +#include <memory> + #include "parser/parser.h" #include "parser/antlr_tracing.h" #include "smt/command.h" @@ -205,7 +206,7 @@ parseExpr returns [CVC4::parser::smt2::myExpr expr] */ parseCommand returns [CVC4::Command* cmd_return = NULL] @declarations { - CVC4::PtrCloser<CVC4::Command> cmd; + std::unique_ptr<CVC4::Command> cmd; std::string name; } @after { @@ -241,7 +242,7 @@ parseCommand returns [CVC4::Command* cmd_return = NULL] */ parseSygus returns [CVC4::Command* cmd_return = NULL] @declarations { - CVC4::PtrCloser<CVC4::Command> cmd; + std::unique_ptr<CVC4::Command> cmd; std::string name; } @after { @@ -255,7 +256,7 @@ parseSygus returns [CVC4::Command* cmd_return = NULL] * Parse the internal portion of the command, ignoring the surrounding * parentheses. */ -command [CVC4::PtrCloser<CVC4::Command>* cmd] +command [std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name; std::vector<std::string> names; @@ -455,7 +456,7 @@ command [CVC4::PtrCloser<CVC4::Command>* cmd] PARSER_STATE->pushUnsatCoreNameScope(); cmd->reset(new PushCommand()); } else { - CVC4::PtrCloser<CommandSequence> seq(new CommandSequence()); + std::unique_ptr<CommandSequence> seq(new CommandSequence()); do { PARSER_STATE->pushScope(); PARSER_STATE->pushUnsatCoreNameScope(); @@ -495,7 +496,7 @@ command [CVC4::PtrCloser<CVC4::Command>* cmd] PARSER_STATE->popScope(); cmd->reset(new PopCommand()); } else { - CVC4::PtrCloser<CommandSequence> seq(new CommandSequence()); + std::unique_ptr<CommandSequence> seq(new CommandSequence()); do { PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); @@ -554,7 +555,7 @@ command [CVC4::PtrCloser<CVC4::Command>* cmd] } ; -sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] +sygusCommand [std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name, fun; std::vector<std::string> names; @@ -565,7 +566,7 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] std::vector<Expr> sygus_vars; std::vector<std::pair<std::string, Type> > sortedVarNames; SExpr sexpr; - CVC4::PtrCloser<CVC4::CommandSequence> seq; + std::unique_ptr<CVC4::CommandSequence> seq; std::vector< std::vector< CVC4::SygusGTerm > > sgts; std::vector< CVC4::Datatype > datatypes; std::vector< std::vector<Expr> > ops; @@ -1075,7 +1076,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] ; // Separate this into its own rule (can be invoked by set-info or meta-info) -metaInfoInternal[CVC4::PtrCloser<CVC4::Command>* cmd] +metaInfoInternal[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name; SExpr sexpr; @@ -1105,7 +1106,7 @@ metaInfoInternal[CVC4::PtrCloser<CVC4::Command>* cmd] } ; -setOptionInternal[CVC4::PtrCloser<CVC4::Command>* cmd] +setOptionInternal[std::unique_ptr<CVC4::Command>* cmd] @init { std::string name; SExpr sexpr; @@ -1122,7 +1123,7 @@ setOptionInternal[CVC4::PtrCloser<CVC4::Command>* cmd] } ; -smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd] +smt25Command[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name; std::string fname; @@ -1136,7 +1137,7 @@ smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd] std::vector<Expr> funcs; std::vector<Expr> func_defs; Expr aexpr; - CVC4::PtrCloser<CVC4::CommandSequence> seq; + std::unique_ptr<CVC4::CommandSequence> seq; } /* meta-info */ : META_INFO_TOK metaInfoInternal[cmd] @@ -1330,7 +1331,7 @@ smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd] // GET_UNSAT_ASSUMPTIONS ; -extendedCommand[CVC4::PtrCloser<CVC4::Command>* cmd] +extendedCommand[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<CVC4::Datatype> dts; Expr e, e2; @@ -1340,7 +1341,7 @@ extendedCommand[CVC4::PtrCloser<CVC4::Command>* cmd] std::vector<Expr> terms; std::vector<Type> sorts; std::vector<std::pair<std::string, Type> > sortedVarNames; - CVC4::PtrCloser<CVC4::CommandSequence> seq; + std::unique_ptr<CVC4::CommandSequence> seq; } /* Extended SMT-LIB set of commands syntax, not permitted in * --smtlib2 compliance mode. */ @@ -1495,7 +1496,7 @@ extendedCommand[CVC4::PtrCloser<CVC4::Command>* cmd] ; -datatypes_2_5_DefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] +datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<CVC4::Datatype> dts; std::string name; @@ -1515,7 +1516,7 @@ datatypes_2_5_DefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] } ; -datatypeDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] +datatypeDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<CVC4::Datatype> dts; std::string name; @@ -1530,7 +1531,7 @@ datatypeDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] { cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); } ; -datatypesDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] +datatypesDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<CVC4::Datatype> dts; std::string name; @@ -1593,7 +1594,7 @@ datatypesDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd] } ; -rewriterulesCommand[CVC4::PtrCloser<CVC4::Command>* cmd] +rewriterulesCommand[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<std::pair<std::string, Type> > sortedVarNames; std::vector<Expr> args, guards, heads, triggers; diff --git a/src/parser/tptp/Makefile.am b/src/parser/tptp/Makefile.am index eab01103f..43bbc595d 100644 --- a/src/parser/tptp/Makefile.am +++ b/src/parser/tptp/Makefile.am @@ -5,6 +5,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTH # Compile generated C files using C++ compiler AM_CFLAGS = $(AM_CXXFLAGS) +CFLAGS=$(CXXFLAGS) CC=$(CXX) ANTLR_OPTS = diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index fe4ea6f98..fbd3d8cfb 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -93,6 +93,8 @@ using namespace CVC4::parser; // files. See the documentation in "parser/antlr_undefines.h" for more details. #include "parser/antlr_undefines.h" +#include <memory> + #include "smt/command.h" #include "parser/parser.h" #include "parser/tptp/tptp.h" diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index ef22e1c0d..30b9ca0b5 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -105,11 +105,7 @@ bool Variable::isTranscendentalMember(Node n) { bool VarList::isSorted(iterator start, iterator end) { -#if IS_SORTED_IN_GNUCXX_NAMESPACE - return __gnu_cxx::is_sorted(start, end); -#else /* IS_SORTED_IN_GNUCXX_NAMESPACE */ return std::is_sorted(start, end); -#endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */ } bool VarList::isMember(Node n) { @@ -198,8 +194,7 @@ VarList VarList::operator*(const VarList& other) const { otherEnd = other.internalEnd(); Variable::VariableNodeCmp cmp; - - merge_ranges(thisBegin, thisEnd, otherBegin, otherEnd, result, cmp); + std::merge(thisBegin, thisEnd, otherBegin, otherEnd, std::back_inserter(result), cmp); Assert(result.size() >= 2); Node mult = NodeManager::currentNM()->mkNode(kind::NONLINEAR_MULT, result); @@ -356,7 +351,7 @@ void Monomial::printList(const std::vector<Monomial>& list) { Polynomial Polynomial::operator+(const Polynomial& vl) const { std::vector<Monomial> sortedMonos; - merge_ranges(begin(), end(), vl.begin(), vl.end(), sortedMonos); + std::merge(begin(), end(), vl.begin(), vl.end(), std::back_inserter(sortedMonos)); Monomial::combineAdjacentMonomials(sortedMonos); //std::vector<Monomial> combined = Monomial::sumLikeTerms(sortedMonos); diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index d8f5259fc..21301da91 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -23,10 +23,6 @@ #include <algorithm> #include <list> -#if IS_SORTED_IN_GNUCXX_NAMESPACE -# include <ext/algorithm> -#endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */ - #include "base/output.h" #include "expr/node.h" #include "expr/node_self_iterator.h" @@ -284,7 +280,7 @@ public: } struct VariableNodeCmp { - static inline int cmp(Node n, Node m) { + static inline int cmp(const Node& n, const Node& m) { if ( n == m ) { return 0; } // this is now slightly off of the old variable order. @@ -320,7 +316,7 @@ public: } } - bool operator()(Node n, Node m) const { + bool operator()(const Node& n, const Node& m) const { return VariableNodeCmp::cmp(n,m) < 0; } }; @@ -431,56 +427,6 @@ inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) { return Node(nb); }/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */ - -template <class GetNodeIterator, class T> -static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector<T>& result){ - while(begin != end){ - result.push_back(*begin); - ++begin; - } -} - -template <class GetNodeIterator, class T> -static void merge_ranges(GetNodeIterator first1, - GetNodeIterator last1, - GetNodeIterator first2, - GetNodeIterator last2, - std::vector<T>& result) { - - while(first1 != last1 && first2 != last2){ - if( (*first1) < (*first2) ){ - result.push_back(*first1); - ++ first1; - }else{ - result.push_back(*first2); - ++ first2; - } - } - copy_range(first1, last1, result); - copy_range(first2, last2, result); -} - -template <class GetNodeIterator, class T, class Cmp> -static void merge_ranges(GetNodeIterator first1, - GetNodeIterator last1, - GetNodeIterator first2, - GetNodeIterator last2, - std::vector<T>& result, - const Cmp& cmp) { - - while(first1 != last1 && first2 != last2){ - if( cmp(*first1, *first2) ){ - result.push_back(*first1); - ++ first1; - }else{ - result.push_back(*first2); - ++ first2; - } - } - copy_range(first1, last1, result); - copy_range(first2, last2, result); -} - /** * A VarList is a sorted list of variables representing a product. * If the VarList is empty, it represents an empty product or 1. @@ -749,11 +695,7 @@ public: } static bool isSorted(const std::vector<Monomial>& m) { -#if IS_SORTED_IN_GNUCXX_NAMESPACE - return __gnu_cxx::is_sorted(m.begin(), m.end()); -#else /* IS_SORTED_IN_GNUCXX_NAMESPACE */ return std::is_sorted(m.begin(), m.end()); -#endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */ } static bool isStrictlySorted(const std::vector<Monomial>& m) { @@ -852,7 +794,7 @@ private: public: static bool isMember(TNode n); - class iterator { + class iterator : public std::iterator<std::input_iterator_tag, Monomial> { private: internal_iterator d_iter; @@ -954,7 +896,7 @@ public: iterator tailStart = begin(); ++tailStart; std::vector<Monomial> subrange; - copy_range(tailStart, end(), subrange); + std::copy(tailStart, end(), std::back_inserter(subrange)); return mkPolynomial(subrange); } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index f70db9823..a2a56e137 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -17,8 +17,6 @@ #include <algorithm> #include "theory/sets/theory_sets_private.h" -#include <boost/foreach.hpp> - #include "expr/emptyset.h" #include "options/sets_options.h" #include "smt/smt_statistics_registry.h" @@ -56,7 +54,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, { d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external); - + d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); @@ -79,9 +77,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, TheorySetsPrivate::~TheorySetsPrivate(){ delete d_rels; - for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end(); i != iend; ++i){ - EqcInfo* current = (*i).second; - delete current; + for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info) { + delete current_pair.second; } }/* TheorySetsPrivate::~TheorySetsPrivate() */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index cd6f0e11c..877525de7 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -34,6 +34,7 @@ libutil_la_SOURCES = \ floatingpoint.h \ gmp_util.h \ hash.h \ + index.cpp \ index.h \ maybe.h \ ntuple.h \ diff --git a/src/util/index.cpp b/src/util/index.cpp new file mode 100644 index 000000000..bd15e2d80 --- /dev/null +++ b/src/util/index.cpp @@ -0,0 +1,21 @@ +#include "util/index.h" + +#include <cstddef> +#include <limits> + +namespace CVC4 { + +static_assert(sizeof(Index) <= sizeof(size_t), + "Index cannot be larger than size_t"); +static_assert(!std::numeric_limits<Index>::is_signed, + "Index must be unsigned"); + +/* Discussion: Why is Index a uint32_t instead of size_t (or uint_fast32_t)? + * + * size_t is a more appropriate choice than uint32_t as the choice is dictated + * by uniqueness in arrays and vectors. These correspond to size_t. However, the + * using size_t with a sizeof == 8 on 64 bit platforms is noticeably slower. + * (Limited testing suggests a ~1/16 of running time.) Interestingly, + * uint_fast32_t also has a sizeof == 8 on x86_64. + */ +}/* CVC4 namespace */ diff --git a/src/util/index.h b/src/util/index.h index a8910a696..7329e3f8d 100644 --- a/src/util/index.h +++ b/src/util/index.h @@ -9,39 +9,23 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Standardized type for efficient array indexing. ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** Standardized type for efficient array indexing. **/ #include "cvc4_private.h" -#pragma once +#ifndef __CVC4__INDEX_H +#define __CVC4__INDEX_H -#include <stdint.h> -#include <boost/static_assert.hpp> -#include <limits> +#include <cstdint> namespace CVC4 { -/** - * Index is an unsigned integer used for array indexing. - * - * This gives a standardized type for independent pieces of code to use as an agreement. - */ -typedef uint32_t Index; - -BOOST_STATIC_ASSERT(sizeof(Index) <= sizeof(size_t)); -BOOST_STATIC_ASSERT(!std::numeric_limits<Index>::is_signed); - -/* Discussion: Why is Index a uint32_t instead of size_t (or uint_fast32_t)? - * - * size_t is a more appropriate choice than uint32_t as the choice is dictated by - * uniqueness in arrays and vectors. These correspond to size_t. - * However, the using size_t with a sizeof == 8 on 64 bit platforms is noticeably - * slower. (Limited testing suggests a ~1/16 of running time.) - * (Interestingly, uint_fast32_t also has a sizeof == 8 on x86_64. Filthy Liars!) - */ +/** Index is a standardized unsigned integer used for efficient indexing. */ +using Index = uint32_t; }/* CVC4 namespace */ + +#endif /* __CVC4__INDEX_H */ |