From b2845d888ec44abb6ea4a6f2d58c93046a5061eb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 May 2019 10:16:15 +0400 Subject: [PATCH] add get_lstring per #2286 Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 6 ++++++ src/api/api_context.h | 1 + src/api/api_seq.cpp | 19 +++++++++++++++++++ src/api/z3_api.h | 11 ++++++++++- src/ast/ast.cpp | 4 ++-- src/ast/seq_decl_plugin.cpp | 11 +++++++++++ src/ast/seq_decl_plugin.h | 1 + src/smt/asserted_formulas.cpp | 15 +++++++++++---- src/smt/asserted_formulas.h | 2 +- src/smt/theory_bv.cpp | 2 +- src/tactic/tactic.cpp | 2 +- 11 files changed, 64 insertions(+), 10 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 811cb30ee..7fbbd965e 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -166,6 +166,12 @@ namespace api { m_string_buffer = str?str:""; return const_cast(m_string_buffer.c_str()); } + + char * context::mk_external_string(char const * str, unsigned n) { + m_string_buffer.clear(); + m_string_buffer.append(str, n); + return const_cast(m_string_buffer.c_str()); + } char * context::mk_external_string(std::string && str) { m_string_buffer = std::move(str); diff --git a/src/api/api_context.h b/src/api/api_context.h index 1c4145810..917d3f0af 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -181,6 +181,7 @@ namespace api { // Store a copy of str in m_string_buffer, and return a reference to it. // This method is used to communicate local/internal strings with the "external world" + char * mk_external_string(char const * str, unsigned n); char * mk_external_string(char const * str); char * mk_external_string(std::string && str); diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 7554fff8a..34d295898 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -150,6 +150,25 @@ extern "C" { Z3_CATCH_RETURN(""); } + Z3_string Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length) { + Z3_TRY; + LOG_Z3_get_lstring(c, s, length); + RESET_ERROR_CODE(); + zstring str; + if (!length) { + SET_ERROR_CODE(Z3_INVALID_ARG, "length argument is null"); + return ""; + } + if (!mk_c(c)->sutil().str.is_string(to_expr(s), str)) { + SET_ERROR_CODE(Z3_INVALID_ARG, "expression is not a string literal"); + return ""; + } + std::string s = str.as_string(); + *length = static_cast(s.size()); + return mk_c(c)->mk_external_string(s.c_str(), s.size()); + Z3_CATCH_RETURN(""); + } + #define MK_SORTED(NAME, FN ) \ Z3_ast Z3_API NAME(Z3_context c, Z3_sort s) { \ Z3_TRY; \ diff --git a/src/api/z3_api.h b/src/api/z3_api.h index f3fc1ed7e..6834a68da 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3375,7 +3375,7 @@ extern "C" { /** \brief Create a string constant out of the string that is passed in It takes the length of the string as well to take into account - 0 characters. + 0 characters. The string is unescaped. def_API('Z3_mk_lstring' ,AST ,(_in(CONTEXT), _in(UINT), _in(STRING))) */ @@ -3397,6 +3397,15 @@ extern "C" { */ Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s); + /** + \brief Retrieve the unescaped string constant stored in \c s. + + \pre Z3_is_string(c, s) + + def_API('Z3_get_lstring' ,STRING ,(_in(CONTEXT), _in(AST), _out(UINT))) + */ + Z3_string Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length); + /** \brief Create an empty sequence of the sequence sort \c seq. diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 4b79edf7f..9d5c50827 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -3453,9 +3453,9 @@ void scoped_mark::pop_scope(unsigned num_scopes) { // show an expr_ref on stdout void prexpr(expr_ref &e){ - std::cout << mk_pp(e.get(), e.get_manager()) << std::endl; + std::cout << mk_pp(e.get(), e.get_manager()) << std::endl; } void ast_manager::show_id_gen(){ - std::cout << "id_gen: " << m_expr_id_gen.show_hash() << " " << m_decl_id_gen.show_hash() << "\n"; + std::cout << "id_gen: " << m_expr_id_gen.show_hash() << " " << m_decl_id_gen.show_hash() << "\n"; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 7073c68f8..c0a5db050 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -224,6 +224,17 @@ std::string zstring::encode() const { return strm.str(); } +std::string zstring::as_string() const { + SASSERT(m_encoding == ascii); + std::ostringstream strm; + for (unsigned i = 0; i < m_buffer.size(); ++i) { + unsigned char ch = m_buffer[i]; + strm << (char)(ch); + } + return strm.str(); +} + + bool zstring::suffixof(zstring const& other) const { if (length() > other.length()) return false; bool suffix = true; diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 0185e473c..f3b82a60c 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -107,6 +107,7 @@ public: unsigned num_bits() const { return (m_encoding==ascii)?8:16; } encoding get_encoding() const { return m_encoding; } std::string encode() const; + std::string as_string() const; unsigned length() const { return m_buffer.size(); } unsigned operator[](unsigned i) const { return m_buffer[i]; } bool empty() const { return m_buffer.empty(); } diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 164d36ae2..26d8df0ab 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -258,6 +258,7 @@ void asserted_formulas::reduce() { if (!invoke(m_max_bv_sharing_fn)) return; if (!invoke(m_elim_bvs_from_quantifiers)) return; if (!invoke(m_reduce_asserted_formulas)) return; +// if (!invoke(m_propagate_values)) return; IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done)\n";); TRACE("after_reduce", display(tout);); @@ -431,11 +432,15 @@ void asserted_formulas::commit() { } void asserted_formulas::commit(unsigned new_qhead) { + TRACE("asserted_formulas", tout << "commit " << new_qhead << "\n";); m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.c_ptr() + m_qhead); m_expr2depth.reset(); + bool new_sub = false; for (unsigned i = m_qhead; i < new_qhead; ++i) { justified_expr const& j = m_formulas[i]; - update_substitution(j.get_fml(), j.get_proof()); + if (update_substitution(j.get_fml(), j.get_proof())) { + new_sub = true; + } } m_qhead = new_qhead; } @@ -473,6 +478,7 @@ void asserted_formulas::propagate_values() { } num_prop = prop; } + TRACE("asserted_formulas", tout << num_prop << "\n";); if (num_prop > 0) m_reduce_asserted_formulas(); } @@ -496,7 +502,7 @@ unsigned asserted_formulas::propagate_values(unsigned i) { return n != new_n ? 1 : 0; } -void asserted_formulas::update_substitution(expr* n, proof* pr) { +bool asserted_formulas::update_substitution(expr* n, proof* pr) { expr* lhs, *rhs, *n1; proof_ref pr1(m); if (is_ground(n) && m.is_eq(n, lhs, rhs)) { @@ -505,13 +511,13 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) { if (is_gt(lhs, rhs)) { TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";); m_scoped_substitution.insert(lhs, rhs, pr); - return; + return true; } if (is_gt(rhs, lhs)) { TRACE("propagate_values", tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";); pr1 = m.proofs_enabled() ? m.mk_symmetry(pr) : nullptr; m_scoped_substitution.insert(rhs, lhs, pr1); - return; + return true; } TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";); } @@ -523,6 +529,7 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) { pr1 = m.proofs_enabled() ? m.mk_iff_true(pr) : nullptr; m_scoped_substitution.insert(n, m.mk_true(), pr1); } + return false; } diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 9c82b1314..e2411e03a 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -213,7 +213,7 @@ class asserted_formulas { void set_eliminate_and(bool flag); void propagate_values(); unsigned propagate_values(unsigned i); - void update_substitution(expr* n, proof* p); + bool update_substitution(expr* n, proof* p); bool is_gt(expr* lhs, expr* rhs); void compute_depth(expr* e); unsigned depth(expr* e) { return m_expr2depth[e]; } diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 5fad04f00..79e16dc04 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -766,7 +766,7 @@ namespace smt { bits.swap(new_bits); \ } \ init_bits(e, bits); \ - TRACE("bv", tout << arg_bits << " " << bits << " " << new_bits << "\n";); \ + TRACE("bv_verbose", tout << arg_bits << " " << bits << " " << new_bits << "\n";); \ } diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 95eeaa251..bad35fa3e 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -187,7 +187,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p else if (is_decided_unsat(r)) { goal * final = r[0]; SASSERT(m.is_false(final->form(0))); - if (proofs_enabled) pr = final->pr(0); + pr = final->pr(0); if (cores_enabled) core = final->dep(0); return l_false; }