From bdf755156cd761c1247d83cbb034306455b45a28 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 1 Oct 2015 20:31:40 -0400 Subject: [PATCH] fix model generation: don't build interpretations for Length() --- src/ast/str_decl_plugin.cpp | 16 +++++++++- src/ast/str_decl_plugin.h | 4 +++ src/smt/theory_str.cpp | 60 ++++++++++++++++++++++++++++++++----- src/smt/theory_str.h | 9 +++++- 4 files changed, 80 insertions(+), 9 deletions(-) diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp index c72a5dbc2..5589db56c 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/src/ast/str_decl_plugin.cpp @@ -64,7 +64,7 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) { MK_OP(m_concat_decl, "Concat", OP_STRCAT, s); - m_length_decl = m->mk_func_decl(symbol("Length"), s, i); m_manager->inc_ref(m_length_decl); + m_length_decl = m->mk_func_decl(symbol("Length"), s, i, func_decl_info(id, OP_STRLEN)); m_manager->inc_ref(m_length_decl); } decl_plugin * str_decl_plugin::mk_fresh() { @@ -120,6 +120,20 @@ app * str_decl_plugin::mk_string(const char * val) { return mk_string(key); } +app * str_decl_plugin::mk_fresh_string() { + // cheating. + // take the longest string in the cache, append the letter "A", and call it fresh. + std::string longestString = ""; + std::map::iterator it = string_cache.begin(); + for (; it != string_cache.end(); ++it) { + if (it->first.length() > longestString.length()) { + longestString = it->first; + } + } + longestString += "A"; + return mk_string(longestString); +} + void str_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { op_names.push_back(builtin_name("Concat", OP_STRCAT)); op_names.push_back(builtin_name("Length", OP_STRLEN)); diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h index 61d1bc2f2..f1978ab8b 100644 --- a/src/ast/str_decl_plugin.h +++ b/src/ast/str_decl_plugin.h @@ -62,6 +62,7 @@ public: app * mk_string(const char * val); app * mk_string(std::string & val); + app * mk_fresh_string(); virtual void get_op_names(svector & op_names, symbol const & logic); virtual void get_sort_names(svector & sort_names, symbol const & logic); @@ -97,6 +98,9 @@ public: app * mk_string(std::string & val) { return m_plugin->mk_string(val); } + app * mk_fresh_string() { + return m_plugin->mk_fresh_string(); + } // TODO }; diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 7514f8a23..221f472d2 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -279,6 +279,11 @@ app * theory_str::mk_nonempty_str_var() { SASSERT(lhs_gt_rhs); assert_axiom(lhs_gt_rhs); } + + // add 'a' to variable sets, so we can keep track of it + variable_set.insert(a); + internal_variable_set.insert(a); + return a; } @@ -1685,9 +1690,17 @@ void theory_str::set_up_axioms(expr * ex) { SASSERT(n); m_basicstr_axiom_todo.push_back(n); - // if additionally ex is a concatenation, set up concatenation axioms - if (is_app(ex) && is_concat(to_app(ex))) { - m_concat_axiom_todo.push_back(n); + + if (is_app(ex)) { + app * ap = to_app(ex); + if (is_concat(ap)) { + // if ex is a concat, set up concat axioms later + m_concat_axiom_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" << std::endl;); + variable_set.insert(ex); + } } } else { TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << @@ -1824,12 +1837,41 @@ void theory_str::dump_assignments() { } final_check_status theory_str::final_check_eh() { - // TODO - TRACE("t_str", tout << "final check" << std::endl;); + ast_manager & m = get_manager(); + context & ctx = get_context(); + TRACE("t_str", tout << "final check" << std::endl;); TRACE("t_str_detail", dump_assignments();); - return FC_DONE; + // Check every variable to see if it's eq. to some string constant. + // If not, mark it as free. + bool needToAssignFreeVars = false; + std::set free_variables; + for (std::set::iterator it = variable_set.begin(); it != variable_set.end(); ++it) { + bool has_eqc_value = false; + get_eqc_value(*it, has_eqc_value); + if (!has_eqc_value) { + needToAssignFreeVars = true; + free_variables.insert(*it); + } + } + + if (!needToAssignFreeVars) { + TRACE("t_str", tout << "All variables are assigned. Done!" << std::endl;); + return FC_DONE; + } + + for (std::set::iterator it = free_variables.begin(); it != free_variables.end(); ++it) { + expr * var = *it; + if (internal_variable_set.find(var) != internal_variable_set.end()) { + TRACE("t_str", tout << "assigning arbitrary string to internal variable " << mk_ismt2_pp(var, m) << std::endl;); + app * val = m_strutil.mk_string("**unused**"); + assert_axiom(ctx.mk_eq_atom(var, val)); + } else { + NOT_IMPLEMENTED_YET(); // TODO free variable assignment from strTheory::cb_final_check() + } + } + return FC_CONTINUE; } void theory_str::init_model(model_generator & mg) { @@ -1899,7 +1941,11 @@ model_value_proc * theory_str::mk_value(enode * n, model_generator & mg) { if (val != NULL) { return alloc(expr_wrapper_proc, val); } else { - m.raise_exception("failed to find concrete value"); return NULL; + TRACE("t_str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;); + // TODO make absolutely sure the reason we can't find a concrete value is because of an unassigned temporary + // e.g. for an expression like (Concat X $$_str0) + //return alloc(expr_wrapper_proc, m_strutil.mk_string("")); + NOT_IMPLEMENTED_YET(); } } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 930c8e9c8..1c2e2fbee 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -43,7 +43,11 @@ namespace smt { v2 = m_util.mk_string("value 2"); return true; } - virtual expr * get_fresh_value(sort * s) { NOT_IMPLEMENTED_YET(); } + virtual expr * get_fresh_value(sort * s) { + // TODO this may be causing crashes in model gen? investigate + //return m_util.mk_fresh_string(); + NOT_IMPLEMENTED_YET(); + } virtual void register_value(expr * n) { /* Ignore */ } }; @@ -75,6 +79,9 @@ namespace smt { bool avoidLoopCut; bool loopDetected; std::map > cut_var_map; + + std::set variable_set; + std::set internal_variable_set; protected: void assert_axiom(expr * e); void assert_implication(expr * premise, expr * conclusion);