mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

remove dead code

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-26 13:48:55 -08:00
parent d3a6521185
commit c58171478f
2 changed files with 0 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/sls/sls_bv_plugin.cpp
View file

@ -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 bv_plugin::is_sat() {
bool is_sat = true; bool is_sat = true;
for (auto t : ctx.subterms()) for (auto t : ctx.subterms())

2
src/ast/sls/sls_bv_plugin.h
View file

@ -30,10 +30,8 @@ namespace sls {
bv::sls_stats m_stats; bv::sls_stats m_stats;
bool m_initialized = false; bool m_initialized = false;
void init_bool_var_assignment(sat::bool_var v);
std::ostream& trace_repair(bool down, expr* e); std::ostream& trace_repair(bool down, expr* e);
void trace(); void trace();
bool can_propagate();
bool is_bv_predicate(expr* e); bool is_bv_predicate(expr* e);
void log(expr* e, bool up_down, bool success); void log(expr* e, bool up_down, bool success);