mirror of
https://github.com/Z3Prover/z3
synced 2025-05-06 07:15:47 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
Christoph M. Wintersteiger
commit
07a4fb4381
6 changed files with 221 additions and 111 deletions
|
|
@ -31,7 +31,7 @@ Revision History:
|
|||
#include"ast_smt2_pp.h"
|
||||
#include"th_rewriter.h"
|
||||
#include"var_subst.h"
|
||||
#include"expr_substitution.h"
|
||||
#include"expr_safe_replace.h"
|
||||
#include"pp.h"
|
||||
#include"scoped_ctrl_c.h"
|
||||
#include"cancel_eh.h"
|
||||
|
|
@ -786,17 +786,12 @@ extern "C" {
|
|||
RETURN_Z3(of_expr(0));
|
||||
}
|
||||
}
|
||||
|
||||
expr_substitution subst(m);
|
||||
expr_safe_replace subst(m);
|
||||
for (unsigned i = 0; i < num_exprs; i++) {
|
||||
subst.insert(from[i], to[i]);
|
||||
}
|
||||
th_rewriter m_rw(m);
|
||||
m_rw.set_substitution(&subst);
|
||||
|
||||
expr_ref new_a(m);
|
||||
proof_ref pr(m);
|
||||
m_rw(a, new_a, pr);
|
||||
subst(a, new_a);
|
||||
mk_c(c)->save_ast_trail(new_a);
|
||||
r = new_a.get();
|
||||
RETURN_Z3(of_expr(r));
|
||||
|
|
|
|||
|
|
@ -61,9 +61,6 @@ namespace datalog {
|
|||
}
|
||||
|
||||
cost get_cost() const {
|
||||
/*if(m_instantiated) {
|
||||
return std::numeric_limits<cost>::min();
|
||||
}*/
|
||||
SASSERT(m_consumers > 0);
|
||||
cost amortized = m_total_cost/m_consumers;
|
||||
if (m_stratified) {
|
||||
|
|
@ -81,13 +78,14 @@ namespace datalog {
|
|||
by the time of a call to this function
|
||||
*/
|
||||
void add_rule(join_planner & pl, app * t1, app * t2, rule * r,
|
||||
const var_idx_set & non_local_vars_normalized) {
|
||||
const var_idx_set & non_local_vars_normalized,
|
||||
const var_idx_set & non_local_vars) {
|
||||
if (m_rules.empty()) {
|
||||
m_total_cost = pl.compute_cost(t1, t2);
|
||||
m_total_cost = pl.compute_cost(t1, t2, non_local_vars);
|
||||
m_src_stratum = std::max(pl.get_stratum(t1->get_decl()), pl.get_stratum(t2->get_decl()));
|
||||
}
|
||||
m_rules.push_back(r);
|
||||
if(pl.m_rules_content.find_core(r)->get_data().m_value.size()>2) {
|
||||
if (pl.m_rules_content.find(r).size()>2) {
|
||||
m_consumers++;
|
||||
}
|
||||
if (m_stratified) {
|
||||
|
|
@ -274,8 +272,6 @@ namespace datalog {
|
|||
by the time of a call to this function
|
||||
*/
|
||||
void register_pair(app * t1, app * t2, rule * r, const var_idx_set & non_local_vars) {
|
||||
TRACE("dl", tout << mk_pp(t1, m) << " " << mk_pp(t2, m) << "\n";
|
||||
r->display(m_context, tout); tout << "\n";);
|
||||
SASSERT(t1!=t2);
|
||||
cost_map::entry * e = m_costs.insert_if_not_there2(get_key(t1, t2), 0);
|
||||
pair_info * & ptr_inf = e->get_data().m_value;
|
||||
|
|
@ -295,13 +291,18 @@ namespace datalog {
|
|||
normalized_vars.insert(norm_var);
|
||||
}
|
||||
|
||||
inf.add_rule(*this, t1, t2, r, normalized_vars);
|
||||
inf.add_rule(*this, t1, t2, r, normalized_vars, non_local_vars);
|
||||
TRACE("dl", tout << mk_pp(t1, m) << " " << mk_pp(t2, m) << " ";
|
||||
vit = non_local_vars.begin();
|
||||
for (; vit != vend; ++vit) tout << *vit << " ";
|
||||
tout << "\n";
|
||||
r->display(m_context, tout);
|
||||
if (inf.can_be_joined()) tout << "cost: " << inf.get_cost() << "\n";);
|
||||
|
||||
}
|
||||
|
||||
pair_info & get_pair(app_pair key) const {
|
||||
cost_map::entry * e = m_costs.find_core(key);
|
||||
SASSERT(e);
|
||||
return *e->get_data().m_value;
|
||||
return *m_costs.find(key);
|
||||
}
|
||||
|
||||
void remove_rule_from_pair(app_pair key, rule * r, unsigned original_len) {
|
||||
|
|
@ -503,7 +504,7 @@ namespace datalog {
|
|||
void apply_binary_rule(rule * r, app_pair pair_key, app * t_new) {
|
||||
app * t1 = pair_key.first;
|
||||
app * t2 = pair_key.second;
|
||||
ptr_vector<app> & rule_content = m_rules_content.find_core(r)->get_data().m_value;
|
||||
ptr_vector<app> & rule_content = m_rules_content.find(r);
|
||||
unsigned len = rule_content.size();
|
||||
if (len==1) {
|
||||
return;
|
||||
|
|
@ -600,21 +601,39 @@ namespace datalog {
|
|||
return res;
|
||||
}
|
||||
|
||||
cost compute_cost(app * t1, app * t2) const {
|
||||
cost compute_cost(app * t1, app * t2, const var_idx_set & non_local_vars) const {
|
||||
func_decl * t1_pred = t1->get_decl();
|
||||
func_decl * t2_pred = t2->get_decl();
|
||||
cost inters_size = 1;
|
||||
variable_intersection vi(m_context.get_manager());
|
||||
vi.populate(t1, t2);
|
||||
unsigned n = vi.size();
|
||||
// remove contributions from joined columns.
|
||||
for(unsigned i=0; i<n; i++) {
|
||||
unsigned arg_index1, arg_index2;
|
||||
vi.get(i, arg_index1, arg_index2);
|
||||
SASSERT(is_var(t1->get_arg(arg_index1)));
|
||||
if (non_local_vars.contains(to_var(t1->get_arg(arg_index1))->get_idx())) {
|
||||
inters_size *= get_domain_size(t1_pred, arg_index1);
|
||||
}
|
||||
//joined arguments must have the same domain
|
||||
SASSERT(get_domain_size(t1_pred, arg_index1)==get_domain_size(t2_pred, arg_index2));
|
||||
}
|
||||
cost res = estimate_size(t1)*estimate_size(t2)/(inters_size*inters_size);
|
||||
// remove contributions from projected columns.
|
||||
for (unsigned i = 0; i < t1->get_num_args(); ++i) {
|
||||
if (is_var(t1->get_arg(i)) &&
|
||||
!non_local_vars.contains(to_var(t1->get_arg(i))->get_idx())) {
|
||||
inters_size *= get_domain_size(t1_pred, i);
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < t2->get_num_args(); ++i) {
|
||||
if (is_var(t2->get_arg(i)) &&
|
||||
!non_local_vars.contains(to_var(t2->get_arg(i))->get_idx())) {
|
||||
inters_size *= get_domain_size(t2_pred, i);
|
||||
}
|
||||
}
|
||||
|
||||
cost res = estimate_size(t1)*estimate_size(t2)/ inters_size; // (inters_size*inters_size);
|
||||
//cost res = -inters_size;
|
||||
|
||||
/*unsigned t1_strat = get_stratum(t1_pred);
|
||||
|
|
|
|||
|
|
@ -31,7 +31,6 @@ namespace datalog {
|
|||
rm(ctx.get_rule_manager()),
|
||||
m_rewriter(m, m_params),
|
||||
m_simplifier(ctx),
|
||||
m_sub(m),
|
||||
m_next_var(0) {
|
||||
m_params.set_bool("expand_select_store",true);
|
||||
m_rewriter.updt_params(m_params);
|
||||
|
|
@ -82,7 +81,6 @@ namespace datalog {
|
|||
return false;
|
||||
}
|
||||
if (v) {
|
||||
m_sub.insert(e, v);
|
||||
m_defs.insert(e, to_var(v));
|
||||
}
|
||||
else {
|
||||
|
|
@ -92,71 +90,113 @@ namespace datalog {
|
|||
m_next_var = vars.size() + 1;
|
||||
}
|
||||
v = m.mk_var(m_next_var, m.get_sort(e));
|
||||
m_sub.insert(e, v);
|
||||
m_defs.insert(e, v);
|
||||
++m_next_var;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool mk_array_blast::ackermanize(rule const& r, expr_ref& body, expr_ref& head) {
|
||||
expr_ref_vector conjs(m);
|
||||
qe::flatten_and(body, conjs);
|
||||
m_defs.reset();
|
||||
m_sub.reset();
|
||||
m_next_var = 0;
|
||||
ptr_vector<expr> todo;
|
||||
todo.push_back(head);
|
||||
for (unsigned i = 0; i < conjs.size(); ++i) {
|
||||
expr* e = conjs[i].get();
|
||||
bool mk_array_blast::is_select_eq_var(expr* e, app*& s, var*& v) const {
|
||||
expr* x, *y;
|
||||
if (m.is_eq(e, x, y) || m.is_iff(e, x, y)) {
|
||||
if (a.is_select(y)) {
|
||||
std::swap(x,y);
|
||||
}
|
||||
if (a.is_select(x) && is_var(y)) {
|
||||
if (!insert_def(r, to_app(x), to_var(y))) {
|
||||
s = to_app(x);
|
||||
v = to_var(y);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
bool mk_array_blast::ackermanize(rule const& r, expr_ref& body, expr_ref& head) {
|
||||
expr_ref_vector conjs(m), trail(m);
|
||||
qe::flatten_and(body, conjs);
|
||||
m_defs.reset();
|
||||
m_next_var = 0;
|
||||
ptr_vector<expr> todo;
|
||||
obj_map<expr, expr*> cache;
|
||||
ptr_vector<expr> args;
|
||||
app_ref e1(m);
|
||||
app* s;
|
||||
var* v;
|
||||
|
||||
for (unsigned i = 0; i < conjs.size(); ++i) {
|
||||
expr* e = conjs[i].get();
|
||||
if (is_select_eq_var(e, s, v)) {
|
||||
todo.append(s->get_num_args(), s->get_args());
|
||||
}
|
||||
}
|
||||
if (a.is_select(e) && !insert_def(r, to_app(e), 0)) {
|
||||
return false;
|
||||
}
|
||||
else {
|
||||
todo.push_back(e);
|
||||
}
|
||||
// now make sure to cover all occurrences.
|
||||
ast_mark mark;
|
||||
}
|
||||
while (!todo.empty()) {
|
||||
expr* e = todo.back();
|
||||
if (cache.contains(e)) {
|
||||
todo.pop_back();
|
||||
if (mark.is_marked(e)) {
|
||||
continue;
|
||||
}
|
||||
mark.mark(e, true);
|
||||
if (is_var(e)) {
|
||||
cache.insert(e, e);
|
||||
todo.pop_back();
|
||||
continue;
|
||||
}
|
||||
if (!is_app(e)) {
|
||||
return false;
|
||||
}
|
||||
app* ap = to_app(e);
|
||||
if (a.is_select(ap) && !m_defs.contains(ap)) {
|
||||
if (!insert_def(r, ap, 0)) {
|
||||
bool valid = true;
|
||||
args.reset();
|
||||
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
|
||||
expr* arg;
|
||||
if (cache.find(ap->get_arg(i), arg)) {
|
||||
args.push_back(arg);
|
||||
}
|
||||
else {
|
||||
todo.push_back(ap->get_arg(i));
|
||||
valid = false;
|
||||
}
|
||||
}
|
||||
if (valid) {
|
||||
todo.pop_back();
|
||||
e1 = m.mk_app(ap->get_decl(), args.size(), args.c_ptr());
|
||||
trail.push_back(e1);
|
||||
if (a.is_select(ap)) {
|
||||
if (m_defs.find(e1, v)) {
|
||||
cache.insert(e, v);
|
||||
}
|
||||
else if (!insert_def(r, e1, 0)) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
if (a.is_select(e)) {
|
||||
get_select_args(e, todo);
|
||||
continue;
|
||||
}
|
||||
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
|
||||
todo.push_back(ap->get_arg(i));
|
||||
else {
|
||||
cache.insert(e, m_defs.find(e1));
|
||||
}
|
||||
}
|
||||
else {
|
||||
cache.insert(e, e1);
|
||||
}
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < conjs.size(); ++i) {
|
||||
expr* e = conjs[i].get();
|
||||
if (is_select_eq_var(e, s, v)) {
|
||||
args.reset();
|
||||
for (unsigned j = 0; j < s->get_num_args(); ++j) {
|
||||
args.push_back(cache.find(s->get_arg(j)));
|
||||
}
|
||||
e1 = m.mk_app(s->get_decl(), args.size(), args.c_ptr());
|
||||
if (!m_defs.contains(e1) && !insert_def(r, e1, v)) {
|
||||
return false;
|
||||
}
|
||||
conjs[i] = m.mk_eq(v, m_defs.find(e1));
|
||||
}
|
||||
else {
|
||||
conjs[i] = cache.find(e);
|
||||
}
|
||||
}
|
||||
m_sub(body);
|
||||
m_sub(head);
|
||||
conjs.reset();
|
||||
|
||||
// perform the Ackermann reduction by creating implications
|
||||
// i1 = i2 => val1 = val2 for each equality pair:
|
||||
|
|
@ -171,6 +211,7 @@ namespace datalog {
|
|||
for (; it2 != end; ++it2) {
|
||||
app* a2 = it2->m_key;
|
||||
var* v2 = it2->m_value;
|
||||
TRACE("dl", tout << mk_pp(a1, m) << " " << mk_pp(a2, m) << "\n";);
|
||||
if (get_select(a1) != get_select(a2)) {
|
||||
continue;
|
||||
}
|
||||
|
|
@ -184,10 +225,7 @@ namespace datalog {
|
|||
conjs.push_back(m.mk_implies(m.mk_and(eqs.size(), eqs.c_ptr()), m.mk_eq(v1, v2)));
|
||||
}
|
||||
}
|
||||
if (!conjs.empty()) {
|
||||
conjs.push_back(body);
|
||||
body = m.mk_and(conjs.size(), conjs.c_ptr());
|
||||
}
|
||||
m_rewriter(body);
|
||||
return true;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -44,7 +44,6 @@ namespace datalog {
|
|||
mk_interp_tail_simplifier m_simplifier;
|
||||
|
||||
defs_t m_defs;
|
||||
expr_safe_replace m_sub;
|
||||
unsigned m_next_var;
|
||||
|
||||
bool blast(rule& r, rule_set& new_rules);
|
||||
|
|
@ -59,6 +58,8 @@ namespace datalog {
|
|||
|
||||
bool insert_def(rule const& r, app* e, var* v);
|
||||
|
||||
bool is_select_eq_var(expr* e, app*& s, var*& v) const;
|
||||
|
||||
public:
|
||||
/**
|
||||
\brief Create rule transformer that removes array stores and selects by ackermannization.
|
||||
|
|
|
|||
56
src/test/expr_substitution.cpp
Normal file
56
src/test/expr_substitution.cpp
Normal file
|
|
@ -0,0 +1,56 @@
|
|||
#include "expr_substitution.h"
|
||||
#include "smt_params.h"
|
||||
#include "substitution.h"
|
||||
#include "unifier.h"
|
||||
#include "bv_decl_plugin.h"
|
||||
#include "ast_pp.h"
|
||||
#include "arith_decl_plugin.h"
|
||||
#include "reg_decl_plugins.h"
|
||||
#include "th_rewriter.h"
|
||||
|
||||
expr* mk_bv_xor(bv_util& bv, expr* a, expr* b) {
|
||||
expr* args[2];
|
||||
args[0] = a;
|
||||
args[1] = b;
|
||||
return bv.mk_bv_xor(2, args);
|
||||
}
|
||||
|
||||
expr* mk_bv_and(bv_util& bv, expr* a, expr* b) {
|
||||
expr* args[2];
|
||||
args[0] = a;
|
||||
args[1] = b;
|
||||
ast_manager& m = bv.get_manager();
|
||||
return m.mk_app(bv.get_family_id(), OP_BAND, 2, args);
|
||||
}
|
||||
|
||||
void tst_expr_substitution() {
|
||||
memory::initialize(0);
|
||||
ast_manager m;
|
||||
reg_decl_plugins(m);
|
||||
bv_util bv(m);
|
||||
|
||||
expr_ref a(m), b(m), c(m), d(m);
|
||||
expr_ref x(m);
|
||||
expr_ref new_a(m);
|
||||
proof_ref pr(m);
|
||||
x = m.mk_const(symbol("x"), bv.mk_sort(8));
|
||||
a = mk_bv_and(bv, mk_bv_xor(bv, x,bv.mk_numeral(8,8)), mk_bv_xor(bv,x,x));
|
||||
b = x;
|
||||
c = bv.mk_bv_sub(x, bv.mk_numeral(4, 8));
|
||||
|
||||
expr_substitution subst(m);
|
||||
th_rewriter rw(m);
|
||||
|
||||
// normalizing c does not help.
|
||||
rw(c, d, pr);
|
||||
subst.insert(b, d);
|
||||
|
||||
rw.set_substitution(&subst);
|
||||
|
||||
|
||||
enable_trace("th_rewriter_step");
|
||||
rw(a, new_a, pr);
|
||||
|
||||
std::cout << mk_pp(new_a, m) << "\n";
|
||||
|
||||
}
|
||||
|
|
@ -215,6 +215,7 @@ int main(int argc, char ** argv) {
|
|||
TST(rcf);
|
||||
TST(polynorm);
|
||||
TST(qe_arith);
|
||||
TST(expr_substitution);
|
||||
}
|
||||
|
||||
void initialize_mam() {}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue