mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

strengthen support for int.to.str and length reasoning. Issue #589

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-28 12:26:47 -07:00
parent 8c99d3c431
commit c3f498a640
9 changed files with 103 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/ast/ast.cpp
View file

@ -1420,7 +1420,7 @@ ast_manager::~ast_manager() {
std::cout << to_sort(a)->get_name() << "\n";
}
else {
std::cout << mk_ll_pp(a, *this, false);
std::cout << mk_ll_pp(a, *this, false) << "id: " << a->get_id() << "\n";
}
}
});
@ -1575,6 +1575,26 @@ bool ast_manager::are_equal(expr * a, expr * b) const {
return false;
}
void ast_manager::inc_ref(ast * n) {
if (n && n->get_id() == 362568) {
std::cout << "inc-ref " << n->get_ref_count() << "\n";
}
if (n)
n->inc_ref();
}
void ast_manager::dec_ref(ast* n) {
if (n && n->get_id() == 362568) {
std::cout << "dec-ref " << n->get_ref_count() << "\n";
}
if (n) {
n->dec_ref();
if (n->get_ref_count() == 0)
delete_node(n);
}
}
bool ast_manager::are_distinct(expr* a, expr* b) const {
if (is_app(a) && is_app(b)) {
app* ap = to_app(a), *bp = to_app(b);

13
src/ast/ast.h
View file

@ -1571,18 +1571,9 @@ public:
void debug_ref_count() { m_debug_ref_count = true; }
void inc_ref(ast * n) {
if (n)
n->inc_ref();
}
void inc_ref(ast * n);
void dec_ref(ast * n) {
if (n) {
n->dec_ref();
if (n->get_ref_count() == 0)
delete_node(n);
}
}
void dec_ref(ast * n);
template<typename T>
void inc_array_ref(unsigned sz, T * const * a) {

14
src/cmd_context/cmd_context.cpp
View file

@ -1487,18 +1487,18 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
return;
}
display_sat_result(r);
if (r == l_true) {
validate_model();
}
validate_check_sat_result(r);
if (was_opt && r != l_false && !was_pareto) {
get_opt()->display_assignment(regular_stream());
}
if (r == l_true) {
validate_model();
if (m_params.m_dump_models) {
model_ref md;
get_check_sat_result()->get_model(md);
display_model(md);
}
if (r == l_true && m_params.m_dump_models) {
model_ref md;
get_check_sat_result()->get_model(md);
display_model(md);
}
}

18
src/muz/rel/dl_compiler.cpp
View file

@ -26,7 +26,8 @@ Revision History:
#include"dl_util.h"
#include"dl_compiler.h"
#include"ast_pp.h"
#include"ast_smt2_pp.h"
// include"ast_smt2_pp.h"
#include"ast_util.h"
namespace datalog {
@ -185,10 +186,11 @@ namespace datalog {
}
}
void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result,
void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort& s, reg_idx & result,
bool & dealloc, instruction_block & acc) {
TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";);
TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager())
<< " " << m_context.get_rel_context()->get_rmanager().to_nice_string(s) << "\n";);
IF_VERBOSE(3, {
expr_ref e(m_context.get_manager());
m_context.get_rule_manager().to_formula(*compiled_rule, e);
@ -328,13 +330,15 @@ namespace datalog {
continue;
}
unsigned bound_column_index;
if(acis[i].kind!=ACK_UNBOUND_VAR || !handled_unbound.find(acis[i].var_index,bound_column_index)) {
if(acis[i].kind != ACK_UNBOUND_VAR || !handled_unbound.find(acis[i].var_index,bound_column_index)) {
bound_column_index=curr_sig->size();
if(acis[i].kind==ACK_CONSTANT) {
make_add_constant_column(head_pred, curr, acis[i].domain, acis[i].constant, curr, dealloc, acc);
}
else {
SASSERT(acis[i].kind==ACK_UNBOUND_VAR);
TRACE("dl", tout << head_pred->get_name() << " index: " << i
<< " " << m_context.get_rel_context()->get_rmanager().to_nice_string(acis[i].domain) << "\n";);
make_add_unbound_column(compiled_rule, i, head_pred, curr, acis[i].domain, curr, dealloc, acc);
handled_unbound.insert(acis[i].var_index,bound_column_index);
}
@ -598,14 +602,15 @@ namespace datalog {
// add unbounded columns for interpreted filter
unsigned ut_len = r->get_uninterpreted_tail_size();
unsigned ft_len = r->get_tail_size(); // full tail
ptr_vector<expr> tail;
expr_ref_vector tail(m);
for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) {
tail.push_back(r->get_tail(tail_index));
}
expr_ref_vector binding(m);
if (!tail.empty()) {
app_ref filter_cond(tail.size() == 1 ? to_app(tail.back()) : m.mk_and(tail.size(), tail.c_ptr()), m);
expr_ref filter_cond = mk_and(tail);
m_free_vars.reset();
m_free_vars(filter_cond);
// create binding
binding.resize(m_free_vars.size()+1);
@ -620,6 +625,7 @@ namespace datalog {
} else {
// we have an unbound variable, so we add an unbound column for it
relation_sort unbound_sort = m_free_vars[v];
TRACE("dl", tout << "unbound: " << v << "\n" << filter_cond << " " << mk_pp(unbound_sort, m) << "\n";);
make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, filtered_res, dealloc, acc);
src_col = single_res_expr.size();

2
src/muz/rel/dl_compiler.h
View file

@ -180,7 +180,7 @@ namespace datalog {
void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort s, const relation_element val,
reg_idx & result, bool & dealloc, instruction_block & acc);
void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result,
void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort& s, reg_idx & result,
bool & dealloc, instruction_block & acc);
void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result,
instruction_block & acc);

3
src/muz/rel/dl_instruction.cpp
View file

@ -1052,7 +1052,8 @@ namespace datalog {
}
virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const {
out << "mk_total into " << m_tgt << " sort:"
<< ctx.get_rel_context().get_rmanager().to_nice_string(m_sig);
<< ctx.get_rel_context().get_rmanager().to_nice_string(m_sig)
<< " " << m_pred->get_name();
}
virtual void make_annotations(execution_context & ctx) {
std::string s;

4
src/muz/rel/dl_relation_manager.cpp
View file

@ -488,7 +488,9 @@ namespace datalog {
}
std::string relation_manager::to_nice_string(const relation_sort & s) const {
return std::string(s->get_name().bare_str());
std::ostringstream strm;
strm << mk_pp(s, get_context().get_manager());
return strm.str();
}
std::string relation_manager::to_nice_string(const relation_signature & s) const {

57
src/smt/theory_seq.cpp
View file

@ -1398,7 +1398,9 @@ bool theory_seq::is_var(expr* a) {
!m_util.str.is_concat(a) &&
!m_util.str.is_empty(a) &&
!m_util.str.is_string(a) &&
!m_util.str.is_unit(a);
!m_util.str.is_unit(a) &&
!m_util.str.is_itos(a) &&
!m.is_ite(a);
}
@ -2216,7 +2218,10 @@ bool theory_seq::add_itos_axiom(expr* e) {
m_itos_axioms.insert(val);
app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);
expr_ref n1(arith_util(m).mk_numeral(val, true), m);
add_axiom(mk_eq(m_util.str.mk_itos(n1), e1, false));
add_axiom(~mk_eq(n1, n , false), mk_eq(e, e1, false));
add_axiom(mk_eq(n1, n, false), ~mk_eq(e, e1, false));
m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_itos_axioms, val));
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
return true;
@ -2883,7 +2888,7 @@ void theory_seq::add_length_axiom(expr* n) {
add_axiom(mk_eq(len, n, false));
}
else if (m_util.str.is_itos(x)) {
add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(1))));
add_itos_length_axiom(n);
}
else {
add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
@ -2891,6 +2896,52 @@ void theory_seq::add_length_axiom(expr* n) {
if (!ctx.at_base_level()) {
m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
}
}
void theory_seq::add_itos_length_axiom(expr* len) {
expr* x, *n;
VERIFY(m_util.str.is_length(len, x));
VERIFY(m_util.str.is_itos(x, n));
add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(1))));
rational val;
if (get_value(n, val)) {
bool neg = val.is_neg();
rational ten(10);
if (neg) val.neg();
unsigned num_char = neg?2:1;
// 0 < x < 10
// 10 < x < 100
// 100 < x < 1000
rational hi(10);
while (val > hi) {
++num_char;
hi *= ten;
}
rational lo(div(hi - rational(1), ten));
literal len_le(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(num_char))));
literal len_ge(mk_literal(m_autil.mk_le(len, m_autil.mk_int(num_char))));
if (neg) {
// n <= -lo => len >= num_char
// -hi < n <= 0 => len <= num_char
// n <= -hi or ~(n <= 0) or len <= num_char
literal l1(mk_literal(m_autil.mk_le(n, m_autil.mk_numeral(-lo, true))));
add_axiom(~l1, len_ge);
literal l3(mk_literal(m_autil.mk_le(n, m_autil.mk_numeral(-hi, true))));
literal l4(mk_literal(m_autil.mk_le(n, m_autil.mk_int(0))));
add_axiom(l3, ~l4, len_le);
}
else {
// n >= lo => len >= num_char
// 0 <= n < hi => len <= num_char
literal l1(mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(lo, true))));
add_axiom(~l1, len_ge);
literal l3(mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(hi, true))));
literal l4(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
add_axiom(l3, ~l4, len_le);
}
}
}

1
src/smt/theory_seq.h
View file

@ -494,6 +494,7 @@ namespace smt {
void add_at_axiom(expr* n);
void add_in_re_axiom(expr* n);
bool add_itos_axiom(expr* n);
void add_itos_length_axiom(expr* n);
literal mk_literal(expr* n);
literal mk_eq_empty(expr* n, bool phase = true);
literal mk_seq_eq(expr* a, expr* b);