mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-08-07 19:58:44 -07:00
parent 5b9ec3dec7 ec22156ae1
commit 85391b6f35
3 changed files with 113 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

105
src/muz_qe/dl_mk_array_blast.cpp
View file

@ -18,7 +18,6 @@ Revision History:
--*/
#include "dl_mk_array_blast.h"
#include "expr_safe_replace.h"
namespace datalog {
@ -31,7 +30,9 @@ namespace datalog {
a(m),
rm(ctx.get_rule_manager()),
m_rewriter(m, m_params),
m_simplifier(ctx) {
m_simplifier(ctx),
m_sub(m),
m_next_var(0) {
m_params.set_bool("expand_select_store",true);
m_rewriter.updt_params(m_params);
}
@ -50,14 +51,63 @@ namespace datalog {
}
return false;
}
expr* mk_array_blast::get_select(expr* e) const {
while (a.is_select(e)) {
e = to_app(e)->get_arg(0);
}
return e;
}
void mk_array_blast::get_select_args(expr* e, ptr_vector<expr>& args) const {
while (a.is_select(e)) {
app* ap = to_app(e);
for (unsigned i = 1; i < ap->get_num_args(); ++i) {
args.push_back(ap->get_arg(i));
}
e = ap->get_arg(0);
}
}
bool mk_array_blast::insert_def(rule const& r, app* e, var* v) {
//
// For the Ackermann reduction we would like the arrays
// to be variables, so that variables can be
// assumed to represent difference (alias)
// classes. Ehm., Soundness of this approach depends on
// if the arrays are finite domains...
//
if (!is_var(get_select(e))) {
return false;
}
if (v) {
m_sub.insert(e, v);
m_defs.insert(e, to_var(v));
}
else {
if (m_next_var == 0) {
ptr_vector<sort> vars;
r.get_vars(vars);
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(expr_ref& body, expr_ref& head) {
bool mk_array_blast::ackermanize(rule const& r, expr_ref& body, expr_ref& head) {
expr_ref_vector conjs(m);
flatten_and(body, conjs);
defs_t defs;
expr_safe_replace sub(m);
m_defs.reset();
m_sub.reset();
m_next_var = 0;
ptr_vector<expr> todo;
todo.push_back(head);
unsigned next_var = 0;
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
expr* x, *y;
@ -66,22 +116,17 @@ namespace datalog {
std::swap(x,y);
}
if (a.is_select(x) && is_var(y)) {
//
// For the Ackermann reduction we would like the arrays
// to be variables, so that variables can be
// assumed to represent difference (alias)
// classes.
//
if (!is_var(to_app(x)->get_arg(0))) {
if (!insert_def(r, to_app(x), to_var(y))) {
return false;
}
sub.insert(x, y);
defs.insert(to_app(x), to_var(y));
}
}
if (a.is_select(e) && !insert_def(r, to_app(e), 0)) {
return false;
}
todo.push_back(e);
}
// now check that all occurrences of select have been covered.
// now make sure to cover all occurrences.
ast_mark mark;
while (!todo.empty()) {
expr* e = todo.back();
@ -97,22 +142,28 @@ namespace datalog {
return false;
}
app* ap = to_app(e);
if (a.is_select(e) && !defs.contains(ap)) {
return false;
if (a.is_select(ap) && !m_defs.contains(ap)) {
if (!insert_def(r, ap, 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));
}
}
sub(body);
sub(head);
m_sub(body);
m_sub(head);
conjs.reset();
// perform the Ackermann reduction by creating implications
// i1 = i2 => val1 = val2 for each equality pair:
// (= val1 (select a_i i1))
// (= val2 (select a_i i2))
defs_t::iterator it1 = defs.begin(), end = defs.end();
defs_t::iterator it1 = m_defs.begin(), end = m_defs.end();
for (; it1 != end; ++it1) {
app* a1 = it1->m_key;
var* v1 = it1->m_value;
@ -121,12 +172,15 @@ namespace datalog {
for (; it2 != end; ++it2) {
app* a2 = it2->m_key;
var* v2 = it2->m_value;
if (a1->get_arg(0) != a2->get_arg(0)) {
if (get_select(a1) != get_select(a2)) {
continue;
}
expr_ref_vector eqs(m);
for (unsigned j = 1; j < a1->get_num_args(); ++j) {
eqs.push_back(m.mk_eq(a1->get_arg(j), a2->get_arg(j)));
ptr_vector<expr> args1, args2;
get_select_args(a1, args1);
get_select_args(a2, args2);
for (unsigned j = 0; j < args1.size(); ++j) {
eqs.push_back(m.mk_eq(args1[j], args2[j]));
}
conjs.push_back(m.mk_implies(m.mk_and(eqs.size(), eqs.c_ptr()), m.mk_eq(v1, v2)));
}
@ -179,15 +233,14 @@ namespace datalog {
}
}
expr_ref fml1(m), fml2(m), body(m), head(m);
r.to_formula(fml1);
expr_ref fml2(m), body(m), head(m);
body = m.mk_and(new_conjs.size(), new_conjs.c_ptr());
head = r.get_head();
sub(body);
m_rewriter(body);
sub(head);
m_rewriter(head);
change = ackermanize(body, head) || change;
change = ackermanize(r, body, head) || change;
if (!inserted && !change) {
rules.add_rule(&r);
return false;

15
src/muz_qe/dl_mk_array_blast.h
View file

@ -25,6 +25,7 @@ Revision History:
#include"dl_mk_interp_tail_simplifier.h"
#include "equiv_proof_converter.h"
#include "array_decl_plugin.h"
#include "expr_safe_replace.h"
namespace datalog {
@ -32,6 +33,8 @@ namespace datalog {
\brief Blast occurrences of arrays in rules
*/
class mk_array_blast : public rule_transformer::plugin {
typedef obj_map<app, var*> defs_t;
context& m_ctx;
ast_manager& m;
array_util a;
@ -40,13 +43,21 @@ namespace datalog {
th_rewriter m_rewriter;
mk_interp_tail_simplifier m_simplifier;
typedef obj_map<app, var*> defs_t;
defs_t m_defs;
expr_safe_replace m_sub;
unsigned m_next_var;
bool blast(rule& r, rule_set& new_rules);
bool is_store_def(expr* e, expr*& x, expr*& y);
bool ackermanize(expr_ref& body, expr_ref& head);
bool ackermanize(rule const& r, expr_ref& body, expr_ref& head);
expr* get_select(expr* e) const;
void get_select_args(expr* e, ptr_vector<expr>& args) const;
bool insert_def(rule const& r, app* e, var* v);
public:
/**

25
src/muz_qe/pdr_context.cpp
View file

@ -765,6 +765,7 @@ namespace pdr {
ini_state = m.mk_and(ini_tags, pt().initial_state(), state());
model_ref mdl;
pt().get_solver().set_model(&mdl);
TRACE("pdr", tout << mk_pp(ini_state, m) << "\n";);
VERIFY(l_true == pt().get_solver().check_conjunction_as_assumptions(ini_state));
datalog::rule const& rl2 = pt().find_rule(*mdl);
SASSERT(is_ini(rl2));
@ -958,12 +959,14 @@ namespace pdr {
*/
void model_search::update_models() {
obj_map<expr, model*> models;
obj_map<expr, datalog::rule const*> rules;
ptr_vector<model_node> todo;
todo.push_back(m_root);
while (!todo.empty()) {
model_node* n = todo.back();
if (n->get_model_ptr()) {
models.insert(n->state(), n->get_model_ptr());
rules.insert(n->state(), n->get_rule());
}
todo.pop_back();
todo.append(n->children().size(), n->children().c_ptr());
@ -973,9 +976,13 @@ namespace pdr {
while (!todo.empty()) {
model_node* n = todo.back();
model* md = 0;
ast_manager& m = n->pt().get_manager();
if (!n->get_model_ptr() && models.find(n->state(), md)) {
TRACE("pdr", tout << mk_pp(n->state(), m) << "\n";);
model_ref mr(md);
n->set_model(mr);
datalog::rule const* rule = rules.find(n->state());
n->set_rule(rule);
}
todo.pop_back();
todo.append(n->children().size(), n->children().c_ptr());
@ -1037,10 +1044,6 @@ namespace pdr {
}
first = false;
predicates.pop_back();
for (unsigned i = 0; i < rule->get_uninterpreted_tail_size(); ++i) {
subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
predicates.push_back(tmp);
}
for (unsigned i = rule->get_uninterpreted_tail_size(); i < rule->get_tail_size(); ++i) {
subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
dctx.get_rewriter()(tmp);
@ -1051,9 +1054,22 @@ namespace pdr {
for (unsigned i = 0; i < constraints.size(); ++i) {
max_var = std::max(vc.get_max_var(constraints[i].get()), max_var);
}
if (n->children().empty()) {
// nodes whose states are repeated
// in the search tree do not have children.
continue;
}
SASSERT(n->children().size() == rule->get_uninterpreted_tail_size());
for (unsigned i = 0; i < rule->get_uninterpreted_tail_size(); ++i) {
subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
predicates.push_back(tmp);
}
for (unsigned i = 0; i < predicates.size(); ++i) {
max_var = std::max(vc.get_max_var(predicates[i].get()), max_var);
}
children.append(n->children());
}
return pm.mk_and(constraints);
@ -1230,6 +1246,7 @@ namespace pdr {
m_expanded_lvl(0),
m_cancel(false)
{
enable_trace("pdr");
}
context::~context() {