notes on gc

src/math/polysat/solver.cpp

@@ -14,6 +14,21 @@ Author:
     Nikolaj Bjorner (nbjorner) 2021-03-19
     Jakob Rath 2021-04-06
 
+Notes:
+
+
+TODO: at some point we should add proper garbage collection
+- currently solver::del_var is disabled because we may introduce helper variables during conflict resolution
+- each non-polynomial term (extract/concat/pseudo-inverse/...) is represented by a pvar ("special variable")
+- garbage collection:
+    - could go over trail to discover active variables/constraints
+    - could do reference counting, e.g., by counting the occurrences of special variables in constraints and clauses
+- alternatively, reinit clauses after backtracking:
+    - note all 'special' variables that have been used
+    - recreate them after backtracking
+    - replace the old variables by the newly created ones
+    - here, we would track clauses by the level they're created on, and reinit brings the clause to a lower level
+
 --*/
 
 #include "math/polysat/solver.h"

src/math/polysat/types.h

@@ -40,6 +40,14 @@ namespace polysat {
     using pvar_vector = unsigned_vector;
     inline const pvar null_var = UINT_MAX;
 
+    enum class pvar_kind : std::uint8_t {
+        external,           // regular variables (from the input formula)
+        name,               // name for a polynomial term
+        op,                 // result of an op_constraint
+        extract,            // result of an extract operation
+        concat,             // result of a concat operation
+    };
+
     class dependency {
         unsigned m_val;
     public: