mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

introduce proxies to differentiate from arithmetical variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-12-29 11:13:15 +08:00
parent e40884725b
commit f8a3300026
4 changed files with 53 additions and 32 deletions

50
src/qe/qe_mbi.cpp
View file

@ -126,30 +126,29 @@ namespace qe {
struct euf_arith_mbi_plugin::is_arith_var_proc {
ast_manager& m;
app_ref_vector& m_avars;
arith_util arith;
app_ref_vector& m_proxies;
arith_util m_arith;
obj_hashtable<expr> m_seen;
is_arith_var_proc(app_ref_vector& avars):
m(avars.m()), m_avars(avars), arith(m) {
is_arith_var_proc(app_ref_vector& avars, app_ref_vector& proxies):
m(avars.m()), m_avars(avars), m_proxies(proxies), m_arith(m) {
}
void operator()(app* a) {
if (is_arith_op(a) || a->get_family_id() == m.get_basic_family_id()) {
// no-op
return;
}
else if (!arith.is_int_real(a)) {
for (expr* arg : *a) {
if (is_app(arg) && !m_seen.contains(arg) && is_arith_op(to_app(arg))) {
m_avars.push_back(to_app(arg));
m_seen.insert(arg);
}
}
}
else if (!m_seen.contains(a)) {
m_seen.insert(a);
if (m_arith.is_int_real(a)) {
m_avars.push_back(a);
}
for (expr* arg : *a) {
if (is_app(arg) && !m_seen.contains(arg) && m_arith.is_int_real(arg)) {
m_proxies.push_back(to_app(arg));
m_seen.insert(arg);
}
}
}
bool is_arith_op(app* a) {
return a->get_family_id() == arith.get_family_id();
return a->get_family_id() == m_arith.get_family_id();
}
void operator()(expr*) {}
};
@ -221,9 +220,9 @@ namespace qe {
/**
* \brief extract arithmetical variables and arithmetical terms in shared positions.
*/
app_ref_vector euf_arith_mbi_plugin::get_arith_vars(model_ref& mdl, expr_ref_vector& lits) {
app_ref_vector euf_arith_mbi_plugin::get_arith_vars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& proxies) {
app_ref_vector avars(m);
is_arith_var_proc _proc(avars);
is_arith_var_proc _proc(avars, proxies);
for_each_expr(_proc, lits);
return avars;
}
@ -259,14 +258,15 @@ namespace qe {
TRACE("qe", tout << lits << "\n" << *mdl << "\n";);
// 1. arithmetical variables - atomic and in purified positions
app_ref_vector avars = get_arith_vars(mdl, lits);
TRACE("qe", tout << "vars: " << avars << "\nlits: " << lits << "\n";);
app_ref_vector proxies(m);
app_ref_vector avars = get_arith_vars(mdl, lits, proxies);
TRACE("qe", tout << "vars: " << avars << "\nproxies: " << proxies << "\nlits: " << lits << "\n";);
// 2. project private non-arithmetical variables from lits
project_euf(mdl, lits, avars);
// 3. Order arithmetical variables and purified positions
order_avars(mdl, lits, avars);
order_avars(mdl, lits, avars, proxies);
TRACE("qe", tout << "ordered: " << lits << "\n";);
// 4. Perform arithmetical projection
@ -307,15 +307,14 @@ namespace qe {
/**
* \brief Order arithmetical variables:
* 1. add literals that order the variable according to the model.
* 2. remove non-atomic arithmetical terms from projection.
* 1. add literals that order the proxies according to the model.
* 2. sort arithmetical terms, such that deepest terms are first.
*/
void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars) {
void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies) {
arith_util a(m);
model_evaluator mev(*mdl.get());
vector<std::pair<rational, app*>> vals;
for (app* v : avars) {
for (app* v : proxies) {
rational val;
expr_ref tmp = mev(v);
VERIFY(a.is_numeral(tmp, val));
@ -327,7 +326,7 @@ namespace qe {
return x.first < y.first;
}
};
// add linear order between avars
// add linear order between proxies
compare_first cmp;
std::sort(vals.begin(), vals.end(), cmp);
for (unsigned i = 1; i < vals.size(); ++i) {
@ -338,6 +337,7 @@ namespace qe {
lits.push_back(a.mk_lt(vals[i-1].second, vals[i].second));
}
}
// filter out only private variables
filter_private_arith(avars);

4
src/qe/qe_mbi.h
View file

@ -103,12 +103,12 @@ namespace qe {
struct is_atom_proc;
struct is_arith_var_proc;
app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits);
app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& proxies);
bool get_literals(model_ref& mdl, expr_ref_vector& lits);
void collect_atoms(expr_ref_vector const& fmls);
void project(model_ref& mdl, expr_ref_vector& lits);
void project_euf(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars);
void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars);
void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies);
void substitute(vector<def> const& defs, expr_ref_vector& lits);
void filter_private_arith(app_ref_vector& avars);
public:

1
src/smt/smt_context_pp.cpp
View file

@ -200,6 +200,7 @@ namespace smt {
out << "current assignment:\n";
for (literal lit : m_assigned_literals) {
display_literal(out, lit);
if (!is_relevant(lit)) out << " n ";
out << ": ";
display_verbose(out, m_manager, 1, &lit, m_bool_var2expr.c_ptr());
out << "\n";

30
src/smt/theory_bv.cpp
View file

@ -53,6 +53,7 @@ namespace smt {
unsigned bv_size = get_bv_size(n);
context & ctx = get_context();
literal_vector & bits = m_bits[v];
TRACE("bv", tout << "v" << v << "\n";);
bits.reset();
for (unsigned i = 0; i < bv_size; i++) {
app * bit = mk_bit2bool(owner, i);
@ -77,6 +78,7 @@ namespace smt {
context & ctx = get_context();
SASSERT(!ctx.b_internalized(n));
TRACE("bv", tout << "bit2bool: " << mk_pp(n, ctx.get_manager()) << "\n";);
expr* first_arg = n->get_arg(0);
if (!ctx.e_internalized(first_arg)) {
@ -98,17 +100,20 @@ namespace smt {
rational val;
unsigned sz;
if (!ctx.b_internalized(n) && m_util.is_numeral(first_arg, val, sz)) {
TRACE("bv", tout << "bit2bool constants\n";);
theory_var v = first_arg_enode->get_th_var(get_id());
app* owner = first_arg_enode->get_owner();
for (unsigned i = 0; i < sz; ++i) {
ctx.internalize(mk_bit2bool(owner, i), true);
app* e = mk_bit2bool(owner, i);
ctx.internalize(e, true);
}
m_bits[v].reset();
rational bit;
for (unsigned i = 0; i < sz; ++i) {
div(val, rational::power_of_two(i), bit);
mod(bit, rational(2), bit);
m_bits[v].push_back(bit.is_zero()?false_literal:true_literal);
m_bits[v].push_back(bit.is_zero()?false_literal:true_literal);
}
}
}
@ -135,6 +140,18 @@ namespace smt {
SASSERT(a->m_occs == 0);
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
}
rational val;
unsigned sz;
if (m_util.is_numeral(first_arg, val, sz)) {
rational bit;
unsigned idx = n->get_decl()->get_parameter(0).get_int();
div(val, rational::power_of_two(idx), bit);
mod(bit, rational(2), bit);
literal lit = ctx.get_literal(n);
if (bit.is_zero()) lit.neg();
ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), 1, &lit);
}
}
void theory_bv::process_args(app * n) {
@ -622,7 +639,9 @@ namespace smt {
context& ctx = get_context();
process_args(n);
mk_enode(n);
mk_bits(ctx.get_enode(n)->get_th_var(get_id()));
theory_var v = ctx.get_enode(n)->get_th_var(get_id());
mk_bits(v);
if (!ctx.relevancy()) {
assert_int2bv_axiom(n);
}
@ -1179,7 +1198,7 @@ namespace smt {
m_prop_queue.push_back(var_pos(curr->m_var, curr->m_idx));
curr = curr->m_next;
}
TRACE("bv", tout << m_prop_queue.size() << "\n";);
TRACE("bv", tout << "prop queue size: " << m_prop_queue.size() << "\n";);
propagate_bits();
}
}
@ -1196,7 +1215,7 @@ namespace smt {
literal_vector & bits = m_bits[v];
literal bit = bits[idx];
lbool val = ctx.get_assignment(bit);
lbool val = ctx.get_assignment(bit);
if (val == l_undef) {
continue;
}
@ -1213,6 +1232,7 @@ namespace smt {
SASSERT(bit != ~bit2);
lbool val2 = ctx.get_assignment(bit2);
TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";);
TRACE("bv", tout << bit << " " << bit2 << "\n";);
if (val != val2) {
literal consequent = bit2;