From c58171478f25a60a70db1b449708db4c050806ce Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Dec 2024 13:48:55 -0800 Subject: [PATCH] remove dead code --- src/ast/sls/sls_bv_plugin.cpp | 12 ------------ src/ast/sls/sls_bv_plugin.h | 2 -- 2 files changed, 14 deletions(-) diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp index 4973bfaee..4c2877235 100644 --- a/src/ast/sls/sls_bv_plugin.cpp +++ b/src/ast/sls/sls_bv_plugin.cpp @@ -81,18 +81,6 @@ namespace sls { } } - void bv_plugin::init_bool_var_assignment(sat::bool_var v) { - auto a = ctx.atom(v); - if (!a || !is_app(a)) - return; - if (to_app(a)->get_family_id() != bv.get_family_id()) - return; - bool is_true = m_eval.bval1(to_app(a)); - - if (is_true != ctx.is_true(v)) - ctx.flip(v); - } - bool bv_plugin::is_sat() { bool is_sat = true; for (auto t : ctx.subterms()) diff --git a/src/ast/sls/sls_bv_plugin.h b/src/ast/sls/sls_bv_plugin.h index 7d9e338e7..ea750163e 100644 --- a/src/ast/sls/sls_bv_plugin.h +++ b/src/ast/sls/sls_bv_plugin.h @@ -30,10 +30,8 @@ namespace sls { bv::sls_stats m_stats; bool m_initialized = false; - void init_bool_var_assignment(sat::bool_var v); std::ostream& trace_repair(bool down, expr* e); void trace(); - bool can_propagate(); bool is_bv_predicate(expr* e); void log(expr* e, bool up_down, bool success);