-
Notifications
You must be signed in to change notification settings - Fork 1.5k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
38e0968
commit 19409a2
Showing
6 changed files
with
271 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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); | ||
}; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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"; | ||
} | ||
} |