mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 03:32:28 +00:00
1063 lines
32 KiB
C++
1063 lines
32 KiB
C++
/*++
|
|
Copyright (c) 2022 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
expr_inverter.cpp
|
|
|
|
Abstract:
|
|
|
|
inverter interface and instance
|
|
|
|
Author:
|
|
|
|
Nikolaj Bjorner (nbjorner) 2022-10-11
|
|
|
|
--*/
|
|
|
|
#include "ast/ast_pp.h"
|
|
#include "ast/ast_ll_pp.h"
|
|
#include "ast/ast_util.h"
|
|
#include "ast/arith_decl_plugin.h"
|
|
#include "ast/seq_decl_plugin.h"
|
|
#include "ast/pb_decl_plugin.h"
|
|
#include "ast/rewriter/seq_rewriter.h"
|
|
#include "ast/converters/expr_inverter.h"
|
|
|
|
class basic_expr_inverter : public iexpr_inverter {
|
|
iexpr_inverter& inv;
|
|
|
|
bool process_eq(func_decl* f, expr* arg1, expr* arg2, expr_ref& r) {
|
|
expr* v;
|
|
expr* t;
|
|
if (uncnstr(arg1))
|
|
v = arg1, t = arg2;
|
|
else if (uncnstr(arg2))
|
|
v = arg2, t = arg1;
|
|
else
|
|
return false;
|
|
|
|
expr_ref d(m);
|
|
if (!inv.mk_diff(t, d))
|
|
return false;
|
|
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc)
|
|
add_def(v, m.mk_ite(r, t, d));
|
|
|
|
return true;
|
|
}
|
|
|
|
public:
|
|
|
|
basic_expr_inverter(ast_manager& m, iexpr_inverter& inv) : iexpr_inverter(m), inv(inv) {}
|
|
|
|
family_id get_fid() const override { return m.get_basic_family_id(); }
|
|
|
|
/**
|
|
* if (c, x, x') -> fresh
|
|
* x := fresh
|
|
* x' := fresh
|
|
*
|
|
* if (x, x', e) -> fresh
|
|
* x := true
|
|
* x' := fresh
|
|
*
|
|
* if (x, t, x') -> fresh
|
|
* x := false
|
|
* x' := fresh
|
|
*
|
|
* not x -> fresh
|
|
* x := not fresh
|
|
*
|
|
* x & x' -> fresh
|
|
* x := fresh
|
|
* x' := true
|
|
*
|
|
* x or x' -> fresh
|
|
* x := fresh
|
|
* x' := false
|
|
*
|
|
* x = t -> fresh
|
|
* x := if(fresh, t, diff(t))
|
|
* where diff is a diagonalization function available in domains of size > 1.
|
|
*
|
|
*/
|
|
|
|
bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
|
|
SASSERT(f->get_family_id() == m.get_basic_family_id());
|
|
switch (f->get_decl_kind()) {
|
|
case OP_ITE:
|
|
SASSERT(num == 3);
|
|
if (uncnstr(args[1]) && uncnstr(args[2])) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
add_def(args[1], r);
|
|
add_def(args[2], r);
|
|
return true;
|
|
}
|
|
if (uncnstr(args[0]) && uncnstr(args[1])) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
add_def(args[0], m.mk_true());
|
|
add_def(args[1], r);
|
|
return true;
|
|
}
|
|
if (uncnstr(args[0]) && uncnstr(args[2])) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
add_def(args[0], m.mk_false());
|
|
add_def(args[2], r);
|
|
return true;
|
|
}
|
|
return false;
|
|
case OP_NOT:
|
|
SASSERT(num == 1);
|
|
if (uncnstr(args[0])) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
add_def(args[0], m.mk_not(r));
|
|
return true;
|
|
}
|
|
return false;
|
|
case OP_AND:
|
|
if (num > 0 && uncnstr(num, args)) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
add_defs(num, args, r, m.mk_true());
|
|
return true;
|
|
}
|
|
return false;
|
|
case OP_OR:
|
|
if (num > 0 && uncnstr(num, args)) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
add_defs(num, args, r, m.mk_false());
|
|
return true;
|
|
}
|
|
return false;
|
|
case OP_EQ:
|
|
SASSERT(num == 2);
|
|
return process_eq(f, args[0], args[1], r);
|
|
default:
|
|
return false;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool mk_diff(expr* t, expr_ref& r) override {
|
|
SASSERT(m.is_bool(t));
|
|
r = mk_not(m, t);
|
|
return true;
|
|
}
|
|
};
|
|
|
|
class arith_expr_inverter : public iexpr_inverter {
|
|
arith_util a;
|
|
public:
|
|
|
|
arith_expr_inverter(ast_manager& m) : iexpr_inverter(m), a(m) {}
|
|
|
|
family_id get_fid() const override { return a.get_family_id(); }
|
|
|
|
bool process_le_ge(func_decl* f, expr* arg1, expr* arg2, bool le, expr_ref& r) {
|
|
expr* v;
|
|
expr* t;
|
|
if (uncnstr(arg1)) {
|
|
v = arg1;
|
|
t = arg2;
|
|
}
|
|
else if (uncnstr(arg2)) {
|
|
v = arg2;
|
|
t = arg1;
|
|
le = !le;
|
|
}
|
|
else
|
|
return false;
|
|
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc) {
|
|
// v = ite(u, t, t + 1) if le
|
|
// v = ite(u, t, t - 1) if !le
|
|
add_def(v, m.mk_ite(r, t, a.mk_add(t, a.mk_numeral(rational(le ? 1 : -1), arg1->get_sort()))));
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool process_add(unsigned num, expr* const* args, expr_ref& u) {
|
|
if (num == 0)
|
|
return false;
|
|
unsigned i;
|
|
expr* v = nullptr;
|
|
for (i = 0; i < num; i++) {
|
|
expr* arg = args[i];
|
|
if (uncnstr(arg)) {
|
|
v = arg;
|
|
break;
|
|
}
|
|
}
|
|
if (v == nullptr)
|
|
return false;
|
|
mk_fresh_uncnstr_var_for(v->get_sort(), u);
|
|
if (!m_mc)
|
|
return true;
|
|
ptr_buffer<expr> new_args;
|
|
for (unsigned j = 0; j < num; j++)
|
|
if (j != i)
|
|
new_args.push_back(args[j]);
|
|
|
|
if (new_args.empty())
|
|
add_def(v, u);
|
|
else {
|
|
expr* rest = a.mk_add(new_args);
|
|
add_def(v, a.mk_sub(u, rest));
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool process_arith_mul(unsigned num, expr* const* args, expr_ref & u) {
|
|
if (num == 0)
|
|
return false;
|
|
sort* s = args[0]->get_sort();
|
|
if (uncnstr(num, args)) {
|
|
mk_fresh_uncnstr_var_for(s, u);
|
|
if (m_mc)
|
|
add_defs(num, args, u, a.mk_numeral(rational(1), s));
|
|
return true;
|
|
}
|
|
// c * v case for reals
|
|
bool is_int;
|
|
rational val;
|
|
if (num == 2 && uncnstr(args[1]) && a.is_numeral(args[0], val, is_int) && !is_int) {
|
|
if (val.is_zero())
|
|
return false;
|
|
mk_fresh_uncnstr_var_for(s, u);
|
|
if (m_mc) {
|
|
val = rational(1) / val;
|
|
add_def(args[1], a.mk_mul(a.mk_numeral(val, false), u));
|
|
}
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
|
|
bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
|
|
SASSERT(f->get_family_id() == a.get_family_id());
|
|
switch (f->get_decl_kind()) {
|
|
case OP_ADD:
|
|
return process_add(num, args, r);
|
|
case OP_MUL:
|
|
return process_arith_mul(num, args, r);
|
|
case OP_LE:
|
|
SASSERT(num == 2);
|
|
return process_le_ge(f, args[0], args[1], true, r);
|
|
case OP_GE:
|
|
SASSERT(num == 2);
|
|
return process_le_ge(f, args[0], args[1], false, r);
|
|
default:
|
|
return false;
|
|
}
|
|
}
|
|
|
|
|
|
bool mk_diff(expr* t, expr_ref& r) override {
|
|
SASSERT(a.is_int_real(t));
|
|
r = a.mk_add(t, a.mk_numeral(rational(1), a.is_int(t)));
|
|
return true;
|
|
}
|
|
};
|
|
|
|
class bv_expr_inverter : public iexpr_inverter {
|
|
bv_util bv;
|
|
|
|
bool process_add(unsigned num, expr* const* args, expr_ref& u) {
|
|
if (num == 0)
|
|
return false;
|
|
unsigned i;
|
|
expr* v = nullptr;
|
|
for (i = 0; i < num; i++) {
|
|
expr* arg = args[i];
|
|
if (uncnstr(arg)) {
|
|
v = arg;
|
|
break;
|
|
}
|
|
}
|
|
if (!v)
|
|
return false;
|
|
mk_fresh_uncnstr_var_for(v->get_sort(), u);
|
|
if (!m_mc)
|
|
return true;
|
|
ptr_buffer<expr> new_args;
|
|
for (unsigned j = 0; j < num; j++)
|
|
if (j != i)
|
|
new_args.push_back(args[j]);
|
|
|
|
if (new_args.empty())
|
|
add_def(v, u);
|
|
else {
|
|
expr* rest = bv.mk_bv_add(new_args);
|
|
add_def(v, bv.mk_bv_sub(u, rest));
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool process_bv_mul(func_decl* f, unsigned num, expr* const* args, expr_ref& r) {
|
|
if (num == 0)
|
|
return false;
|
|
if (uncnstr(num, args)) {
|
|
sort* s = args[0]->get_sort();
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc)
|
|
add_defs(num, args, r, bv.mk_one(s));
|
|
return true;
|
|
}
|
|
// c * v (c is odd) case
|
|
unsigned sz;
|
|
rational val;
|
|
rational inv;
|
|
if (num == 2 &&
|
|
uncnstr(args[1]) &&
|
|
bv.is_numeral(args[0], val, sz) &&
|
|
val.mult_inverse(sz, inv)) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc)
|
|
add_def(args[1], bv.mk_bv_mul(bv.mk_numeral(inv, sz), r));
|
|
return true;
|
|
}
|
|
|
|
//
|
|
// x * K -> fresh[hi-sh-1:0] ++ 0...0
|
|
// where sh = parity of K
|
|
// then x -> J^-1*fresh
|
|
// where J = K >> sh
|
|
// Because x * K = fresh * K * J^-1 = fresh * 2^sh = fresh[hi-sh-1:0] ++ 0...0
|
|
//
|
|
if (num == 2 &&
|
|
uncnstr(args[1]) &&
|
|
bv.is_numeral(args[0], val, sz) &&
|
|
val.is_pos()) {
|
|
unsigned sh = 0;
|
|
while (val.is_even()) {
|
|
val /= rational(2);
|
|
++sh;
|
|
}
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (sh > 0)
|
|
r = bv.mk_concat(bv.mk_extract(sz - sh - 1, 0, r), bv.mk_zero(sh));
|
|
|
|
if (m_mc) {
|
|
rational inv_r;
|
|
VERIFY(val.mult_inverse(sz, inv_r));
|
|
add_def(args[1], bv.mk_bv_mul(bv.mk_numeral(inv_r, sz), r));
|
|
}
|
|
return true;
|
|
}
|
|
|
|
//
|
|
// assume x is unconstrained, we can handle general multiplication as follows:
|
|
// x * y -> if y = 0 then y else fresh << parity(y)
|
|
// and x -> if y = 0 then y else (y >> parity(y))^-1
|
|
// parity can be defined using a "giant" ite expression.
|
|
//
|
|
|
|
#if 0
|
|
for (unsigned i = 0; i < num; ++i)
|
|
if (uncnstr(args[i]))
|
|
IF_VERBOSE(11, verbose_stream() << "MISSED mult-unconstrained " << mk_bounded_pp(args[i], m) << "\n");
|
|
#endif
|
|
|
|
return false;
|
|
}
|
|
|
|
|
|
bool process_extract(func_decl* f, expr* arg, expr_ref& r) {
|
|
if (!uncnstr(arg))
|
|
return false;
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (!m_mc)
|
|
return true;
|
|
unsigned high = bv.get_extract_high(f);
|
|
unsigned low = bv.get_extract_low(f);
|
|
unsigned bv_size = bv.get_bv_size(arg->get_sort());
|
|
if (bv_size == high - low + 1)
|
|
add_def(arg, r);
|
|
else {
|
|
ptr_buffer<expr> args;
|
|
if (high < bv_size - 1)
|
|
args.push_back(bv.mk_zero(bv_size - high - 1));
|
|
args.push_back(r);
|
|
if (low > 0)
|
|
args.push_back(bv.mk_zero(low));
|
|
add_def(arg, bv.mk_concat(args.size(), args.data()));
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool process_bv_div(func_decl* f, expr* arg1, expr* arg2, expr_ref& r) {
|
|
if (uncnstr(arg1) && uncnstr(arg2)) {
|
|
sort* s = arg1->get_sort();
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc) {
|
|
add_def(arg1, r);
|
|
add_def(arg2, bv.mk_one(s));
|
|
}
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool process_concat(func_decl* f, unsigned num, expr* const* args, expr_ref& r) {
|
|
// return false;
|
|
if (num == 0)
|
|
return false;
|
|
if (!uncnstr(num, args))
|
|
return false;
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc) {
|
|
unsigned i = num;
|
|
unsigned low = 0;
|
|
while (i > 0) {
|
|
--i;
|
|
expr* arg = args[i];
|
|
unsigned sz = bv.get_bv_size(arg);
|
|
add_def(arg, bv.mk_extract(low + sz - 1, low, r));
|
|
low += sz;
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool process_bv_le(func_decl* f, expr* arg1, expr* arg2, bool is_signed, expr_ref& r) {
|
|
unsigned bv_sz = bv.get_bv_size(arg1);
|
|
if (uncnstr(arg1) && uncnstr(arg2)) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc) {
|
|
add_def(arg1, m.mk_ite(r, bv.mk_zero(bv_sz), bv.mk_one(bv_sz)));
|
|
add_def(arg2, bv.mk_zero(bv_sz));
|
|
}
|
|
return true;
|
|
}
|
|
if (uncnstr(arg1)) {
|
|
// v <= t
|
|
expr* v = arg1;
|
|
expr* t = arg2;
|
|
// v <= t ---> (u or t == MAX) u is fresh
|
|
// add definition v = ite(u or t == MAX, t, t+1)
|
|
|
|
rational MAX;
|
|
if (is_signed)
|
|
MAX = rational::power_of_two(bv_sz - 1) - rational(1);
|
|
else
|
|
MAX = rational::power_of_two(bv_sz) - rational(1);
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
r = m.mk_or(r, m.mk_eq(t, bv.mk_numeral(MAX, bv_sz)));
|
|
if (m_mc)
|
|
add_def(v, m.mk_ite(r, t, bv.mk_bv_add(t, bv.mk_one(bv_sz))));
|
|
return true;
|
|
}
|
|
if (uncnstr(arg2)) {
|
|
// v >= t
|
|
expr* v = arg2;
|
|
expr* t = arg1;
|
|
// v >= t ---> (u ot t == MIN) u is fresh
|
|
// add definition v = ite(u or t == MIN, t, t-1)
|
|
rational MIN;
|
|
if (is_signed)
|
|
MIN = -rational::power_of_two(bv_sz - 1);
|
|
else
|
|
MIN = rational(0);
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
r = m.mk_or(r, m.mk_eq(t, bv.mk_numeral(MIN, bv_sz)));
|
|
if (m_mc)
|
|
add_def(v, m.mk_ite(r, t, bv.mk_bv_sub(t, bv.mk_one(bv_sz))));
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool process_bvnot(expr* e, expr_ref& r) {
|
|
if (!uncnstr(e))
|
|
return false;
|
|
mk_fresh_uncnstr_var_for(e->get_sort(), r);
|
|
if (m_mc)
|
|
add_def(e, bv.mk_bv_not(r));
|
|
return true;
|
|
}
|
|
|
|
bool process_shift(func_decl* f, expr* arg1, expr* arg2, expr_ref& r) {
|
|
if (uncnstr(arg1) && uncnstr(arg2)) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc) {
|
|
add_def(arg1, r);
|
|
add_def(arg2, bv.mk_zero(arg2->get_sort()));
|
|
}
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
public:
|
|
bv_expr_inverter(ast_manager& m) : iexpr_inverter(m), bv(m) {}
|
|
|
|
family_id get_fid() const override { return bv.get_family_id(); }
|
|
|
|
/**
|
|
* x + t -> fresh
|
|
* x := fresh - t
|
|
*
|
|
* x * x' * x'' -> fresh
|
|
* x := fresh
|
|
* x', x'' := 1
|
|
*
|
|
* c * x -> fresh, c is odd
|
|
* x := fresh*c^-1
|
|
*
|
|
* x[sz-1:0] -> fresh
|
|
* x := fresh
|
|
*
|
|
* x[hi:lo] -> fresh
|
|
* x := fresh1 ++ fresh ++ fresh2
|
|
*
|
|
* x udiv x', x sdiv x' -> fresh
|
|
* x' := 1
|
|
* x := fresh
|
|
*
|
|
* x ++ x' ++ x'' -> fresh
|
|
* x := fresh[hi1:lo1]
|
|
* x' := fresh[hi2:lo2]
|
|
* x'' := fresh[hi3:lo3]
|
|
*
|
|
* x <= t -> fresh or t == MAX
|
|
* x := if(fresh, t, t + 1)
|
|
* t <= x -> fresh or t == MIN
|
|
* x := if(fresh, t, t - 1)
|
|
*
|
|
* ~x -> fresh
|
|
* x := ~fresh
|
|
*
|
|
* x | y -> fresh
|
|
* x := fresh
|
|
* y := 0
|
|
*
|
|
*/
|
|
bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
|
|
SASSERT(f->get_family_id() == bv.get_family_id());
|
|
switch (f->get_decl_kind()) {
|
|
case OP_BADD:
|
|
return process_add(num, args, r);
|
|
case OP_BMUL:
|
|
return process_bv_mul(f, num, args, r);
|
|
case OP_BSDIV:
|
|
case OP_BUDIV:
|
|
case OP_BSDIV_I:
|
|
case OP_BUDIV_I:
|
|
SASSERT(num == 2);
|
|
return process_bv_div(f, args[0], args[1], r);
|
|
case OP_SLEQ:
|
|
SASSERT(num == 2);
|
|
return process_bv_le(f, args[0], args[1], true, r);
|
|
case OP_ULEQ:
|
|
SASSERT(num == 2);
|
|
return process_bv_le(f, args[0], args[1], false, r);
|
|
case OP_CONCAT:
|
|
return process_concat(f, num, args, r);
|
|
case OP_EXTRACT:
|
|
SASSERT(num == 1);
|
|
return process_extract(f, args[0], r);
|
|
case OP_BNOT:
|
|
SASSERT(num == 1);
|
|
return process_bvnot(args[0], r);
|
|
case OP_BOR:
|
|
if (num > 0 && uncnstr(num, args)) {
|
|
sort* s = args[0]->get_sort();
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc)
|
|
add_defs(num, args, r, bv.mk_zero(s));
|
|
return true;
|
|
}
|
|
return false;
|
|
case OP_BAND:
|
|
if (num > 0 && uncnstr(num, args)) {
|
|
sort* s = args[0]->get_sort();
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc)
|
|
add_defs(num, args, r, bv.mk_numeral(rational::power_of_two(bv.get_bv_size(s)) - 1, s));
|
|
return true;
|
|
}
|
|
return false;
|
|
case OP_BSHL:
|
|
case OP_BASHR:
|
|
case OP_BLSHR:
|
|
return process_shift(f, args[0], args[1], r);
|
|
default:
|
|
return false;
|
|
}
|
|
}
|
|
|
|
bool mk_diff(expr* t, expr_ref& r) override {
|
|
SASSERT(bv.is_bv(t));
|
|
r = bv.mk_bv_not(t);
|
|
return true;
|
|
}
|
|
};
|
|
|
|
|
|
|
|
/**
|
|
* F[select(x, i)] -> F[fresh]
|
|
* x := const(fresh)
|
|
|
|
* F[store(x, ..., x')] -> F[fresh]
|
|
* x' := select(x, ...)
|
|
* x := fresh
|
|
*/
|
|
|
|
class array_expr_inverter : public iexpr_inverter {
|
|
array_util a;
|
|
iexpr_inverter& inv;
|
|
public:
|
|
array_expr_inverter(ast_manager& m, iexpr_inverter& s) : iexpr_inverter(m), a(m), inv(s) {}
|
|
|
|
family_id get_fid() const override { return a.get_family_id(); }
|
|
|
|
bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
|
|
SASSERT(f->get_family_id() == a.get_family_id());
|
|
switch (f->get_decl_kind()) {
|
|
case OP_SELECT:
|
|
if (uncnstr(args[0])) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
sort* s = args[0]->get_sort();
|
|
if (m_mc)
|
|
add_def(args[0], a.mk_const_array(s, r));
|
|
return true;
|
|
}
|
|
return false;
|
|
case OP_STORE:
|
|
if (uncnstr(args[0]) && uncnstr(args[num - 1])) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc) {
|
|
add_def(args[num - 1], m.mk_app(a.get_family_id(), OP_SELECT, num - 1, args));
|
|
add_def(args[0], r);
|
|
}
|
|
return true;
|
|
}
|
|
return false;
|
|
default:
|
|
return false;
|
|
}
|
|
}
|
|
|
|
bool mk_diff(expr* t, expr_ref& r) override {
|
|
sort* s = t->get_sort();
|
|
SASSERT(a.is_array(s));
|
|
if (m.is_uninterp(get_array_range(s)))
|
|
return false;
|
|
unsigned arity = get_array_arity(s);
|
|
for (unsigned i = 0; i < arity; i++)
|
|
if (m.is_uninterp(get_array_domain(s, i)))
|
|
return false;
|
|
// building
|
|
// r = (store t i1 ... in d)
|
|
// where i1 ... in are arbitrary values
|
|
// and d is a term different from (select t i1 ... in)
|
|
expr_ref_vector new_args(m);
|
|
new_args.push_back(t);
|
|
for (unsigned i = 0; i < arity; i++)
|
|
new_args.push_back(m.get_some_value(get_array_domain(s, i)));
|
|
expr_ref sel(m);
|
|
sel = a.mk_select(new_args);
|
|
expr_ref diff_sel(m);
|
|
if (!inv.mk_diff(sel, diff_sel))
|
|
return false;
|
|
new_args.push_back(diff_sel);
|
|
r = a.mk_store(new_args);
|
|
return true;
|
|
}
|
|
};
|
|
|
|
|
|
|
|
class dt_expr_inverter : public iexpr_inverter {
|
|
datatype_util dt;
|
|
public:
|
|
|
|
dt_expr_inverter(ast_manager& m) : iexpr_inverter(m), dt(m) {}
|
|
|
|
family_id get_fid() const override { return dt.get_family_id(); }
|
|
/**
|
|
* head(x) -> fresh
|
|
* x := cons(fresh, arb)
|
|
*/
|
|
bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
|
|
if (dt.is_accessor(f)) {
|
|
SASSERT(num == 1);
|
|
if (uncnstr(args[0])) {
|
|
if (!m_mc) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
return true;
|
|
}
|
|
func_decl* c = dt.get_accessor_constructor(f);
|
|
for (unsigned i = 0; i < c->get_arity(); i++)
|
|
if (!m.is_fully_interp(c->get_domain(i)))
|
|
return false;
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
ptr_vector<func_decl> const& accs = *dt.get_constructor_accessors(c);
|
|
ptr_buffer<expr> new_args;
|
|
for (unsigned i = 0; i < accs.size(); i++) {
|
|
if (accs[i] == f)
|
|
new_args.push_back(r);
|
|
else
|
|
new_args.push_back(m.get_some_value(c->get_domain(i)));
|
|
}
|
|
add_def(args[0], m.mk_app(c, new_args));
|
|
return true;
|
|
}
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool mk_diff(expr* t, expr_ref& r) override {
|
|
// In the current implementation, I only handle the case where
|
|
// the datatype has a recursive constructor.
|
|
sort* s = t->get_sort();
|
|
ptr_vector<func_decl> const& constructors = *dt.get_datatype_constructors(s);
|
|
for (func_decl* constructor : constructors) {
|
|
unsigned num = constructor->get_arity();
|
|
unsigned target = UINT_MAX;
|
|
for (unsigned i = 0; i < num; i++) {
|
|
sort* s_arg = constructor->get_domain(i);
|
|
if (s == s_arg) {
|
|
target = i;
|
|
continue;
|
|
}
|
|
if (m.is_uninterp(s_arg))
|
|
break;
|
|
}
|
|
if (target == UINT_MAX)
|
|
continue;
|
|
// use the constructor the distinct term constructor(...,t,...)
|
|
ptr_buffer<expr> new_args;
|
|
for (unsigned i = 0; i < num; i++) {
|
|
if (i == target)
|
|
new_args.push_back(t);
|
|
else
|
|
new_args.push_back(m.get_some_value(constructor->get_domain(i)));
|
|
}
|
|
r = m.mk_app(constructor, new_args);
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
};
|
|
|
|
#if 0
|
|
class pb_expr_inverter : public iexpr_inverter {
|
|
pb_util pb;
|
|
public:
|
|
pb_expr_inverter(ast_manager& m) : iexpr_inverter(m), pb(m) {}
|
|
|
|
family_id get_fid() const override { return pb.get_family_id(); }
|
|
|
|
bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
|
|
rational k, c;
|
|
unsigned new_k = 0;
|
|
expr_ref_vector new_args(m), uncnstr_args(m);
|
|
vector<rational> coeffs;
|
|
switch (f->get_decl_kind()) {
|
|
case OP_AT_MOST_K:
|
|
// a' + b' + c + d <= 3 -> r := c + d <= 1
|
|
// a' + b' + c + d <= 1 -> r := c + d <= 1
|
|
// a' + b' + c' + d <= 2 -> r := fresh
|
|
// a', b', c' := ~r
|
|
k = pb.get_k(f);
|
|
if (!k.is_unsigned())
|
|
return false;
|
|
for (unsigned i = 0; i < num; ++i)
|
|
if (uncnstr(args[i]))
|
|
uncnstr_args.push_back(args[i]);
|
|
else
|
|
new_args.push_back(args[i]);
|
|
if (uncnstr_args.empty())
|
|
return false;
|
|
if (new_args.size() <= k && uncnstr_args.size() > k)
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
else if (new_args.size() <= k) // k >= uncnstr_args.size()
|
|
r = pb.mk_at_most_k(new_args, k.get_unsigned() - uncnstr_args.size());
|
|
else // |new_args| > k
|
|
r = pb.mk_at_most_k(new_args, k.get_unsigned());
|
|
if (m_mc) {
|
|
for (unsigned i = 0; i < uncnstr_args.size(); ++i)
|
|
add_def(uncnstr_args.get(i), m.mk_not(r));
|
|
}
|
|
return true;
|
|
case OP_AT_LEAST_K:
|
|
k = pb.get_k(f);
|
|
if (!k.is_unsigned())
|
|
return false;
|
|
for (unsigned i = 0; i < num; ++i)
|
|
if (uncnstr(args[i]))
|
|
uncnstr_args.push_back(args[i]);
|
|
else
|
|
new_args.push_back(args[i]);
|
|
if (uncnstr_args.empty())
|
|
return false;
|
|
// cases k <= uncstr_args.size()
|
|
// k > uncstr_args.size()
|
|
return false;
|
|
case OP_PB_LE:
|
|
// 2*x + 3*y + z + 2*u <= k -> r
|
|
// r := z + 2u <=
|
|
//
|
|
k = pb.get_k(f);
|
|
for (unsigned i = 0; i < num; ++i)
|
|
if (uncnstr(args[i]))
|
|
uncnstr_args.push_back(args[i]), c += pb.get_coeff(f, i);
|
|
else
|
|
new_args.push_back(args[i]), coeffs.push_back(pb.get_coeff(f, i));
|
|
if (uncnstr_args.empty())
|
|
return false;
|
|
return false;
|
|
default:
|
|
return false;
|
|
}
|
|
}
|
|
|
|
bool mk_diff(expr* t, expr_ref& r) override {
|
|
return false;
|
|
}
|
|
};
|
|
#endif
|
|
|
|
class finite_set_inverter : public iexpr_inverter {
|
|
finite_set_util fs;
|
|
public:
|
|
finite_set_inverter(ast_manager& m): iexpr_inverter(m), fs(m) {}
|
|
|
|
bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
|
|
switch (f->get_decl_kind()) {
|
|
case OP_FINITE_SET_UNION:
|
|
// x union y -> fresh
|
|
// x := fresh, y := empty
|
|
if (num == 2 && uncnstr(args[0]) && uncnstr(args[1])) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc) {
|
|
add_def(args[0], r);
|
|
add_def(args[1], fs.mk_empty(args[1]->get_sort()));
|
|
}
|
|
return true;
|
|
}
|
|
return false;
|
|
default:
|
|
break;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool mk_diff(expr* t, expr_ref& r) override {
|
|
return false;
|
|
}
|
|
};
|
|
|
|
class seq_expr_inverter : public iexpr_inverter {
|
|
seq_util seq;
|
|
seq_rewriter rw;
|
|
public:
|
|
seq_expr_inverter(ast_manager& m) : iexpr_inverter(m), seq(m), rw(m) {}
|
|
|
|
family_id get_fid() const override { return seq.get_family_id(); }
|
|
|
|
bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
|
|
switch (f->get_decl_kind()) {
|
|
case _OP_STRING_CONCAT:
|
|
case OP_SEQ_CONCAT: {
|
|
expr* x, *y;
|
|
|
|
if (uncnstr(args[0]) && num == 2 &&
|
|
args[1]->get_ref_count() == 1 &&
|
|
seq.str.is_concat(args[1], x, y) &&
|
|
uncnstr(x)) {
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc) {
|
|
add_def(args[0], seq.str.mk_empty(args[0]->get_sort()));
|
|
add_def(x, r);
|
|
}
|
|
r = seq.str.mk_concat(r, y);
|
|
return true;
|
|
}
|
|
|
|
if (!uncnstr(num, args))
|
|
return false;
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc) {
|
|
add_def(args[0], r);
|
|
for (unsigned i = 1; i < num; ++i)
|
|
add_def(args[i], seq.str.mk_empty(args[0]->get_sort()));
|
|
}
|
|
return true;
|
|
}
|
|
case OP_SEQ_CONTAINS:
|
|
if (uncnstr(args[0])) {
|
|
// x contains y -> r or y is empty
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
expr_ref emp(seq.str.mk_is_empty(args[0]), m);
|
|
if (m_mc)
|
|
add_def(args[0], m.mk_ite(r, args[1], seq.str.mk_empty(args[0]->get_sort())));
|
|
r = m.mk_or(r, emp);
|
|
return true;
|
|
}
|
|
if (uncnstr(args[1]) && seq.is_string(args[0]->get_sort())) {
|
|
// x contains y -> r
|
|
// y -> if r then x else x + x + a
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
if (m_mc)
|
|
add_def(args[1], m.mk_ite(r, args[0], seq.str.mk_concat(args[0], args[0], seq.str.mk_string(zstring("a")))));
|
|
return true;
|
|
}
|
|
return false;
|
|
case OP_SEQ_IN_RE:
|
|
if (uncnstr(args[0]) && seq.re.is_ground(args[1]) && seq.is_string(args[0]->get_sort())) {
|
|
zstring s1;
|
|
expr* re = args[1];
|
|
if (l_true != rw.some_string_in_re(re, s1))
|
|
return false;
|
|
zstring s2;
|
|
expr_ref not_re(seq.re.mk_complement(re), m);
|
|
if (l_true != rw.some_string_in_re(not_re, s2))
|
|
return false;
|
|
|
|
mk_fresh_uncnstr_var_for(f, r);
|
|
expr_ref witness1 = expr_ref(seq.str.mk_string(s1), m);
|
|
expr_ref witness2 = expr_ref(seq.str.mk_string(s2), m);
|
|
if (m_mc)
|
|
add_def(args[0], m.mk_ite(r, witness1, witness2));
|
|
return true;
|
|
}
|
|
return false;
|
|
default:
|
|
verbose_stream() << mk_pp(f, m) << "\n";
|
|
return false;
|
|
|
|
}
|
|
}
|
|
|
|
bool mk_diff(expr* t, expr_ref& r) override {
|
|
if (seq.is_string(t->get_sort())) {
|
|
r = seq.str.mk_concat(t, seq.str.mk_string(zstring("a")));
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
};
|
|
|
|
|
|
expr_inverter::~expr_inverter() {
|
|
for (auto* v : m_inverters)
|
|
dealloc(v);
|
|
}
|
|
|
|
|
|
bool iexpr_inverter::uncnstr(unsigned num, expr * const * args) const {
|
|
for (unsigned i = 0; i < num; i++)
|
|
if (!m_is_var(args[i]))
|
|
return false;
|
|
return true;
|
|
}
|
|
|
|
/**
|
|
\brief Create a fresh variable for abstracting (f args[0] ... args[num-1])
|
|
Return true if a new variable was created, and false if the variable already existed for this
|
|
application. Store the variable in v
|
|
*/
|
|
void iexpr_inverter::mk_fresh_uncnstr_var_for(sort * s, expr_ref & v) {
|
|
v = m.mk_fresh_const(nullptr, s);
|
|
if (m_mc)
|
|
m_mc->hide(v);
|
|
}
|
|
|
|
void iexpr_inverter::add_def(expr * v, expr * def) {
|
|
expr_ref _v(v, m);
|
|
expr_ref _d(def, m);
|
|
if (!m_mc)
|
|
return;
|
|
SASSERT(uncnstr(v));
|
|
SASSERT(to_app(v)->get_num_args() == 0);
|
|
m_mc->add(v, def);
|
|
}
|
|
|
|
void iexpr_inverter::add_defs(unsigned num, expr* const* args, expr* u, expr* identity) {
|
|
expr_ref _id(identity, m);
|
|
if (!m_mc)
|
|
return;
|
|
add_def(args[0], u);
|
|
for (unsigned i = 1; i < num; i++)
|
|
add_def(args[i], identity);
|
|
}
|
|
|
|
|
|
expr_inverter::expr_inverter(ast_manager& m): iexpr_inverter(m) {
|
|
auto add = [&](iexpr_inverter* i) {
|
|
m_inverters.setx(i->get_fid(), i, nullptr);
|
|
};
|
|
add(alloc(arith_expr_inverter, m));
|
|
add(alloc(bv_expr_inverter, m));
|
|
add(alloc(array_expr_inverter, m, *this));
|
|
add(alloc(dt_expr_inverter, m));
|
|
add(alloc(basic_expr_inverter, m, *this));
|
|
add(alloc(seq_expr_inverter, m));
|
|
//add(alloc(pb_expr_inverter, m));
|
|
}
|
|
|
|
|
|
bool expr_inverter::operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& new_expr) {
|
|
if (num == 0)
|
|
return false;
|
|
|
|
for (unsigned i = 0; i < num; i++)
|
|
if (!is_ground(args[i]))
|
|
return false;
|
|
|
|
family_id fid = f->get_family_id();
|
|
if (fid == null_family_id)
|
|
return false;
|
|
|
|
auto* p = m_inverters.get(fid, nullptr);
|
|
return p && (*p)(f, num, args, new_expr);
|
|
}
|
|
|
|
bool expr_inverter::mk_diff(expr* t, expr_ref& r) {
|
|
sort * s = t->get_sort();
|
|
if (!m.is_fully_interp(s))
|
|
return false;
|
|
|
|
// If the interpreted sort has only one element,
|
|
// then it is unsound to eliminate the unconstrained variable in the equality
|
|
sort_size sz = s->get_num_elements();
|
|
if (sz.is_finite() && sz.size() <= 1)
|
|
return false;
|
|
|
|
if (!m_mc) {
|
|
// easy case, model generation is disabled.
|
|
mk_fresh_uncnstr_var_for(s, r);
|
|
return true;
|
|
}
|
|
|
|
family_id fid = s->get_family_id();
|
|
auto* p = m_inverters.get(fid, nullptr);
|
|
return p && p->mk_diff(t, r);
|
|
}
|
|
|
|
void expr_inverter::set_is_var(std::function<bool(expr*)>& is_var) {
|
|
for (auto* p : m_inverters)
|
|
if (p)
|
|
p->set_is_var(is_var);
|
|
}
|
|
|
|
void expr_inverter::set_model_converter(generic_model_converter* mc) {
|
|
m_mc = mc;
|
|
for (auto* p : m_inverters)
|
|
if (p)
|
|
p->set_model_converter(mc);
|
|
}
|
|
|
|
void expr_inverter::set_produce_proofs(bool pr) {
|
|
m_produce_proofs = pr;
|
|
for (auto* p : m_inverters)
|
|
if (p)
|
|
p->set_produce_proofs(pr);
|
|
}
|