mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix unit test build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-07-15 14:23:47 -07:00
parent 428361b22e
commit 04ad63c732
6 changed files with 40 additions and 415 deletions
Download patch file Download diff file Expand all files Collapse all files

284
src/ast/sls/bv_sls.cpp
View file

@ -1,284 +0,0 @@
/*++
Copyright (c) 2024 Microsoft Corporation
Module Name:
bv_sls.cpp
Abstract:
A Stochastic Local Search (SLS) engine
Uses invertibility conditions,
interval annotations
don't care annotations
Author:
Nikolaj Bjorner (nbjorner) 2024-02-07
--*/
#include "ast/sls/bv_sls.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "params/sls_params.hpp"
namespace bvu {
sls::sls(ast_manager& m, params_ref const& p):
m(m),
bv(m),
m_terms(m),
m_eval(m)
{
updt_params(p);
}
void sls::init() {
m_terms.init();
}
void sls::init_eval(std::function<bool(expr*, unsigned)>& eval) {
m_eval.init_eval(m_terms.assertions(), eval);
m_eval.tighten_range(m_terms.assertions());
init_repair();
}
void sls::init_repair() {
m_repair_down = UINT_MAX;
m_repair_up.reset();
m_repair_roots.reset();
for (auto* e : m_terms.assertions()) {
if (!m_eval.bval0(e)) {
m_eval.set(e, true);
m_repair_roots.insert(e->get_id());
}
}
for (auto* t : m_terms.terms()) {
if (t && !m_eval.re_eval_is_correct(t))
m_repair_roots.insert(t->get_id());
}
}
void sls::set_model() {
if (!m_set_model)
return;
if (m_repair_roots.size() >= m_min_repair_size)
return;
m_min_repair_size = m_repair_roots.size();
IF_VERBOSE(2, verbose_stream() << "(sls-update-model :num-unsat " << m_min_repair_size << ")\n");
m_set_model(*get_model());
}
void sls::init_repair_goal(app* t) {
m_eval.init_eval(t);
}
void sls::init_repair_candidates() {
m_to_repair.reset();
ptr_vector<expr> todo;
expr_fast_mark1 mark;
for (auto index : m_repair_roots)
todo.push_back(m_terms.term(index));
for (unsigned i = 0; i < todo.size(); ++i) {
expr* e = todo[i];
if (mark.is_marked(e))
continue;
mark.mark(e);
if (!is_app(e))
continue;
for (expr* arg : *to_app(e))
todo.push_back(arg);
if (is_uninterp_const(e))
m_to_repair.insert(e->get_id());
}
}
void sls::reinit_eval() {
init_repair();
}
std::pair<bool, app*> sls::next_to_repair() {
#if 0
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(m_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(m_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);
}
#endif
return { false, nullptr };
}
lbool sls::search1() {
// init and init_eval were invoked
unsigned n = 0;
for (; n < m_config.m_max_repairs && m.inc(); ++n) {
auto [down, e] = next_to_repair();
if (!e)
return l_true;
IF_VERBOSE(20, trace_repair(down, e));
++m_stats.m_moves;
if (down)
try_repair_down(e);
else
try_repair_up(e);
}
return l_undef;
}
lbool sls::operator()() {
lbool res = l_undef;
m_stats.reset();
m_stats.m_restarts = 0;
do {
res = search1();
if (res != l_undef)
break;
trace();
reinit_eval();
}
while (m.inc() && m_stats.m_restarts++ < m_config.m_max_restarts);
return res;
}
void sls::try_repair_down(app* e) {
unsigned n = e->get_num_args();
if (n == 0) {
m_eval.commit_eval(e);
for (auto p : m_terms.parents(e))
m_repair_up.insert(p->get_id());
return;
}
if (n == 2) {
auto d1 = get_depth(e->get_arg(0));
auto d2 = get_depth(e->get_arg(1));
unsigned s = m_rand(d1 + d2 + 2);
if (s <= d1 && m_eval.try_repair(e, 0)) {
set_repair_down(e->get_arg(0));
return;
}
if (m_eval.try_repair(e, 1)) {
set_repair_down(e->get_arg(1));
return;
}
if (m_eval.try_repair(e, 0)) {
set_repair_down(e->get_arg(0));
return;
}
}
else {
unsigned s = m_rand(n);
for (unsigned i = 0; i < n; ++i) {
auto j = (i + s) % n;
if (m_eval.try_repair(e, j)) {
set_repair_down(e->get_arg(j));
return;
}
}
}
IF_VERBOSE(3, verbose_stream() << "init-repair " << mk_bounded_pp(e, m) << "\n");
// repair was not successful, so reset the state to find a different way to repair
init_repair();
}
void sls::try_repair_up(app* e) {
if (m_terms.is_assertion(e))
m_repair_roots.insert(e->get_id());
else if (!m_eval.repair_up(e)) {
IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e));
if (m_rand(10) != 0) {
m_eval.set_random(e);
m_repair_roots.insert(e->get_id());
}
else
init_repair();
}
else {
if (!m_eval.eval_is_correct(e)) {
verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
}
SASSERT(m_eval.eval_is_correct(e));
for (auto p : m_terms.parents(e))
m_repair_up.insert(p->get_id());
}
}
std::ostream& sls::display(std::ostream& out) {
#if 0
auto& terms = m_eval.sort_assertions(m_terms.assertions());
for (expr* e : terms) {
out << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " ";
if (m_eval.is_fixed0(e))
out << "f ";
if (m_repair_up.contains(e->get_id()))
out << "u ";
if (m_repair_roots.contains(e->get_id()))
out << "r ";
m_eval.display_value(out, e);
out << "\n";
}
terms.reset();
#endif
return out;
}
void sls::updt_params(params_ref const& _p) {
sls_params p(_p);
m_config.m_max_restarts = p.max_restarts();
m_config.m_max_repairs = p.max_repairs();
m_rand.set_seed(p.random_seed());
m_terms.updt_params(_p);
params_ref q = _p;
q.set_uint("max_restarts", 10);
}
std::ostream& sls::trace_repair(bool down, expr* e) {
verbose_stream() << (down ? "d #" : "u #")
<< e->get_id() << ": "
<< mk_bounded_pp(e, m, 1) << " ";
m_eval.display_value(verbose_stream(), e) << "\n";
return verbose_stream();
}
void sls::trace() {
IF_VERBOSE(2, verbose_stream()
<< "(bvsls :restarts " << m_stats.m_restarts
<< " :repair-up " << m_repair_up.size()
<< " :repair-roots " << m_repair_roots.size() << ")\n");
}
}

122
src/ast/sls/bv_sls.h
View file

@ -1,122 +0,0 @@
/*++
Copyright (c) 2024 Microsoft Corporation
Module Name:
bv_sls.h
Abstract:
A Stochastic Local Search (SLS) engine
Author:
Nikolaj Bjorner (nbjorner) 2024-02-07
--*/
#pragma once
#include "util/lbool.h"
#include "util/params.h"
#include "util/scoped_ptr_vector.h"
#include "util/uint_set.h"
#include "ast/ast.h"
#include "ast/sls/sls_stats.h"
#include "ast/sls/sls_powers.h"
#include "ast/sls/sls_valuation.h"
#include "ast/sls/bv_sls_terms.h"
#include "ast/sls/bv_sls_eval.h"
#include "ast/bv_decl_plugin.h"
#include "model/model.h"
namespace bvu {
class sls {
struct config {
unsigned m_max_restarts = 1000;
unsigned m_max_repairs = 1000;
};
ast_manager& m;
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;
ptr_vector<expr> m_todo;
random_gen m_rand;
config m_config;
bool m_engine_model = false;
bool m_engine_init = false;
std::function<expr_ref()> m_get_unit;
std::function<void(model& mdl)> m_set_model;
unsigned m_min_repair_size = UINT_MAX;
std::pair<bool, app*> next_to_repair();
void init_repair_goal(app* e);
void set_model();
void try_repair_down(app* e);
void try_repair_up(app* e);
void set_repair_down(expr* e) { m_repair_down = e->get_id(); }
lbool search1();
lbool search2();
void reinit_eval();
void init_repair();
void trace();
std::ostream& trace_repair(bool down, expr* e);
indexed_uint_set m_to_repair;
void init_repair_candidates();
public:
sls(ast_manager& m, params_ref const& p);
/*
* Invoke init after all expressions are asserted.
*/
void init();
/**
* Invoke init_eval to initialize, or re-initialize, values of
* uninterpreted constants.
*/
void init_eval(std::function<bool(expr*, unsigned)>& eval);
/**
* add callback to retrieve new units
*/
void init_unit(std::function<expr_ref()> get_unit) { m_get_unit = get_unit; }
/**
* Add callback to set model
*/
void set_model(std::function<void(model& mdl)> f) { m_set_model = f; }
/**
* Run (bounded) local search to find feasible assignments.
*/
lbool operator()();
void updt_params(params_ref const& p);
void collect_statistics(statistics& st) const { m_stats.collect_statistics(st); }
void reset_statistics() { m_stats.reset(); }
unsigned get_num_moves() { return m_stats.m_moves; }
std::ostream& display(std::ostream& out);
/**
* Retrieve valuation
*/
bv::sls_valuation const& wval(expr* e) const { return m_eval.wval(e); }
model_ref get_model();
void cancel() { m.limit().cancel(); }
};
}

6
src/ast/sls/bv_sls_eval.cpp
View file

@ -13,7 +13,7 @@ Author:
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/sls/bv_sls.h"
#include "ast/sls/bv_sls_eval.h"
#include "ast/rewriter/th_rewriter.h"
namespace bv {
@ -206,6 +206,10 @@ namespace bv {
return val;
}
void sls_eval::set(expr* e, sls_valuation const& val) {
m_values[e->get_id()]->set(val.bits());
}
void sls_eval::eval(app* e, sls_valuation& val) const {
SASSERT(bv.is_bv(e));
if (m.is_ite(e)) {

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

@ -148,6 +148,8 @@ namespace bv {
sls_valuation& wval(expr* e) const;
void set(expr* e, sls_valuation const& val);
bool is_fixed0(expr* e) const { return m_fixed.get(e->get_id(), false); }
sls_valuation& eval(app* e) const;

1
src/sat/smt/sls_solver.h
View file

@ -18,7 +18,6 @@ Author:
#include "util/rlimit.h"
#include "ast/sls/bv_sls.h"
#include "ast/sls/sat_ddfw.h"
#include "sat/smt/sat_th.h"

40
src/test/sls_test.cpp
View file

@ -1,10 +1,32 @@
#include "ast/sls/bv_sls_eval.h"
#include "ast/sls/bv_sls_terms.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/reg_decl_plugins.h"
#include "ast/ast_pp.h"
namespace bv {
class my_sat_solver_context : public sls::sat_solver_context {
vector<sat::clause_info> m_clauses;
indexed_uint_set s;
public:
my_sat_solver_context() {}
vector<sat::clause_info> const& clauses() const override { return m_clauses; }
sat::clause_info const& get_clause(unsigned idx) const override { return m_clauses[idx]; }
ptr_iterator<unsigned> get_use_list(sat::literal lit) override { return ptr_iterator<unsigned>(nullptr, nullptr); }
void flip(sat::bool_var v) override {}
double reward(sat::bool_var v) override { return 0; }
double get_weigth(unsigned clause_idx) override { return 0; }
bool is_true(sat::literal lit) override { return true; }
unsigned num_vars() const override { return 0; }
indexed_uint_set const& unsat() const override { return s; }
void on_model(model_ref& mdl) override {}
sat::bool_var add_var() override { return sat::null_bool_var;}
void add_clause(unsigned n, sat::literal const* lits) override {}
};
class sls_test {
ast_manager& m;
bv_util bv;
@ -28,9 +50,11 @@ namespace bv {
expr_ref_vector es(m);
bv_util bv(m);
es.push_back(e);
sls_eval ev(m);
ev.init_eval(es, value);
ev.tighten_range(es);
my_sat_solver_context solver;
sls::context ctx(m, solver);
sls_terms terms(ctx);
sls_eval ev(terms, ctx);
th_rewriter rw(m);
expr_ref r(e, m);
rw(r);
@ -142,9 +166,11 @@ namespace bv {
rw(r);
es.push_back(m.is_false(r) ? m.mk_not(e1) : e1);
es.push_back(m.is_false(r) ? m.mk_not(e2) : e2);
sls_eval ev(m);
ev.init_eval(es, value);
ev.tighten_range(es);
my_sat_solver_context solver;
sls::context ctx(m, solver);
sls_terms terms(ctx);
sls_eval ev(terms, ctx);
if (m.is_bool(e1)) {
SASSERT(m.is_true(r) || m.is_false(r));
@ -159,7 +185,7 @@ namespace bv {
auto val3 = ev.bval0(e2);
if (val3 != val) {
verbose_stream() << "Repaired but not corrected " << mk_pp(e2, m) << "\n";
ev.display(std::cout, es);
ev.display(std::cout);
exit(0);
}
//SASSERT(rep1);