From 2226f508e80b66f8eb48a20c4c385d0aa97fa8c6 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 24 Jul 2023 10:53:57 +0200 Subject: [PATCH] notes on gc --- src/math/polysat/solver.cpp | 15 +++++++++++++++ src/math/polysat/types.h | 8 ++++++++ 2 files changed, 23 insertions(+) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index c077512c9..10a6ccf7a 100644 --- a/src/math/polysat/solver.cpp +++ b/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" diff --git a/src/math/polysat/types.h b/src/math/polysat/types.h index 19b191d4e..bcc8d76fa 100644 --- a/src/math/polysat/types.h +++ b/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: