diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-11-08 13:41:21 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-08 13:41:21 -0800 |
commit | e50e990e5a0a85c5e36c6a6b6d8a59c3482b08fb (patch) | |
tree | 3b981f3ca75cc788cd934f5d18215c14c51060ce /src/prop/cnf_stream.h | |
parent | cbd86eb4ed8bafc17f28244b746a376a019462f1 (diff) |
cmake: Disable C++ GNU extensions. (#3446)
Fixes #971.
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 19 |
1 files changed, 0 insertions, 19 deletions
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) { |