mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
54bb33615e
|
@ -90,7 +90,7 @@ FPMATH="Default"
|
|||
FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
|
||||
|
||||
def check_output(cmd):
|
||||
return (subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).decode("utf-8").rstrip('\r\n')
|
||||
return (subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).decode(sys.stdout.encoding).rstrip('\r\n')
|
||||
|
||||
def git_hash():
|
||||
try:
|
||||
|
|
|
@ -96,7 +96,7 @@ if sys.version < '3':
|
|||
return s
|
||||
else:
|
||||
def _to_pystr(s):
|
||||
return s.decode('utf-8')
|
||||
return s.decode(sys.stdout.encoding)
|
||||
|
||||
def init(PATH):
|
||||
global _lib
|
||||
|
|
|
@ -23,6 +23,8 @@ Revision History:
|
|||
#include"api_context.h"
|
||||
#include"api_model.h"
|
||||
#include"cancel_eh.h"
|
||||
#include"scoped_timer.h"
|
||||
#include"rlimit.h"
|
||||
|
||||
extern "C" {
|
||||
|
||||
|
@ -34,7 +36,7 @@ extern "C" {
|
|||
mk_c(c)->push();
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
|
||||
void Z3_API Z3_pop(Z3_context c, unsigned num_scopes) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_pop(c, num_scopes);
|
||||
|
@ -62,7 +64,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_assert_cnstr(c, a);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_FORMULA(a,);
|
||||
CHECK_FORMULA(a,);
|
||||
mk_c(c)->assert_cnstr(to_expr(a));
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
@ -75,17 +77,22 @@ extern "C" {
|
|||
cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
|
||||
api::context::set_interruptable si(*(mk_c(c)), eh);
|
||||
flet<bool> _model(mk_c(c)->fparams().m_model, true);
|
||||
unsigned timeout = mk_c(c)->params().m_timeout;
|
||||
unsigned rlimit = mk_c(c)->params().m_rlimit;
|
||||
lbool result;
|
||||
try {
|
||||
scoped_timer timer(timeout, &eh);
|
||||
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
|
||||
|
||||
model_ref _m;
|
||||
result = mk_c(c)->check(_m);
|
||||
if (m) {
|
||||
if (_m) {
|
||||
Z3_model_ref * m_ref = alloc(Z3_model_ref);
|
||||
Z3_model_ref * m_ref = alloc(Z3_model_ref);
|
||||
m_ref->m_model = _m;
|
||||
// Must bump reference counter for backward compatibility reasons.
|
||||
// Don't need to invoke save_object, since the counter was bumped
|
||||
m_ref->inc_ref();
|
||||
m_ref->inc_ref();
|
||||
*m = of_model(m_ref);
|
||||
}
|
||||
else {
|
||||
|
@ -100,21 +107,21 @@ extern "C" {
|
|||
RETURN_Z3_check_and_get_model static_cast<Z3_lbool>(result);
|
||||
Z3_CATCH_RETURN(Z3_L_UNDEF);
|
||||
}
|
||||
|
||||
|
||||
Z3_lbool Z3_API Z3_check(Z3_context c) {
|
||||
Z3_TRY;
|
||||
// This is just syntax sugar...
|
||||
RESET_ERROR_CODE();
|
||||
// This is just syntax sugar...
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_SEARCHING(c);
|
||||
Z3_lbool r = Z3_check_and_get_model(c, 0);
|
||||
return r;
|
||||
Z3_CATCH_RETURN(Z3_L_UNDEF);
|
||||
}
|
||||
|
||||
|
||||
Z3_lbool Z3_API Z3_check_assumptions(Z3_context c,
|
||||
unsigned num_assumptions, Z3_ast const assumptions[],
|
||||
Z3_model * m, Z3_ast* proof,
|
||||
|
||||
Z3_lbool Z3_API Z3_check_assumptions(Z3_context c,
|
||||
unsigned num_assumptions, Z3_ast const assumptions[],
|
||||
Z3_model * m, Z3_ast* proof,
|
||||
unsigned* core_size, Z3_ast core[]) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_check_assumptions(c, num_assumptions, assumptions, m, proof, core_size, core);
|
||||
|
@ -130,11 +137,11 @@ extern "C" {
|
|||
model_ref _m;
|
||||
mk_c(c)->get_smt_kernel().get_model(_m);
|
||||
if (_m) {
|
||||
Z3_model_ref * m_ref = alloc(Z3_model_ref);
|
||||
Z3_model_ref * m_ref = alloc(Z3_model_ref);
|
||||
m_ref->m_model = _m;
|
||||
// Must bump reference counter for backward compatibility reasons.
|
||||
// Don't need to invoke save_object, since the counter was bumped
|
||||
m_ref->inc_ref();
|
||||
m_ref->inc_ref();
|
||||
*m = of_model(m_ref);
|
||||
}
|
||||
else {
|
||||
|
@ -159,7 +166,7 @@ extern "C" {
|
|||
else if (proof) {
|
||||
*proof = 0; // breaks abstraction.
|
||||
}
|
||||
RETURN_Z3_check_assumptions static_cast<Z3_lbool>(result);
|
||||
RETURN_Z3_check_assumptions static_cast<Z3_lbool>(result);
|
||||
Z3_CATCH_RETURN(Z3_L_UNDEF);
|
||||
}
|
||||
|
||||
|
@ -185,7 +192,7 @@ extern "C" {
|
|||
symbol const& get_label() const { return m_label; }
|
||||
expr* get_literal() { return m_literal.get(); }
|
||||
};
|
||||
|
||||
|
||||
typedef vector<labeled_literal> labels;
|
||||
|
||||
Z3_literals Z3_API Z3_get_relevant_labels(Z3_context c) {
|
||||
|
@ -196,7 +203,7 @@ extern "C" {
|
|||
ast_manager& m = mk_c(c)->m();
|
||||
expr_ref_vector lits(m);
|
||||
mk_c(c)->get_smt_kernel().get_relevant_labels(0, labl_syms);
|
||||
mk_c(c)->get_smt_kernel().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits);
|
||||
mk_c(c)->get_smt_kernel().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits);
|
||||
labels* lbls = alloc(labels);
|
||||
SASSERT(labl_syms.size() == lits.size());
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
|
@ -212,12 +219,12 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
expr_ref_vector lits(m);
|
||||
mk_c(c)->get_smt_kernel().get_relevant_literals(lits);
|
||||
mk_c(c)->get_smt_kernel().get_relevant_literals(lits);
|
||||
labels* lbls = alloc(labels);
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
lbls->push_back(labeled_literal(m,lits[i].get()));
|
||||
}
|
||||
RETURN_Z3(reinterpret_cast<Z3_literals>(lbls));
|
||||
RETURN_Z3(reinterpret_cast<Z3_literals>(lbls));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -227,12 +234,12 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
expr_ref_vector lits(m);
|
||||
mk_c(c)->get_smt_kernel().get_guessed_literals(lits);
|
||||
mk_c(c)->get_smt_kernel().get_guessed_literals(lits);
|
||||
labels* lbls = alloc(labels);
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
lbls->push_back(labeled_literal(m,lits[i].get()));
|
||||
}
|
||||
RETURN_Z3(reinterpret_cast<Z3_literals>(lbls));
|
||||
RETURN_Z3(reinterpret_cast<Z3_literals>(lbls));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -248,7 +255,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_get_num_literals(c, lbls);
|
||||
RESET_ERROR_CODE();
|
||||
return reinterpret_cast<labels*>(lbls)->size();
|
||||
return reinterpret_cast<labels*>(lbls)->size();
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -256,7 +263,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_get_label_symbol(c, lbls, idx);
|
||||
RESET_ERROR_CODE();
|
||||
return of_symbol((*reinterpret_cast<labels*>(lbls))[idx].get_label());
|
||||
return of_symbol((*reinterpret_cast<labels*>(lbls))[idx].get_label());
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -274,7 +281,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_disable_literal(c, lbls, idx);
|
||||
RESET_ERROR_CODE();
|
||||
(*reinterpret_cast<labels*>(lbls))[idx].disable();
|
||||
(*reinterpret_cast<labels*>(lbls))[idx].disable();
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
|
@ -348,4 +355,4 @@ void Z3_display_statistics(Z3_context c, std::ostream& s) {
|
|||
void Z3_display_istatistics(Z3_context c, std::ostream& s) {
|
||||
mk_c(c)->get_smt_kernel().display_istatistics(s);
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -22,7 +22,7 @@ Revision History:
|
|||
#include"ast.h"
|
||||
|
||||
|
||||
inline sort* get_array_range(sort const * s) {
|
||||
inline sort* get_array_range(sort const * s) {
|
||||
return to_sort(s->get_parameter(s->get_num_parameters() - 1).get_ast());
|
||||
}
|
||||
|
||||
|
@ -104,20 +104,20 @@ class array_decl_plugin : public decl_plugin {
|
|||
}
|
||||
|
||||
//
|
||||
// Contract for sort:
|
||||
// parameters[0] - 1st dimension
|
||||
// Contract for sort:
|
||||
// parameters[0] - 1st dimension
|
||||
// ...
|
||||
// parameters[n-1] - nth dimension
|
||||
// parameters[n] - range
|
||||
//
|
||||
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
|
||||
|
||||
|
||||
//
|
||||
// Contract for func_decl:
|
||||
// parameters[0] - array sort
|
||||
// Contract for others:
|
||||
// no parameters
|
||||
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range);
|
||||
|
||||
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
|
||||
|
@ -184,6 +184,11 @@ public:
|
|||
sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); }
|
||||
|
||||
sort * mk_array_sort(unsigned arity, sort* const* domain, sort* range);
|
||||
|
||||
app * mk_as_array(sort * s, func_decl * f) {
|
||||
parameter param(f);
|
||||
return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, ¶m, 0, 0, s);
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
|
|
|
@ -2648,9 +2648,8 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
|
|||
|
||||
SASSERT(num == 2);
|
||||
SASSERT(m_util.is_float(f->get_range()));
|
||||
SASSERT(m_bv_util.is_bv(args[0]));
|
||||
SASSERT(m_bv_util.is_bv(args[1]));
|
||||
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
|
||||
SASSERT(m_bv_util.is_bv(args[1]));
|
||||
|
||||
expr_ref bv_rm(m), x(m);
|
||||
bv_rm = to_app(args[0])->get_arg(0);
|
||||
|
|
|
@ -84,7 +84,7 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg
|
|||
ptr_buffer<expr> buffer;
|
||||
expr_fast_mark1 neg_lits;
|
||||
expr_fast_mark2 pos_lits;
|
||||
|
||||
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
expr * arg = args[i];
|
||||
if (m().is_true(arg)) {
|
||||
|
@ -120,9 +120,9 @@ br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * arg
|
|||
}
|
||||
buffer.push_back(arg);
|
||||
}
|
||||
|
||||
|
||||
unsigned sz = buffer.size();
|
||||
|
||||
|
||||
switch(sz) {
|
||||
case 0:
|
||||
result = m().mk_true();
|
||||
|
@ -208,9 +208,9 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
|
|||
}
|
||||
buffer.push_back(arg);
|
||||
}
|
||||
|
||||
|
||||
unsigned sz = buffer.size();
|
||||
|
||||
|
||||
switch(sz) {
|
||||
case 0:
|
||||
result = m().mk_false();
|
||||
|
@ -222,7 +222,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
|
|||
if (m_local_ctx && m_local_ctx_cost <= m_local_ctx_limit) {
|
||||
neg_lits.reset();
|
||||
pos_lits.reset();
|
||||
if (local_ctx_simp(sz, buffer.c_ptr(), result))
|
||||
if (local_ctx_simp(sz, buffer.c_ptr(), result))
|
||||
return BR_DONE;
|
||||
}
|
||||
if (s) {
|
||||
|
@ -273,11 +273,11 @@ expr * bool_rewriter::mk_or_app(unsigned num_args, expr * const * args) {
|
|||
|
||||
/**
|
||||
\brief Auxiliary method for local_ctx_simp.
|
||||
|
||||
|
||||
Replace args[i] by true if marked in neg_lits.
|
||||
Replace args[i] by false if marked in pos_lits.
|
||||
*/
|
||||
bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args,
|
||||
bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args,
|
||||
expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result) {
|
||||
ptr_buffer<expr> new_args;
|
||||
bool simp = false;
|
||||
|
@ -307,13 +307,13 @@ bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args,
|
|||
}
|
||||
if (simp) {
|
||||
switch(new_args.size()) {
|
||||
case 0:
|
||||
result = m().mk_true();
|
||||
case 0:
|
||||
result = m().mk_true();
|
||||
return true;
|
||||
case 1:
|
||||
mk_not(new_args[0], result);
|
||||
case 1:
|
||||
mk_not(new_args[0], result);
|
||||
return true;
|
||||
default:
|
||||
default:
|
||||
result = m().mk_not(m().mk_or(new_args.size(), new_args.c_ptr()));
|
||||
return true;
|
||||
}
|
||||
|
@ -358,7 +358,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul
|
|||
result = t;
|
||||
return;
|
||||
}
|
||||
|
||||
|
||||
if (m().is_false(c)) {
|
||||
result = e;
|
||||
return;
|
||||
|
@ -368,7 +368,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul
|
|||
result = t;
|
||||
return;
|
||||
}
|
||||
|
||||
|
||||
if (m().is_bool(t)) {
|
||||
if (m().is_true(t)) {
|
||||
if (m().is_false(e)) {
|
||||
|
@ -384,13 +384,13 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul
|
|||
return;
|
||||
}
|
||||
expr_ref tmp(m());
|
||||
mk_not(e, tmp);
|
||||
mk_not(e, tmp);
|
||||
result = m().mk_not(m().mk_or(c, tmp));
|
||||
return;
|
||||
}
|
||||
if (m().is_true(e)) {
|
||||
expr_ref tmp(m());
|
||||
mk_not(c, tmp);
|
||||
mk_not(c, tmp);
|
||||
result = m().mk_or(tmp, t);
|
||||
return;
|
||||
}
|
||||
|
@ -406,7 +406,7 @@ void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & resul
|
|||
result = m().mk_or(c, e);
|
||||
return;
|
||||
}
|
||||
if (m().is_complement_core(t, e)) { // t = not(e)
|
||||
if (m().is_complement_core(t, e)) { // t = not(e)
|
||||
mk_eq(c, t, result);
|
||||
return;
|
||||
}
|
||||
|
@ -443,8 +443,8 @@ bool bool_rewriter::simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, exp
|
|||
expr * new_e = simp_arg(to_app(t)->get_arg(2), neg_lits, pos_lits, modified);
|
||||
if (!modified)
|
||||
return false;
|
||||
// It is not safe to invoke mk_ite here, since it can recursively call
|
||||
// local_ctx_simp by
|
||||
// It is not safe to invoke mk_ite here, since it can recursively call
|
||||
// local_ctx_simp by
|
||||
// - transforming the ITE into an OR
|
||||
// - and invoked mk_or, that will invoke local_ctx_simp
|
||||
// mk_ite(new_c, new_t, new_e, result);
|
||||
|
@ -522,7 +522,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
|
|||
PUSH_NEW_ARG(arg); \
|
||||
} \
|
||||
}
|
||||
|
||||
|
||||
m_local_ctx_cost += 2*num_args;
|
||||
#if 0
|
||||
static unsigned counter = 0;
|
||||
|
@ -567,9 +567,9 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
|
|||
|
||||
/**
|
||||
\brief Apply simplification if ite is an if-then-else tree where every leaf is a value.
|
||||
|
||||
This is an efficient way to
|
||||
|
||||
|
||||
This is an efficient way to
|
||||
|
||||
*/
|
||||
br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) {
|
||||
SASSERT(m().is_ite(ite));
|
||||
|
@ -585,7 +585,7 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
|
|||
tout << t << " " << e << " " << val << "\n";);
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
|
||||
if (t == val && e == val) {
|
||||
result = m().mk_true();
|
||||
|
@ -598,7 +598,7 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
|
|||
}
|
||||
|
||||
SASSERT(e == val);
|
||||
|
||||
|
||||
mk_not(ite->get_arg(0), result);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
@ -642,14 +642,14 @@ static bool is_ite_value_tree_neq_value(ast_manager & m, app * ite, app * val) {
|
|||
|
||||
return true;
|
||||
}
|
||||
#endif
|
||||
#endif
|
||||
|
||||
br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
|
||||
if (lhs == rhs) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
if (m().are_distinct(lhs, rhs)) {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
|
@ -662,7 +662,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
// return BR_DONE;
|
||||
// }
|
||||
r = try_ite_value(to_app(lhs), to_app(rhs), result);
|
||||
CTRACE("try_ite_value", r != BR_FAILED,
|
||||
CTRACE("try_ite_value", r != BR_FAILED,
|
||||
tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";);
|
||||
}
|
||||
else if (m().is_ite(rhs) && m().is_value(lhs)) {
|
||||
|
@ -671,7 +671,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
// return BR_DONE;
|
||||
// }
|
||||
r = try_ite_value(to_app(rhs), to_app(lhs), result);
|
||||
CTRACE("try_ite_value", r != BR_FAILED,
|
||||
CTRACE("try_ite_value", r != BR_FAILED,
|
||||
tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";);
|
||||
}
|
||||
if (r != BR_FAILED)
|
||||
|
@ -708,6 +708,19 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
result = m().mk_eq(lhs, rhs);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
expr *la, *lb, *ra, *rb;
|
||||
// fold (iff (iff a b) (iff (not a) b)) to false
|
||||
if (m().is_iff(lhs, la, lb) && m().is_iff(rhs, ra, rb)) {
|
||||
expr *n;
|
||||
if ((la == ra && ((m().is_not(rb, n) && n == lb) ||
|
||||
(m().is_not(lb, n) && n == rb))) ||
|
||||
(lb == rb && ((m().is_not(ra, n) && n == la) ||
|
||||
(m().is_not(la, n) && n == ra)))) {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
@ -756,13 +769,13 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
|
|||
result = m().mk_and(new_diseqs.size(), new_diseqs.c_ptr());
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result) {
|
||||
bool s = false;
|
||||
|
||||
|
||||
// (ite (not c) a b) ==> (ite c b a)
|
||||
if (m().is_not(c)) {
|
||||
c = to_app(c)->get_arg(0);
|
||||
|
@ -788,7 +801,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
|
|||
result = t;
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
if (m().is_false(c)) {
|
||||
result = e;
|
||||
return BR_DONE;
|
||||
|
@ -814,18 +827,18 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
|
|||
return BR_DONE;
|
||||
}
|
||||
expr_ref tmp(m());
|
||||
mk_not(c, tmp);
|
||||
mk_not(c, tmp);
|
||||
mk_and(tmp, e, result);
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m().is_true(e)) {
|
||||
expr_ref tmp(m());
|
||||
mk_not(c, tmp);
|
||||
mk_not(c, tmp);
|
||||
mk_or(tmp, t, result);
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m().is_false(e)) {
|
||||
mk_and(c, t, result);
|
||||
mk_and(c, t, result);
|
||||
return BR_DONE;
|
||||
}
|
||||
if (c == e) {
|
||||
|
@ -833,10 +846,10 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
|
|||
return BR_DONE;
|
||||
}
|
||||
if (c == t) {
|
||||
mk_or(c, e, result);
|
||||
mk_or(c, e, result);
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m().is_complement_core(t, e)) { // t = not(e)
|
||||
if (m().is_complement_core(t, e)) { // t = not(e)
|
||||
mk_eq(c, t, result);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
@ -863,10 +876,10 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
|
|||
result = m().mk_ite(new_c, to_app(t)->get_arg(1), e);
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
|
||||
|
||||
if (m().is_ite(e)) {
|
||||
// (ite c1 (ite c2 t1 t2) (ite c3 t1 t2)) ==> (ite (or (and c1 c2) (and (not c1) c3)) t1 t2)
|
||||
if (to_app(t)->get_arg(1) == to_app(e)->get_arg(1) &&
|
||||
if (to_app(t)->get_arg(1) == to_app(e)->get_arg(1) &&
|
||||
to_app(t)->get_arg(2) == to_app(e)->get_arg(2)) {
|
||||
expr_ref and1(m());
|
||||
expr_ref and2(m());
|
||||
|
@ -879,9 +892,9 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
|
|||
result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2));
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
|
||||
|
||||
// (ite c1 (ite c2 t1 t2) (ite c3 t2 t1)) ==> (ite (or (and c1 c2) (and (not c1) (not c3))) t1 t2)
|
||||
if (to_app(t)->get_arg(1) == to_app(e)->get_arg(2) &&
|
||||
if (to_app(t)->get_arg(1) == to_app(e)->get_arg(2) &&
|
||||
to_app(t)->get_arg(2) == to_app(e)->get_arg(1)) {
|
||||
expr_ref and1(m());
|
||||
expr_ref and2(m());
|
||||
|
@ -922,10 +935,10 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
|
|||
result = m().mk_ite(c, t, e);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
||||
br_status bool_rewriter::mk_not_core(expr * t, expr_ref & result) {
|
||||
if (m().is_not(t)) {
|
||||
result = to_app(t)->get_arg(0);
|
||||
|
|
377
src/tactic/bv/bvarray2uf_rewriter.cpp
Normal file
377
src/tactic/bv/bvarray2uf_rewriter.cpp
Normal file
|
@ -0,0 +1,377 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
bvarray2uf_rewriter.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Rewriter that rewrites bit-vector arrays into bit-vector
|
||||
(uninterpreted) functions.
|
||||
|
||||
Author:
|
||||
|
||||
Christoph (cwinter) 2015-11-04
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
|
||||
#include"cooperate.h"
|
||||
#include"bv_decl_plugin.h"
|
||||
#include"array_decl_plugin.h"
|
||||
#include"params.h"
|
||||
#include"ast_pp.h"
|
||||
#include"bvarray2uf_rewriter.h"
|
||||
|
||||
// [1] C. M. Wintersteiger, Y. Hamadi, and L. de Moura: Efficiently Solving
|
||||
// Quantified Bit-Vector Formulas, in Formal Methods in System Design,
|
||||
// vol. 42, no. 1, pp. 3-23, Springer, 2013.
|
||||
|
||||
bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p) :
|
||||
m_manager(m),
|
||||
m_out(m),
|
||||
m_bindings(m),
|
||||
m_bv_util(m),
|
||||
m_array_util(m),
|
||||
m_emc(0),
|
||||
m_fmc(0),
|
||||
extra_assertions(m) {
|
||||
updt_params(p);
|
||||
// We need to make sure that the mananger has the BV and array plugins loaded.
|
||||
symbol s_bv("bv");
|
||||
if (!m_manager.has_plugin(s_bv))
|
||||
m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
|
||||
symbol s_array("array");
|
||||
if (!m_manager.has_plugin(s_array))
|
||||
m_manager.register_plugin(s_array, alloc(array_decl_plugin));
|
||||
}
|
||||
|
||||
bvarray2uf_rewriter_cfg::~bvarray2uf_rewriter_cfg() {
|
||||
for (obj_map<expr, func_decl*>::iterator it = m_arrays_fs.begin();
|
||||
it != m_arrays_fs.end();
|
||||
it++)
|
||||
m_manager.dec_ref(it->m_value);
|
||||
}
|
||||
|
||||
void bvarray2uf_rewriter_cfg::reset() {}
|
||||
|
||||
sort * bvarray2uf_rewriter_cfg::get_index_sort(expr * e) {
|
||||
return get_index_sort(m_manager.get_sort(e));
|
||||
}
|
||||
|
||||
sort * bvarray2uf_rewriter_cfg::get_index_sort(sort * s) {
|
||||
SASSERT(s->get_num_parameters() >= 2);
|
||||
unsigned total_width = 0;
|
||||
for (unsigned i = 0; i < s->get_num_parameters() - 1; i++) {
|
||||
parameter const & p = s->get_parameter(i);
|
||||
SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast())));
|
||||
SASSERT(m_bv_util.is_bv_sort(to_sort(p.get_ast())));
|
||||
total_width += m_bv_util.get_bv_size(to_sort(p.get_ast()));
|
||||
}
|
||||
return m_bv_util.mk_sort(total_width);
|
||||
}
|
||||
|
||||
sort * bvarray2uf_rewriter_cfg::get_value_sort(expr * e) {
|
||||
return get_value_sort(m_manager.get_sort(e));
|
||||
}
|
||||
|
||||
sort * bvarray2uf_rewriter_cfg::get_value_sort(sort * s) {
|
||||
SASSERT(s->get_num_parameters() >= 2);
|
||||
parameter const & p = s->get_parameter(s->get_num_parameters() - 1);
|
||||
SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast())));
|
||||
return to_sort(p.get_ast());
|
||||
}
|
||||
|
||||
bool bvarray2uf_rewriter_cfg::is_bv_array(expr * e) {
|
||||
return is_bv_array(m_manager.get_sort(e));
|
||||
}
|
||||
|
||||
bool bvarray2uf_rewriter_cfg::is_bv_array(sort * s) {
|
||||
if (!m_array_util.is_array(s))
|
||||
return false;
|
||||
|
||||
SASSERT(s->get_num_parameters() >= 2);
|
||||
for (unsigned i = 0; i < s->get_num_parameters(); i++) {
|
||||
parameter const & p = s->get_parameter(i);
|
||||
if (!p.is_ast() || !is_sort(to_sort(p.get_ast())) ||
|
||||
!m_bv_util.is_bv_sort(to_sort(p.get_ast())))
|
||||
return false;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
|
||||
SASSERT(is_bv_array(e));
|
||||
|
||||
if (m_array_util.is_as_array(e))
|
||||
return func_decl_ref(static_cast<func_decl*>(to_app(e)->get_decl()->get_parameter(0).get_ast()), m_manager);
|
||||
else {
|
||||
app * a = to_app(e);
|
||||
func_decl * bv_f = 0;
|
||||
if (!m_arrays_fs.find(e, bv_f)) {
|
||||
sort * domain = get_index_sort(a);
|
||||
sort * range = get_value_sort(a);
|
||||
bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range);
|
||||
if (is_uninterp_const(e)) {
|
||||
if (m_emc)
|
||||
m_emc->insert(to_app(e)->get_decl(),
|
||||
m_array_util.mk_as_array(m_manager.get_sort(e), bv_f));
|
||||
}
|
||||
else if (m_fmc)
|
||||
m_fmc->insert(bv_f);
|
||||
m_arrays_fs.insert(e, bv_f);
|
||||
m_manager.inc_ref(bv_f);
|
||||
}
|
||||
|
||||
return func_decl_ref(bv_f, m_manager);
|
||||
}
|
||||
}
|
||||
|
||||
br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
br_status res = BR_FAILED;
|
||||
|
||||
if (m_manager.is_eq(f) && is_bv_array(f->get_domain()[0])) {
|
||||
SASSERT(num == 2);
|
||||
// From [1]: Finally, we replace equations of the form t = s,
|
||||
// where t and s are arrays, with \forall x . f_t(x) = f_s(x).
|
||||
func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager);
|
||||
func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager);
|
||||
|
||||
sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) };
|
||||
symbol names[1] = { symbol("x") };
|
||||
var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
|
||||
|
||||
expr_ref body(m_manager);
|
||||
body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get()));
|
||||
|
||||
result = m_manager.mk_forall(1, sorts, names, body);
|
||||
res = BR_DONE;
|
||||
}
|
||||
else if (m_manager.is_distinct(f) && is_bv_array(f->get_domain()[0])) {
|
||||
result = m_manager.mk_distinct_expanded(num, args);
|
||||
res = BR_REWRITE1;
|
||||
}
|
||||
else if (f->get_family_id() == null_family_id) {
|
||||
TRACE("bvarray2uf_rw", tout << "UF APP: " << f->get_name() << std::endl; );
|
||||
|
||||
bool has_bv_arrays = false;
|
||||
func_decl_ref f_t(m_manager);
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
if (is_bv_array(args[i])) {
|
||||
SASSERT(m_array_util.is_as_array(args[i]));
|
||||
has_bv_arrays = true;
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref t(m_manager);
|
||||
t = m_manager.mk_app(f, num, args);
|
||||
|
||||
if (is_bv_array(t)) {
|
||||
// From [1]: For every array term t we create a fresh uninterpreted function f_t.
|
||||
f_t = mk_uf_for_array(t);
|
||||
result = m_array_util.mk_as_array(m_manager.get_sort(t), f_t);
|
||||
res = BR_DONE;
|
||||
}
|
||||
else if (has_bv_arrays) {
|
||||
result = t;
|
||||
res = BR_DONE;
|
||||
}
|
||||
else
|
||||
res = BR_FAILED;
|
||||
}
|
||||
else if (m_array_util.get_family_id() == f->get_family_id()) {
|
||||
TRACE("bvarray2uf_rw", tout << "APP: " << f->get_name() << std::endl; );
|
||||
|
||||
if (m_array_util.is_select(f)) {
|
||||
SASSERT(num == 2);
|
||||
expr * t = args[0];
|
||||
expr * i = args[1];
|
||||
TRACE("bvarray2uf_rw", tout <<
|
||||
"select; array: " << mk_ismt2_pp(t, m()) <<
|
||||
" index: " << mk_ismt2_pp(i, m()) << std::endl;);
|
||||
|
||||
if (!is_bv_array(t))
|
||||
res = BR_FAILED;
|
||||
else {
|
||||
// From [1]: Then, we replace terms of the form select(t, i) with f_t(i).
|
||||
func_decl_ref f_t(mk_uf_for_array(t), m_manager);
|
||||
result = m_manager.mk_app(f_t, i);
|
||||
res = BR_DONE;
|
||||
}
|
||||
}
|
||||
else {
|
||||
if (!is_bv_array(f->get_range()))
|
||||
res = BR_FAILED;
|
||||
else {
|
||||
if (m_array_util.is_const(f)) {
|
||||
SASSERT(num == 1);
|
||||
expr_ref t(m_manager.mk_app(f, num, args), m_manager);
|
||||
expr * v = args[0];
|
||||
func_decl_ref f_t(mk_uf_for_array(t), m_manager);
|
||||
|
||||
result = m_array_util.mk_as_array(f->get_range(), f_t);
|
||||
res = BR_DONE;
|
||||
|
||||
// Add \forall x . f_t(x) = v
|
||||
sort * sorts[1] = { get_index_sort(f->get_range()) };
|
||||
symbol names[1] = { symbol("x") };
|
||||
var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
|
||||
|
||||
expr_ref body(m_manager);
|
||||
body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), v);
|
||||
|
||||
expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
|
||||
extra_assertions.push_back(frllx);
|
||||
}
|
||||
else if (m_array_util.is_as_array(f)) {
|
||||
res = BR_FAILED;
|
||||
}
|
||||
else if (m_array_util.is_map(f)) {
|
||||
SASSERT(f->get_num_parameters() == 1);
|
||||
SASSERT(f->get_parameter(0).is_ast());
|
||||
expr_ref t(m_manager.mk_app(f, num, args), m_manager);
|
||||
func_decl_ref f_t(mk_uf_for_array(t), m_manager);
|
||||
func_decl_ref map_f(to_func_decl(f->get_parameter(0).get_ast()), m_manager);
|
||||
|
||||
func_decl_ref_vector ss(m_manager);
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
SASSERT(m_array_util.is_array(args[i]));
|
||||
func_decl_ref fd(mk_uf_for_array(args[i]), m_manager);
|
||||
ss.push_back(fd);
|
||||
}
|
||||
|
||||
// Add \forall x . f_t(x) = map_f(a[x], b[x], ...)
|
||||
sort * sorts[1] = { get_index_sort(f->get_range()) };
|
||||
symbol names[1] = { symbol("x") };
|
||||
var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
|
||||
|
||||
expr_ref_vector new_args(m_manager);
|
||||
for (unsigned i = 0; i < num; i++)
|
||||
new_args.push_back(m_manager.mk_app(ss[i].get(), x.get()));
|
||||
|
||||
expr_ref body(m_manager);
|
||||
body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()),
|
||||
m_manager.mk_app(map_f, num, new_args.c_ptr()));
|
||||
|
||||
expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
|
||||
extra_assertions.push_back(frllx);
|
||||
|
||||
result = m_array_util.mk_as_array(f->get_range(), f_t);
|
||||
res = BR_DONE;
|
||||
}
|
||||
else if (m_array_util.is_store(f)) {
|
||||
SASSERT(num == 3);
|
||||
expr * s = args[0];
|
||||
expr * i = args[1];
|
||||
expr * v = args[2];
|
||||
TRACE("bvarray2uf_rw", tout <<
|
||||
"store; array: " << mk_ismt2_pp(s, m()) <<
|
||||
" index: " << mk_ismt2_pp(i, m()) <<
|
||||
" value: " << mk_ismt2_pp(v, m()) << std::endl;);
|
||||
if (!is_bv_array(s))
|
||||
res = BR_FAILED;
|
||||
else {
|
||||
expr_ref t(m_manager.mk_app(f, num, args), m_manager);
|
||||
// From [1]: For every term t of the form store(s, i, v), we add the universal
|
||||
// formula \forall x . x = i \vee f_t(x) = f_s(x), and the ground atom f_t(i) = v.
|
||||
func_decl_ref f_s(mk_uf_for_array(s), m_manager);
|
||||
func_decl_ref f_t(mk_uf_for_array(t), m_manager);
|
||||
|
||||
result = m_array_util.mk_as_array(f->get_range(), f_t);
|
||||
res = BR_DONE;
|
||||
|
||||
sort * sorts[1] = { get_index_sort(f->get_range()) };
|
||||
symbol names[1] = { symbol("x") };
|
||||
var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
|
||||
|
||||
expr_ref body(m_manager);
|
||||
body = m_manager.mk_or(m_manager.mk_eq(x, i),
|
||||
m_manager.mk_eq(m_manager.mk_app(f_t, x.get()),
|
||||
m_manager.mk_app(f_s, x.get())));
|
||||
|
||||
expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
|
||||
extra_assertions.push_back(frllx);
|
||||
|
||||
expr_ref ground_atom(m_manager);
|
||||
ground_atom = m_manager.mk_eq(m_manager.mk_app(f_t, i), v);
|
||||
extra_assertions.push_back(ground_atom);
|
||||
TRACE("bvarray2uf_rw", tout << "ground atom: " << mk_ismt2_pp(ground_atom, m()) << std::endl; );
|
||||
}
|
||||
}
|
||||
else {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
res = BR_FAILED;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
CTRACE("bvarray2uf_rw", res==BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; );
|
||||
return res;
|
||||
}
|
||||
|
||||
bool bvarray2uf_rewriter_cfg::pre_visit(expr * t)
|
||||
{
|
||||
TRACE("bvarray2uf_rw_q", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;);
|
||||
|
||||
if (is_quantifier(t)) {
|
||||
quantifier * q = to_quantifier(t);
|
||||
TRACE("bvarray2uf_rw_q", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;);
|
||||
sort_ref_vector new_bindings(m_manager);
|
||||
for (unsigned i = 0; i < q->get_num_decls(); i++)
|
||||
new_bindings.push_back(q->get_decl_sort(i));
|
||||
SASSERT(new_bindings.size() == q->get_num_decls());
|
||||
m_bindings.append(new_bindings);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool bvarray2uf_rewriter_cfg::reduce_quantifier(quantifier * old_q,
|
||||
expr * new_body,
|
||||
expr * const * new_patterns,
|
||||
expr * const * new_no_patterns,
|
||||
expr_ref & result,
|
||||
proof_ref & result_pr) {
|
||||
unsigned curr_sz = m_bindings.size();
|
||||
SASSERT(old_q->get_num_decls() <= curr_sz);
|
||||
unsigned num_decls = old_q->get_num_decls();
|
||||
unsigned old_sz = curr_sz - num_decls;
|
||||
string_buffer<> name_buffer;
|
||||
ptr_buffer<sort> new_decl_sorts;
|
||||
sbuffer<symbol> new_decl_names;
|
||||
for (unsigned i = 0; i < num_decls; i++) {
|
||||
symbol const & n = old_q->get_decl_name(i);
|
||||
sort * s = old_q->get_decl_sort(i);
|
||||
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
||||
}
|
||||
result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(),
|
||||
new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
|
||||
old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
|
||||
result_pr = 0;
|
||||
m_bindings.shrink(old_sz);
|
||||
TRACE("bvarray2uf_rw_q", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " <<
|
||||
mk_ismt2_pp(old_q->get_expr(), m()) << std::endl <<
|
||||
" new body: " << mk_ismt2_pp(new_body, m()) << std::endl;
|
||||
tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;);
|
||||
return true;
|
||||
}
|
||||
|
||||
bool bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
|
||||
if (t->get_idx() >= m_bindings.size())
|
||||
return false;
|
||||
|
||||
expr_ref new_exp(m());
|
||||
sort * s = t->get_sort();
|
||||
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
||||
result = new_exp;
|
||||
result_pr = 0;
|
||||
TRACE("bvarray2uf_rw_q", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;);
|
||||
return true;
|
||||
}
|
87
src/tactic/bv/bvarray2uf_rewriter.h
Normal file
87
src/tactic/bv/bvarray2uf_rewriter.h
Normal file
|
@ -0,0 +1,87 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
bvarray2uf_rewriter.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Rewriter that rewrites bit-vector arrays into bit-vector
|
||||
(uninterpreted) functions.
|
||||
|
||||
Author:
|
||||
|
||||
Christoph (cwinter) 2015-11-04
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef BVARRAY2UF_REWRITER_H_
|
||||
#define BVARRAY2UF_REWRITER_H_
|
||||
|
||||
#include"rewriter_def.h"
|
||||
#include"extension_model_converter.h"
|
||||
#include"filter_model_converter.h"
|
||||
|
||||
class bvarray2uf_rewriter_cfg : public default_rewriter_cfg {
|
||||
ast_manager & m_manager;
|
||||
expr_ref_vector m_out;
|
||||
sort_ref_vector m_bindings;
|
||||
bv_util m_bv_util;
|
||||
array_util m_array_util;
|
||||
extension_model_converter * m_emc;
|
||||
filter_model_converter * m_fmc;
|
||||
|
||||
obj_map<expr, func_decl*> m_arrays_fs;
|
||||
|
||||
public:
|
||||
bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p);
|
||||
~bvarray2uf_rewriter_cfg();
|
||||
|
||||
ast_manager & m() const { return m_manager; }
|
||||
void updt_params(params_ref const & p) {}
|
||||
|
||||
void reset();
|
||||
|
||||
bool pre_visit(expr * t);
|
||||
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr);
|
||||
|
||||
bool reduce_quantifier(quantifier * old_q,
|
||||
expr * new_body,
|
||||
expr * const * new_patterns,
|
||||
expr * const * new_no_patterns,
|
||||
expr_ref & result,
|
||||
proof_ref & result_pr);
|
||||
|
||||
bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr);
|
||||
|
||||
expr_ref_vector extra_assertions;
|
||||
|
||||
void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_emc = emc; m_fmc = fmc; }
|
||||
|
||||
protected:
|
||||
sort * get_index_sort(expr * e);
|
||||
sort * get_index_sort(sort * s);
|
||||
sort * get_value_sort(expr * e);
|
||||
sort * get_value_sort(sort * s);
|
||||
bool is_bv_array(expr * e);
|
||||
bool is_bv_array(sort * e);
|
||||
func_decl_ref mk_uf_for_array(expr * e);
|
||||
};
|
||||
|
||||
template class rewriter_tpl<bvarray2uf_rewriter_cfg>;
|
||||
|
||||
struct bvarray2uf_rewriter : public rewriter_tpl<bvarray2uf_rewriter_cfg> {
|
||||
bvarray2uf_rewriter_cfg m_cfg;
|
||||
bvarray2uf_rewriter(ast_manager & m, params_ref const & p) :
|
||||
rewriter_tpl<bvarray2uf_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
|
||||
m_cfg(m, p) {
|
||||
}
|
||||
|
||||
void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_cfg.set_mcs(emc, fmc); }
|
||||
};
|
||||
|
||||
#endif
|
||||
|
168
src/tactic/bv/bvarray2uf_tactic.cpp
Normal file
168
src/tactic/bv/bvarray2uf_tactic.cpp
Normal file
|
@ -0,0 +1,168 @@
|
|||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
bvarray2uf_tactic.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Tactic that rewrites bit-vector arrays into bit-vector
|
||||
(uninterpreted) functions.
|
||||
|
||||
Author:
|
||||
|
||||
Christoph (cwinter) 2015-11-04
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include"tactical.h"
|
||||
#include"bv_decl_plugin.h"
|
||||
#include"expr_replacer.h"
|
||||
#include"extension_model_converter.h"
|
||||
#include"filter_model_converter.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
|
||||
#include"bvarray2uf_tactic.h"
|
||||
#include"bvarray2uf_rewriter.h"
|
||||
|
||||
class bvarray2uf_tactic : public tactic {
|
||||
|
||||
struct imp {
|
||||
ast_manager & m_manager;
|
||||
bool m_produce_models;
|
||||
bool m_produce_proofs;
|
||||
bool m_produce_cores;
|
||||
volatile bool m_cancel;
|
||||
bvarray2uf_rewriter m_rw;
|
||||
|
||||
ast_manager & m() { return m_manager; }
|
||||
|
||||
imp(ast_manager & m, params_ref const & p) :
|
||||
m_manager(m),
|
||||
m_produce_models(false),
|
||||
m_cancel(false),
|
||||
m_produce_proofs(false),
|
||||
m_produce_cores(false),
|
||||
m_rw(m, p) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
void set_cancel(bool f) {
|
||||
m_cancel = f;
|
||||
}
|
||||
|
||||
void checkpoint() {
|
||||
if (m_cancel)
|
||||
throw tactic_exception(TACTIC_CANCELED_MSG);
|
||||
}
|
||||
|
||||
void operator()(goal_ref const & g,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core)
|
||||
{
|
||||
SASSERT(g->is_well_sorted());
|
||||
tactic_report report("bvarray2uf", *g);
|
||||
mc = 0; pc = 0; core = 0; result.reset();
|
||||
fail_if_proof_generation("bvarray2uf", g);
|
||||
fail_if_unsat_core_generation("bvarray2uf", g);
|
||||
|
||||
TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); );
|
||||
m_produce_models = g->models_enabled();
|
||||
|
||||
if (m_produce_models) {
|
||||
extension_model_converter * emc = alloc(extension_model_converter, m_manager);
|
||||
filter_model_converter * fmc = alloc(filter_model_converter, m_manager);
|
||||
mc = concat(emc, fmc);
|
||||
m_rw.set_mcs(emc, fmc);
|
||||
|
||||
}
|
||||
|
||||
|
||||
m_rw.reset();
|
||||
expr_ref new_curr(m_manager);
|
||||
proof_ref new_pr(m_manager);
|
||||
unsigned size = g->size();
|
||||
for (unsigned idx = 0; idx < size; idx++) {
|
||||
if (g->inconsistent())
|
||||
break;
|
||||
expr * curr = g->form(idx);
|
||||
m_rw(curr, new_curr, new_pr);
|
||||
//if (m_produce_proofs) {
|
||||
// proof * pr = g->pr(idx);
|
||||
// new_pr = m.mk_modus_ponens(pr, new_pr);
|
||||
//}
|
||||
g->update(idx, new_curr, new_pr, g->dep(idx));
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < m_rw.m_cfg.extra_assertions.size(); i++)
|
||||
g->assert_expr(m_rw.m_cfg.extra_assertions[i].get());
|
||||
|
||||
g->inc_depth();
|
||||
result.push_back(g.get());
|
||||
TRACE("bvarray2uf", tout << "After: " << std::endl; g->display(tout););
|
||||
SASSERT(g->is_well_sorted());
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
}
|
||||
};
|
||||
|
||||
imp * m_imp;
|
||||
params_ref m_params;
|
||||
|
||||
public:
|
||||
bvarray2uf_tactic(ast_manager & m, params_ref const & p) :
|
||||
m_params(p) {
|
||||
m_imp = alloc(imp, m, p);
|
||||
}
|
||||
|
||||
virtual tactic * translate(ast_manager & m) {
|
||||
return alloc(bvarray2uf_tactic, m, m_params);
|
||||
}
|
||||
|
||||
virtual ~bvarray2uf_tactic() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
m_params = p;
|
||||
m_imp->updt_params(p);
|
||||
}
|
||||
|
||||
virtual void collect_param_descrs(param_descrs & r) {
|
||||
insert_produce_models(r);
|
||||
}
|
||||
|
||||
virtual void operator()(goal_ref const & in,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
(*m_imp)(in, result, mc, pc, core);
|
||||
}
|
||||
|
||||
virtual void cleanup() {
|
||||
ast_manager & m = m_imp->m();
|
||||
imp * d = alloc(imp, m, m_params);
|
||||
#pragma omp critical (tactic_cancel)
|
||||
{
|
||||
std::swap(d, m_imp);
|
||||
}
|
||||
dealloc(d);
|
||||
}
|
||||
|
||||
virtual void set_cancel(bool f) {
|
||||
if (m_imp)
|
||||
m_imp->set_cancel(f);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
||||
tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p) {
|
||||
return clean(alloc(bvarray2uf_tactic, m, p));
|
||||
}
|
33
src/tactic/bv/bvarray2uf_tactic.h
Normal file
33
src/tactic/bv/bvarray2uf_tactic.h
Normal file
|
@ -0,0 +1,33 @@
|
|||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
bvarray2ufbvarray2uf_tactic.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Tactic that rewrites bit-vector arrays into bit-vector
|
||||
(uninterpreted) functions.
|
||||
|
||||
Author:
|
||||
|
||||
Christoph (cwinter) 2015-11-04
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef BV_ARRAY2UF_TACTIC_H_
|
||||
#define BV_ARRAY2UF_TACTIC_H_
|
||||
|
||||
#include"params.h"
|
||||
class ast_manager;
|
||||
class tactic;
|
||||
|
||||
tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
/*
|
||||
ADD_TACTIC("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf_tactic(m, p)")
|
||||
*/
|
||||
|
||||
|
||||
#endif
|
|
@ -25,6 +25,7 @@ Notes:
|
|||
#include"max_bv_sharing_tactic.h"
|
||||
#include"bv_size_reduction_tactic.h"
|
||||
#include"reduce_args_tactic.h"
|
||||
#include"qfbv_tactic.h"
|
||||
|
||||
tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref main_p;
|
||||
|
@ -41,13 +42,11 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
|
|||
);
|
||||
|
||||
tactic * st = using_params(and_then(preamble_st,
|
||||
mk_smt_tactic()),
|
||||
cond(mk_is_qfbv_probe(),
|
||||
mk_qfbv_tactic(m),
|
||||
mk_smt_tactic())),
|
||||
main_p);
|
||||
|
||||
//cond(is_qfbv(),
|
||||
// and_then(mk_bit_blaster(m),
|
||||
// mk_sat_solver(m)),
|
||||
// mk_smt_solver())
|
||||
st->updt_params(p);
|
||||
return st;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue