From 5635016205279623e2c00420934525c9fe22d801 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 9 Nov 2016 18:06:02 -0500 Subject: [PATCH] theory_str str.from-int very WIP --- src/smt/theory_str.cpp | 98 ++++++++++++++++++++++++++++++++++++++++-- src/smt/theory_str.h | 4 ++ 2 files changed, 98 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 40dc3f42f..881045815 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -924,6 +924,8 @@ void theory_str::propagate() { enode * e = m_library_aware_axiom_todo[i]; if (is_str_to_int(e)) { instantiate_axiom_str_to_int(e); + } else if (is_int_to_str(e)) { + instantiate_axiom_int_to_str(e); } else { TRACE("t_str", tout << "BUG: unhandled library-aware term " << mk_pp(e->get_owner(), get_manager()) << std::endl;); NOT_IMPLEMENTED_YET(); @@ -1637,6 +1639,30 @@ void theory_str::instantiate_axiom_str_to_int(enode * e) { } } +void theory_str::instantiate_axiom_int_to_str(enode * e) { + context & ctx = get_context(); + ast_manager & m = get_manager(); + + app * ex = e->get_owner(); + if (axiomatized_terms.contains(ex)) { + TRACE("t_str_detail", tout << "already set up str.from-int axiom for " << mk_pp(ex, m) << std::endl;); + return; + } + axiomatized_terms.insert(ex); + + TRACE("t_str_detail", tout << "instantiate str.from-int axiom for " << mk_pp(ex, m) << std::endl;); + + // axiom 1: N < 0 <==> (str.from-int N) = "" + expr * N = ex->get_arg(0); + { + expr_ref axiom1_lhs(m.mk_not(m_autil.mk_ge(N, m_autil.mk_numeral(rational::zero(), true))), m); + expr_ref axiom1_rhs(ctx.mk_eq_atom(ex, m_strutil.mk_string("")), m); + expr_ref axiom1(ctx.mk_eq_atom(axiom1_lhs, axiom1_rhs), m); + SASSERT(axiom1); + assert_axiom(axiom1); + } +} + expr * theory_str::mk_RegexIn(expr * str, expr * regexp) { expr * args[2] = {str, regexp}; app * regexIn = get_manager().mk_app(get_id(), OP_RE_REGEXIN, 0, 0, 2, args); @@ -6476,7 +6502,7 @@ void theory_str::set_up_axioms(expr * ex) { m_axiom_Indexof2_todo.push_back(n); } else if (is_LastIndexof(ap)) { m_axiom_LastIndexof_todo.push_back(n); - } else if (is_str_to_int(ap)) { + } else if (is_str_to_int(ap) || is_int_to_str(ap)) { string_int_conversion_terms.push_back(ap); m_library_aware_axiom_todo.push_back(n); } @@ -7630,7 +7656,7 @@ bool theory_str::finalcheck_str2int(app * a) { std::string Ival_str = Ival.to_string(); expr_ref premise(ctx.mk_eq_atom(a, m_autil.mk_numeral(Ival, true)), m); expr_ref conclusion(ctx.mk_eq_atom(S, m_strutil.mk_string(Ival_str)), m); - expr_ref axiom(m.mk_or(m.mk_not(premise), conclusion), m); + expr_ref axiom(rewrite_implication(premise, conclusion), m); if (!string_int_axioms.contains(axiom)) { string_int_axioms.insert(axiom); assert_axiom(axiom); @@ -7647,6 +7673,66 @@ bool theory_str::finalcheck_str2int(app * a) { return axiomAdd; } +bool theory_str::finalcheck_int2str(app * a) { + bool axiomAdd = false; + context & ctx = get_context(); + ast_manager & m = get_manager(); + + expr * N = a->get_arg(0); + + // check string theory + bool Sval_expr_exists; + expr * Sval_expr = get_eqc_value(a, Sval_expr_exists); + if (Sval_expr_exists) { + std::string Sval = m_strutil.get_string_constant_value(Sval_expr); + TRACE("t_str_detail", tout << "string theory assigns \"" << mk_pp(a, m) << " = " << Sval << std::endl;); + // empty string --> integer value < 0 + if (Sval.empty()) { + // ignore this. we should already assert the axiom for what happens when the string is "" + } else { + // nonempty string --> convert to correct integer value, or disallow it + // TODO think about whether we need to persist the axiom in this case? + rational convertedRepresentation(0); + rational ten(10); + bool conversionOK = true; + for (unsigned i = 0; i < Sval.length(); ++i) { + char digit = Sval.at(i); + if (isdigit((int)digit)) { + std::string sDigit(1, digit); + int val = atoi(sDigit.c_str()); + convertedRepresentation = (ten * convertedRepresentation) + rational(val); + } else { + // not a digit, invalid + TRACE("t_str_rw", tout << "str.to-int argument contains non-digit character '" << digit << "'" << std::endl;); + conversionOK = false; + break; + } + } + if (conversionOK) { + expr_ref premise(ctx.mk_eq_atom(a, m_strutil.mk_string(Sval)), m); + expr_ref conclusion(ctx.mk_eq_atom(N, m_autil.mk_numeral(convertedRepresentation, true)), m); + expr_ref axiom(rewrite_implication(premise, conclusion), m); + if (!string_int_axioms.contains(axiom)) { + string_int_axioms.insert(axiom); + assert_axiom(axiom); + m_trail_stack.push(insert_obj_trail(string_int_axioms, axiom)); + axiomAdd = true; + } + } else { + expr_ref axiom(m.mk_not(ctx.mk_eq_atom(a, m_strutil.mk_string(Sval))), m); + // always assert this axiom because this is a conflict clause + assert_axiom(axiom); + axiomAdd = true; + } + } + } else { + TRACE("t_str_detail", tout << "string theory has no assignment for " << mk_pp(a, m) << std::endl;); + NOT_IMPLEMENTED_YET(); + } + // TODO also check assignment in integer theory + return axiomAdd; +} + final_check_status theory_str::final_check_eh() { context & ctx = get_context(); ast_manager & m = get_manager(); @@ -7758,9 +7844,13 @@ final_check_status theory_str::final_check_eh() { if (axiomAdd) { addedStrIntAxioms = true; } + } else if (is_int_to_str(ex)) { + bool axiomAdd = finalcheck_int2str(ex); + if (axiomAdd) { + addedStrIntAxioms = true; + } } else { - // TODO int.to-str - NOT_IMPLEMENTED_YET(); + UNREACHABLE(); } } if (addedStrIntAxioms) { diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index e99774034..c7d931d1e 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -359,6 +359,8 @@ namespace smt { bool is_Replace(enode const * n) const { return is_Replace(n->get_owner()); } bool is_str_to_int(app const * a) const { return a->is_app_of(get_id(), OP_STR_STR2INT); } bool is_str_to_int(enode const * n) const { return is_str_to_int(n->get_owner()); } + bool is_int_to_str(app const * a) const { return a->is_app_of(get_id(), OP_STR_INT2STR); } + bool is_int_to_str(enode const * n) const { return is_int_to_str(n->get_owner()); } bool is_RegexIn(app const * a) const { return a->is_app_of(get_id(), OP_RE_REGEXIN); } bool is_RegexIn(enode const * n) const { return is_RegexIn(n->get_owner()); } @@ -388,6 +390,7 @@ namespace smt { void instantiate_axiom_Substr(enode * e); void instantiate_axiom_Replace(enode * e); void instantiate_axiom_str_to_int(enode * e); + void instantiate_axiom_int_to_str(enode * e); expr * mk_RegexIn(expr * str, expr * regexp); void instantiate_axiom_RegexIn(enode * e); @@ -510,6 +513,7 @@ namespace smt { expr * eval_concat(expr * n1, expr * n2); bool finalcheck_str2int(app * a); + bool finalcheck_int2str(app * a); // strRegex