From 9d751576bc72bbe02ad0d819f162bae3ee30ee14 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 2 Apr 2023 16:12:26 -0700
Subject: [PATCH] add utility to count clauses

---
 src/math/polysat/constraint_manager.cpp | 1 +
 src/math/polysat/constraint_manager.h   | 7 +++++++
 2 files changed, 8 insertions(+)

diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index 5b336a2d5..91a4ba358 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -232,6 +232,7 @@ namespace polysat {
     void constraint_manager::gc_clauses() {
         LOG_H3("gc_clauses");
         // place to gc redundant clauses
+        // clauses on_reinit_stack() cannot be gc'ed
     }
 
     void constraint_manager::gc_constraints() {
diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h
index 2710dfb70..1619223c8 100644
--- a/src/math/polysat/constraint_manager.h
+++ b/src/math/polysat/constraint_manager.h
@@ -106,6 +106,13 @@ namespace polysat {
         bool watch(clause& cl);
         void unwatch(clause& cl);
 
+        unsigned num_clauses() const {
+            unsigned n = 0;
+            for (auto const& lvl : m_clauses)
+                n += lvl.size();
+            return n;
+        }
+
         constraint* lookup(sat::bool_var var) const;
         signed_constraint lookup(sat::literal lit) const;