From 19409a25a6ab92b182d9e9e82da64f265ff57372 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Apr 2020 18:58:43 -0700 Subject: [PATCH] value sweep --- src/ast/rewriter/CMakeLists.txt | 1 + src/ast/rewriter/value_sweep.cpp | 158 +++++++++++++++++++++++++++++++ src/ast/rewriter/value_sweep.h | 73 ++++++++++++++ src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/value_sweep.cpp | 37 ++++++++ 6 files changed, 271 insertions(+) create mode 100644 src/ast/rewriter/value_sweep.cpp create mode 100644 src/ast/rewriter/value_sweep.h create mode 100644 src/test/value_sweep.cpp diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index cb51085a16d..a7d5e08ed49 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -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 diff --git a/src/ast/rewriter/value_sweep.cpp b/src/ast/rewriter/value_sweep.cpp new file mode 100644 index 00000000000..fee2c7805d2 --- /dev/null +++ b/src/ast/rewriter/value_sweep.cpp @@ -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& 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); +} diff --git a/src/ast/rewriter/value_sweep.h b/src/ast/rewriter/value_sweep.h new file mode 100644 index 00000000000..4f6b15b0ca8 --- /dev/null +++ b/src/ast/rewriter/value_sweep.h @@ -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> 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 m_queue; + ptr_vector 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& values); +}; diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index a9fb5aa6962..7bfc0569ceb 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -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 diff --git a/src/test/main.cpp b/src/test/main.cpp index c8c16ba1828..002fc920dda 100644 --- a/src/test/main.cpp +++ b/src/test/main.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); diff --git a/src/test/value_sweep.cpp b/src/test/value_sweep.cpp new file mode 100644 index 00000000000..015a8be7cf2 --- /dev/null +++ b/src/test/value_sweep.cpp @@ -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 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"; + } +}