cmake: Disable C++ GNU extensions. (#3446)

Fixes #971.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5efce12608a042ea31a21579fad31e199c43fe04..294286e30169bf61d55868842c647e8f0043507d 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -26,6 +26,7 @@ endif()
 set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
 set(CMAKE_C_STANDARD 99)
 set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_EXTENSIONS OFF)
 
 # Generate compile_commands.json, which can be used for various code completion
 # plugins.

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 8e60863fabc8d4569a8e9a49ead534c32d818d4e..a9b786615377c21b8027b34ee12a290113069ff0 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -88,25 +88,6 @@ class CnfStream {
   /** Pointer to the proof corresponding to this CnfStream */
   CnfProof* d_cnfProof;
 
-  /**
-   * How many literals were already mapped at the top-level when we
-   * tried to convertAndAssert() something.  This
-   * achieves early detection of units and leads to fewer
-   * clauses.  It's motivated by the following pattern:
-   *
-   *   ASSERT  BIG FORMULA => x
-   *   (and then later...)
-   *   ASSERT  BIG FORMULA
-   *
-   * With the first assert, BIG FORMULA is clausified, and a literal
-   * is assigned for the top level so that the final clause for the
-   * implication is "lit => x".  But without "fortunate literal
-   * detection," when BIG FORMULA is later asserted, it is clausified
-   * separately, and "lit" is never asserted as a unit clause.
-   */
-  // KEEP_STATISTIC(IntStat, d_fortunateLiterals,
-  //               "prop::CnfStream::fortunateLiterals", 0);
-
   /** Remove nots from the node */
   TNode stripNot(TNode node) {
     while (node.getKind() == kind::NOT) {

diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h
index e6932a084db2359eacfef89f75a04052b4e8e4f0..1a0993d1de66d75f80fd6a2b8d159dd9b076a86b 100644 (file)
--- a/src/smt/smt_statistics_registry.h
+++ b/src/smt/smt_statistics_registry.h
@@ -28,34 +28,4 @@ namespace CVC4 {
  */
 StatisticsRegistry* smtStatisticsRegistry();
 
-
-/**
- * To use a statistic, you need to declare it, initialize it in your
- * constructor, register it in your constructor, and deregister it in
- * your destructor.  Instead, this macro does it all for you (and
- * therefore also keeps the statistic type, field name, and output
- * string all in the same place in your class's header.  Its use is
- * like in this example, which takes the place of the declaration of a
- * statistics field "d_checkTimer":
- *
- *   KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::checkTime");
- *
- * If any args need to be passed to the constructor, you can specify
- * them after the string.
- *
- * The macro works by creating a nested class type, derived from the
- * statistic type you give it, which declares a registry-aware
- * constructor/destructor pair.
- */
-#define KEEP_STATISTIC(_StatType, _StatField, _StatName, _CtorArgs...)  \
-  struct Statistic_##_StatField : public _StatType {                    \
-    Statistic_##_StatField() : _StatType(_StatName, ## _CtorArgs) {     \
-      smtStatisticsRegistry()->registerStat(this);                 \
-    }                                                                   \
-    ~Statistic_##_StatField() {                                         \
-      smtStatisticsRegistry()->unregisterStat(this);                         \
-    }                                                                   \
-  } _StatField
-
-
 }/* CVC4 namespace */

diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index a369be272d83d0ca1b4e684b8f26787b404dce31..4d4cc76df4f54dfb7a49ecbf6658e377ef662f46 100644 (file)
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -780,11 +780,7 @@ public:
 /**
  * Resource-acquisition-is-initialization idiom for statistics
  * registry.  Useful for stack-based statistics (like in the driver).
- * Generally, for statistics kept in a member field of class, it's
- * better to use the above KEEP_STATISTIC(), which does declaration of
- * the member, construction of the statistic, and
- * registration/unregistration.  This RAII class only does
- * registration and unregistration.
+ * This RAII class only does registration and unregistration.
  */
 class CVC4_PUBLIC RegisterStatistic {
 public: