mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-04-06 15:40:13 +01:00
parent ee7b09b3b6 e2b7ad246a
commit 324fcc6a13
23 changed files with 1176 additions and 194 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
contrib/cmake/src/ast/rewriter/CMakeLists.txt
View file

@ -20,6 +20,8 @@ z3_add_component(rewriter
seq_rewriter.cpp
th_rewriter.cpp
var_subst.cpp
bv_trailing.cpp
mk_extract_proc.cpp
COMPONENT_DEPENDENCIES
ast
automata

18
src/ackermannization/ackr_model_converter.cpp
View file

@ -63,19 +63,13 @@ protected:
void add_entry(model_evaluator & evaluator,
app* term, expr* value,
obj_map<func_decl, func_interp*>& interpretations);
void convert_sorts(model * source, model * destination);
void convert_constants(model * source, model * destination);
};
void ackr_model_converter::convert(model * source, model * destination) {
//SASSERT(source->get_num_functions() == 0);
for (unsigned i = 0; i < source->get_num_functions(); i++) {
func_decl * const fd = source->get_function(i);
func_interp * const fi = source->get_func_interp(fd);
destination->register_decl(fd, fi);
}
destination->copy_func_interps(*source);
destination->copy_usort_interps(*source);
convert_constants(source,destination);
convert_sorts(source,destination);
}
void ackr_model_converter::convert_constants(model * source, model * destination) {
@ -136,14 +130,6 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
}
}
void ackr_model_converter::convert_sorts(model * source, model * destination) {
for (unsigned i = 0; i < source->get_num_uninterpreted_sorts(); i++) {
sort * const s = source->get_uninterpreted_sort(i);
ptr_vector<expr> u = source->get_universe(s);
destination->register_usort(s, u.size(), u.c_ptr());
}
}
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info) {
return alloc(ackr_model_converter, m, info);
}

5
src/api/z3_api.h
View file

@ -4538,6 +4538,9 @@ extern "C" {
If \c model_completion is Z3_TRUE, then Z3 will assign an interpretation for any constant or function that does
not have an interpretation in \c m. These constants and functions were essentially don't cares.
If \c model_completion is Z3_FALSE, then Z3 will not assign interpretations to constants for functions that do
not have interpretations in \c m. Evaluation behaves as the identify function in this case.
The evaluation may fail for the following reasons:
- \c t contains a quantifier.
@ -4547,6 +4550,8 @@ extern "C" {
- \c t is type incorrect.
- \c Z3_interrupt was invoked during evaluation.
def_API('Z3_model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST)))
*/
Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast * v);

85
src/ast/bv_decl_plugin.cpp
View file

@ -51,7 +51,7 @@ void bv_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_bit1 = m->mk_const_decl(symbol("bit1"), get_bv_sort(1), func_decl_info(m_family_id, OP_BIT1));
m->inc_ref(m_bit0);
m->inc_ref(m_bit1);
sort * b = m->mk_bool_sort();
sort * d[3] = {b, b, b};
m_carry = m_manager->mk_func_decl(symbol("carry"), 3, d, b, func_decl_info(m_family_id, OP_CARRY));
@ -105,7 +105,7 @@ void bv_decl_plugin::finalize() {
DEC_REF(m_bv_slt);
DEC_REF(m_bv_ugt);
DEC_REF(m_bv_sgt);
DEC_REF(m_bv_and);
DEC_REF(m_bv_or);
DEC_REF(m_bv_not);
@ -113,7 +113,7 @@ void bv_decl_plugin::finalize() {
DEC_REF(m_bv_nand);
DEC_REF(m_bv_nor);
DEC_REF(m_bv_xnor);
DEC_REF(m_bv_redor);
DEC_REF(m_bv_redand);
DEC_REF(m_bv_comp);
@ -181,7 +181,7 @@ sort * bv_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter c
func_decl * bv_decl_plugin::mk_binary(ptr_vector<func_decl> & decls, decl_kind k,
char const * name, unsigned bv_size, bool ac, bool idempotent) {
force_ptr_array_size(decls, bv_size + 1);
if (decls[bv_size] == 0) {
sort * s = get_bv_sort(bv_size);
func_decl_info info(m_family_id, k);
@ -198,7 +198,7 @@ func_decl * bv_decl_plugin::mk_binary(ptr_vector<func_decl> & decls, decl_kind k
func_decl * bv_decl_plugin::mk_unary(ptr_vector<func_decl> & decls, decl_kind k, char const * name, unsigned bv_size) {
force_ptr_array_size(decls, bv_size + 1);
if (decls[bv_size] == 0) {
sort * s = get_bv_sort(bv_size);
decls[bv_size] = m_manager->mk_func_decl(symbol(name), s, s, func_decl_info(m_family_id, k));
@ -223,7 +223,7 @@ func_decl * bv_decl_plugin::mk_int2bv(unsigned bv_size, unsigned num_parameters,
if (m_int2bv[bv_size] == 0) {
sort * s = get_bv_sort(bv_size);
m_int2bv[bv_size] = m_manager->mk_func_decl(symbol("int2bv"), domain[0], s,
m_int2bv[bv_size] = m_manager->mk_func_decl(symbol("int2bv"), domain[0], s,
func_decl_info(m_family_id, OP_INT2BV, num_parameters, parameters));
m_manager->inc_ref(m_int2bv[bv_size]);
}
@ -239,9 +239,9 @@ func_decl * bv_decl_plugin::mk_bv2int(unsigned bv_size, unsigned num_parameters,
m_manager->raise_exception("expecting one argument to bv2int");
return 0;
}
if (m_bv2int[bv_size] == 0) {
m_bv2int[bv_size] = m_manager->mk_func_decl(symbol("bv2int"), domain[0], m_int_sort,
m_bv2int[bv_size] = m_manager->mk_func_decl(symbol("bv2int"), domain[0], m_int_sort,
func_decl_info(m_family_id, OP_BV2INT));
m_manager->inc_ref(m_bv2int[bv_size]);
}
@ -251,7 +251,7 @@ func_decl * bv_decl_plugin::mk_bv2int(unsigned bv_size, unsigned num_parameters,
func_decl * bv_decl_plugin::mk_pred(ptr_vector<func_decl> & decls, decl_kind k, char const * name, unsigned bv_size) {
force_ptr_array_size(decls, bv_size + 1);
if (decls[bv_size] == 0) {
sort * s = get_bv_sort(bv_size);
decls[bv_size] = m_manager->mk_func_decl(symbol(name), s, s, m_manager->mk_bool_sort(), func_decl_info(m_family_id, k));
@ -263,7 +263,7 @@ func_decl * bv_decl_plugin::mk_pred(ptr_vector<func_decl> & decls, decl_kind k,
func_decl * bv_decl_plugin::mk_reduction(ptr_vector<func_decl> & decls, decl_kind k, char const * name, unsigned bv_size) {
force_ptr_array_size(decls, bv_size + 1);
if (decls[bv_size] == 0) {
sort * d = get_bv_sort(bv_size);
sort * r = get_bv_sort(1);
@ -276,7 +276,7 @@ func_decl * bv_decl_plugin::mk_reduction(ptr_vector<func_decl> & decls, decl_kin
func_decl * bv_decl_plugin::mk_comp(unsigned bv_size) {
force_ptr_array_size(m_bv_comp, bv_size + 1);
if (m_bv_comp[bv_size] == 0) {
sort * d = get_bv_sort(bv_size);
sort * r = get_bv_sort(1);
@ -326,7 +326,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned bv_size) {
case OP_BXOR: return mk_binary(m_bv_xor, k, "bvxor", bv_size, true);
case OP_BNAND: return mk_binary(m_bv_nand, k, "bvnand", bv_size, false);
case OP_BNOR: return mk_binary(m_bv_nor, k, "bvnor", bv_size, false);
case OP_BXNOR: return mk_binary(m_bv_xnor, k, "bvxnor", bv_size, false);
case OP_BXNOR: return mk_binary(m_bv_xnor, k, "bvxnor", bv_size, false);
case OP_BREDOR: return mk_reduction(m_bv_redor, k, "bvredor", bv_size);
case OP_BREDAND: return mk_reduction(m_bv_redand, k, "bvredand", bv_size);
@ -334,7 +334,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned bv_size) {
case OP_BUMUL_NO_OVFL: return mk_pred(m_bv_mul_ovfl, k, "bvumul_noovfl", bv_size);
case OP_BSMUL_NO_OVFL: return mk_pred(m_bv_smul_ovfl, k, "bvsmul_noovfl", bv_size);
case OP_BSMUL_NO_UDFL: return mk_pred(m_bv_smul_udfl, k, "bvsmul_noudfl", bv_size);
case OP_BSHL: return mk_binary(m_bv_shl, k, "bvshl", bv_size, false);
case OP_BLSHR: return mk_binary(m_bv_lshr, k, "bvlshr", bv_size, false);
case OP_BASHR: return mk_binary(m_bv_ashr, k, "bvashr", bv_size, false);
@ -369,23 +369,24 @@ bool bv_decl_plugin::get_concat_size(unsigned arity, sort * const * domain, int
return true;
}
bool bv_decl_plugin::get_extend_size(unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, int & result) {
bool bv_decl_plugin::get_extend_size(unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, int & result) {
int arg_sz;
if (arity != 1 || num_parameters != 1 || !parameters[0].is_int() || !get_bv_size(domain[0], arg_sz)) {
if (arity != 1 || !get_bv_size(domain[0], arg_sz) ||
num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) {
return false;
}
result = arg_sz + parameters[0].get_int();
return true;
}
bool bv_decl_plugin::get_extract_size(unsigned num_parameters, parameter const * parameters,
bool bv_decl_plugin::get_extract_size(unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, int & result) {
int arg_sz;
if (arity != 1 ||
!get_bv_size(domain[0], arg_sz) ||
num_parameters != 2 ||
!parameters[0].is_int() ||
!get_bv_size(domain[0], arg_sz) ||
num_parameters != 2 ||
!parameters[0].is_int() ||
!parameters[1].is_int() ||
parameters[1].get_int() > parameters[0].get_int() ||
parameters[0].get_int() >= arg_sz) {
@ -432,7 +433,7 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps));
}
func_decl * bv_decl_plugin::mk_bit2bool(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
func_decl * bv_decl_plugin::mk_bit2bool(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain) {
if (!(num_parameters == 1 && parameters[0].is_int() && arity == 1 && parameters[0].get_int() < static_cast<int>(bv_size))) {
m_manager->raise_exception("invalid bit2bool declaration");
@ -443,7 +444,7 @@ func_decl * bv_decl_plugin::mk_bit2bool(unsigned bv_size, unsigned num_parameter
ptr_vector<func_decl> & v = m_bit2bool[bv_size];
v.reserve(bv_size, 0);
if (v[idx] == 0) {
v[idx] = m_manager->mk_func_decl(m_bit2bool_sym, domain[0], m_manager->mk_bool_sort(),
v[idx] = m_manager->mk_func_decl(m_bit2bool_sym, domain[0], m_manager->mk_bool_sort(),
func_decl_info(m_family_id, OP_BIT2BOOL, num_parameters, parameters));
m_manager->inc_ref(v[idx]);
}
@ -520,34 +521,34 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
switch (k) {
case OP_BIT2BOOL:
return mk_bit2bool(bv_size, num_parameters, parameters, arity, domain);
case OP_INT2BV:
case OP_INT2BV:
return mk_int2bv(bv_size, num_parameters, parameters, arity, domain);
case OP_BV2INT:
case OP_BV2INT:
return mk_bv2int(bv_size, num_parameters, parameters, arity, domain);
case OP_CONCAT:
case OP_CONCAT:
if (!get_concat_size(arity, domain, r_size))
m_manager->raise_exception("invalid concat application");
return m_manager->mk_func_decl(m_concat_sym, arity, domain, get_bv_sort(r_size),
return m_manager->mk_func_decl(m_concat_sym, arity, domain, get_bv_sort(r_size),
func_decl_info(m_family_id, k));
case OP_SIGN_EXT:
if (!get_extend_size(num_parameters, parameters, arity, domain, r_size))
m_manager->raise_exception("invalid sign_extend application");
return m_manager->mk_func_decl(m_sign_extend_sym, arity, domain, get_bv_sort(r_size),
return m_manager->mk_func_decl(m_sign_extend_sym, arity, domain, get_bv_sort(r_size),
func_decl_info(m_family_id, k, num_parameters, parameters));
case OP_ZERO_EXT:
if (!get_extend_size(num_parameters, parameters, arity, domain, r_size))
m_manager->raise_exception("invalid zero_extend application");
return m_manager->mk_func_decl(m_zero_extend_sym, arity, domain, get_bv_sort(r_size),
return m_manager->mk_func_decl(m_zero_extend_sym, arity, domain, get_bv_sort(r_size),
func_decl_info(m_family_id, k, num_parameters, parameters));
case OP_EXTRACT:
if (!get_extract_size(num_parameters, parameters, arity, domain, r_size))
m_manager->raise_exception("invalid extract application");
return m_manager->mk_func_decl(m_extract_sym, arity, domain, get_bv_sort(r_size),
return m_manager->mk_func_decl(m_extract_sym, arity, domain, get_bv_sort(r_size),
func_decl_info(m_family_id, k, num_parameters, parameters));
case OP_ROTATE_LEFT:
if (arity != 1)
m_manager->raise_exception("rotate left expects one argument");
return m_manager->mk_func_decl(m_rotate_left_sym, arity, domain, domain[0],
return m_manager->mk_func_decl(m_rotate_left_sym, arity, domain, domain[0],
func_decl_info(m_family_id, k, num_parameters, parameters));
case OP_ROTATE_RIGHT:
if (arity != 1)
@ -561,14 +562,14 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
m_manager->raise_exception("repeat expects one nonzero integer parameter");
if (!get_bv_size(domain[0], bv_size))
m_manager->raise_exception("repeat expects an argument with bit-vector sort");
return m_manager->mk_func_decl(m_repeat_sym, arity, domain, get_bv_sort(bv_size * parameters[0].get_int()),
return m_manager->mk_func_decl(m_repeat_sym, arity, domain, get_bv_sort(bv_size * parameters[0].get_int()),
func_decl_info(m_family_id, k, num_parameters, parameters));
default:
return 0;
}
}
func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range) {
ast_manager& m = *m_manager;
int bv_size;
@ -657,7 +658,7 @@ bool bv_decl_plugin::are_distinct(app * a, app * b) const {
expr * b_term;
get_offset_term(a, a_term, a_offset);
get_offset_term(b, b_term, b_offset);
TRACE("bv_are_distinct",
TRACE("bv_are_distinct",
tout << mk_ismt2_pp(a, *m_manager) << "\n" << mk_ismt2_pp(b, *m_manager) << "\n";
tout << "---->\n";
tout << "a: " << a_offset << " + " << mk_ismt2_pp(a_term, *m_manager) << "\n";
@ -715,24 +716,24 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
op_names.push_back(builtin_name("bvashr",OP_BASHR));
op_names.push_back(builtin_name("rotate_left",OP_ROTATE_LEFT));
op_names.push_back(builtin_name("rotate_right",OP_ROTATE_RIGHT));
if (logic == symbol::null) {
op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL));
op_names.push_back(builtin_name("bvsmul_noovfl",OP_BSMUL_NO_OVFL));
op_names.push_back(builtin_name("bvsmul_noudfl",OP_BSMUL_NO_UDFL));
op_names.push_back(builtin_name("bvsdiv0", OP_BSDIV0));
op_names.push_back(builtin_name("bvudiv0", OP_BUDIV0));
op_names.push_back(builtin_name("bvsrem0", OP_BSREM0));
op_names.push_back(builtin_name("bvurem0", OP_BUREM0));
op_names.push_back(builtin_name("bvsmod0", OP_BSMOD0));
op_names.push_back(builtin_name("bvsdiv_i", OP_BSDIV_I));
op_names.push_back(builtin_name("bvudiv_i", OP_BUDIV_I));
op_names.push_back(builtin_name("bvsrem_i", OP_BSREM_I));
op_names.push_back(builtin_name("bvurem_i", OP_BUREM_I));
op_names.push_back(builtin_name("bvumod_i", OP_BSMOD_I));
op_names.push_back(builtin_name("ext_rotate_left",OP_EXT_ROTATE_LEFT));
op_names.push_back(builtin_name("ext_rotate_right",OP_EXT_ROTATE_RIGHT));
op_names.push_back(builtin_name("int2bv",OP_INT2BV));
@ -755,7 +756,7 @@ rational bv_recognizers::norm(rational const & val, unsigned bv_size, bool is_si
if (r >= rational::power_of_two(bv_size - 1)) {
r -= rational::power_of_two(bv_size);
}
if (r < -rational::power_of_two(bv_size - 1)) {
if (r < -rational::power_of_two(bv_size - 1)) {
r += rational::power_of_two(bv_size);
}
}
@ -770,7 +771,7 @@ bool bv_recognizers::has_sign_bit(rational const & n, unsigned bv_size) const {
}
bool bv_recognizers::is_bv_sort(sort const * s) const {
return (s->get_family_id() == get_fid() && s->get_decl_kind() == BV_SORT && s->get_num_parameters() == 1);
return (s->get_family_id() == get_fid() && s->get_decl_kind() == BV_SORT && s->get_num_parameters() == 1);
}
bool bv_recognizers::is_numeral(expr const * n, rational & val, unsigned & bv_size) const {
@ -821,11 +822,11 @@ bool bv_recognizers::mult_inverse(rational const & n, unsigned bv_size, rational
result = n;
return true;
}
if (!mod(n, rational(2)).is_one()) {
return false;
}
rational g;
rational x;
rational y;
@ -874,5 +875,5 @@ unsigned bv_util::get_int2bv_size(parameter const& p) {
app * bv_util::mk_bv2int(expr* e) {
sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT);
parameter p(s);
return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e);
return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e);
}

44
src/ast/rewriter/bv_rewriter.cpp
View file

@ -22,45 +22,13 @@ Notes:
#include"ast_smt2_pp.h"
mk_extract_proc::mk_extract_proc(bv_util & u):
m_util(u),
m_high(0),
m_low(UINT_MAX),
m_domain(0),
m_f_cached(0) {
}
mk_extract_proc::~mk_extract_proc() {
if (m_f_cached) {
// m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
ast_manager & m = m_util.get_manager();
m.dec_ref(m_f_cached);
}
}
app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) {
ast_manager & m = m_util.get_manager();
sort * s = m.get_sort(arg);
if (m_low == low && m_high == high && m_domain == s)
return m.mk_app(m_f_cached, arg);
// m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
if (m_f_cached)
m.dec_ref(m_f_cached);
app * r = to_app(m_util.mk_extract(high, low, arg));
m_high = high;
m_low = low;
m_domain = s;
m_f_cached = r->get_decl();
m.inc_ref(m_f_cached);
return r;
}
void bv_rewriter::updt_local_params(params_ref const & _p) {
bv_rewriter_params p(_p);
m_hi_div0 = p.hi_div0();
m_elim_sign_ext = p.elim_sign_ext();
m_mul2concat = p.mul2concat();
m_bit2bool = p.bit2bool();
m_trailing = p.bv_trailing();
m_blast_eq_value = p.blast_eq_value();
m_split_concat_eq = p.split_concat_eq();
m_udiv2mul = p.udiv2mul();
@ -2124,6 +2092,15 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
return st;
}
if (m_trailing) {
st = m_rm_trailing.eq_remove_trailing(lhs, rhs, result);
m_rm_trailing.reset_cache(1 << 12);
if (st != BR_FAILED) {
TRACE("eq_remove_trailing", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result, m()) << "\n";);
return st;
}
}
st = mk_mul_eq(lhs, rhs, result);
if (st != BR_FAILED) {
TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result,m()) << "\n";);
@ -2187,6 +2164,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
return BR_FAILED;
}
br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & result) {
if (m_mkbv2num) {
unsigned i;

17
src/ast/rewriter/bv_rewriter.h
View file

@ -22,18 +22,8 @@ Notes:
#include"poly_rewriter.h"
#include"bv_decl_plugin.h"
#include"arith_decl_plugin.h"
class mk_extract_proc {
bv_util & m_util;
unsigned m_high;
unsigned m_low;
sort * m_domain;
func_decl * m_f_cached;
public:
mk_extract_proc(bv_util & u);
~mk_extract_proc();
app * operator()(unsigned high, unsigned low, expr * arg);
};
#include"mk_extract_proc.h"
#include"bv_trailing.h"
class bv_rewriter_core {
protected:
@ -58,6 +48,7 @@ public:
class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
mk_extract_proc m_mk_extract;
bv_trailing m_rm_trailing;
arith_util m_autil;
bool m_hi_div0;
bool m_elim_sign_ext;
@ -69,6 +60,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
bool m_udiv2mul;
bool m_bvnot2arith;
bool m_bv_sort_ac;
bool m_trailing;
bool is_zero_bit(expr * x, unsigned idx);
@ -148,6 +140,7 @@ public:
bv_rewriter(ast_manager & m, params_ref const & p = params_ref()):
poly_rewriter<bv_rewriter_core>(m, p),
m_mk_extract(m_util),
m_rm_trailing(m_mk_extract),
m_autil(m) {
updt_local_params(p);
}

3
src/ast/rewriter/bv_rewriter_params.pyg
View file

@ -9,5 +9,6 @@ def_module_params(module_name='rewriter',
("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"),
("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"),
("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)"),
("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators")
("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators"),
("bv_trailing", BOOL, False, "lean removal of trailing zeros")
))

402
src/ast/rewriter/bv_trailing.cpp Normal file
View file

@ -0,0 +1,402 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
bv_trailing.cpp
Abstract:
Author:
Mikolas Janota (MikolasJanota)
Revision History:
--*/
#include"bv_trailing.h"
#include"bv_decl_plugin.h"
#include"ast_smt2_pp.h"
// The analyzer gives up analysis after going TRAILING_DEPTH deep.
// This number shouldn't be too big.
#define TRAILING_DEPTH 5
struct bv_trailing::imp {
typedef rational numeral;
typedef obj_map<expr, std::pair<unsigned,unsigned> > map;
mk_extract_proc& m_mk_extract;
bv_util& m_util;
ast_manager& m;
// keep a cache for each depth, using the convention that m_count_cache[TRAILING_DEPTH] is top-level
map* m_count_cache[TRAILING_DEPTH + 1];
imp(mk_extract_proc& mk_extract)
: m_mk_extract(mk_extract)
, m_util(mk_extract.bvutil())
, m(mk_extract.m()) {
for (unsigned i = 0; i <= TRAILING_DEPTH; ++i)
m_count_cache[i] = NULL;
}
virtual ~imp() {
reset_cache(0);
}
br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) {
TRACE("bv-trailing", tout << mk_ismt2_pp(e1, m) << "\n=\n" << mk_ismt2_pp(e2, m) << "\n";);
SASSERT(m_util.is_bv(e1) && m_util.is_bv(e2));
SASSERT(m_util.get_bv_size(e1) == m_util.get_bv_size(e2));
unsigned max1, min1, max2, min2;
count_trailing(e1, min1, max1, TRAILING_DEPTH);
count_trailing(e2, min2, max2, TRAILING_DEPTH);
if (min1 > max2 || min2 > max1) { // bounds have empty intersection
result = m.mk_false();
return BR_DONE;
}
const unsigned min = std::min(min1, min2); // remove the minimum of the two lower bounds
if (min == 0) { // nothing to remove
result = m.mk_eq(e1, e2);
return BR_FAILED;
}
const unsigned sz = m_util.get_bv_size(e1);
if (min == sz) { // everything removed, unlikely but we check anyhow for safety
result = m.mk_true();
return BR_DONE;
}
expr_ref out1(m);
expr_ref out2(m);
const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH);
const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH);
SASSERT(rm1 == min && rm2 == min);
const bool are_eq = m.are_equal(out1, out2);
result = are_eq ? m.mk_true() : m.mk_eq(out1, out2);
return are_eq ? BR_DONE : BR_REWRITE2;
}
// This routine needs to be implemented carefully so that whenever it
// returns a lower bound on trailing zeros min, the routine remove_trailing
// must be capable of removing at least that many zeros from the expression.
void count_trailing(expr * e, unsigned& min, unsigned& max, unsigned depth) {
SASSERT(e && m_util.is_bv(e));
if (is_cached(depth, e, min, max)) return;
count_trailing_core(e, min, max, depth);
TRACE("bv-trailing", tout << mk_ismt2_pp(e, m) << "\n:" << min << " - " << max << "\n";);
SASSERT(min <= max);
SASSERT(max <= m_util.get_bv_size(e));
cache(depth, e, min, max); // store result into the cache
}
unsigned remove_trailing(expr * e, unsigned n, expr_ref& result, unsigned depth) {
const unsigned retv = remove_trailing_core(e, n, result, depth);
CTRACE("bv-trailing", result.get(), tout << mk_ismt2_pp(e, m) << "\n--->\n" << mk_ismt2_pp(result.get(), m) << "\n";);
CTRACE("bv-trailing", !result.get(), tout << mk_ismt2_pp(e, m) << "\n---> [EMPTY]\n";);
return retv;
}
// Assumes that count_trailing gives me a lower bound that we can also remove from each summand.
unsigned remove_trailing_add(app * a, unsigned n, expr_ref& result, unsigned depth) {
SASSERT(m_util.is_bv_add(a));
const unsigned num = a->get_num_args();
if (depth <= 1) {
result = a;
return 0;
}
unsigned min, max;
count_trailing(a, min, max, depth); // caching is important here
const unsigned to_rm = std::min(min, n);
if (to_rm == 0) {
result = a;
return 0;
}
const unsigned sz = m_util.get_bv_size(a);
if (to_rm == sz) {
result = NULL;
return sz;
}
expr_ref_vector new_args(m);
expr_ref tmp(m);
for (unsigned i = 0; i < num; ++i) {
expr * const curr = a->get_arg(i);
const unsigned crm = remove_trailing(curr, to_rm, tmp, depth - 1);
new_args.push_back(tmp);
SASSERT(crm == to_rm);
}
result = m.mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr());
return to_rm;
}
unsigned remove_trailing_mul(app * a, unsigned n, expr_ref& result, unsigned depth) {
SASSERT(m_util.is_bv_mul(a));
const unsigned num = a->get_num_args();
if (depth <= 1 || !num) {
result = a;
return 0;
}
expr_ref tmp(m);
expr * const coefficient = a->get_arg(0);
const unsigned retv = remove_trailing(coefficient, n, tmp, depth - 1);
SASSERT(retv <= n);
if (retv == 0) {
result = a;
return 0;
}
expr_ref_vector new_args(m);
numeral c_val;
unsigned c_sz;
if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one())
new_args.push_back(tmp);
const unsigned sz = m_util.get_bv_size(coefficient);
const unsigned new_sz = sz - retv;
if (!new_sz) {
result = NULL;
return retv;
}
SASSERT(m_util.get_bv_size(tmp) == new_sz);
for (unsigned i = 1; i < num; i++) {
expr * const curr = a->get_arg(i);
new_args.push_back(m_mk_extract(new_sz - 1, 0, curr));
}
switch (new_args.size()) {
case 0: result = m_util.mk_numeral(1, new_sz); break;
case 1: result = new_args.get(0); break;
default: result = m.mk_app(m_util.get_fid(), OP_BMUL, new_args.size(), new_args.c_ptr());
}
return retv;
}
unsigned remove_trailing_concat(app * a, unsigned n, expr_ref& result, unsigned depth) {
SASSERT(m_util.is_concat(a));
if (depth <= 1) {
result = a;
return 0;
}
const unsigned num = a->get_num_args();
unsigned retv = 0;
unsigned i = num;
expr_ref new_last(NULL, m);
while (i && retv < n) {
i--;
expr * const curr = a->get_arg(i);
const unsigned cur_rm = remove_trailing(curr, n, new_last, depth - 1);
const unsigned curr_sz = m_util.get_bv_size(curr);
retv += cur_rm;
if (cur_rm < curr_sz) break;
}
if (retv == 0) {
result = a;
return 0;
}
if (!i) {// all args eaten completely
SASSERT(new_last.get() == NULL);
SASSERT(retv == m_util.get_bv_size(a));
result = NULL;
return retv;
}
expr_ref_vector new_args(m);
for (unsigned j = 0; j < i; ++j)
new_args.push_back(a->get_arg(j));
if (new_last.get()) new_args.push_back(new_last);
result = new_args.size() == 1 ? new_args.get(0)
: m_util.mk_concat(new_args.size(), new_args.c_ptr());
return retv;
}
unsigned remove_trailing(size_t max_rm, numeral& a) {
numeral two(2);
unsigned retv = 0;
while (max_rm && a.is_even()) {
div(a, two, a);
++retv;
--max_rm;
}
return retv;
}
unsigned remove_trailing_core(expr * e, unsigned n, expr_ref& result, unsigned depth) {
SASSERT(m_util.is_bv(e));
if (!depth || !n) return 0;
unsigned sz;
unsigned retv = 0;
numeral e_val;
if (m_util.is_numeral(e, e_val, sz)) {
retv = remove_trailing(n, e_val);
const unsigned new_sz = sz - retv;
result = new_sz ? (retv ? m_util.mk_numeral(e_val, new_sz) : e) : NULL;
return retv;
}
if (m_util.is_bv_mul(e))
return remove_trailing_mul(to_app(e), n, result, depth);
if (m_util.is_bv_add(e))
return remove_trailing_add(to_app(e), n, result, depth);
if (m_util.is_concat(e))
return remove_trailing_concat(to_app(e), n, result, depth);
return 0;
}
void count_trailing_concat(app * a, unsigned& min, unsigned& max, unsigned depth) {
if (depth <= 1) {
min = 0;
max = m_util.get_bv_size(a);
}
max = min = 0; // treat empty concat as the empty string
unsigned num = a->get_num_args();
bool update_min = true;
bool update_max = true;
unsigned tmp_min, tmp_max;
while (num-- && update_max) {
expr * const curr = a->get_arg(num);
const unsigned curr_sz = m_util.get_bv_size(curr);
count_trailing(curr, tmp_min, tmp_max, depth - 1);
SASSERT(curr_sz != tmp_min || curr_sz == tmp_max);
max += tmp_max;
if (update_min) min += tmp_min;
// continue updating only if eaten away completely
update_min &= curr_sz == tmp_min;
update_max &= curr_sz == tmp_max;
}
}
void count_trailing_add(app * a, unsigned& min, unsigned& max, unsigned depth) {
if (depth <= 1) {
min = 0;
max = m_util.get_bv_size(a);
}
const unsigned num = a->get_num_args();
const unsigned sz = m_util.get_bv_size(a);
min = max = sz; // treat empty addition as 0
unsigned tmp_min;
unsigned tmp_max;
bool known_parity = true;
bool is_odd = false;
for (unsigned i = 0; i < num; ++i) {
expr * const curr = a->get_arg(i);
count_trailing(curr, tmp_min, tmp_max, depth - 1);
min = std::min(min, tmp_min);
known_parity = known_parity && (!tmp_max || tmp_min);
if (known_parity && !tmp_max) is_odd = !is_odd;
if (!known_parity && !min) break; // no more information can be gained
}
max = known_parity && is_odd ? 0 : sz; // max is known if parity is 1
}
void count_trailing_mul(app * a, unsigned& min, unsigned& max, unsigned depth) {
if (depth <= 1) {
min = 0;
max = m_util.get_bv_size(a);
}
const unsigned num = a->get_num_args();
if (!num) {
max = min = 0; // treat empty multiplication as 1
return;
}
// assume that numerals are pushed in the front, count only for the first element
expr * const curr = a->get_arg(0);
unsigned tmp_max;
count_trailing(curr, min, tmp_max, depth - 1);
max = num == 1 ? tmp_max : m_util.get_bv_size(a);
return;
}
void count_trailing_core(expr * e, unsigned& min, unsigned& max, unsigned depth) {
if (!depth) {
min = 0;
max = m_util.get_bv_size(e);
return;
}
unsigned sz;
numeral e_val;
if (m_util.is_numeral(e, e_val, sz)) {
min = max = 0;
numeral two(2);
while (sz-- && e_val.is_even()) {
++max;
++min;
div(e_val, two, e_val);
}
return;
}
if (m_util.is_bv_mul(e)) count_trailing_mul(to_app(e), min, max, depth);
else if (m_util.is_bv_add(e)) count_trailing_add(to_app(e), min, max, depth);
else if (m_util.is_concat(e)) count_trailing_concat(to_app(e), min, max, depth);
else {
min = 0;
max = m_util.get_bv_size(e);
}
}
void cache(unsigned depth, expr * e, unsigned min, unsigned max) {
SASSERT(depth <= TRAILING_DEPTH);
if (depth == 0) return;
if (m_count_cache[depth] == NULL)
m_count_cache[depth] = alloc(map);
m.inc_ref(e);
m_count_cache[depth]->insert(e, std::make_pair(min, max));
TRACE("bv-trailing", tout << "caching@" << depth <<": " << mk_ismt2_pp(e, m) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";);
}
bool is_cached(unsigned depth, expr * e, unsigned& min, unsigned& max) {
SASSERT(depth <= TRAILING_DEPTH);
if (depth == 0) {
min = 0;
max = m_util.get_bv_size(e);
return true;
}
if (m_count_cache[depth] == NULL)
return false;
const map::obj_map_entry * const oe = m_count_cache[depth]->find_core(e);
if (oe == NULL) return false;
min = oe->get_data().m_value.first;
max = oe->get_data().m_value.second;
TRACE("bv-trailing", tout << "cached@" << depth << ": " << mk_ismt2_pp(e, m) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";);
return true;
}
void reset_cache(unsigned condition) {
SASSERT(m_count_cache[0] == NULL);
for (unsigned i = 1; i <= TRAILING_DEPTH; ++i) {
if (m_count_cache[i] == NULL) continue;
if (m_count_cache[i]->size() < condition) continue;
map::iterator it = m_count_cache[i]->begin();
map::iterator end = m_count_cache[i]->end();
for (; it != end; ++it) m.dec_ref(it->m_key);
dealloc(m_count_cache[i]);
m_count_cache[i] = NULL;
}
}
};
bv_trailing::bv_trailing(mk_extract_proc& mk_extract) {
m_imp = alloc(imp, mk_extract);
}
bv_trailing::~bv_trailing() {
dealloc(m_imp);
}
br_status bv_trailing::eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) {
return m_imp->eq_remove_trailing(e1, e2, result);
}
void bv_trailing::count_trailing(expr * e, unsigned& min, unsigned& max) {
m_imp->count_trailing(e, min, max, TRAILING_DEPTH);
}
unsigned bv_trailing::remove_trailing(expr * e, unsigned n, expr_ref& result) {
return m_imp->remove_trailing(e, n, result, TRAILING_DEPTH);
}
void bv_trailing::reset_cache(unsigned condition) {
m_imp->reset_cache(condition);
}

46
src/ast/rewriter/bv_trailing.h Normal file
View file

@ -0,0 +1,46 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
bv_trailing.h
Abstract:
A utility to count trailing zeros of an expression. Treats 2x and x++0 equivalently.
Author:
Mikolas Janota (MikolasJanota)
Revision History:
--*/
#ifndef BV_TRAILING_H_
#define BV_TRAILING_H_
#include"ast.h"
#include"rewriter_types.h"
#include"mk_extract_proc.h"
class bv_trailing {
public:
bv_trailing(mk_extract_proc& ep);
virtual ~bv_trailing();
public:
// Remove trailing zeros from both sides of an equality (might give False).
br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result);
// Gives a lower and upper bound on trailing zeros in e.
void count_trailing(expr * e, unsigned& min, unsigned& max);
// Attempts removing n trailing zeros from e. Returns how many were successfully removed.
// We're assuming that it can remove at least as many zeros as min returned by count_training.
// Removing the bit-width of e, sets result to NULL.
unsigned remove_trailing(expr * e, unsigned n, expr_ref& result);
// Reset cache(s) if it exceeded size condition.
void reset_cache(unsigned condition);
protected:
struct imp;
imp * m_imp;
};
#endif /* BV_TRAILING_H_ */

49
src/ast/rewriter/mk_extract_proc.cpp Normal file
View file

@ -0,0 +1,49 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
mk_extract_proc.cpp
Abstract:
Author:
Mikolas Janota (MikolasJanota)
Revision History:
--*/
#include"mk_extract_proc.h"
mk_extract_proc::mk_extract_proc(bv_util & u):
m_util(u),
m_high(0),
m_low(UINT_MAX),
m_domain(0),
m_f_cached(0) {
}
mk_extract_proc::~mk_extract_proc() {
if (m_f_cached) {
// m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
ast_manager & m = m_util.get_manager();
m.dec_ref(m_f_cached);
}
}
app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) {
ast_manager & m = m_util.get_manager();
sort * s = m.get_sort(arg);
if (m_low == low && m_high == high && m_domain == s)
return m.mk_app(m_f_cached, arg);
// m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
if (m_f_cached)
m.dec_ref(m_f_cached);
app * r = to_app(m_util.mk_extract(high, low, arg));
m_high = high;
m_low = low;
m_domain = s;
m_f_cached = r->get_decl();
m.inc_ref(m_f_cached);
return r;
}

34
src/ast/rewriter/mk_extract_proc.h Normal file
View file

@ -0,0 +1,34 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
mk_extract_proc.h
Abstract:
Author:
Mikolas Janota (MikolasJanota)
Revision History:
--*/
#ifndef MK_EXTRACT_PROC_H_
#define MK_EXTRACT_PROC_H_
#include"ast.h"
#include"bv_decl_plugin.h"
class mk_extract_proc {
bv_util & m_util;
unsigned m_high;
unsigned m_low;
sort * m_domain;
func_decl * m_f_cached;
public:
mk_extract_proc(bv_util & u);
~mk_extract_proc();
app * operator()(unsigned high, unsigned low, expr * arg);
ast_manager & m() { return m_util.get_manager(); }
bv_util & bvutil() { return m_util; }
};
#endif /* MK_EXTRACT_PROC_H_ */

18
src/ast/rewriter/poly_rewriter_def.h
View file

@ -825,15 +825,17 @@ br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool m
if (c_at_rhs) {
c.neg();
normalize(c);
new_rhs_monomials[0] = mk_numeral(c);
lhs_result = mk_add_app(new_lhs_monomials.size() - 1, new_lhs_monomials.c_ptr() + 1);
rhs_result = mk_add_app(new_rhs_monomials.size(), new_rhs_monomials.c_ptr());
}
else {
new_lhs_monomials[0] = mk_numeral(c);
lhs_result = mk_add_app(new_lhs_monomials.size(), new_lhs_monomials.c_ptr());
rhs_result = mk_add_app(new_rhs_monomials.size() - 1, new_rhs_monomials.c_ptr() + 1);
}
// When recreating the lhs and rhs also insert coefficient on the appropriate side.
// Ignore coefficient if it's 0 and there are no other summands.
const bool insert_c_lhs = !c_at_rhs && (new_lhs_monomials.size() == 1 || !c.is_zero());
const bool insert_c_rhs = c_at_rhs && (new_rhs_monomials.size() == 1 || !c.is_zero());
const unsigned lhs_offset = insert_c_lhs ? 0 : 1;
const unsigned rhs_offset = insert_c_rhs ? 0 : 1;
new_rhs_monomials[0] = insert_c_rhs ? mk_numeral(c) : NULL;
new_lhs_monomials[0] = insert_c_lhs ? mk_numeral(c) : NULL;
lhs_result = mk_add_app(new_lhs_monomials.size() - lhs_offset, new_lhs_monomials.c_ptr() + lhs_offset);
rhs_result = mk_add_app(new_rhs_monomials.size() - rhs_offset, new_rhs_monomials.c_ptr() + rhs_offset);
return BR_DONE;
}

23
src/model/model.cpp
View file

@ -25,7 +25,7 @@ Revision History:
#include"used_symbols.h"
#include"model_evaluator.h"
model::model(ast_manager & m):
model::model(ast_manager & m):
model_core(m) {
}
@ -56,7 +56,7 @@ void model::copy_func_interps(model const & source) {
register_decl(it2->m_key, it2->m_value->copy());
}
}
void model::copy_usort_interps(model const & source) {
sort2universe::iterator it3 = source.m_usort2universe.begin();
sort2universe::iterator end3 = source.m_usort2universe.end();
@ -67,7 +67,7 @@ void model::copy_usort_interps(model const & source) {
model * model::copy() const {
model * m = alloc(model, m_manager);
m->copy_const_interps(*this);
m->copy_func_interps(*this);
m->copy_usort_interps(*this);
@ -121,16 +121,15 @@ bool model::has_uninterpreted_sort(sort * s) const {
return u != 0;
}
unsigned model::get_num_uninterpreted_sorts() const {
return m_usorts.size();
unsigned model::get_num_uninterpreted_sorts() const {
return m_usorts.size();
}
sort * model::get_uninterpreted_sort(unsigned idx) const {
return m_usorts[idx];
sort * model::get_uninterpreted_sort(unsigned idx) const {
return m_usorts[idx];
}
void model::register_usort(sort * s, unsigned usize, expr * const * universe) {
SASSERT(m_manager.is_uninterp(s));
sort2universe::obj_map_entry * entry = m_usort2universe.insert_if_not_there2(s, 0);
m_manager.inc_array_ref(usize, universe);
if (entry->get_data().m_value == 0) {
@ -151,7 +150,7 @@ void model::register_usort(sort * s, unsigned usize, expr * const * universe) {
}
model * model::translate(ast_translation & translator) const {
model * res = alloc(model, translator.to());
model * res = alloc(model, translator.to());
// Translate const interps
decl2expr::iterator it1 = m_interp.begin();
@ -167,7 +166,7 @@ model * model::translate(ast_translation & translator) const {
func_interp * fi = it2->m_value;
res->register_decl(translator(it2->m_key), fi->translate(translator));
}
// Translate usort interps
sort2universe::iterator it3 = m_usort2universe.begin();
sort2universe::iterator end3 = m_usort2universe.end();
@ -175,8 +174,8 @@ model * model::translate(ast_translation & translator) const {
ptr_vector<expr> new_universe;
for (unsigned i=0; i<it3->m_value->size(); i++)
new_universe.push_back(translator(it3->m_value->get(i)));
res->register_usort(translator(it3->m_key),
new_universe.size(),
res->register_usort(translator(it3->m_key),
new_universe.size(),
new_universe.c_ptr());
}

2
src/model/model_core.cpp
View file

@ -31,7 +31,7 @@ model_core::~model_core() {
for (; it2 != end2; ++it2) {
m_manager.dec_ref(it2->m_key);
dealloc(it2->m_value);
}
}
}
bool model_core::eval(func_decl* f, expr_ref & r) const {

88
src/model/model_evaluator.cpp
View file

@ -30,6 +30,7 @@ Revision History:
#include"fpa_rewriter.h"
#include"rewriter_def.h"
#include"cooperate.h"
#include"ast_pp.h"
struct evaluator_cfg : public default_rewriter_cfg {
@ -42,6 +43,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
pb_rewriter m_pb_rw;
fpa_rewriter m_f_rw;
seq_rewriter m_seq_rw;
array_util m_ar;
unsigned long long m_max_memory;
unsigned m_max_steps;
bool m_model_completion;
@ -59,7 +61,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
m_dt_rw(m),
m_pb_rw(m),
m_f_rw(m),
m_seq_rw(m) {
m_seq_rw(m),
m_ar(m) {
bool flat = true;
m_b_rw.set_flat(flat);
m_a_rw.set_flat(flat);
@ -116,6 +119,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
if (val != 0) {
result = val;
return BR_DONE;
// return m().is_value(val)?BR_DONE:BR_REWRITE_FULL;
}
if (m_model_completion) {
@ -146,6 +150,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
st = m_f_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_seq_rw.get_fid())
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
else if (fid == m_ar_rw.get_fid())
st = mk_array_eq(args[0], args[1], result);
if (st != BR_FAILED)
return st;
}
@ -182,6 +188,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
return st;
}
bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
#define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
@ -230,6 +237,85 @@ struct evaluator_cfg : public default_rewriter_cfg {
bool cache_results() const { return m_cache; }
br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
if (a == b) {
result = m().mk_true();
return BR_DONE;
}
vector<expr_ref_vector> stores;
expr_ref else1(m()), else2(m());
if (extract_array_func_interp(a, stores, else1) &&
extract_array_func_interp(b, stores, else2)) {
expr_ref_vector conj(m()), args1(m()), args2(m());
conj.push_back(m().mk_eq(else1, else2));
args1.push_back(a);
args2.push_back(b);
for (unsigned i = 0; i < stores.size(); ++i) {
args1.resize(1); args1.append(stores[i].size() - 1, stores[i].c_ptr());
args2.resize(1); args2.append(stores[i].size() - 1, stores[i].c_ptr());
expr* s1 = m_ar.mk_select(args1.size(), args1.c_ptr());
expr* s2 = m_ar.mk_select(args2.size(), args2.c_ptr());
conj.push_back(m().mk_eq(s1, s2));
}
result = m().mk_and(conj.size(), conj.c_ptr());
return BR_REWRITE_FULL;
}
return BR_FAILED;
}
bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case) {
SASSERT(m_ar.is_array(a));
while (m_ar.is_store(a)) {
expr_ref_vector store(m());
store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
stores.push_back(store);
a = to_app(a)->get_arg(0);
}
if (m_ar.is_const(a)) {
else_case = to_app(a)->get_arg(0);
return true;
}
if (m_ar.is_as_array(a)) {
func_decl* f = m_ar.get_as_array_func_decl(to_app(a));
func_interp* g = m_model.get_func_interp(f);
unsigned sz = g->num_entries();
unsigned arity = f->get_arity();
for (unsigned i = 0; i < sz; ++i) {
expr_ref_vector store(m());
func_entry const* fe = g->get_entry(i);
store.append(arity, fe->get_args());
store.push_back(fe->get_result());
for (unsigned j = 0; j < store.size(); ++j) {
if (!is_ground(store[j].get())) {
TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m()) << "\n" << mk_pp(store[j].get(), m()) << "\n";);
return false;
}
}
stores.push_back(store);
}
else_case = g->get_else();
if (!else_case) {
TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n";);
return false;
}
if (!is_ground(else_case)) {
TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << mk_pp(else_case, m()) << "\n";);
return false;
}
TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m()) << "\n";);
return true;
}
TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);
return false;
}
};
template class rewriter_tpl<evaluator_cfg>;

2
src/sat/sat_simplifier.cpp
View file

@ -401,7 +401,7 @@ namespace sat {
literal_vector::iterator l_it = m_bs_ls.begin();
for (; it != end; ++it, ++l_it) {
clause & c2 = *(*it);
if (*l_it == null_literal) {
if (!c2.was_removed() && *l_it == null_literal) {
// c2 was subsumed
if (c1.is_learned() && !c2.is_learned())
c1.unset_learned();

73
src/smt/proto_model/proto_model.cpp
View file

@ -34,7 +34,7 @@ proto_model::proto_model(ast_manager & m, params_ref const & p):
register_factory(alloc(basic_factory, m));
m_user_sort_factory = alloc(user_sort_factory, m);
register_factory(m_user_sort_factory);
m_model_partial = model_params(p).partial();
}
@ -85,8 +85,8 @@ expr * proto_model::mk_some_interp_for(func_decl * d) {
bool proto_model::is_select_of_model_value(expr* e) const {
return
is_app_of(e, m_afid, OP_SELECT) &&
return
is_app_of(e, m_afid, OP_SELECT) &&
is_as_array(to_app(e)->get_arg(0)) &&
has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0))));
}
@ -115,7 +115,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
It returns \c true if succeeded, and false otherwise. If the evaluation fails,
then r contains a term that is simplified as much as possible using the interpretations
available in the model.
When model_completion == true, if the model does not assign an interpretation to a
declaration it will build one for it. Moreover, partial functions will also be completed.
So, if model_completion == true, the evaluator never fails if it doesn't contain quantifiers.
@ -194,7 +194,7 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au
if (!cache.find(fi_else, a)) {
UNREACHABLE();
}
fi->set_else(a);
}
@ -225,12 +225,12 @@ void proto_model::cleanup() {
func_interp * fi = (*it).m_value;
cleanup_func_interp(fi, found_aux_fs);
}
// remove auxiliary declarations that are not used.
if (found_aux_fs.size() != m_aux_decls.size()) {
remove_aux_decls_not_in_set(m_decls, found_aux_fs);
remove_aux_decls_not_in_set(m_func_decls, found_aux_fs);
func_decl_set::iterator it2 = m_aux_decls.begin();
func_decl_set::iterator end2 = m_aux_decls.end();
for (; it2 != end2; ++it2) {
@ -262,7 +262,6 @@ void proto_model::freeze_universe(sort * s) {
\brief Return the known universe of an uninterpreted sort.
*/
obj_hashtable<expr> const & proto_model::get_known_universe(sort * s) const {
SASSERT(m_manager.is_uninterp(s));
return m_user_sort_factory->get_known_universe(s);
}
@ -277,13 +276,13 @@ ptr_vector<expr> const & proto_model::get_universe(sort * s) const {
return tmp;
}
unsigned proto_model::get_num_uninterpreted_sorts() const {
return m_user_sort_factory->get_num_sorts();
unsigned proto_model::get_num_uninterpreted_sorts() const {
return m_user_sort_factory->get_num_sorts();
}
sort * proto_model::get_uninterpreted_sort(unsigned idx) const {
SASSERT(idx < get_num_uninterpreted_sorts());
return m_user_sort_factory->get_sort(idx);
sort * proto_model::get_uninterpreted_sort(unsigned idx) const {
SASSERT(idx < get_num_uninterpreted_sorts());
return m_user_sort_factory->get_sort(idx);
}
/**
@ -301,7 +300,7 @@ expr * proto_model::get_some_value(sort * s) {
else {
family_id fid = s->get_family_id();
value_factory * f = get_factory(fid);
if (f)
if (f)
return f->get_some_value(s);
// there is no factory for the family id, then assume s is uninterpreted.
return m_user_sort_factory->get_some_value(s);
@ -315,7 +314,7 @@ bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
else {
family_id fid = s->get_family_id();
value_factory * f = get_factory(fid);
if (f)
if (f)
return f->get_some_values(s, v1, v2);
else
return false;
@ -327,9 +326,9 @@ expr * proto_model::get_fresh_value(sort * s) {
return m_user_sort_factory->get_fresh_value(s);
}
else {
family_id fid = s->get_family_id();
family_id fid = s->get_family_id();
value_factory * f = get_factory(fid);
if (f)
if (f)
return f->get_fresh_value(s);
else
// Use user_sort_factory if the theory has no support for model construnction.
@ -374,7 +373,7 @@ void proto_model::complete_partial_func(func_decl * f) {
func_interp * fi = get_func_interp(f);
if (fi && fi->is_partial()) {
expr * else_value = 0;
#if 0
#if 0
// For UFBV benchmarks, setting the "else" to false is not a good idea.
// TODO: find a permanent solution. A possibility is to add another option.
if (m_manager.is_bool(f->get_range())) {
@ -395,7 +394,7 @@ void proto_model::complete_partial_func(func_decl * f) {
}
/**
\brief Set the (else) field of function interpretations...
\brief Set the (else) field of function interpretations...
*/
void proto_model::complete_partial_funcs() {
if (m_model_partial)
@ -424,7 +423,7 @@ model * proto_model::mk_model() {
m->register_decl(it2->m_key, it2->m_value);
m_manager.dec_ref(it2->m_key);
}
m_finterp.reset(); // m took the ownership of the func_interp's
unsigned sz = get_num_uninterpreted_sorts();
@ -450,7 +449,7 @@ model * proto_model::mk_model() {
// It uses the simplifier s during the computation.
bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & result) {
bool actuals_are_values = true;
if (fi.num_entries() != 0) {
for (unsigned i = 0; actuals_are_values && i < fi.get_arity(); i++) {
actuals_are_values = fi.m().is_value(args[i]);
@ -462,16 +461,16 @@ bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & resu
result = entry->get_result();
return true;
}
TRACE("func_interp", tout << "failed to find entry for: ";
for(unsigned i = 0; i < fi.get_arity(); i++)
tout << mk_pp(args[i], fi.m()) << " ";
TRACE("func_interp", tout << "failed to find entry for: ";
for(unsigned i = 0; i < fi.get_arity(); i++)
tout << mk_pp(args[i], fi.m()) << " ";
tout << "\nis partial: " << fi.is_partial() << "\n";);
if (!fi.eval_else(args, result)) {
return false;
}
if (actuals_are_values && fi.args_are_values()) {
// cheap case... we are done
return true;
@ -506,14 +505,14 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
SASSERT(is_well_sorted(m_manager, e));
TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n";
tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";);
obj_map<expr, expr*> eval_cache;
expr_ref_vector trail(m_manager);
sbuffer<std::pair<expr*, expr*>, 128> todo;
ptr_buffer<expr> args;
expr * null = static_cast<expr*>(0);
todo.push_back(std::make_pair(e, null));
simplifier m_simplifier(m_manager);
expr * a;
@ -528,7 +527,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
SASSERT(r != 0);
todo.pop_back();
eval_cache.insert(a, r);
TRACE("model_eval",
TRACE("model_eval",
tout << "orig:\n" << mk_pp(a, m_manager) << "\n";
tout << "after beta reduction:\n" << mk_pp(expanded_a, m_manager) << "\n";
tout << "new:\n" << mk_pp(r, m_manager) << "\n";);
@ -556,7 +555,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
SASSERT(args.size() == t->get_num_args());
expr_ref new_t(m_manager);
func_decl * f = t->get_decl();
if (!has_interpretation(f)) {
// the model does not assign an interpretation to f.
SASSERT(new_t.get() == 0);
@ -606,7 +605,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
if (!::eval(*fi, m_simplifier, args.c_ptr(), r1)) {
SASSERT(fi->is_partial()); // fi->eval only fails when fi is partial.
if (model_completion) {
expr * r = get_some_value(f->get_range());
expr * r = get_some_value(f->get_range());
fi->set_else(r);
SASSERT(!fi->is_partial());
new_t = r;
@ -635,7 +634,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
}
}
}
TRACE("model_eval",
TRACE("model_eval",
tout << "orig:\n" << mk_pp(t, m_manager) << "\n";
tout << "new:\n" << mk_pp(new_t, m_manager) << "\n";);
todo.pop_back();
@ -643,12 +642,12 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
eval_cache.insert(t, new_t);
break;
}
case AST_VAR:
case AST_VAR:
SASSERT(a != 0);
eval_cache.insert(a, a);
todo.pop_back();
break;
case AST_QUANTIFIER:
case AST_QUANTIFIER:
TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";);
is_ok = false; // evaluator does not handle quantifiers.
SASSERT(a != 0);
@ -669,12 +668,12 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
result = a;
std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n";
TRACE("model_eval",
TRACE("model_eval",
ast_ll_pp(tout << "original: ", m_manager, e);
ast_ll_pp(tout << "evaluated: ", m_manager, a);
ast_ll_pp(tout << "reduced: ", m_manager, result.get());
tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";
);
);
SASSERT(is_well_sorted(m_manager, result.get()));
return is_ok;
}

2
src/smt/smt_farkas_util.cpp
View file

@ -62,7 +62,7 @@ namespace smt {
app* farkas_util::mk_ge(expr* e1, expr* e2) {
mk_coerce(e1, e2);
return a.mk_gt(e1, e2);
return a.mk_ge(e1, e2);
}
app* farkas_util::mk_gt(expr* e1, expr* e2) {

3
src/smt/theory_arith_core.h
View file

@ -3212,7 +3212,8 @@ namespace smt {
template<typename Ext>
bool theory_arith<Ext>::get_value(enode * n, expr_ref & r) {
theory_var v = n->get_th_var(get_id());
return v != null_theory_var && to_expr(get_value(v), is_int(v), r);
inf_numeral val;
return v != null_theory_var && (val = get_value(v), (!is_int(v) || val.is_int())) && to_expr(val, is_int(v), r);
}
template<typename Ext>

380
src/smt/theory_seq.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History:
// Use instead reference counts for dependencies to GC?
--*/
@ -258,7 +257,7 @@ final_check_status theory_seq::final_check_eh() {
TRACE("seq", tout << ">>fixed_length\n";);
return FC_CONTINUE;
}
if (branch_variable()) {
if (reduce_length_eq() || branch_unit_variable() || branch_binary_variable() || branch_variable_mb() || branch_variable()) {
++m_stats.m_branch_variable;
TRACE("seq", tout << ">>branch_variable\n";);
return FC_CONTINUE;
@ -291,8 +290,7 @@ final_check_status theory_seq::final_check_eh() {
return FC_GIVEUP;
}
bool theory_seq::branch_variable() {
bool theory_seq::reduce_length_eq() {
context& ctx = get_context();
unsigned sz = m_eqs.size();
int start = ctx.get_random_value();
@ -304,25 +302,344 @@ bool theory_seq::branch_variable() {
return true;
}
}
return false;
}
bool theory_seq::branch_binary_variable() {
unsigned sz = m_eqs.size();
for (unsigned i = 0; i < sz; ++i) {
eq const& e = m_eqs[i];
if (branch_binary_variable(e)) {
return true;
}
}
return false;
}
bool theory_seq::branch_binary_variable(eq const& e) {
if (is_complex(e)) {
return false;
}
ptr_vector<expr> xs, ys;
expr* x, *y;
bool is_binary = is_binary_eq(e.ls(), e.rs(), x, xs, ys, y);
if (!is_binary) {
is_binary = is_binary_eq(e.rs(), e.ls(), x, xs, ys, y);
}
if (!is_binary) {
return false;
}
if (x == y) {
return false;
}
// Equation is of the form x ++ xs = ys ++ y
// where xs, ys are units.
// x is either a prefix of ys, all of ys ++ y or ys ++ y1, such that y = y1 ++ y2, y2 = xs
rational lenX, lenY;
context& ctx = get_context();
if (branch_variable(e)) {
return true;
}
if (!get_length(x, lenX)) {
enforce_length(ensure_enode(x));
return true;
}
if (!get_length(y, lenY)) {
enforce_length(ensure_enode(y));
return true;
}
if (lenX + rational(xs.size()) != lenY + rational(ys.size())) {
// |x| - |y| = |ys| - |xs|
expr_ref a(mk_sub(m_util.str.mk_length(x), m_util.str.mk_length(y)), m);
expr_ref b(m_autil.mk_int(ys.size()-xs.size()), m);
propagate_lit(e.dep(), 0, 0, mk_eq(a, b, false));
return true;
}
if (lenX <= rational(ys.size())) {
expr_ref_vector Ys(m);
Ys.append(ys.size(), ys.c_ptr());
branch_unit_variable(e.dep(), x, Ys);
return true;
}
expr_ref le(m_autil.mk_le(m_util.str.mk_length(x), m_autil.mk_int(ys.size())), m);
literal lit = mk_literal(le);
if (l_false == ctx.get_assignment(lit)) {
// |x| > |ys| => x = ys ++ y1, y = y1 ++ y2, y2 = xs
expr_ref Y1(mk_skolem(symbol("seq.left"), x, y), m);
expr_ref Y2(mk_skolem(symbol("seq.right"), x, y), m);
ys.push_back(Y1);
expr_ref ysY1(m_util.str.mk_concat(ys.size(), ys.c_ptr()), m);
expr_ref xsE(m_util.str.mk_concat(xs.size(), xs.c_ptr()), m);
expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m);
literal_vector lits;
lits.push_back(~lit);
dependency* dep = e.dep();
propagate_eq(dep, lits, x, ysY1, true);
propagate_eq(dep, lits, y, Y1Y2, true);
propagate_eq(dep, lits, Y2, xsE, true);
}
else {
ctx.mark_as_relevant(lit);
}
return true;
}
bool theory_seq::branch_unit_variable() {
unsigned sz = m_eqs.size();
for (unsigned i = 0; i < sz; ++i) {
eq const& e = m_eqs[i];
if (is_unit_eq(e.ls(), e.rs())) {
branch_unit_variable(e.dep(), e.ls()[0], e.rs());
return true;
}
else if (is_unit_eq(e.rs(), e.ls())) {
branch_unit_variable(e.dep(), e.rs()[0], e.ls());
return true;
}
}
return false;
}
/**
\brief ls := X... == rs := abcdef
*/
bool theory_seq::is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs) {
if (ls.empty() || !is_var(ls[0])) {
return false;
}
for (unsigned i = 0; i < rs.size(); ++i) {
if (!m_util.str.is_unit(rs[i])) {
return false;
}
}
return true;
}
void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units) {
SASSERT(is_var(X));
context& ctx = get_context();
rational lenX;
if (!get_length(X, lenX)) {
enforce_length(ensure_enode(X));
return;
}
if (lenX > rational(units.size())) {
expr_ref le(m_autil.mk_le(m_util.str.mk_length(X), m_autil.mk_int(units.size())), m);
propagate_lit(dep, 0, 0, mk_literal(le));
return;
}
SASSERT(lenX.is_unsigned());
unsigned lX = lenX.get_unsigned();
if (lX == 0) {
set_empty(X);
}
else {
literal lit = mk_eq(m_autil.mk_int(lX), m_util.str.mk_length(X), false);
if (l_true == ctx.get_assignment(lit)) {
expr_ref R(m_util.str.mk_concat(lX, units.c_ptr()), m);
literal_vector lits;
lits.push_back(lit);
propagate_eq(dep, lits, X, R, true);
}
else {
ctx.mark_as_relevant(lit);
ctx.force_phase(lit);
}
}
}
bool theory_seq::branch_variable_mb() {
context& ctx = get_context();
bool change = false;
for (unsigned i = 0; i < m_eqs.size(); ++i) {
eq const& e = m_eqs[i];
vector<rational> len1, len2;
if (!is_complex(e)) {
continue;
}
if (e.ls().empty() || e.rs().empty() ||
(!is_var(e.ls()[0]) && !is_var(e.rs()[0]))) {
continue;
}
if (!enforce_length(e.ls(), len1) || !enforce_length(e.rs(), len2)) {
change = true;
continue;
}
rational l1, l2;
for (unsigned j = 0; j < len1.size(); ++j) l1 += len1[j];
for (unsigned j = 0; j < len2.size(); ++j) l2 += len2[j];
if (l1 != l2) {
TRACE("seq", tout << "lengths are not compatible\n";);
expr_ref l = mk_concat(e.ls().size(), e.ls().c_ptr());
expr_ref r = mk_concat(e.rs().size(), e.rs().c_ptr());
expr_ref lnl(m_util.str.mk_length(l), m), lnr(m_util.str.mk_length(r), m);
literal_vector lits;
propagate_eq(e.dep(), lits, lnl, lnr, false);
change = true;
continue;
}
if (split_lengths(e.dep(), e.ls(), e.rs(), len1, len2)) {
TRACE("seq", tout << "split lengths\n";);
return true;
}
}
return change;
}
unsigned s = 0;
bool theory_seq::is_complex(eq const& e) {
unsigned num_vars1 = 0, num_vars2 = 0;
for (unsigned i = 0; i < e.ls().size(); ++i) {
if (is_var(e.ls()[i])) ++num_vars1;
}
for (unsigned i = 0; i < e.rs().size(); ++i) {
if (is_var(e.rs()[i])) ++num_vars2;
}
return num_vars1 > 0 && num_vars2 > 0 && num_vars1 + num_vars2 > 2;
}
/*
\brief Decompose ls = rs into Xa = bYc, such that
1.
- X != Y
- |b| <= |X| <= |bY| in currrent model
- b is non-empty.
2. X != Y
- b is empty
- |X| <= |Y|
3. |X| = 0
- propagate X = empty
*/
bool theory_seq::split_lengths(dependency* dep,
expr_ref_vector const& ls, expr_ref_vector const& rs,
vector<rational> const& ll, vector<rational> const& rl) {
context& ctx = get_context();
expr_ref X(m), Y(m), b(m);
if (ls.empty() || rs.empty()) {
return false;
}
if (is_var(ls[0]) && ll[0].is_zero()) {
return set_empty(ls[0]);
}
if (is_var(rs[0]) && rl[0].is_zero()) {
return set_empty(rs[0]);
}
if (is_var(rs[0]) && !is_var(ls[0])) {
return split_lengths(dep, rs, ls, rl, ll);
}
if (!is_var(ls[0])) {
return false;
}
X = ls[0];
rational lenX = ll[0];
expr_ref_vector bs(m);
SASSERT(lenX.is_pos());
rational lenB(0), lenY(0);
for (unsigned i = 0; lenX > lenB && i < rs.size(); ++i) {
bs.push_back(rs[i]);
lenY = rl[i];
lenB += lenY;
}
SASSERT(lenX <= lenB);
SASSERT(!bs.empty());
Y = bs.back();
bs.pop_back();
if (!is_var(Y) && !m_util.str.is_unit(Y)) {
TRACE("seq", tout << "TBD: non variable or unit split: " << Y << "\n";);
return false;
}
if (X == Y) {
TRACE("seq", tout << "Cycle: " << X << "\n";);
return false;
}
if (lenY.is_zero()) {
return set_empty(Y);
}
b = mk_concat(bs, m.get_sort(X));
SASSERT(X != Y);
// |b| < |X| <= |b| + |Y| => x = bY1, Y = Y1Y2
expr_ref lenXE(m_util.str.mk_length(X), m);
expr_ref lenYE(m_util.str.mk_length(Y), m);
expr_ref lenb(m_util.str.mk_length(b), m);
expr_ref le1(m_autil.mk_le(mk_sub(lenXE, lenb), m_autil.mk_int(0)), m);
expr_ref le2(m_autil.mk_le(mk_sub(mk_sub(lenXE, lenb), lenYE),
m_autil.mk_int(0)), m);
literal lit1(~mk_literal(le1));
literal lit2(mk_literal(le2));
literal_vector lits;
lits.push_back(lit1);
lits.push_back(lit2);
if (ctx.get_assignment(lit1) != l_true ||
ctx.get_assignment(lit2) != l_true) {
ctx.mark_as_relevant(lit1);
ctx.mark_as_relevant(lit2);
}
else if (m_util.str.is_unit(Y)) {
SASSERT(lenB == lenX);
bs.push_back(Y);
expr_ref bY(m_util.str.mk_concat(bs), m);
propagate_eq(dep, lits, X, bY, true);
}
else {
SASSERT(is_var(Y));
expr_ref Y1(mk_skolem(symbol("seq.left"), X, b, Y), m);
expr_ref Y2(mk_skolem(symbol("seq.right"), X, b, Y), m);
expr_ref bY1(m_util.str.mk_concat(b, Y1), m);
expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m);
propagate_eq(dep, lits, X, bY1, true);
propagate_eq(dep, lits, Y, Y1Y2, true);
}
return true;
}
bool theory_seq::set_empty(expr* x) {
add_axiom(~mk_eq(m_autil.mk_int(0), m_util.str.mk_length(x), false), mk_eq_empty(x));
return true;
}
bool theory_seq::enforce_length(expr_ref_vector const& es, vector<rational> & len) {
bool all_have_length = true;
rational val;
zstring s;
for (unsigned i = 0; i < es.size(); ++i) {
expr* e = es[i];
if (m_util.str.is_unit(e)) {
len.push_back(rational(1));
}
else if (m_util.str.is_empty(e)) {
len.push_back(rational(0));
}
else if (m_util.str.is_string(e, s)) {
len.push_back(rational(s.length()));
}
else if (get_length(e, val)) {
len.push_back(val);
}
else {
enforce_length(ensure_enode(e));
all_have_length = false;
}
}
return all_have_length;
}
bool theory_seq::branch_variable() {
context& ctx = get_context();
unsigned sz = m_eqs.size();
int start = ctx.get_random_value();
for (unsigned i = 0; i < sz; ++i) {
unsigned k = (i + start) % sz;
eq const& e = m_eqs[k];
unsigned id = e.id();
s = find_branch_start(2*id);
TRACE("seq", tout << s << " " << id << ": " << e.ls() << " = " << e.rs() << "\n";);
bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs());
insert_branch_start(2*id, s);
if (found) {
return true;
}
s = find_branch_start(2*id + 1);
found = find_branch_candidate(s, e.dep(), e.rs(), e.ls());
insert_branch_start(2*id + 1, s);
if (found) {
if (branch_variable(e)) {
return true;
}
@ -338,6 +655,22 @@ bool theory_seq::branch_variable() {
return ctx.inconsistent();
}
bool theory_seq::branch_variable(eq const& e) {
unsigned id = e.id();
unsigned s = find_branch_start(2*id);
TRACE("seq", tout << s << " " << id << ": " << e.ls() << " = " << e.rs() << "\n";);
bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs());
insert_branch_start(2*id, s);
if (found) {
return true;
}
s = find_branch_start(2*id + 1);
found = find_branch_candidate(s, e.dep(), e.rs(), e.ls());
insert_branch_start(2*id + 1, s);
return found;
}
void theory_seq::insert_branch_start(unsigned k, unsigned s) {
m_branch_start.insert(k, s);
m_trail_stack.push(pop_branch(k));
@ -483,7 +816,6 @@ lbool theory_seq::assume_equality(expr* l, expr* r) {
return l_false;
}
return ctx.get_assignment(mk_eq(l, r, false));
//return l_undef;
}
@ -1901,12 +2233,15 @@ void theory_seq::display(std::ostream & out) const {
void theory_seq::display_equations(std::ostream& out) const {
for (unsigned i = 0; i < m_eqs.size(); ++i) {
eq const& e = m_eqs[i];
out << e.ls() << " = " << e.rs() << " <- \n";
display_deps(out, e.dep());
display_equation(out, m_eqs[i]);
}
}
void theory_seq::display_equation(std::ostream& out, eq const& e) const {
out << e.ls() << " = " << e.rs() << " <- \n";
display_deps(out, e.dep());
}
void theory_seq::display_disequations(std::ostream& out) const {
bool first = true;
for (unsigned i = 0; i < m_nqs.size(); ++i) {
@ -3050,6 +3385,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
else if (m_util.str.is_in_re(e)) {
propagate_in_re(e, is_true);
}
else if (is_skolem(symbol("seq.split"), e)) {
// propagate equalities
}
else {
UNREACHABLE();
}

15
src/smt/theory_seq.h
View file

@ -358,6 +358,10 @@ namespace smt {
void init_model(expr_ref_vector const& es);
// final check
bool simplify_and_solve_eqs(); // solve unitary equalities
bool reduce_length_eq();
bool branch_unit_variable(); // branch on XYZ = abcdef
bool branch_binary_variable(); // branch on abcX = Ydefg
bool branch_variable_mb(); // branch on a variable, model based on length
bool branch_variable(); // branch on a variable
bool split_variable(); // split a variable
bool is_solved();
@ -366,7 +370,16 @@ namespace smt {
bool check_length_coherence(expr* e);
bool fixed_length();
bool fixed_length(expr* e);
void branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units);
bool branch_variable(eq const& e);
bool branch_binary_variable(eq const& e);
bool is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs);
bool propagate_length_coherence(expr* e);
bool split_lengths(dependency* dep,
expr_ref_vector const& ls, expr_ref_vector const& rs,
vector<rational> const& ll, vector<rational> const& rl);
bool set_empty(expr* x);
bool is_complex(eq const& e);
bool check_extensionality();
bool check_contains();
@ -465,6 +478,7 @@ namespace smt {
bool has_length(expr *e) const { return m_length.contains(e); }
void add_length(expr* e);
void enforce_length(enode* n);
bool enforce_length(expr_ref_vector const& es, vector<rational>& len);
void enforce_length_coherence(enode* n1, enode* n2);
void add_elim_string_axiom(expr* n);
@ -532,6 +546,7 @@ namespace smt {
// diagnostics
void display_equations(std::ostream& out) const;
void display_equation(std::ostream& out, eq const& e) const;
void display_disequations(std::ostream& out) const;
void display_disequation(std::ostream& out, ne const& e) const;
void display_deps(std::ostream& out, dependency* deps) const;

48
src/tactic/extension_model_converter.cpp
View file

@ -43,6 +43,41 @@ static void display_decls_info(std::ostream & out, model_ref & md) {
}
}
bool extension_model_converter::is_fi_entry_expr(expr * e, unsigned arity, ptr_vector<expr> & args) {
args.reset();
if (!is_app(e) || !m().is_ite(to_app(e)))
return false;
app * a = to_app(e);
expr * c = a->get_arg(0);
expr * t = a->get_arg(1);
expr * f = a->get_arg(2);
if ((arity == 0) ||
(arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) ||
(arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != arity)))
return false;
args.resize(arity, 0);
for (unsigned i = 0; i < arity; i++) {
expr * ci = (arity == 1 && i == 0) ? to_app(c) : to_app(c)->get_arg(i);
if (!m().is_eq(ci) || to_app(ci)->get_num_args() != 2)
return false;
expr * a0 = to_app(ci)->get_arg(0);
expr * a1 = to_app(ci)->get_arg(1);
if (is_var(a0) && to_var(a0)->get_idx() == i)
args[i] = a1;
else if (is_var(a1) && to_var(a1)->get_idx() == i)
args[i] = a0;
else
return false;
}
return true;
}
void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
SASSERT(goal_idx == 0);
TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md););
@ -62,7 +97,14 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
}
else {
func_interp * new_fi = alloc(func_interp, m(), arity);
new_fi->set_else(val);
expr * e = val.get();
ptr_vector<expr> args;
while (is_fi_entry_expr(e, arity, args)) {
TRACE("extension_mc", tout << "fi entry: " << mk_ismt2_pp(e, m()) << std::endl;);
new_fi->insert_entry(args.c_ptr(), to_app(e)->get_arg(1));
e = to_app(e)->get_arg(2);
}
new_fi->set_else(e);
md->register_decl(f, new_fi);
}
}
@ -86,10 +128,10 @@ void extension_model_converter::display(std::ostream & out) {
}
model_converter * extension_model_converter::translate(ast_translation & translator) {
extension_model_converter * res = alloc(extension_model_converter, translator.to());
extension_model_converter * res = alloc(extension_model_converter, translator.to());
for (unsigned i = 0; i < m_vars.size(); i++)
res->m_vars.push_back(translator(m_vars[i].get()));
for (unsigned i = 0; i < m_defs.size(); i++)
res->m_defs.push_back(translator(m_defs[i].get()));
res->m_defs.push_back(translator(m_defs[i].get()));
return res;
}

11
src/tactic/extension_model_converter.h
View file

@ -27,14 +27,14 @@ Notes:
class extension_model_converter : public model_converter {
func_decl_ref_vector m_vars;
expr_ref_vector m_defs;
public:
public:
extension_model_converter(ast_manager & m):m_vars(m), m_defs(m) {
}
virtual ~extension_model_converter();
ast_manager & m() const { return m_vars.get_manager(); }
virtual void operator()(model_ref & md, unsigned goal_idx);
virtual void display(std::ostream & out);
@ -43,6 +43,9 @@ public:
void insert(func_decl * v, expr * def);
virtual model_converter * translate(ast_translation & translator);
private:
bool is_fi_entry_expr(expr * e, unsigned arity, ptr_vector<expr> & args);
};