From 64ba2a9fc9919cfddcc963d0b951e6f793ebc7be Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 19 Jan 2021 03:38:00 -0800
Subject: [PATCH] fix gc of pb constraints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_extension.h    |  1 +
 src/sat/sat_gc.cpp         |  3 +++
 src/sat/smt/ba_solver.cpp  | 24 +++++++++++++++++++++++-
 src/sat/smt/ba_solver.h    |  2 ++
 src/sat/smt/euf_solver.cpp |  5 +++++
 src/sat/smt/euf_solver.h   |  1 +
 6 files changed, 35 insertions(+), 1 deletion(-)

diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index 815118309..ce504bea6 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -117,6 +117,7 @@ namespace sat {
         virtual void init_use_list(ext_use_list& ul) {}
         virtual bool is_blocked(literal l, ext_constraint_idx) { return false; }
         virtual bool check_model(model const& m) const { return true; }
+        virtual void gc_vars(unsigned num_vars) {}
 
         virtual bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
                                 std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) {                                
diff --git a/src/sat/sat_gc.cpp b/src/sat/sat_gc.cpp
index 2179a324f..6b5618b2b 100644
--- a/src/sat/sat_gc.cpp
+++ b/src/sat/sat_gc.cpp
@@ -470,6 +470,9 @@ namespace sat {
         };
         gc_clauses(m_learned);
         gc_clauses(m_clauses);
+
+        if (m_ext)
+            m_ext->gc_vars(max_var);
         
         unsigned j = 0;
         for (literal lit : m_trail) {
diff --git a/src/sat/smt/ba_solver.cpp b/src/sat/smt/ba_solver.cpp
index c29694ac3..9bed103f4 100644
--- a/src/sat/smt/ba_solver.cpp
+++ b/src/sat/smt/ba_solver.cpp
@@ -1892,9 +1892,31 @@ namespace sat {
         m_stats.m_num_gc += removed;
         m_learned.shrink(new_sz);
         IF_VERBOSE(2, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << removed << ")\n";);
-
     }
 
+
+    void ba_solver::gc_vars(unsigned num_vars) {
+        gc_vars(num_vars, m_constraints);
+        gc_vars(num_vars, m_learned);
+    }
+
+    void ba_solver::gc_vars(unsigned num_vars, ptr_vector<constraint>& cs) {
+        unsigned j = 0;
+        for (unsigned i = 0; i < cs.size(); ++i) {
+            auto* c = cs[i];
+            unsigned m = c->fold_max_var(0);
+            if (m >= num_vars) {
+                clear_watch(*c);
+                c->nullify_tracking_literal(*this);
+                c->deallocate(m_allocator);
+            }
+            else 
+                cs[j++] = c;
+        }
+        cs.shrink(j);
+    }
+
+
     lbool ba_solver::add_assign(card& c, literal alit) {
         // literal is assigned to false.        
         unsigned sz = c.size();
diff --git a/src/sat/smt/ba_solver.h b/src/sat/smt/ba_solver.h
index b87697e94..0cf4b001f 100644
--- a/src/sat/smt/ba_solver.h
+++ b/src/sat/smt/ba_solver.h
@@ -187,6 +187,7 @@ namespace sat {
         void cleanup_constraints();
         void cleanup_constraints(ptr_vector<constraint>& cs, bool learned);
         void remove_constraint(constraint& c, char const* reason);
+        void gc_vars(unsigned num_vars, ptr_vector<constraint>& cs);
 
         // constraints
         constraint& index2constraint(size_t idx) const { return *reinterpret_cast<constraint*>(constraint_base::from_index(idx)->mem()); }
@@ -424,6 +425,7 @@ namespace sat {
         void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override;
         void pop_reinit() override;
         void gc() override;
+        void gc_vars(unsigned num_vars) override;
         bool is_extended_binary(ext_justification_idx idx, literal_vector & r) override;
         void init_use_list(ext_use_list& ul) override;
         bool is_blocked(literal l, ext_constraint_idx idx) override;
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index c9897a049..7ae2875d3 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -728,6 +728,11 @@ namespace euf {
                 return false;
         return true;
     }
+
+    void solver::gc_vars(unsigned num_vars) {
+        for (auto* e : m_solvers)
+            e->gc_vars(num_vars);
+    }
     
     double solver::get_reward(literal l, ext_constraint_idx idx, sat::literal_occs_fun& occs) const {
         auto* ext = sat::constraint_base::to_extension(idx);
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index d9ec97dc7..f03a7a109 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -304,6 +304,7 @@ namespace euf {
         void init_use_list(sat::ext_use_list& ul) override;
         bool is_blocked(literal l, ext_constraint_idx) override;
         bool check_model(sat::model const& m) const override;
+        void gc_vars(unsigned num_vars) override;
 
         // proof
         bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }