mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 09:04:07 +00:00
value sweep
This commit is contained in:
parent
38e0968845
commit
19409a25a6
|
@ -33,6 +33,7 @@ z3_add_component(rewriter
|
|||
rewriter.cpp
|
||||
seq_rewriter.cpp
|
||||
th_rewriter.cpp
|
||||
value_sweep.cpp
|
||||
var_subst.cpp
|
||||
mk_extract_proc.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
|
|
158
src/ast/rewriter/value_sweep.cpp
Normal file
158
src/ast/rewriter/value_sweep.cpp
Normal file
|
@ -0,0 +1,158 @@
|
|||
/*++
|
||||
Copyright (c) 2020 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
value_sweep.cpp
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner 2020-04-25
|
||||
|
||||
--*/
|
||||
|
||||
#include "ast/for_each_expr.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/rewriter/value_sweep.h"
|
||||
|
||||
value_sweep::value_sweep(ast_manager& m):
|
||||
m(m),
|
||||
m_gen(m),
|
||||
m_rec(m),
|
||||
m_dt(m),
|
||||
m_rewrite(m),
|
||||
m_values(m),
|
||||
m_args(m),
|
||||
m_pinned(m),
|
||||
m_rounds(10),
|
||||
m_range(20),
|
||||
m_qhead(0)
|
||||
{}
|
||||
|
||||
void value_sweep::set_value_core(expr* e, expr* v) {
|
||||
m_values.reserve(e->get_id() + 1);
|
||||
m_values[e->get_id()] = v;
|
||||
}
|
||||
|
||||
void value_sweep::set_value(expr* e, expr* v) {
|
||||
set_value_core(e, v);
|
||||
m_pinned.push_back(e);
|
||||
}
|
||||
|
||||
void value_sweep::reset_values() {
|
||||
m_values.reset();
|
||||
m_pinned.reset();
|
||||
}
|
||||
|
||||
expr* value_sweep::get_value(expr* e) const {
|
||||
if (m_values.size() <= e->get_id())
|
||||
return nullptr;
|
||||
return m_values[e->get_id()];
|
||||
}
|
||||
|
||||
void value_sweep::unassign(unsigned sz) {
|
||||
for (unsigned i = m_queue.size(); i-- > sz; ) {
|
||||
expr* e = m_queue[i];
|
||||
m_values[e->get_id()] = nullptr;
|
||||
}
|
||||
m_queue.shrink(sz);
|
||||
m_qhead = sz;
|
||||
}
|
||||
|
||||
bool value_sweep::assign_next_value() {
|
||||
for (; m_vhead < m_vars.size(); ) {
|
||||
expr* v = m_vars[m_vhead];
|
||||
++m_vhead;
|
||||
if (!get_value(v)) {
|
||||
unsigned index = m_rand() % m_range;
|
||||
expr_ref val = m_gen.get_value(m.get_sort(v), index);
|
||||
set_value_core(v, val);
|
||||
m_queue.push_back(v);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool value_sweep::is_reducible(expr* e) const {
|
||||
if (!is_app(e))
|
||||
return false;
|
||||
app* a = to_app(e);
|
||||
return
|
||||
m_rec.is_defined(a) ||
|
||||
a->get_family_id() == m_dt.get_family_id() ||
|
||||
a->get_family_id() == m.get_basic_family_id();
|
||||
}
|
||||
|
||||
bool value_sweep::all_args_have_values(app* p) const {
|
||||
for (expr* arg : *p) {
|
||||
if (!get_value(arg))
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
void value_sweep::propagate_values() {
|
||||
for (; m_qhead < m_queue.size(); ++m_qhead) {
|
||||
expr* e = m_queue[m_qhead];
|
||||
for (app* p : m_parents[e->get_id()]) {
|
||||
if (get_value(p))
|
||||
continue;
|
||||
if (!is_reducible(p))
|
||||
continue;
|
||||
if (!all_args_have_values(p))
|
||||
continue;
|
||||
m_args.reset();
|
||||
for (expr* arg : *p)
|
||||
m_args.push_back(get_value(arg));
|
||||
expr_ref new_value(m.mk_app(p->get_decl(), m_args), m);
|
||||
m_rewrite(new_value);
|
||||
TRACE("value_sweep", tout << "propagate " << mk_pp(p, m) << " " << new_value << "\n";);
|
||||
set_value_core(p, new_value);
|
||||
m_queue.push_back(p);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void value_sweep::init(expr_ref_vector const& terms) {
|
||||
m_parents.reset();
|
||||
m_queue.reset();
|
||||
m_vars.reset();
|
||||
m_qhead = 0;
|
||||
m_vhead = 0;
|
||||
for (expr* t : subterms(terms)) {
|
||||
m_parents.reserve(t->get_id() + 1);
|
||||
if (get_value(t))
|
||||
m_queue.push_back(t);
|
||||
else if (!is_reducible(t))
|
||||
m_vars.push_back(t);
|
||||
}
|
||||
for (expr* t : subterms(terms)) {
|
||||
if (!is_app(t))
|
||||
continue;
|
||||
for (expr* arg : *to_app(t))
|
||||
m_parents[arg->get_id()].push_back(to_app(t));
|
||||
}
|
||||
}
|
||||
|
||||
void value_sweep::operator()(expr_ref_vector const& terms,
|
||||
vector<expr_ref_vector>& values) {
|
||||
|
||||
unsigned qhead0 = m_queue.size();
|
||||
init(terms);
|
||||
propagate_values();
|
||||
unsigned qhead = m_queue.size();
|
||||
for (unsigned i = 0; i < m_rounds; ++i) {
|
||||
m_vhead = 0;
|
||||
while (assign_next_value()) {
|
||||
propagate_values();
|
||||
}
|
||||
expr_ref_vector vec(m);
|
||||
for (expr* t : terms) {
|
||||
vec.push_back(get_value(t));
|
||||
}
|
||||
values.push_back(vec);
|
||||
unassign(qhead);
|
||||
}
|
||||
unassign(qhead0);
|
||||
}
|
73
src/ast/rewriter/value_sweep.h
Normal file
73
src/ast/rewriter/value_sweep.h
Normal file
|
@ -0,0 +1,73 @@
|
|||
/*++
|
||||
Copyright (c) 2020 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
value_sweep.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Evaluate terms using different random initial assignments.
|
||||
Return the assignments.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner 2020-04-27
|
||||
|
||||
--*/
|
||||
|
||||
#pragma once
|
||||
|
||||
#include "ast/value_generator.h"
|
||||
#include "ast/recfun_decl_plugin.h"
|
||||
#include "ast/datatype_decl_plugin.h"
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
|
||||
class value_sweep {
|
||||
typedef vector<ptr_vector<app>> parents_t;
|
||||
|
||||
ast_manager& m;
|
||||
value_generator m_gen;
|
||||
recfun::util m_rec;
|
||||
datatype::util m_dt;
|
||||
th_rewriter m_rewrite;
|
||||
expr_ref_vector m_values;
|
||||
expr_ref_vector m_args;
|
||||
expr_ref_vector m_pinned;
|
||||
unsigned m_rounds;
|
||||
unsigned m_range;
|
||||
random_gen m_rand;
|
||||
|
||||
parents_t m_parents;
|
||||
ptr_vector<expr> m_queue;
|
||||
ptr_vector<expr> m_vars;
|
||||
unsigned m_qhead;
|
||||
unsigned m_vhead;
|
||||
|
||||
void init(expr_ref_vector const& terms);
|
||||
|
||||
void set_value_core(expr* e, expr* v);
|
||||
|
||||
expr* get_value(expr* e) const;
|
||||
|
||||
void unassign(unsigned qhead);
|
||||
|
||||
void propagate_values();
|
||||
|
||||
bool assign_next_value();
|
||||
|
||||
bool is_reducible(expr* e) const;
|
||||
|
||||
bool all_args_have_values(app* p) const;
|
||||
|
||||
|
||||
public:
|
||||
value_sweep(ast_manager& m);
|
||||
void set_rounds(unsigned r) { m_rounds = r; }
|
||||
void set_range(unsigned r) { m_range = r; }
|
||||
void set_value(expr* e, expr* v);
|
||||
void reset_values();
|
||||
|
||||
void operator()(expr_ref_vector const& terms,
|
||||
vector<expr_ref_vector>& values);
|
||||
};
|
|
@ -123,6 +123,7 @@ add_executable(test-z3
|
|||
uint_set.cpp
|
||||
upolynomial.cpp
|
||||
value_generator.cpp
|
||||
value_sweep.cpp
|
||||
var_subst.cpp
|
||||
vector.cpp
|
||||
lp/lp.cpp
|
||||
|
|
|
@ -218,6 +218,7 @@ int main(int argc, char ** argv) {
|
|||
TST(ext_numeral);
|
||||
TST(interval);
|
||||
TST(value_generator);
|
||||
TST(value_sweep);
|
||||
TST(vector);
|
||||
TST(f2n);
|
||||
TST(hwf);
|
||||
|
|
37
src/test/value_sweep.cpp
Normal file
37
src/test/value_sweep.cpp
Normal file
|
@ -0,0 +1,37 @@
|
|||
#include "ast/rewriter/value_sweep.h"
|
||||
#include "ast/reg_decl_plugins.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
#include "ast/array_decl_plugin.h"
|
||||
|
||||
void tst_value_sweep() {
|
||||
ast_manager m;
|
||||
reg_decl_plugins(m);
|
||||
datatype_util dt(m);
|
||||
arith_util a(m);
|
||||
array_util ar(m);
|
||||
seq_util seq(m);
|
||||
sort_ref int_sort(a.mk_int(), m);
|
||||
func_decl_ref cons(m), is_cons(m), head(m), tail(m), nil(m), is_nil(m);
|
||||
|
||||
sort_ref ilist = dt.mk_list_datatype(int_sort, symbol("ilist"),
|
||||
cons, is_cons, head, tail, nil, is_nil);
|
||||
|
||||
expr_ref n(m.mk_const("n", int_sort), m);
|
||||
expr_ref v1(m.mk_const("v1", ilist), m);
|
||||
expr_ref v2(m.mk_const("v2", ilist), m);
|
||||
std::cout << cons << "\n";
|
||||
expr_ref v3(m.mk_app(cons.get(), n, v1), m);
|
||||
expr_ref_vector terms(m);
|
||||
terms.push_back(v1).push_back(v2).push_back(v3);
|
||||
vector<expr_ref_vector> values;
|
||||
value_sweep ws(m);
|
||||
ws.set_range(30);
|
||||
ws(terms, values);
|
||||
for (auto const& vec : values) {
|
||||
for (expr* v : vec) {
|
||||
std::cout << mk_pp(v, m) << "\n";
|
||||
}
|
||||
std::cout << "\n";
|
||||
}
|
||||
}
|
Loading…
Reference in a new issue