From e50e990e5a0a85c5e36c6a6b6d8a59c3482b08fb Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Fri, 8 Nov 2019 13:41:21 -0800
Subject: [PATCH] cmake: Disable C++ GNU extensions. (#3446)

Fixes #971.
---
 CMakeLists.txt                    |  1 +
 src/prop/cnf_stream.h             | 19 -------------------
 src/smt/smt_statistics_registry.h | 30 ------------------------------
 src/util/statistics_registry.h    |  6 +-----
 4 files changed, 2 insertions(+), 54 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5efce1260..294286e30 100644
--- 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 8e60863fa..a9b786615 100644
--- 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 e6932a084..1a0993d1d 100644
--- 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 a369be272..4d4cc76df 100644
--- 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:
-- 
2.30.2