mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 04:01:22 +00:00
Code Activity

base working mbi

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-13 15:45:06 -08:00
parent 77689ed002
commit 453ef631a0
10 changed files with 234 additions and 140 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/qe/qe_arith.cpp
View file

@ -325,6 +325,7 @@ namespace qe {
}
}
fmls.shrink(j);
TRACE("qe", tout << "formulas\n" << fmls << "\n";);
// fmls holds residue,
// mbo holds linear inequalities that are in scope
@ -380,7 +381,11 @@ namespace qe {
}
mbo.display(tout););
vector<opt::model_based_opt::def> defs = mbo.project(real_vars.size(), real_vars.c_ptr(), compute_def);
TRACE("qe", mbo.display(tout););
TRACE("qe", mbo.display(tout << "mbo result\n");
for (auto const& d : defs) {
tout << "def: " << d << "\n";
}
);
vector<row> rows;
mbo.get_live_rows(rows);

8
src/qe/qe_arrays.cpp
View file

@ -1442,13 +1442,13 @@ namespace qe {
for_each_store_proc(imp& i, term_graph& tg) : m_imp(i), tg(tg) {}
void operator()(app* n) {
if (m_imp.a.is_array(n) && tg.get_model_based_rep(n)) {
if (m_imp.a.is_array(n) && tg.rep_of(n)) {
m_imp.add_array(n);
}
if (m_imp.a.is_store(n) &&
(tg.get_model_based_rep(n->get_arg(0)) ||
tg.get_model_based_rep(n->get_arg(n->get_num_args() - 1)))) {
(tg.rep_of(n->get_arg(0)) ||
tg.rep_of(n->get_arg(n->get_num_args() - 1)))) {
m_imp.m_stores.push_back(n);
for (unsigned i = 1; i + 1 < n->get_num_args(); ++i) {
m_imp.add_index_sort(n->get_arg(i));
@ -1466,7 +1466,7 @@ namespace qe {
void operator()(app* n) {
auto* v = m_imp.is_index(n);
if (v && tg.get_model_based_rep(n)) {
if (v && tg.rep_of(n)) {
v->push_back(n);
}
}

74
src/qe/qe_mbi.cpp
View file

@ -117,7 +117,8 @@ namespace qe {
}
void prop_mbi_plugin::block(expr_ref_vector const& lits) {
m_solver->assert_expr(mk_not(mk_and(lits)));
expr_ref clause(mk_not(mk_and(lits)), m);
m_solver->assert_expr(clause);
}
// -------------------------------
@ -171,6 +172,7 @@ namespace qe {
bool uflia_mbi::get_literals(model_ref& mdl, expr_ref_vector& lits) {
lits.reset();
IF_VERBOSE(10, verbose_stream() << "atoms: " << m_atoms << "\n");
for (expr* e : m_atoms) {
if (mdl->is_true(e)) {
lits.push_back(e);
@ -204,7 +206,7 @@ namespace qe {
*
* The result is ordered using deepest term first.
*/
app_ref_vector uflia_mbi::get_arith_vars(expr_ref_vector& lits) {
app_ref_vector uflia_mbi::get_arith_vars(expr_ref_vector const& lits) {
app_ref_vector avars(m);
svector<bool> seen;
arith_util a(m);
@ -221,7 +223,7 @@ namespace qe {
}
}
order_avars(avars);
TRACE("qe", tout << "vars: " << avars << "\n";);
TRACE("qe", tout << "vars: " << avars << " from " << lits << "\n";);
return avars;
}
@ -263,14 +265,57 @@ namespace qe {
*/
void uflia_mbi::project(model_ref& mdl, expr_ref_vector& lits) {
TRACE("qe",
tout << lits << "\n" << *mdl << "\n";
tout << "project literals: " << lits << "\n" << *mdl << "\n";
tout << m_solver->get_assertions() << "\n";);
add_dcert(mdl, lits);
expr_ref_vector alits(m), uflits(m);
split_arith(lits, alits, uflits);
auto avars = get_arith_vars(lits);
auto defs = arith_project(mdl, avars, lits);
substitute(defs, lits);
project_euf(mdl, lits);
vector<def> defs = arith_project(mdl, avars, alits);
prune_defs(defs);
substitute(defs, uflits);
project_euf(mdl, uflits);
lits.reset();
lits.append(alits);
lits.append(uflits);
IF_VERBOSE(10, verbose_stream() << "projection : " << lits << "\n");
}
void uflia_mbi::split_arith(expr_ref_vector const& lits,
expr_ref_vector& alits,
expr_ref_vector& uflits) {
arith_util a(m);
for (expr* lit : lits) {
expr* atom = lit, *x = nullptr, *y = nullptr;
m.is_not(lit, atom);
if (m.is_eq(atom, x, y)) {
if (a.is_int_real(x)) {
alits.push_back(lit);
}
uflits.push_back(lit);
}
else if (a.is_arith_expr(atom)) {
alits.push_back(lit);
}
else {
uflits.push_back(lit);
}
}
}
/**
* prune defs to only contain substitutions of terms with leading uninterpreted function.
*/
void uflia_mbi::prune_defs(vector<def>& defs) {
unsigned i = 0;
for (auto& d : defs) {
if (!is_shared(to_app(d.var)->get_decl())) {
defs[i++] = d;
}
}
defs.shrink(i);
}
/**
@ -284,8 +329,7 @@ namespace qe {
term_graph tg(m);
func_decl_ref_vector shared(m_shared_trail);
tg.set_vars(shared, false);
tg.add_lits(lits);
lits.append(tg.get_ackerman_disequalities());
lits.append(tg.dcert(*mdl.get(), lits));
TRACE("qe", tout << "project: " << lits << "\n";);
}
@ -293,13 +337,14 @@ namespace qe {
* \brief substitute solution to arithmetical variables into lits
*/
void uflia_mbi::substitute(vector<def> const& defs, expr_ref_vector& lits) {
TRACE("qe", tout << "start substitute: " << lits << "\n";);
for (auto const& def : defs) {
expr_safe_replace rep(m);
rep.insert(def.var, def.term);
rep(lits);
TRACE("qe", tout << "substitute: " << def.var << " |-> " << def.term << ": " << lits << "\n";);
}
TRACE("qe", tout << "substitute: " << lits << "\n";);
IF_VERBOSE(1, verbose_stream() << lits << "\n");
IF_VERBOSE(1, verbose_stream() << "substituted: " << lits << "\n");
}
/**
@ -333,10 +378,11 @@ namespace qe {
}
void uflia_mbi::block(expr_ref_vector const& lits) {
// want to rely only on atoms from original literals: collect_atoms(lits);
expr_ref conj(mk_not(mk_and(lits)), m);
expr_ref clause(mk_not(mk_and(lits)), m);
collect_atoms(lits);
m_fmls.push_back(clause);
TRACE("qe", tout << "block " << lits << "\n";);
m_solver->assert_expr(conj);
m_solver->assert_expr(clause);
}

6
src/qe/qe_mbi.h
View file

@ -120,10 +120,14 @@ namespace qe {
void order_avars(app_ref_vector& avars);
void add_dcert(model_ref& mdl, expr_ref_vector& lits);
app_ref_vector get_arith_vars(expr_ref_vector& lits);
app_ref_vector get_arith_vars(expr_ref_vector const& lits);
vector<def> arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits);
void substitute(vector<def> const& defs, expr_ref_vector& lits);
void project_euf(model_ref& mdl, expr_ref_vector& lits);
void split_arith(expr_ref_vector const& lits,
expr_ref_vector& alits,
expr_ref_vector& uflits);
void prune_defs(vector<def>& defs);
public:
uflia_mbi(solver* s, solver* emptySolver);
~uflia_mbi() override {}

82
src/qe/qe_term_graph.cpp
View file

@ -19,6 +19,7 @@ Notes:
#include "util/util.h"
#include "util/uint_set.h"
#include "util/obj_pair_hashtable.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "ast/for_each_expr.h"
@ -217,7 +218,7 @@ namespace qe {
bool term_graph::is_variable_proc::operator()(const expr * e) const {
if (!is_app(e)) return false;
const app *a = ::to_app(e);
TRACE("qe", tout << a->get_family_id() << " " << m_solved.contains(a->get_decl()) << " " << m_decls.contains(a->get_decl()) << "\n";);
TRACE("qe_verbose", tout << a->get_family_id() << " " << m_solved.contains(a->get_decl()) << " " << m_decls.contains(a->get_decl()) << "\n";);
return
a->get_family_id() == null_family_id &&
!m_solved.contains(a->get_decl()) &&
@ -1176,56 +1177,95 @@ namespace qe {
}
expr* term_graph::get_model_based_rep(expr* e) {
expr* term_graph::rep_of(expr* e) {
SASSERT(m_projector);
term* t = get_term(e);
SASSERT(t && "only get representatives");
return m_projector->find_term2app(*t);
}
expr_ref_vector term_graph::dcert(model& mdl, expr_ref_vector const& lits) {
#if 0
obj_pair_hashtable<expr, expr> diseqs;
extract_disequalities(lits, diseqs);
svector<std::pair<expr*, expr*>> todo;
for (auto const& p : diseqs) todo.push_back(p);
expr_ref_vector result(m);
TRACE("qe", tout << "dcert " << lits << "\n";);
struct pair_t {
expr* a, *b;
pair_t(): a(nullptr), b(nullptr) {}
pair_t(expr* _a, expr* _b):a(_a), b(_b) {
if (a->get_id() > b->get_id()) std::swap(a, b);
}
struct hash {
unsigned operator()(pair_t const& p) const { return mk_mix(p.a ? p.a->hash() : 0, p.b ? p.b->hash() : 0, 1); }
};
struct eq {
bool operator()(pair_t const& a, pair_t const& b) const { return a.a == b.a && a.b == b.b; }
};
};
hashtable<pair_t, pair_t::hash, pair_t::eq> diseqs;
expr_ref_vector result(m);
add_lits(lits);
auto const partitions = get_partition(mdl);
svector<pair_t> todo;
for (expr* e : lits) {
expr* ne, *a, *b;
if (m.is_not(e, ne) && m.is_eq(ne, a, b) && (is_uninterp(a) || is_uninterp(b))) {
todo.push_back(pair_t(a, b));
}
else if (is_uninterp(e)) {
todo.push_back(pair_t(e, m.mk_false()));
}
else if (m.is_not(e, ne) && is_uninterp(ne)) {
todo.push_back(pair_t(ne, m.mk_true()));
}
}
for (auto& p : todo) diseqs.insert(p);
obj_map<expr, unsigned> term2pid;
unsigned id = 0;
for (auto const& vec : partitions) {
for (expr* e : vec) term2pid.insert(e, id);
++id;
}
auto partition_of = [&](expr* e) { return partitions[term2pid[e]]; };
auto in_table = [&](expr* a, expr* b) {
return diseqs.contains(pair_t(a, b));
};
auto same_function = [](expr* a, expr* b) {
return is_app(a) && is_app(b) &&
to_app(a)->get_decl() == to_app(b)->get_decl() && to_app(a)->get_family_id() == null_family_id;
};
// make sure that diseqs is closed under function applications
// of uninterpreted functions.
for (unsigned idx = 0; idx < todo.size(); ++idx) {
auto p = todo[idx];
for (app* t1 : partition_of(p.first)) {
for (app* t2 : partition_of(p.second)) {
for (expr* t1 : partition_of(p.a)) {
for (expr* t2 : partition_of(p.b)) {
if (same_function(t1, t2)) {
unsigned sz = t1->get_num_args();
unsigned sz = to_app(t1)->get_num_args();
bool found = false;
std::pair<expr*, expr*> q(nullptr, nullptr);
pair_t q(t1, t2);
for (unsigned i = 0; i < sz; ++i) {
expr* arg1 = t1->get_arg(i);
expr* arg2 = t2->get_arg(i);
expr* arg1 = to_app(t1)->get_arg(i);
expr* arg2 = to_app(t2)->get_arg(i);
if (mdl(arg1) == mdl(t2)) {
continue;
}
if (in_table(diseqs, arg1, arg2)) {
if (in_table(arg1, arg2)) {
found = true;
break;
}
q = make_diseq(arg1, arg2);
q = pair_t(arg1, arg2);
}
if (!found) {
diseqs.insert(q);
todo.push_back(q);
result.push_back(m.mk_not(m.mk_eq(q.first, q.second)));
result.push_back(m.mk_not(m.mk_eq(q.a, q.b)));
}
}
}
}
}
TRACE("qe", tout << result << "\n";);
return result;
#endif
NOT_IMPLEMENTED_YET();
return expr_ref_vector(m);
}
}

4
src/qe/qe_term_graph.h
View file

@ -87,7 +87,7 @@ namespace qe {
void display(std::ostream &out);
bool is_pure_def(expr* atom, expr *& v);
public:
term_graph(ast_manager &m);
~term_graph();
@ -150,7 +150,7 @@ namespace qe {
* Map expression that occurs in added literals into representative if it exists.
*/
void add_model_based_terms(model& mdl, expr_ref_vector const& terms);
expr* get_model_based_rep(expr* e);
expr* rep_of(expr* e);
};