From 237ee6b083accd5db2206dc89189f897934cfcb5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 04:54:08 -0800 Subject: [PATCH] tidy' Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat_core.cpp | 10 ++++++++++ src/sat/smt/polysat_core.h | 4 ++-- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/polysat_core.cpp b/src/sat/smt/polysat_core.cpp index f3950adf2..73e9c5a6b 100644 --- a/src/sat/smt/polysat_core.cpp +++ b/src/sat/smt/polysat_core.cpp @@ -290,6 +290,16 @@ namespace polysat { s.ctx.push(push_back_vector(m_prop_queue)); } + dependency_vector core::explain_eval(signed_constraint const& sc) { + dependency_vector deps; + for (auto v : sc.vars()) + if (is_assigned(v)) + deps.push_back(m_justification[v]); + return deps; + } + lbool core::eval(signed_constraint const& sc) { + throw default_exception("nyi"); + } } diff --git a/src/sat/smt/polysat_core.h b/src/sat/smt/polysat_core.h index 802108ffc..6944c39d8 100644 --- a/src/sat/smt/polysat_core.h +++ b/src/sat/smt/polysat_core.h @@ -83,8 +83,8 @@ namespace polysat { signed_constraint get_constraint(unsigned idx, bool sign); - lbool eval(signed_constraint sc) { throw default_exception("nyi"); } - dependency_vector explain_eval(signed_constraint const& dc) { throw default_exception("nyi"); } + lbool eval(signed_constraint const& sc); + dependency_vector explain_eval(signed_constraint const& sc); public: core(solver& s);