mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
remove stale files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
cc208394c3
commit
c7f67f9a72
5 changed files with 17 additions and 169 deletions
|
|
@ -631,9 +631,11 @@ namespace bv {
|
|||
return sls_valuation::random_bits(m_rand);
|
||||
}
|
||||
|
||||
bool sls_eval::try_repair(app* e, unsigned i) {
|
||||
if (e->get_family_id() == bv.get_family_id())
|
||||
return try_repair_bv(e, i);
|
||||
bool sls_eval::repair_down(app* e, unsigned i) {
|
||||
if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
|
||||
ctx.new_value_eh(e->get_arg(i));
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
@ -985,7 +987,7 @@ namespace bv {
|
|||
return true;
|
||||
}
|
||||
// fall back to a random value
|
||||
return a.set_random(m_rand);
|
||||
return i == 0 ? a.set_random(m_rand) : b.set_random(m_rand);
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
|||
|
|
@ -168,7 +168,7 @@ namespace bv {
|
|||
* Try to invert value of child to repair value assignment of parent.
|
||||
*/
|
||||
|
||||
bool try_repair(app* e, unsigned i);
|
||||
bool repair_down(app* e, unsigned i);
|
||||
|
||||
/*
|
||||
* Propagate repair up to parent
|
||||
|
|
|
|||
|
|
@ -1,93 +0,0 @@
|
|||
|
||||
#include "ast/sls/sls_bv.h"
|
||||
|
||||
namespace sls {
|
||||
|
||||
bv_plugin::bv_plugin(context& ctx):
|
||||
plugin(ctx),
|
||||
bv(m),
|
||||
m_terms(m),
|
||||
m_eval(m)
|
||||
{}
|
||||
|
||||
void bv_plugin::init_bool_var(sat::bool_var v) {
|
||||
}
|
||||
|
||||
void bv_plugin::register_term(expr* e) {
|
||||
}
|
||||
|
||||
expr_ref bv_plugin::get_value(expr* e) {
|
||||
return expr_ref(m);
|
||||
}
|
||||
|
||||
lbool bv_plugin::check() {
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
bool bv_plugin::is_sat() {
|
||||
return false;
|
||||
}
|
||||
|
||||
void bv_plugin::reset() {
|
||||
}
|
||||
|
||||
void bv_plugin::on_rescale() {
|
||||
|
||||
}
|
||||
|
||||
void bv_plugin::on_restart() {
|
||||
}
|
||||
|
||||
std::ostream& bv_plugin::display(std::ostream& out) const {
|
||||
return out;
|
||||
}
|
||||
|
||||
void bv_plugin::mk_model(model& mdl) {
|
||||
|
||||
}
|
||||
|
||||
void bv_plugin::set_shared(expr* e) {
|
||||
|
||||
}
|
||||
|
||||
void bv_plugin::set_value(expr* e, expr* v) {
|
||||
|
||||
}
|
||||
|
||||
std::pair<bool, app*> bv_plugin::next_to_repair() {
|
||||
app* e = nullptr;
|
||||
if (m_repair_down != UINT_MAX) {
|
||||
e = m_terms.term(m_repair_down);
|
||||
m_repair_down = UINT_MAX;
|
||||
return { true, e };
|
||||
}
|
||||
|
||||
if (!m_repair_up.empty()) {
|
||||
unsigned index = m_repair_up.elem_at(ctx.rand(m_repair_up.size()));
|
||||
m_repair_up.remove(index);
|
||||
e = m_terms.term(index);
|
||||
return { false, e };
|
||||
}
|
||||
|
||||
while (!m_repair_roots.empty()) {
|
||||
unsigned index = m_repair_roots.elem_at(ctx.rand(m_repair_roots.size()));
|
||||
e = m_terms.term(index);
|
||||
if (m_terms.is_assertion(e) && !m_eval.bval1(e)) {
|
||||
SASSERT(m_eval.bval0(e));
|
||||
return { true, e };
|
||||
}
|
||||
if (!m_eval.re_eval_is_correct(e)) {
|
||||
init_repair_goal(e);
|
||||
return { true, e };
|
||||
}
|
||||
m_repair_roots.remove(index);
|
||||
}
|
||||
|
||||
return { false, nullptr };
|
||||
}
|
||||
|
||||
void bv_plugin::init_repair_goal(app* e) {
|
||||
m_eval.init_eval(e);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,55 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2020 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sls_bv.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Theory plugin for bit-vector local search
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2024-07-06
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "ast/sls/sls_smt.h"
|
||||
#include "ast/bv_decl_plugin.h"
|
||||
#include "ast/sls/bv_sls_terms.h"
|
||||
#include "ast/sls/bv_sls_eval.h"
|
||||
|
||||
namespace sls {
|
||||
|
||||
class bv_plugin : public plugin {
|
||||
bv_util bv;
|
||||
bv::sls_terms m_terms;
|
||||
bv::sls_eval m_eval;
|
||||
bv::sls_stats m_stats;
|
||||
|
||||
indexed_uint_set m_repair_up, m_repair_roots;
|
||||
unsigned m_repair_down = UINT_MAX;
|
||||
|
||||
std::pair<bool, app*> next_to_repair();
|
||||
void init_repair_goal(app* e);
|
||||
public:
|
||||
bv_plugin(context& ctx);
|
||||
~bv_plugin() override {}
|
||||
void init_bool_var(sat::bool_var v) override;
|
||||
void register_term(expr* e) override;
|
||||
expr_ref get_value(expr* e) override;
|
||||
lbool check() override;
|
||||
bool is_sat() override;
|
||||
void reset() override;
|
||||
|
||||
void on_rescale() override;
|
||||
void on_restart() override;
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
void mk_model(model& mdl) override;
|
||||
void set_shared(expr* e) override;
|
||||
void set_value(expr* e, expr* v) override;
|
||||
};
|
||||
|
||||
}
|
||||
|
|
@ -99,7 +99,6 @@ namespace sls {
|
|||
}
|
||||
|
||||
void bv_plugin::repair_down(app* e) {
|
||||
|
||||
unsigned n = e->get_num_args();
|
||||
if (n == 0 || m_eval.eval_is_correct(e)) {
|
||||
m_eval.commit_eval(e);
|
||||
|
|
@ -110,30 +109,25 @@ namespace sls {
|
|||
auto d1 = get_depth(e->get_arg(0));
|
||||
auto d2 = get_depth(e->get_arg(1));
|
||||
unsigned s = ctx.rand(d1 + d2 + 2);
|
||||
if (s <= d1 && m_eval.try_repair(e, 0)) {
|
||||
ctx.new_value_eh(e->get_arg(0));
|
||||
if (s <= d1 && m_eval.repair_down(e, 0))
|
||||
return;
|
||||
}
|
||||
if (m_eval.try_repair(e, 1)) {
|
||||
ctx.new_value_eh(e->get_arg(1));
|
||||
|
||||
if (m_eval.repair_down(e, 1))
|
||||
return;
|
||||
}
|
||||
if (m_eval.try_repair(e, 0)) {
|
||||
ctx.new_value_eh(e->get_arg(0));
|
||||
return;
|
||||
}
|
||||
|
||||
if (m_eval.repair_down(e, 0))
|
||||
return;
|
||||
}
|
||||
else {
|
||||
unsigned s = ctx.rand(n);
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
auto j = (i + s) % n;
|
||||
if (m_eval.try_repair(e, j)) {
|
||||
ctx.new_value_eh(e->get_arg(j));
|
||||
return;
|
||||
}
|
||||
if (m_eval.repair_down(e, j))
|
||||
return;
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(3, verbose_stream() << "init-repair " << mk_bounded_pp(e, m) << "\n");
|
||||
IF_VERBOSE(3, verbose_stream() << "revert repair: " << mk_bounded_pp(e, m) << "\n");
|
||||
repair_up(e);
|
||||
}
|
||||
|
||||
void bv_plugin::repair_up(app* e) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue