From d05dccf331c2c9a200e7ffbc3735d629139e0fad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Apr 2026 13:30:15 -0700 Subject: [PATCH] add current_value access Signed-off-by: Nikolaj Bjorner --- src/smt/nseq_context_solver.h | 4 ++++ src/smt/seq/seq_nielsen.h | 2 ++ 2 files changed, 6 insertions(+) diff --git a/src/smt/nseq_context_solver.h b/src/smt/nseq_context_solver.h index 81a0796b8..c82161647 100644 --- a/src/smt/nseq_context_solver.h +++ b/src/smt/nseq_context_solver.h @@ -88,6 +88,10 @@ namespace smt { return m_arith_value.get_up(e, hi, is_strict) && !is_strict && hi.is_int(); } + bool current_value(expr* e, rational& v) const override { + return m_arith_value.get_value(e, v) && v.is_int(); + } + lbool check_with_assumptions(expr_ref_vector& assumptions, expr_ref_vector& core) override { // TODO: Not ideal // Replay with assumptions diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index a057c587e..99f679798 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -284,6 +284,8 @@ namespace seq { // Default implementation reports "unsupported". virtual bool lower_bound(expr* e, rational& lo) const { return false; } virtual bool upper_bound(expr* e, rational& hi) const { return false; } + virtual bool current_value(expr *e, rational &v) const { return false; } + virtual void reset() = 0; };