3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

include more qsat features

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-19 12:29:23 -07:00
parent f175f864ec
commit c4472ce717
15 changed files with 2197 additions and 190 deletions

View file

@ -64,6 +64,13 @@ namespace nlsat {
for (unsigned i = 0; i < sz; i++)
push_back(ls[i]);
}
void append(scoped_literal_vector const& ls) {
append(ls.size(), ls.c_ptr());
}
void swap(scoped_literal_vector& other) {
SASSERT(&m_solver == &other.m_solver);
m_lits.swap(other.m_lits);
}
};

View file

@ -30,6 +30,8 @@ Notes:
#include"arith_decl_plugin.h"
#include"tactic.h"
#include"ast_smt2_pp.h"
#include"polynomial.h"
#include"algebraic_numbers.h"
struct goal2nlsat::imp {
struct nlsat_expr2polynomial : public expr2polynomial {
@ -257,6 +259,7 @@ struct goal2nlsat::imp {
process(g.form(i), g.dep(i));
}
}
};
struct goal2nlsat::scoped_set_imp {
@ -289,4 +292,154 @@ void goal2nlsat::operator()(goal const & g, params_ref const & p, nlsat::solver
scoped_set_imp setter(*this, local_imp);
local_imp(g);
}
struct nlsat2goal::imp {
ast_manager& m;
arith_util a;
u_map<expr*> const* m_x2t;
public:
imp(ast_manager& m):m(m),a(m) {}
expr_ref operator()(nlsat::solver& s, u_map<expr*> const& b2a, u_map<expr*> const& x2t, nlsat::literal l) {
m_x2t = &x2t;
expr_ref result(m);
expr* t;
if (b2a.find(l.var(), t)) {
result = t;
}
else {
nlsat::atom const* at = s.bool_var2atom(l.var());
SASSERT(at != 0);
if (at->is_ineq_atom()) {
nlsat::ineq_atom const* ia = to_ineq_atom(at);
unsigned sz = ia->size();
expr_ref_vector ps(m);
bool is_int = true;
for (unsigned i = 0; is_int && i < sz; ++i) {
is_int = poly_is_int(ia->p(i));
}
for (unsigned i = 0; i < sz; ++i) {
polynomial::polynomial* p = ia->p(i);
expr_ref t = poly2expr(s, p, is_int);
if (ia->is_even(i)) {
t = a.mk_power(t, a.mk_numeral(rational(2), a.is_int(t)));
}
ps.push_back(t);
}
result = a.mk_mul_simplify(ps);
expr_ref zero(m);
zero = a.mk_numeral(rational(0), a.is_int(result));
switch (ia->get_kind()) {
case nlsat::atom::EQ:
result = m.mk_eq(result, zero);
break;
case nlsat::atom::LT:
if (l.sign()) {
l.neg();
result = a.mk_ge(result, zero);
}
else {
result = a.mk_lt(result, zero);
}
break;
case nlsat::atom::GT:
if (l.sign()) {
l.neg();
result = a.mk_le(result, zero);
}
else {
result = a.mk_gt(result, zero);
}
break;
default:
UNREACHABLE();
}
}
else {
//nlsat::root_atom const* ra = nlsat::to_root_atom(at);
//ra->i();
//expr_ref p = poly2expr(s, ra->p());
//expr* x = m_x2t->find(ra->x());
std::ostringstream strm;
s.display(strm, l.sign()?~l:l);
result = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort());
}
}
if (l.sign()) {
result = m.mk_not(result);
}
return result;
}
expr_ref poly2expr(nlsat::solver& s, polynomial::polynomial* p, bool is_int) {
expr_ref result(m);
unsigned sz = polynomial::manager::size(p);
expr_ref_vector args(m);
for (unsigned i = 0; i < sz; ++i) {
args.push_back(mono2expr(s,
polynomial::manager::coeff(p, i),
polynomial::manager::get_monomial(p, i), is_int));
}
result = a.mk_add_simplify(args);
return result;
}
expr_ref mono2expr(nlsat::solver& s, polynomial::numeral const& c, polynomial::monomial* mon, bool is_int) {
expr_ref result(m);
expr_ref_vector args(m);
unsigned sz = polynomial::manager::size(mon);
for (unsigned i = 0; i < sz; ++i) {
unsigned d = polynomial::manager::degree(mon, i);
expr* t = m_x2t->find(polynomial::manager::get_var(mon, i));
SASSERT(d >= 1);
if (d == 1) {
args.push_back(t);
}
else {
args.push_back(a.mk_power(t, a.mk_numeral(rational(d), a.is_int(t))));
}
}
if (!s.pm().m().is_one(c)) {
args.push_back(a.mk_numeral(c, is_int));
}
result = a.mk_mul_simplify(args);
return result;
}
bool poly_is_int(polynomial::polynomial* p) {
bool is_int = true;
unsigned sz = polynomial::manager::size(p);
for (unsigned i = 0; is_int && i < sz; ++i) {
is_int = mono_is_int(polynomial::manager::get_monomial(p, i));
}
return is_int;
}
bool mono_is_int(polynomial::monomial* mon) {
bool is_int = true;
unsigned sz = polynomial::manager::size(mon);
for (unsigned i = 0; is_int && i < sz; ++i) {
is_int = a.is_int(m_x2t->find(polynomial::manager::get_var(mon, i)));
}
return is_int;
}
};
nlsat2goal::nlsat2goal(ast_manager& m) {
m_imp = alloc(imp, m);
}
nlsat2goal::~nlsat2goal() {
dealloc(m_imp);
}
expr_ref nlsat2goal::operator()(nlsat::solver& s, u_map<expr*> const& b2a, u_map<expr*> const& x2t, nlsat::literal l) {
return (*m_imp)(s, b2a, x2t, l);
}

View file

@ -57,17 +57,16 @@ class nlsat2goal {
struct imp;
imp * m_imp;
public:
nlsat2goal();
nlsat2goal(ast_manager& m);
~nlsat2goal();
static void collect_param_descrs(param_descrs & r);
/**
\brief Translate the state of the nlsat engine back into a goal.
*/
void operator()(nlsat::solver const & s, expr2var const & a2b, expr2var const & t2x,
params_ref const & p, goal & g, model_converter_ref & mc);
\brief Translate a literal into a formula.
*/
expr_ref operator()(nlsat::solver& s, u_map<expr*> const& b2a, u_map<expr*> const& x2t, nlsat::literal l);
};
#endif

View file

@ -36,7 +36,6 @@ Revision History:
#include "expr_functors.h"
#include "quant_hoist.h"
#include "bool_rewriter.h"
#include "qe_util.h"
#include "th_rewriter.h"
#include "smt_kernel.h"
#include "model_evaluator.h"
@ -2281,7 +2280,7 @@ namespace qe {
}
}
static void extract_vars(quantifier* q, expr_ref& new_body, app_ref_vector& vars) {
void extract_vars(quantifier* q, expr_ref& new_body, app_ref_vector& vars) {
ast_manager& m = new_body.get_manager();
expr_ref tmp(m);
unsigned nd = q->get_num_decls();

View file

@ -223,6 +223,8 @@ namespace qe {
qe_solver_plugin* mk_arith_plugin(i_solver_context& ctx, bool produce_models, smt_params& p);
void extract_vars(quantifier* q, expr_ref& new_body, app_ref_vector& vars);
class def_vector {
func_decl_ref_vector m_vars;
expr_ref_vector m_defs;

File diff suppressed because it is too large Load diff

View file

@ -9,16 +9,33 @@ Copyright (c) 2015 Microsoft Corporation
#define QE_ARITH_H_
#include "model.h"
#include "arith_decl_plugin.h"
#include "qe_mbp.h"
namespace qe {
/**
Loos-Weispfenning model-based projection for a basic conjunction.
Lits is a vector of literals.
return vector of variables that could not be projected.
*/
expr_ref arith_project(model& model, app_ref_vector& vars, expr_ref_vector const& lits);
expr_ref arith_project(model& model, app_ref_vector& vars, expr* fml);
class arith_project_plugin : public project_plugin {
struct imp;
imp* m_imp;
public:
arith_project_plugin(ast_manager& m);
virtual ~arith_project_plugin();
virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits);
virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits);
virtual family_id get_family_id();
};
bool arith_project(model& model, app* var, expr_ref_vector& lits);
// match e := t mod k = 0.
bool is_divides(arith_util& a, expr* e, rational& k, expr_ref& t);
};
#endif

View file

@ -32,6 +32,7 @@ Revision History:
#include "nlarith_util.h"
#include "model_evaluator.h"
#include "smt_kernel.h"
#include "qe_arith.h"
namespace qe {
@ -266,23 +267,8 @@ namespace qe {
//
// match 0 == p mod k, p mod k == 0
//
bool is_divides(app* e, numeral& k, expr_ref& p) {
expr* e1, *e2;
if (!m.is_eq(e, e1, e2)) {
return false;
}
return is_divides(e1, e2, k, p) || is_divides(e2, e1, k, p);
}
bool is_divides(expr* e1, expr* e2, numeral& k, expr_ref& p) {
if (m_arith.is_mod(e2) &&
m_arith.is_numeral(e1, k) &&
k.is_zero() &&
m_arith.is_numeral(to_app(e2)->get_arg(1), k)) {
p = to_app(e2)->get_arg(0);
return true;
}
return false;
bool is_divides(expr* e, numeral& k, expr_ref& p) {
return qe::is_divides(m_arith, e, k, p);
}
bool is_not_divides(app* e, app_ref& n, numeral& k, expr_ref& p) {

427
src/qe/qe_arrays.cpp Normal file
View file

@ -0,0 +1,427 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
qe_arrays.cpp
Abstract:
Model based projection for arrays
Author:
Nikolaj Bjorner (nbjorner) 2015-06-13
Revision History:
--*/
#include "qe_arrays.h"
#include "rewriter_def.h"
#include "expr_functors.h"
#include "expr_safe_replace.h"
#include "lbool.h"
#include "ast_util.h"
#include "ast_pp.h"
namespace qe {
struct array_project_plugin::imp {
// rewriter or direct procedure.
struct rw_cfg : public default_rewriter_cfg {
ast_manager& m;
array_util& a;
expr_ref_vector m_lits;
model* m_model;
imp* m_imp;
rw_cfg(ast_manager& m, array_util& a):
m(m), a(a), m_lits(m), m_model(0) {}
br_status reduce_app(func_decl* f, unsigned n, expr* const* args, expr_ref& result, proof_ref & pr) {
if (a.is_select(f) && a.is_store(args[0])) {
expr_ref val1(m), val2(m);
app* b = to_app(args[0]);
SASSERT(b->get_num_args() == n + 1);
for (unsigned i = 1; i < n; ++i) {
expr* arg1 = args[i];
expr* arg2 = b->get_arg(i);
if (arg1 == arg2) {
val1 = val2 = arg1;
}
else {
VERIFY(m_model->eval(arg1, val1));
VERIFY(m_model->eval(arg2, val2));
}
switch(compare(val1, val2)) {
case l_true:
if (arg1 != arg2) {
m_lits.push_back(m.mk_eq(arg1, arg2));
}
break;
case l_false: {
ptr_vector<expr> new_args;
if (i > 0) {
m_lits.resize(m_lits.size() - i);
}
m_lits.push_back(m.mk_not(m.mk_eq(arg1, arg2)));
new_args.push_back(b->get_arg(0));
new_args.append(n-1, args+1);
result = m.mk_app(f, n, new_args.c_ptr());
return BR_REWRITE1;
}
case l_undef:
return BR_FAILED;
}
}
result = b->get_arg(n);
return BR_DONE;
}
return BR_FAILED;
}
lbool compare(expr* x, expr* y) {
NOT_IMPLEMENTED_YET();
return l_undef;
}
};
struct indices {
expr_ref_vector m_values;
expr* const* m_vars;
indices(ast_manager& m, model& model, unsigned n, expr* const* vars):
m_values(m), m_vars(vars) {
expr_ref val(m);
for (unsigned i = 0; i < n; ++i) {
VERIFY(model.eval(vars[i], val));
m_values.push_back(val);
}
}
};
ast_manager& m;
array_util a;
scoped_ptr<contains_app> m_var;
imp(ast_manager& m): m(m), a(m) {}
~imp() {}
virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
return false;
}
bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
TRACE("qe", tout << mk_pp(var, m) << "\n" << lits;);
m_var = alloc(contains_app, m, var);
// reduce select-store redeces based on model.
// rw_cfg rw(m);
// rw(lits);
// try first to solve for var.
if (solve_eq(model, vars, lits)) {
return true;
}
app_ref_vector selects(m);
// check that only non-select occurrences are in disequalities.
if (!check_diseqs(lits, selects)) {
TRACE("qe", tout << "Could not project " << mk_pp(var, m) << " for:\n" << lits << "\n";);
return false;
}
// remove disequalities.
elim_diseqs(lits);
// Ackerman reduction on remaining select occurrences
// either replace occurrences by model value or other node
// that is congruent to model value.
ackermanize_select(model, selects, vars, lits);
TRACE("qe", tout << selects << "\n" << lits << "\n";);
return true;
}
void ackermanize_select(model& model, app_ref_vector const& selects, app_ref_vector& vars, expr_ref_vector& lits) {
expr_ref_vector vals(m), reps(m);
expr_ref val(m);
expr_safe_replace sub(m);
if (selects.empty()) {
return;
}
app_ref sel(m);
for (unsigned i = 0; i < selects.size(); ++i) {
sel = m.mk_fresh_const("sel", m.get_sort(selects[i]));
VERIFY (model.eval(selects[i], val));
model.register_decl(sel->get_decl(), val);
vals.push_back(to_app(val));
reps.push_back(val); // TODO: direct pass could handle nested selects.
vars.push_back(sel);
sub.insert(selects[i], val);
}
sub(lits);
remove_true(lits);
project_plugin::partition_args(model, selects, lits);
project_plugin::partition_values(model, reps, lits);
}
void remove_true(expr_ref_vector& lits) {
for (unsigned i = 0; i < lits.size(); ++i) {
if (m.is_true(lits[i].get())) {
project_plugin::erase(lits, i);
}
}
}
bool contains_x(expr* e) {
return (*m_var)(e);
}
void mk_eq(indices& x, indices y, expr_ref_vector& lits) {
unsigned n = x.m_values.size();
for (unsigned j = 0; j < n; ++j) {
lits.push_back(m.mk_eq(x.m_vars[j], y.m_vars[j]));
}
}
// check that x occurs only under selects or in disequalities.
bool check_diseqs(expr_ref_vector const& lits, app_ref_vector& selects) {
expr_mark mark;
ptr_vector<app> todo;
app* e;
for (unsigned i = 0; i < lits.size(); ++i) {
e = to_app(lits[i]);
if (is_diseq_x(e)) {
continue;
}
if (contains_x(e)) {
todo.push_back(e);
}
}
while (!todo.empty()) {
e = todo.back();
todo.pop_back();
if (mark.is_marked(e)) {
continue;
}
mark.mark(e);
if (m_var->x() == e) {
return false;
}
unsigned start = 0;
if (a.is_select(e)) {
if (e->get_arg(0) == m_var->x()) {
start = 1;
selects.push_back(e);
}
}
for (unsigned i = start; i < e->get_num_args(); ++i) {
todo.push_back(to_app(e->get_arg(i)));
}
}
return true;
}
void elim_diseqs(expr_ref_vector& lits) {
for (unsigned i = 0; i < lits.size(); ++i) {
if (is_diseq_x(lits[i].get())) {
project_plugin::erase(lits, i);
}
}
}
bool is_update_x(app* e) {
do {
if (m_var->x() == e) {
return true;
}
if (a.is_store(e) && contains_x(e->get_arg(0))) {
for (unsigned i = 1; i < e->get_num_args(); ++i) {
if (contains_x(e->get_arg(i))) {
return false;
}
}
e = to_app(e->get_arg(0));
continue;
}
}
while (false);
return false;
}
bool is_diseq_x(expr* e) {
expr *f, * s, *t;
if (m.is_not(e, f) && m.is_eq(f, s, t)) {
if (contains_x(s) && !contains_x(t) && is_update_x(to_app(s))) return true;
if (contains_x(t) && !contains_x(s) && is_update_x(to_app(t))) return true;
}
return false;
}
bool solve_eq(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
// find an equality to solve for.
expr* s, *t;
for (unsigned i = 0; i < lits.size(); ++i) {
if (m.is_eq(lits[i].get(), s, t)) {
vector<indices> idxs;
expr_ref save(m), back(m);
save = lits[i].get();
back = lits.back();
lits[i] = back;
lits.pop_back();
unsigned sz = lits.size();
if (contains_x(s) && !contains_x(t) && is_app(s)) {
if (solve(model, to_app(s), t, idxs, vars, lits)) {
return true;
}
}
else if (contains_x(t) && !contains_x(s) && is_app(t)) {
if (solve(model, to_app(t), s, idxs, vars, lits)) {
return true;
}
}
// put back the equality literal.
lits.resize(sz);
lits.push_back(back);
lits[i] = save;
}
// TBD: not distinct?
}
return false;
}
bool solve(model& model, app* s, expr* t, vector<indices>& idxs, app_ref_vector& vars, expr_ref_vector& lits) {
SASSERT(contains_x(s));
SASSERT(!contains_x(t));
if (s == m_var->x()) {
expr_ref result(s, m);
expr_ref_vector args(m);
sort* range = get_array_range(m.get_sort(s));
for (unsigned i = 0; i < idxs.size(); ++i) {
app_ref var(m);
var = m.mk_fresh_const("value", range);
vars.push_back(var);
args.reset();
args.push_back(result);
args.append(idxs[i].m_values.size(), idxs[i].m_vars);
args.push_back(var);
result = a.mk_store(args.size(), args.c_ptr());
}
expr_safe_replace sub(m);
sub.insert(s, result);
for (unsigned i = 0; i < lits.size(); ++i) {
sub(lits[i].get(), result);
lits[i] = result;
}
return true;
}
if (a.is_store(s)) {
unsigned n = s->get_num_args()-2;
indices idx(m, model, n, s->get_args()+1);
for (unsigned i = 1; i < n; ++i) {
if (contains_x(s->get_arg(i))) {
return false;
}
}
unsigned i;
expr_ref_vector args(m);
switch (contains(idx, idxs, i)) {
case l_true:
mk_eq(idx, idxs[i], lits);
return solve(model, to_app(s->get_arg(0)), t, idxs, vars, lits);
case l_false:
for (unsigned i = 0; i < idxs.size(); ++i) {
expr_ref_vector eqs(m);
mk_eq(idx, idxs[i], eqs);
lits.push_back(m.mk_not(mk_and(eqs))); // TBD: extract single index of difference based on model.
}
args.push_back(t);
args.append(n, s->get_args()+1);
lits.push_back(m.mk_eq(a.mk_select(args.size(), args.c_ptr()), s->get_arg(n+1)));
idxs.push_back(idx);
return solve(model, to_app(s->get_arg(0)), t, idxs, vars, lits);
case l_undef:
return false;
}
}
return false;
}
lbool contains(indices const& idx, vector<indices> const& idxs, unsigned& j) {
for (unsigned i = 0; i < idxs.size(); ++i) {
switch (compare(idx, idxs[i])) {
case l_true:
j = i;
return l_true;
case l_false:
break;
case l_undef:
return l_undef;
}
}
return l_false;
}
lbool compare(indices const& idx1, indices const& idx2) {
unsigned n = idx1.m_values.size();
for (unsigned i = 0; i < n; ++i) {
switch (compare(idx1.m_values[i], idx2.m_values[i])) {
case l_true:
break;
case l_false:
return l_false;
case l_undef:
return l_undef;
}
}
return l_true;
}
lbool compare(expr* val1, expr* val2) {
if (val1 == val2) {
return l_true;
}
if (is_uninterp(val1) ||
is_uninterp(val2)) {
// TBD chase definition of nested array.
return l_undef;
}
return l_true;
}
};
array_project_plugin::array_project_plugin(ast_manager& m) {
m_imp = alloc(imp, m);
}
array_project_plugin::~array_project_plugin() {
dealloc(m_imp);
}
bool array_project_plugin::operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
return (*m_imp)(model, var, vars, lits);
}
bool array_project_plugin::solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
return m_imp->solve(model, vars, lits);
}
family_id array_project_plugin::get_family_id() {
return m_imp->a.get_family_id();
}
};

42
src/qe/qe_arrays.h Normal file
View file

@ -0,0 +1,42 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
qe_arrays.h
Abstract:
Model based projection for arrays
Author:
Nikolaj Bjorner (nbjorner) 2015-06-13
Revision History:
--*/
#ifndef __QE_ARRAYS_H_
#define __QE_ARRAYS_H_
#include "array_decl_plugin.h"
#include "qe_mbp.h"
namespace qe {
class array_project_plugin : public project_plugin {
struct imp;
imp* m_imp;
public:
array_project_plugin(ast_manager& m);
virtual ~array_project_plugin();
virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits);
virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits);
virtual family_id get_family_id();
};
};
#endif

312
src/qe/qe_datatypes.cpp Normal file
View file

@ -0,0 +1,312 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
qe_datatypes.cpp
Abstract:
Simple projection function for algebraic datatypes.
Author:
Nikolaj Bjorner (nbjorner) 2015-06-13
Revision History:
--*/
#include "qe_arith.h"
#include "ast_pp.h"
#include "th_rewriter.h"
#include "expr_functors.h"
#include "model_v2_pp.h"
#include "expr_safe_replace.h"
#include "obj_pair_hashtable.h"
#include "qe_datatypes.h"
namespace qe {
struct datatype_project_plugin::imp {
ast_manager& m;
datatype_util dt;
app_ref m_val;
scoped_ptr<contains_app> m_var;
imp(ast_manager& m):
m(m), dt(m), m_val(m) {}
virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
return lift_foreign(vars, lits);
}
bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
expr_ref val(m);
VERIFY(model.eval(var, val));
SASSERT(is_app(val));
TRACE("qe", tout << mk_pp(var, m) << " := " << val << "\n";);
m_val = to_app(val);
if (!dt.is_constructor(m_val)) {
// assert: var does not occur in lits.
return true;
}
m_var = alloc(contains_app, m, var);
try {
if (dt.is_recursive(m.get_sort(var))) {
project_rec(model, vars, lits);
}
else {
project_nonrec(model, vars, lits);
}
}
catch (cant_project) {
TRACE("qe", tout << "can't project:" << mk_pp(var, m) << "\n";);
return false;
}
return true;
}
void project_nonrec(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
expr_ref tmp(m), val(m);
expr_ref_vector args(m);
app_ref arg(m);
SASSERT(dt.is_constructor(m_val));
func_decl* f = m_val->get_decl();
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f);
for (unsigned i = 0; i < acc.size(); ++i) {
arg = m.mk_fresh_const(acc[i]->get_name().str().c_str(), acc[i]->get_range());
model.register_decl(arg->get_decl(), m_val->get_arg(i));
args.push_back(arg);
}
val = m.mk_app(f, args.size(), args.c_ptr());
TRACE("qe", tout << mk_pp(m_var->x(), m) << " |-> " << val << "\n";);
reduce(val, lits);
}
void project_rec(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
func_decl* f = m_val->get_decl();
expr_ref rhs(m);
expr_ref_vector eqs(m);
for (unsigned i = 0; i < lits.size(); ++i) {
if (solve(model, vars, lits[i].get(), rhs, eqs)) {
project_plugin::erase(lits, i);
reduce(rhs, lits);
lits.append(eqs);
return;
}
}
// otherwise, unfold the constructor associated with m_var
// once according to the model. In this way, selector-constructor
// redexes are reduced and disequalities are eventually solved
// by virtue of the constructors being different.
project_nonrec(model, vars, lits);
}
void reduce(expr* val, expr_ref_vector& lits) {
expr_safe_replace sub(m);
th_rewriter rw(m);
expr_ref tmp(m);
sub.insert(m_var->x(), val);
TRACE("qe", tout << mk_pp(m_var->x(), m) << " = " << mk_pp(val, m) << "\n";
tout << lits << "\n";);
for (unsigned i = 0; i < lits.size(); ++i) {
sub(lits[i].get(), tmp);
rw(tmp);
lits[i] = tmp;
}
}
bool contains_x(expr* e) {
return (*m_var)(e);
}
bool solve(model& model, app_ref_vector& vars, expr* fml, expr_ref& t, expr_ref_vector& eqs) {
expr* t1, *t2;
if (m.is_eq(fml, t1, t2)) {
if (contains_x(t1) && !contains_x(t2) && is_app(t1)) {
return solve(model, vars, to_app(t1), t2, t, eqs);
}
if (contains_x(t2) && !contains_x(t1) && is_app(t2)) {
return solve(model, vars, to_app(t2), t1, t, eqs);
}
}
if (m.is_not(fml, t1) && m.is_distinct(t1)) {
expr_ref eq = project_plugin::pick_equality(m, model, t1);
return solve(model, vars, eq, t, eqs);
}
return false;
}
bool solve(model& model, app_ref_vector& vars, app* a, expr* b, expr_ref& t, expr_ref_vector& eqs) {
SASSERT(contains_x(a));
SASSERT(!contains_x(b));
if (m_var->x() == a) {
t = b;
return true;
}
if (!dt.is_constructor(a)) {
return false;
}
func_decl* c = a->get_decl();
func_decl* rec = dt.get_constructor_recognizer(c);
ptr_vector<func_decl> const & acc = *dt.get_constructor_accessors(c);
SASSERT(acc.size() == a->get_num_args());
//
// It suffices to solve just the first available equality.
// The others are determined by the first.
//
for (unsigned i = 0; i < a->get_num_args(); ++i) {
expr* l = a->get_arg(i);
if (is_app(l) && contains_x(l)) {
expr_ref r(m);
r = access(c, i, acc, b);
if (solve(model, vars, to_app(l), r, t, eqs)) {
for (unsigned j = 0; j < c->get_arity(); ++j) {
if (i != j) {
eqs.push_back(m.mk_eq(access(c, j, acc, b), a->get_arg(j)));
}
}
if (!is_app_of(b, c)) {
eqs.push_back(m.mk_app(rec, b));
}
return true;
}
}
}
return false;
}
expr* access(func_decl* c, unsigned i, ptr_vector<func_decl> const& acc, expr* e) {
if (is_app_of(e,c)) {
return to_app(e)->get_arg(i);
}
else {
return m.mk_app(acc[i], e);
}
}
bool lift_foreign(app_ref_vector const& vars, expr_ref_vector& lits) {
bool reduced = false;
expr_mark visited;
expr_mark has_var;
bool inserted = false;
for (unsigned i = 0; i < vars.size(); ++i) {
if (m.is_bool(vars[i])) continue;
if (dt.is_datatype(m.get_sort(vars[i]))) continue;
inserted = true;
has_var.mark(vars[i]);
visited.mark(vars[i]);
}
if (inserted) {
for (unsigned i = 0; i < lits.size(); ++i) {
expr* e = lits[i].get(), *l, *r;
if (m.is_eq(e, l, r) && reduce_eq(visited, has_var, l, r, lits)) {
project_plugin::erase(lits, i);
reduced = true;
}
}
CTRACE("qe", reduced, tout << vars << "\n" << lits << "\n";);
}
return reduced;
}
bool reduce_eq(expr_mark& has_var, expr_mark& visited, expr* l, expr* r, expr_ref_vector& lits) {
if (!is_app(l) || !is_app(r)) {
return false;
}
bool reduce = false;
if (dt.is_constructor(to_app(r)) && contains_foreign(has_var, visited, r)) {
std::swap(l, r);
reduce = true;
}
reduce |= dt.is_constructor(to_app(l)) && contains_foreign(has_var, visited, l);
if (!reduce) {
return false;
}
func_decl* c = to_app(l)->get_decl();
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(c);
if (!is_app_of(r, c)) {
lits.push_back(m.mk_app(dt.get_constructor_recognizer(c), r));
}
for (unsigned i = 0; i < acc.size(); ++i) {
lits.push_back(m.mk_eq(to_app(l)->get_arg(i), access(c, i, acc, r)));
}
return true;
}
ptr_vector<expr> todo;
bool contains_foreign(expr_mark& has_var, expr_mark& visited, expr* e) {
todo.push_back(e);
while (!todo.empty()) {
expr* _f = todo.back();
if (visited.is_marked(_f)) {
todo.pop_back();
continue;
}
if (!is_app(_f)) {
visited.mark(_f);
todo.pop_back();
continue;
}
app* f = to_app(_f);
bool has_new = false, has_v = false;
for (unsigned i = 0; i < f->get_num_args(); ++i) {
expr* arg = f->get_arg(i);
if (!visited.is_marked(arg)) {
todo.push_back(arg);
has_new = true;
}
else {
has_v |= has_var.is_marked(arg);
}
}
if (has_new) {
continue;
}
todo.pop_back();
if (has_v) {
has_var.mark(f);
}
TRACE("qe", tout << "contains: " << mk_pp(f, m) << " " << has_var.is_marked(f) << "\n";);
visited.mark(f);
}
TRACE("qe", tout << "contains: " << mk_pp(e, m) << " " << has_var.is_marked(e) << "\n";);
return has_var.is_marked(e);
}
};
datatype_project_plugin::datatype_project_plugin(ast_manager& m) {
m_imp = alloc(imp, m);
}
datatype_project_plugin::~datatype_project_plugin() {
dealloc(m_imp);
}
bool datatype_project_plugin::operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
return (*m_imp)(model, var, vars, lits);
}
bool datatype_project_plugin::solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
return m_imp->solve(model, vars, lits);
}
family_id datatype_project_plugin::get_family_id() {
return m_imp->dt.get_family_id();
}
}

42
src/qe/qe_datatypes.h Normal file
View file

@ -0,0 +1,42 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
qe_datatypes.h
Abstract:
Model based projection for algebraic datatypes
Author:
Nikolaj Bjorner (nbjorner) 2015-06-13
Revision History:
--*/
#ifndef __QE_DATATYPES_H_
#define __QE_DATATYPES_H_
#include "datatype_decl_plugin.h"
#include "qe_mbp.h"
namespace qe {
class datatype_project_plugin : public project_plugin {
struct imp;
imp* m_imp;
public:
datatype_project_plugin(ast_manager& m);
virtual ~datatype_project_plugin();
virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits);
virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits);
virtual family_id get_family_id();
};
};
#endif

View file

@ -31,7 +31,6 @@ Revision History:
#include "var_subst.h"
#include "uint_set.h"
#include "ast_util.h"
#include "qe_util.h"
#include "th_rewriter.h"
#include "for_each_expr.h"
#include "expr_safe_replace.h"

369
src/qe/qe_mbp.cpp Normal file
View file

@ -0,0 +1,369 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
qe_mbp.cpp
Abstract:
Model-based projection utilities
Author:
Nikolaj Bjorner (nbjorner) 2015-5-29
Revision History:
--*/
#include "qe_mbp.h"
#include "qe_arith.h"
#include "qe_arrays.h"
#include "qe_datatypes.h"
#include "expr_safe_replace.h"
#include "ast_pp.h"
#include "ast_util.h"
#include "th_rewriter.h"
#include "model_v2_pp.h"
#include "expr_functors.h"
using namespace qe;
/**
\brief return two terms that are equal in the model.
The distinct term t is false in model, so there
are at least two arguments of t that are equal in the model.
*/
expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) {
SASSERT(m.is_distinct(t));
expr_ref val(m);
expr_ref_vector vals(m);
obj_map<expr, expr*> val2expr;
app* alit = to_app(t);
for (unsigned i = 0; i < alit->get_num_args(); ++i) {
expr* e1 = alit->get_arg(i), *e2;
VERIFY(model.eval(e1, val));
if (val2expr.find(val, e2)) {
return expr_ref(m.mk_eq(e1, e2), m);
}
val2expr.insert(val, e1);
vals.push_back(val);
}
UNREACHABLE();
return expr_ref(0, m);
}
void project_plugin::partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits) {
ast_manager& m = vals.get_manager();
expr_ref val(m);
expr_ref_vector trail(m), reps(m);
obj_map<expr, expr*> roots;
for (unsigned i = 0; i < vals.size(); ++i) {
expr* v = vals[i], *root;
VERIFY (model.eval(v, val));
if (roots.find(val, root)) {
lits.push_back(m.mk_eq(v, root));
}
else {
roots.insert(val, v);
trail.push_back(val);
reps.push_back(v);
}
}
if (reps.size() > 1) {
lits.push_back(mk_distinct(reps));
}
}
void project_plugin::partition_args(model& model, app_ref_vector const& selects, expr_ref_vector& lits) {
ast_manager& m = selects.get_manager();
if (selects.empty()) return;
unsigned num_args = selects[0]->get_decl()->get_arity();
for (unsigned j = 1; j < num_args; ++j) {
expr_ref_vector args(m);
for (unsigned i = 0; i < selects.size(); ++i) {
args.push_back(selects[i]->get_arg(j));
}
project_plugin::partition_values(model, args, lits);
}
}
void project_plugin::erase(expr_ref_vector& lits, unsigned& i) {
lits[i] = lits.back();
lits.pop_back();
--i;
}
void project_plugin::push_back(expr_ref_vector& lits, expr* e) {
if (lits.get_manager().is_true(e)) return;
lits.push_back(e);
}
class mbp::impl {
ast_manager& m;
ptr_vector<project_plugin> m_plugins;
void add_plugin(project_plugin* p) {
family_id fid = p->get_family_id();
SASSERT(!m_plugins.get(fid, 0));
m_plugins.setx(fid, p, 0);
}
project_plugin* get_plugin(app* var) {
family_id fid = m.get_sort(var)->get_family_id();
return m_plugins.get(fid, 0);
}
bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
expr_mark is_var, is_rem;
if (vars.empty()) {
return false;
}
bool reduced = false;
for (unsigned i = 0; i < vars.size(); ++i) {
is_var.mark(vars[i].get());
}
expr_ref tmp(m), t(m), v(m);
th_rewriter rw(m);
for (unsigned i = 0; i < lits.size(); ++i) {
expr* e = lits[i].get(), *l, *r;
if (m.is_eq(e, l, r) && reduce_eq(is_var, l, r, v, t)) {
reduced = true;
lits[i] = lits.back();
lits.pop_back();
--i;
expr_safe_replace sub(m);
sub.insert(v, t);
is_rem.mark(v);
for (unsigned j = 0; j < lits.size(); ++j) {
sub(lits[j].get(), tmp);
rw(tmp);
lits[j] = tmp;
}
}
}
if (reduced) {
for (unsigned i = 0; i < vars.size(); ++i) {
if (is_rem.is_marked(vars[i].get())) {
vars[i] = vars.back();
vars.pop_back();
}
}
}
return reduced;
}
bool reduce_eq(expr_mark& is_var, expr* l, expr* r, expr_ref& v, expr_ref& t) {
if (is_var.is_marked(r)) {
std::swap(l, r);
}
if (is_var.is_marked(l)) {
contains_app cont(m, to_app(l));
if (!cont(r)) {
v = to_app(l);
t = r;
return true;
}
}
return false;
}
public:
void extract_literals(model& model, expr_ref_vector& fmls) {
expr_ref val(m);
for (unsigned i = 0; i < fmls.size(); ++i) {
expr* fml = fmls[i].get(), *nfml, *f1, *f2, *f3;
if (m.is_not(fml, nfml) && m.is_distinct(nfml)) {
fmls[i] = project_plugin::pick_equality(m, model, nfml);
--i;
}
else if (m.is_or(fml)) {
for (unsigned j = 0; j < to_app(fml)->get_num_args(); ++j) {
VERIFY (model.eval(to_app(fml)->get_arg(j), val));
if (m.is_true(val)) {
fmls[i] = to_app(fml)->get_arg(j);
--i;
break;
}
}
}
else if (m.is_and(fml)) {
fmls.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());
project_plugin::erase(fmls, i);
}
else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) {
VERIFY (model.eval(f1, val));
if (m.is_false(val)) {
f1 = mk_not(m, f1);
f2 = mk_not(m, f2);
}
project_plugin::push_back(fmls, f1);
project_plugin::push_back(fmls, f2);
project_plugin::erase(fmls, i);
}
else if (m.is_implies(fml, f1, f2)) {
VERIFY (model.eval(f2, val));
if (m.is_true(val)) {
project_plugin::push_back(fmls, f2);
}
else {
project_plugin::push_back(fmls, mk_not(m, f1));
}
project_plugin::erase(fmls, i);
}
else if (m.is_ite(fml, f1, f2, f3)) {
VERIFY (model.eval(f1, val));
if (m.is_true(val)) {
project_plugin::push_back(fmls, f2);
}
else {
project_plugin::push_back(fmls, f3);
}
project_plugin::erase(fmls, i);
}
else if (m.is_not(fml, nfml) && m.is_not(nfml, nfml)) {
project_plugin::push_back(fmls, nfml);
project_plugin::erase(fmls, i);
}
else if (m.is_not(fml, nfml) && m.is_and(nfml)) {
for (unsigned j = 0; j < to_app(nfml)->get_num_args(); ++j) {
VERIFY (model.eval(to_app(nfml)->get_arg(j), val));
if (m.is_false(val)) {
fmls[i] = mk_not(m, to_app(nfml)->get_arg(j));
--i;
break;
}
}
}
else if (m.is_not(fml, nfml) && m.is_or(nfml)) {
for (unsigned j = 0; j < to_app(nfml)->get_num_args(); ++j) {
project_plugin::push_back(fmls, mk_not(m, to_app(nfml)->get_arg(j)));
}
project_plugin::erase(fmls, i);
}
else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) {
VERIFY (model.eval(f1, val));
if (m.is_true(val)) {
f2 = mk_not(m, f2);
}
else {
f1 = mk_not(m, f1);
}
project_plugin::push_back(fmls, f1);
project_plugin::push_back(fmls, f2);
project_plugin::erase(fmls, i);
}
else if (m.is_not(fml, nfml) && m.is_implies(nfml, f1, f2)) {
project_plugin::push_back(fmls, f1);
project_plugin::push_back(fmls, mk_not(m, f2));
project_plugin::erase(fmls, i);
}
else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) {
VERIFY (model.eval(f1, val));
if (m.is_true(val)) {
project_plugin::push_back(fmls, mk_not(m, f2));
}
else {
project_plugin::push_back(fmls, mk_not(m, f3));
}
project_plugin::erase(fmls, i);
}
else {
// TBD other Boolean operations.
}
}
}
impl(ast_manager& m):m(m) {
add_plugin(alloc(arith_project_plugin, m));
add_plugin(alloc(datatype_project_plugin, m));
add_plugin(alloc(array_project_plugin, m));
}
~impl() {
std::for_each(m_plugins.begin(), m_plugins.end(), delete_proc<project_plugin>());
}
void preprocess_solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) {
extract_literals(model, fmls);
bool change = true;
while (change && !vars.empty()) {
change = solve(model, vars, fmls);
for (unsigned i = 0; i < m_plugins.size(); ++i) {
if (m_plugins[i] && m_plugins[i]->solve(model, vars, fmls)) {
change = true;
}
}
}
}
void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls) {
expr_ref val(m), tmp(m);
app_ref var(m);
th_rewriter rw(m);
bool progress = true;
while (progress && !vars.empty()) {
preprocess_solve(model, vars, fmls);
app_ref_vector new_vars(m);
progress = false;
while (!vars.empty()) {
var = vars.back();
vars.pop_back();
project_plugin* p = get_plugin(var);
if (p && (*p)(model, var, vars, fmls)) {
progress = true;
}
else {
new_vars.push_back(var);
}
}
if (!progress && !new_vars.empty() && force_elim) {
var = new_vars.back();
new_vars.pop_back();
expr_safe_replace sub(m);
VERIFY(model.eval(var, val));
sub.insert(var, val);
for (unsigned i = 0; i < fmls.size(); ++i) {
sub(fmls[i].get(), tmp);
rw(tmp);
if (m.is_true(tmp)) {
fmls[i] = fmls.back();
fmls.pop_back();
--i;
}
else {
fmls[i] = tmp;
}
}
progress = true;
}
vars.append(new_vars);
}
}
};
mbp::mbp(ast_manager& m) {
m_impl = alloc(impl, m);
}
mbp::~mbp() {
dealloc(m_impl);
}
void mbp::operator()(bool force_elim, app_ref_vector& vars, model& mdl, expr_ref_vector& fmls) {
(*m_impl)(force_elim, vars, mdl, fmls);
}
void mbp::solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) {
m_impl->preprocess_solve(model, vars, fmls);
}
void mbp::extract_literals(model& model, expr_ref_vector& lits) {
m_impl->extract_literals(model, lits);
}

76
src/qe/qe_mbp.h Normal file
View file

@ -0,0 +1,76 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
qe_mbp.h
Abstract:
Model-based projection utilities
Author:
Nikolaj Bjorner (nbjorner) 2015-5-28
Revision History:
--*/
#ifndef __QE_MBP_H__
#define __QE_MBP_H__
#include "ast.h"
#include "params.h"
#include "model.h"
namespace qe {
struct cant_project {};
class project_plugin {
public:
virtual ~project_plugin() {}
virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) = 0;
virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) = 0;
virtual family_id get_family_id() = 0;
static expr_ref pick_equality(ast_manager& m, model& model, expr* t);
static void partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits);
static void partition_args(model& model, app_ref_vector const& sels, expr_ref_vector& lits);
static void erase(expr_ref_vector& lits, unsigned& i);
static void push_back(expr_ref_vector& lits, expr* lit);
};
class mbp {
class impl;
impl * m_impl;
public:
mbp(ast_manager& m);
~mbp();
/**
\brief
Apply model-based qe on constants provided as vector of variables.
Return the updated formula and updated set of variables that were not eliminated.
*/
void operator()(bool force_elim, app_ref_vector& vars, model& mdl, expr_ref_vector& fmls);
/**
\brief
Solve as many variables as possible using "cheap" quantifier elimination"
*/
void solve(model& model, app_ref_vector& vars, expr_ref_vector& lits);
/**
\brief
Extract literals from formulas based on model.
*/
void extract_literals(model& model, expr_ref_vector& lits);
};
}
#endif