From 1d928663de266022755483d4ad3d04d8d8c7a9bc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Mar 2026 22:57:59 -0700 Subject: [PATCH] add reset method Signed-off-by: Nikolaj Bjorner --- src/smt/nseq_context_solver.h | 4 ++++ src/smt/seq/seq_nielsen.cpp | 5 +---- src/smt/seq/seq_nielsen.h | 1 + 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/smt/nseq_context_solver.h b/src/smt/nseq_context_solver.h index 54139f6c1..803cee39e 100644 --- a/src/smt/nseq_context_solver.h +++ b/src/smt/nseq_context_solver.h @@ -68,6 +68,10 @@ namespace smt { void get_model(model_ref& mdl) override { m_kernel.get_model(mdl); } + + void reset() override { + m_kernel.reset(); + } }; } diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 370927572..1e54ac798 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -538,8 +538,6 @@ namespace seq { m_parikh(alloc(seq_parikh, sg)), m_seq_regex(alloc(seq::seq_regex, sg)), m_len_vars(sg.get_manager()) { - - m_solver.push(); // we start by resetting the graph which will pop it first } nielsen_graph::~nielsen_graph() { @@ -635,8 +633,7 @@ namespace seq { m_len_var_cache.clear(); m_len_vars.reset(); m_dep_mgr.reset(); - m_solver.pop(1); - m_solver.push(); + m_solver.reset(); } std::ostream& nielsen_graph::display(std::ostream& out) const { diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index e597db807..64a5e57c1 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -278,6 +278,7 @@ namespace seq { virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0; virtual void get_model(model_ref& mdl) { mdl = nullptr; } + virtual void reset() = 0; }; // simplification result for constraint processing