From c0f43b9206f7d6a3050ca6a1772f544d7c7b5969 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Mar 2023 09:58:44 -0700 Subject: [PATCH] expose watch/unwatch Signed-off-by: Nikolaj Bjorner --- src/math/polysat/constraint_manager.h | 5 +++-- src/math/polysat/solver.cpp | 3 --- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h index 66a72dea9..0d2328136 100644 --- a/src/math/polysat/constraint_manager.h +++ b/src/math/polysat/constraint_manager.h @@ -77,8 +77,6 @@ namespace polysat { void gc_clauses(); void normalize_watch(clause& cl); - bool watch(clause& cl); - void unwatch(clause& cl); void register_clause(clause* cl); @@ -103,6 +101,9 @@ namespace polysat { void gc(); bool should_gc(); + bool watch(clause& cl); + void unwatch(clause& cl); + constraint* lookup(sat::bool_var var) const; signed_constraint lookup(sat::literal lit) const; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index b51862b18..50222b7c7 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -349,11 +349,8 @@ namespace polysat { clause& c = *m_clauses_to_reinit[i]; SASSERT(c.on_reinit_stack()); bool reinit = false; -#if 0 - // todo, private methods to constraint_manager m_constraints.unwatch(c); reinit = m_constraints.watch(c); -#endif // reinit <- true if clause is used for propagation