From be5cc02a4594c33b76fc1ca01586486071e0f272 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 13 Jun 2016 21:57:08 -0400 Subject: [PATCH] working axiomatization for CharAt --- src/ast/rewriter/str_rewriter.cpp | 4 +-- src/smt/theory_str.cpp | 49 ++++++++++++++++++++++++++++++- src/smt/theory_str.h | 7 +++++ 3 files changed, 57 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp index 3967453d4..76c0d25ae 100644 --- a/src/ast/rewriter/str_rewriter.cpp +++ b/src/ast/rewriter/str_rewriter.cpp @@ -42,8 +42,8 @@ br_status str_rewriter::mk_str_CharAt(expr * arg0, expr * arg1, expr_ref & resul result = m_strutil.mk_string(resultStr); return BR_DONE; } else { - // TODO NEXT - NOT_IMPLEMENTED_YET(); + // TODO if we ever figure out how to assert axioms in here, add this code + return BR_FAILED; /* Z3_ast ts0 = my_mk_internal_string_var(t); Z3_ast ts1 = my_mk_internal_string_var(t); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index aaeb9ccce..fe8f12e81 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -567,7 +567,9 @@ expr * theory_str::mk_concat(expr * n1, expr * n2) { } bool theory_str::can_propagate() { - return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty() || !m_concat_axiom_todo.empty(); + return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty() || !m_concat_axiom_todo.empty() + || !m_axiom_CharAt_todo.empty() + ; } void theory_str::propagate() { @@ -590,6 +592,11 @@ void theory_str::propagate() { instantiate_concat_axiom(m_concat_axiom_todo[i]); } m_concat_axiom_todo.reset(); + + for (unsigned i = 0; i < m_axiom_CharAt_todo.size(); ++i) { + instantiate_axiom_CharAt(m_axiom_CharAt_todo[i]); + } + m_axiom_CharAt_todo.reset(); } } @@ -738,6 +745,44 @@ void theory_str::instantiate_str_eq_length_axiom(enode * lhs, enode * rhs) { assert_implication(premise, conclusion); } +void theory_str::instantiate_axiom_CharAt(enode * e) { + context & ctx = get_context(); + ast_manager & m = get_manager(); + + app * expr = e->get_owner(); + + TRACE("t_str_detail", tout << "instantiate CharAt axiom for " << mk_pp(expr, m) << std::endl;); + + expr_ref ts0(mk_str_var("ts0"), m); + expr_ref ts1(mk_str_var("ts1"), m); + expr_ref ts2(mk_str_var("ts2"), m); + + expr_ref cond(m.mk_and( + m_autil.mk_ge(expr->get_arg(1), mk_int(0)), + // REWRITE for arithmetic theory: + // m_autil.mk_lt(expr->get_arg(1), mk_strlen(expr->get_arg(0))) + m.mk_not(m_autil.mk_ge(m_autil.mk_add(expr->get_arg(1), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(0)))), mk_int(0))) + ), m); + + expr_ref_vector and_item(m); + and_item.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(ts0, mk_concat(ts1, ts2)))); + and_item.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_strlen(ts0))); + and_item.push_back(ctx.mk_eq_atom(mk_strlen(ts1), mk_int(1))); + + expr_ref thenBranch(m.mk_and(and_item.size(), and_item.c_ptr()), m); + expr_ref elseBranch(ctx.mk_eq_atom(ts1, m_strutil.mk_string("")), m); + + expr_ref axiom(m.mk_ite(cond, thenBranch, elseBranch), m); + expr_ref reductionVar(ctx.mk_eq_atom(expr, ts1), m); + + SASSERT(axiom); + SASSERT(reductionVar); + + expr_ref finalAxiom(m.mk_and(axiom, reductionVar), m); + SASSERT(finalAxiom); + assert_axiom(finalAxiom); +} + void theory_str::attach_new_th_var(enode * n) { context & ctx = get_context(); theory_var v = mk_var(n); @@ -3469,6 +3514,8 @@ void theory_str::set_up_axioms(expr * ex) { if (aVar->get_num_args() == 0 && !is_string(aVar)) { input_var_in_len.insert(var); } + } else if (is_CharAt(ap)) { + m_axiom_CharAt_todo.push_back(n); } else if (ap->get_num_args() == 0 && !is_string(ap)) { // if ex is a variable, add it to our list of variables TRACE("t_str_detail", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 562f49004..c86328d30 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -106,6 +106,9 @@ namespace smt { ptr_vector m_concat_axiom_todo; ptr_vector m_string_constant_length_todo; + // enode lists for term-specific axioms + ptr_vector m_axiom_CharAt_todo; + int tmpStringVarCount; int tmpXorVarCount; int tmpLenTestVarCount; @@ -167,10 +170,14 @@ namespace smt { bool is_string(enode const * n) const { return is_string(n->get_owner()); } bool is_strlen(app const * a) const { return a->is_app_of(get_id(), OP_STRLEN); } bool is_strlen(enode const * n) const { return is_strlen(n->get_owner()); } + bool is_CharAt(app const * a) const { return a->is_app_of(get_id(), OP_STR_CHARAT); } + bool is_CharAt(enode const * n) const { return is_CharAt(n->get_owner()); } void instantiate_concat_axiom(enode * cat); void instantiate_basic_string_axioms(enode * str); void instantiate_str_eq_length_axiom(enode * lhs, enode * rhs); + void instantiate_axiom_CharAt(enode * e); + void set_up_axioms(expr * ex); void handle_equality(expr * lhs, expr * rhs);