From f4c0e0b28d1e9aa4fc6452506112222dd270eb70 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sun, 6 Aug 2017 17:17:04 -0400 Subject: [PATCH 01/13] fix regex bug in theory_str for empty string match. need to fix indents --- src/smt/theory_str.cpp | 48 ++++++++++++++++++++++++------------------ 1 file changed, 27 insertions(+), 21 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 89e0123a8..b869abb0a 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6189,27 +6189,33 @@ namespace smt { expr * arg_str = a->get_arg(0); zstring str; if (u.str.is_string(arg_str, str)) { - TRACE("str", tout << "build NFA for '" << str << "'" << "\n";); - /* - * For an n-character string, we make (n-1) intermediate states, - * labelled i_(0) through i_(n-2). - * Then we construct the following transitions: - * start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final - */ - unsigned last = start; - for (int i = 0; i <= ((int)str.length()) - 2; ++i) { - unsigned i_state = next_id(); - make_transition(last, str[i], i_state); - TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";); - last = i_state; - } - make_transition(last, str[(str.length() - 1)], end); - TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); - } else { - TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;); - m_valid = false; - return; - } + if (str.length() == 0) { + // transitioning on the empty string is handled specially + TRACE("str", tout << "empty string epsilon-move " << start << " --> " << end << std::endl;); + make_epsilon_move(start, end); + } else { + TRACE("str", tout << "build NFA for '" << str << "'" << "\n";); + /* + * For an n-character string, we make (n-1) intermediate states, + * labelled i_(0) through i_(n-2). + * Then we construct the following transitions: + * start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final + */ + unsigned last = start; + for (int i = 0; i <= ((int)str.length()) - 2; ++i) { + unsigned i_state = next_id(); + make_transition(last, str[i], i_state); + TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";); + last = i_state; + } + make_transition(last, str[(str.length() - 1)], end); + TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); + } + } else { // ! u.str.is_string(arg_str, str) + TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;); + m_valid = false; + return; + } } else if (u.re.is_concat(e)){ app * a = to_app(e); expr * re1 = a->get_arg(0); From cadde94017b235ef4c18b3164261be75be1dc626 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 7 Aug 2017 23:02:55 -0400 Subject: [PATCH 02/13] fix indentation and add support for re.allchar --- src/smt/theory_str.cpp | 70 ++++++++++++++++++++++++++---------------- 1 file changed, 44 insertions(+), 26 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index b869abb0a..727e7e131 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1685,6 +1685,8 @@ namespace smt { u.str.is_string(range1, range1val); u.str.is_string(range2, range2val); return zstring("[") + range1val + zstring("-") + range2val + zstring("]"); + } else if (u.re.is_full(a_regex)) { + return zstring("."); } else { TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;); UNREACHABLE(); return zstring(""); @@ -1794,6 +1796,13 @@ namespace smt { expr_ref finalAxiom(m.mk_iff(ex, rhs), m); SASSERT(finalAxiom); assert_axiom(finalAxiom); + } else if (u.re.is_full(regex)) { + // equivalent to regex "." operator, match any one character. + // we rewrite to expr IFF len(str) == 1 + expr_ref rhs(ctx.mk_eq_atom(mk_strlen(str), m_autil.mk_numeral(rational::one(), true)), m); + expr_ref finalAxiom(m.mk_iff(ex, rhs), m); + SASSERT(finalAxiom); + assert_axiom(finalAxiom); } else { TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;); NOT_IMPLEMENTED_YET(); @@ -6190,32 +6199,32 @@ namespace smt { zstring str; if (u.str.is_string(arg_str, str)) { if (str.length() == 0) { - // transitioning on the empty string is handled specially - TRACE("str", tout << "empty string epsilon-move " << start << " --> " << end << std::endl;); - make_epsilon_move(start, end); - } else { - TRACE("str", tout << "build NFA for '" << str << "'" << "\n";); - /* - * For an n-character string, we make (n-1) intermediate states, - * labelled i_(0) through i_(n-2). - * Then we construct the following transitions: - * start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final - */ - unsigned last = start; - for (int i = 0; i <= ((int)str.length()) - 2; ++i) { - unsigned i_state = next_id(); - make_transition(last, str[i], i_state); - TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";); - last = i_state; - } - make_transition(last, str[(str.length() - 1)], end); - TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); - } - } else { // ! u.str.is_string(arg_str, str) - TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;); - m_valid = false; - return; - } + // transitioning on the empty string is handled specially + TRACE("str", tout << "empty string epsilon-move " << start << " --> " << end << std::endl;); + make_epsilon_move(start, end); + } else { + TRACE("str", tout << "build NFA for '" << str << "'" << "\n";); + /* + * For an n-character string, we make (n-1) intermediate states, + * labelled i_(0) through i_(n-2). + * Then we construct the following transitions: + * start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final + */ + unsigned last = start; + for (int i = 0; i <= ((int)str.length()) - 2; ++i) { + unsigned i_state = next_id(); + make_transition(last, str[i], i_state); + TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";); + last = i_state; + } + make_transition(last, str[(str.length() - 1)], end); + TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); + } + } else { // ! u.str.is_string(arg_str, str) + TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;); + m_valid = false; + return; + } } else if (u.re.is_concat(e)){ app * a = to_app(e); expr * re1 = a->get_arg(0); @@ -6284,6 +6293,15 @@ namespace smt { } TRACE("str", tout << "range NFA: start = " << start << ", end = " << end << std::endl;); + } else if (u.re.is_full(e)) { + // equivalent to "transition on each character in the alphabet" + + // TODO this hard-codes something about theory_str's char set here + + for (unsigned i = 1; i <= 255; ++i) { + char ch = (char)i; + make_transition(start, ch, end); + } } else { TRACE("str", tout << "invalid regular expression" << std::endl;); m_valid = false; From fce35fdb611c9018a32855a2e46b9ea05161c26c Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 9 Aug 2017 15:37:52 -0400 Subject: [PATCH 03/13] Revert "fix indentation and add support for re.allchar" This reverts commit cadde94017b235ef4c18b3164261be75be1dc626. --- src/smt/theory_str.cpp | 70 ++++++++++++++++-------------------------- 1 file changed, 26 insertions(+), 44 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 727e7e131..b869abb0a 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1685,8 +1685,6 @@ namespace smt { u.str.is_string(range1, range1val); u.str.is_string(range2, range2val); return zstring("[") + range1val + zstring("-") + range2val + zstring("]"); - } else if (u.re.is_full(a_regex)) { - return zstring("."); } else { TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;); UNREACHABLE(); return zstring(""); @@ -1796,13 +1794,6 @@ namespace smt { expr_ref finalAxiom(m.mk_iff(ex, rhs), m); SASSERT(finalAxiom); assert_axiom(finalAxiom); - } else if (u.re.is_full(regex)) { - // equivalent to regex "." operator, match any one character. - // we rewrite to expr IFF len(str) == 1 - expr_ref rhs(ctx.mk_eq_atom(mk_strlen(str), m_autil.mk_numeral(rational::one(), true)), m); - expr_ref finalAxiom(m.mk_iff(ex, rhs), m); - SASSERT(finalAxiom); - assert_axiom(finalAxiom); } else { TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;); NOT_IMPLEMENTED_YET(); @@ -6199,32 +6190,32 @@ namespace smt { zstring str; if (u.str.is_string(arg_str, str)) { if (str.length() == 0) { - // transitioning on the empty string is handled specially - TRACE("str", tout << "empty string epsilon-move " << start << " --> " << end << std::endl;); - make_epsilon_move(start, end); - } else { - TRACE("str", tout << "build NFA for '" << str << "'" << "\n";); - /* - * For an n-character string, we make (n-1) intermediate states, - * labelled i_(0) through i_(n-2). - * Then we construct the following transitions: - * start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final - */ - unsigned last = start; - for (int i = 0; i <= ((int)str.length()) - 2; ++i) { - unsigned i_state = next_id(); - make_transition(last, str[i], i_state); - TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";); - last = i_state; - } - make_transition(last, str[(str.length() - 1)], end); - TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); - } - } else { // ! u.str.is_string(arg_str, str) - TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;); - m_valid = false; - return; - } + // transitioning on the empty string is handled specially + TRACE("str", tout << "empty string epsilon-move " << start << " --> " << end << std::endl;); + make_epsilon_move(start, end); + } else { + TRACE("str", tout << "build NFA for '" << str << "'" << "\n";); + /* + * For an n-character string, we make (n-1) intermediate states, + * labelled i_(0) through i_(n-2). + * Then we construct the following transitions: + * start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final + */ + unsigned last = start; + for (int i = 0; i <= ((int)str.length()) - 2; ++i) { + unsigned i_state = next_id(); + make_transition(last, str[i], i_state); + TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";); + last = i_state; + } + make_transition(last, str[(str.length() - 1)], end); + TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); + } + } else { // ! u.str.is_string(arg_str, str) + TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;); + m_valid = false; + return; + } } else if (u.re.is_concat(e)){ app * a = to_app(e); expr * re1 = a->get_arg(0); @@ -6293,15 +6284,6 @@ namespace smt { } TRACE("str", tout << "range NFA: start = " << start << ", end = " << end << std::endl;); - } else if (u.re.is_full(e)) { - // equivalent to "transition on each character in the alphabet" - - // TODO this hard-codes something about theory_str's char set here - - for (unsigned i = 1; i <= 255; ++i) { - char ch = (char)i; - make_transition(start, ch, end); - } } else { TRACE("str", tout << "invalid regular expression" << std::endl;); m_valid = false; From 84abdae5f755e0e703bf8e4d378712b843140627 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 9 Aug 2017 15:38:56 -0400 Subject: [PATCH 04/13] fix indentation --- src/smt/theory_str.cpp | 52 +++++++++++++++++++++--------------------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index b869abb0a..2016a6501 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6190,32 +6190,32 @@ namespace smt { zstring str; if (u.str.is_string(arg_str, str)) { if (str.length() == 0) { - // transitioning on the empty string is handled specially - TRACE("str", tout << "empty string epsilon-move " << start << " --> " << end << std::endl;); - make_epsilon_move(start, end); - } else { - TRACE("str", tout << "build NFA for '" << str << "'" << "\n";); - /* - * For an n-character string, we make (n-1) intermediate states, - * labelled i_(0) through i_(n-2). - * Then we construct the following transitions: - * start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final - */ - unsigned last = start; - for (int i = 0; i <= ((int)str.length()) - 2; ++i) { - unsigned i_state = next_id(); - make_transition(last, str[i], i_state); - TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";); - last = i_state; - } - make_transition(last, str[(str.length() - 1)], end); - TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); - } - } else { // ! u.str.is_string(arg_str, str) - TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;); - m_valid = false; - return; - } + // transitioning on the empty string is handled specially + TRACE("str", tout << "empty string epsilon-move " << start << " --> " << end << std::endl;); + make_epsilon_move(start, end); + } else { + TRACE("str", tout << "build NFA for '" << str << "'" << "\n";); + /* + * For an n-character string, we make (n-1) intermediate states, + * labelled i_(0) through i_(n-2). + * Then we construct the following transitions: + * start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final + */ + unsigned last = start; + for (int i = 0; i <= ((int)str.length()) - 2; ++i) { + unsigned i_state = next_id(); + make_transition(last, str[i], i_state); + TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";); + last = i_state; + } + make_transition(last, str[(str.length() - 1)], end); + TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); + } + } else { // ! u.str.is_string(arg_str, str) + TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;); + m_valid = false; + return; + } } else if (u.re.is_concat(e)){ app * a = to_app(e); expr * re1 = a->get_arg(0); From b2388464e46e3e44f5448a2b285ce0b35878422d Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 9 Aug 2017 22:03:26 -0400 Subject: [PATCH 05/13] add re.all to theory_str --- src/smt/theory_str.cpp | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 2016a6501..5642339f4 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1685,6 +1685,8 @@ namespace smt { u.str.is_string(range1, range1val); u.str.is_string(range2, range2val); return zstring("[") + range1val + zstring("-") + range2val + zstring("]"); + } else if (u.re.is_full(a_regex)) { + return zstring("(.*)"); } else { TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;); UNREACHABLE(); return zstring(""); @@ -1715,6 +1717,12 @@ namespace smt { expr_ref str(ex->get_arg(0), m); app * regex = to_app(ex->get_arg(1)); + // quick reference for the following code: + // - ex: top-level regex membership term + // - str: string term appearing in ex + // - regex: regex term appearing in ex + // ex ::= (str.in.re str regex) + if (u.re.is_to_re(regex)) { expr_ref rxStr(regex->get_arg(0), m); // want to assert 'expr IFF (str == rxStr)' @@ -1794,6 +1802,9 @@ namespace smt { expr_ref finalAxiom(m.mk_iff(ex, rhs), m); SASSERT(finalAxiom); assert_axiom(finalAxiom); + } else if (u.re.is_full(regex)) { + // trivially true for any string! + assert_axiom(ex); } else { TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;); NOT_IMPLEMENTED_YET(); @@ -6284,6 +6295,10 @@ namespace smt { } TRACE("str", tout << "range NFA: start = " << start << ", end = " << end << std::endl;); + } else if (u.re.is_full(e)) { + NOT_IMPLEMENTED_YET(); + m_valid = false; + return; } else { TRACE("str", tout << "invalid regular expression" << std::endl;); m_valid = false; From 370706b2b7918c7c0a6580042c4306b58c6f43e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Aug 2017 14:33:37 -0700 Subject: [PATCH 06/13] patch Signed-off-by: Nikolaj Bjorner --- src/smt/mam.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index f59a57bf3..72a6d895c 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -2086,6 +2086,7 @@ namespace smt { for (; it != end; ++it) { enode * p = *it; if (p->get_decl() == f && + p->get_num_args() > i && m_context.is_relevant(p) && p->is_cgr() && p->get_arg(i)->get_root() == n) { From 4ab0ee75fa390fce965df05274ebd5a18be04ef9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Aug 2017 08:49:06 -0700 Subject: [PATCH 07/13] mam Signed-off-by: Nikolaj Bjorner --- src/smt/mam.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 72a6d895c..b5975ac63 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -2080,13 +2080,14 @@ namespace smt { */ enode_vector * interpreter::mk_depth1_vector(enode * n, func_decl * f, unsigned i) { enode_vector * v = mk_enode_vector(); + unsigned num_args = n->get_num_args(); n = n->get_root(); enode_vector::const_iterator it = n->begin_parents(); enode_vector::const_iterator end = n->end_parents(); for (; it != end; ++it) { enode * p = *it; if (p->get_decl() == f && - p->get_num_args() > i && + p->get_num_args() == num_args && m_context.is_relevant(p) && p->is_cgr() && p->get_arg(i)->get_root() == n) { @@ -2105,6 +2106,7 @@ namespace smt { enode * n = m_registers[j2->m_reg]->get_root(); if (n->get_num_parents() == 0) return 0; + unsigned num_args = n->get_num_args(); enode_vector * v = mk_enode_vector(); enode_vector::const_iterator it1 = n->begin_parents(); enode_vector::const_iterator end1 = n->end_parents(); @@ -2121,6 +2123,7 @@ namespace smt { for (; it2 != end2; ++it2) { enode * p2 = *it2; if (p2->get_decl() == f && + num_args == n->get_num_args() && m_context.is_relevant(p2) && p2->is_cgr() && p2->get_arg(i)->get_root() == p) { From 6feb7ba79599fd3155ab4d4ee213c584c609c280 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Aug 2017 14:27:46 -0700 Subject: [PATCH 08/13] :q add sequences to ML API Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 38 ++++++++++++++++ src/api/ml/z3.mli | 109 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 147 insertions(+) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 41d2226c5..c4a4da00c 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1215,6 +1215,44 @@ struct let mk_numeral ctx v size = Z3native.mk_numeral ctx v (mk_sort ctx size) end +module Seq = +struct + let mk_seq_sort = Z3native.mk_seq_sort + let is_seq_sort = Z3native.is_seq_sort + let mk_re_sort = Z3native.mk_re_sort + let is_re_sort = Z3native.is_re_sort + let mk_string_sort = Z3native.mk_string_sort + let is_string_sort = Z3native.is_string_sort + let mk_string = Z3native.mk_string + let is_string = Z3native.is_string + let get_string = Z3native.get_string + let mk_seq_empty = Z3native.mk_seq_empty + let mk_seq_unit = Z3native.mk_seq_unit + let mk_seq_concat ctx args = Z3native.mk_seq_concat ctx (List.length args) args + let mk_seq_prefix = Z3native.mk_seq_prefix + let mk_seq_suffix = Z3native.mk_seq_suffix + let mk_seq_contains = Z3native.mk_seq_contains + let mk_seq_extract = Z3native.mk_seq_extract + let mk_seq_replace = Z3native.mk_seq_replace + let mk_seq_at = Z3native.mk_seq_at + let mk_seq_length = Z3native.mk_seq_length + let mk_seq_index = Z3native.mk_seq_index + let mk_str_to_int = Z3native.mk_str_to_int + let mk_int_to_str = Z3native.mk_int_to_str + let mk_seq_to_re = Z3native.mk_seq_to_re + let mk_seq_in_re = Z3native.mk_seq_in_re + let mk_re_plus = Z3native.mk_re_plus + let mk_re_star = Z3native.mk_re_star + let mk_re_option = Z3native.mk_re_option + let mk_re_union ctx args = Z3native.mk_re_union ctx (List.length args) args + let mk_re_concat ctx args = Z3native.mk_re_concat ctx (List.length args) args + let mk_re_range = Z3native.mk_re_range + let mk_re_loop = Z3native.mk_re_loop + let mk_re_intersect = Z3native.mk_re_intersect + let mk_re_complement = Z3native.mk_re_complement + let mk_re_empty = Z3native.mk_re_empty + let mk_re_full = Z3native.mk_re_full +end module FloatingPoint = struct diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 818a635f7..7b561f878 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1825,6 +1825,115 @@ sig val mk_numeral : context -> string -> int -> Expr.expr end +(** Sequences, Strings and Regular Expressions **) +module Seq : +sig + val mk_seq_sort : context -> Sort.sort -> Sort.sort + + (* test if sort is a sequence sort *) + val is_seq_sort : context -> Sort.sort -> bool + + (* create regular expression sorts over sequences of the argument sort *) + val mk_re_sort : context -> Sort.sort -> Sort.sort + + (* test if sort is a regular expression sort *) + val is_re_sort : context -> Sort.sort -> bool + + (* create string sort *) + val mk_string_sort : context -> Sort.sort + + (* test if sort is a string sort (a sequence of 8-bit bit-vectors) *) + val is_string_sort : context -> Sort.sort -> bool + + (* create a string literal *) + val mk_string : context -> string -> Expr.expr + + (* test if expression is a string *) + val is_string : context -> Expr.expr -> bool + + (* retrieve string from string Expr.expr *) + val get_string : context -> Expr.expr -> string + + (* the empty sequence over base sort *) + val mk_seq_empty : context -> Sort.sort -> Expr.expr + + (* a unit sequence *) + val mk_seq_unit : context -> Expr.expr -> Expr.expr + + (* sequence concatenation *) + val mk_seq_concat : context -> Expr.expr list -> Expr.expr + + (* predicate if the first argument is a prefix of the second *) + val mk_seq_prefix : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* predicate if the first argument is a suffix of the second *) + val mk_seq_suffix : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* predicate if the first argument contains the second *) + val mk_seq_contains : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* extract sub-sequence starting at index given by second argument and of length provided by third argument *) + val mk_seq_extract : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + + (* replace first occurrence of second argument by third *) + val mk_seq_replace : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + + (* a unit sequence at index provided by second argument *) + val mk_seq_at : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* length of a sequence *) + val mk_seq_length : context -> Expr.expr -> Expr.expr + + (* index of the first occurrence of the second argument in the first *) + val mk_seq_index : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + + (* retrieve integer expression encoded in string *) + val mk_str_to_int : context -> Expr.expr -> Expr.expr + + (* convert an integer expression to a string *) + val mk_int_to_str : context -> Expr.expr -> Expr.expr + + (* create regular expression that accepts the argument sequence *) + val mk_seq_to_re : context -> Expr.expr -> Expr.expr + + (* regular expression membership predicate *) + val mk_seq_in_re : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* regular expression plus *) + val mk_re_plus : context -> Expr.expr -> Expr.expr + + (* regular expression star *) + val mk_re_star : context -> Expr.expr -> Expr.expr + + (* optional regular expression *) + val mk_re_option : context -> Expr.expr -> Expr.expr + + (* union of regular expressions *) + val mk_re_union : context -> Expr.expr list -> Expr.expr + + (* concatenation of regular expressions* ) + val mk_re_concat : context -> Expr.expr list -> Expr.expr + + (* regular expression for the range between two characters *) + val mk_re_range : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* bounded loop regular expression *) + val mk_re_loop : context -> Expr.expr -> int -> int -> Expr.expr + + (* intersection of regular expressions *) + val mk_re_intersect : context -> int -> Expr.expr list -> Expr.expr + + (* the regular expression complement *) + val mk_re_complement : context -> Expr.expr -> Expr.expr + + (* the regular expression that accepts no sequences *) + val mk_re_empty : context -> Sort.sort -> Expr.expr + + (* the regular expression that accepts all sequences *) + val mk_re_full : context -> Sort.sort -> Expr.expr + +end + (** Floating-Point Arithmetic *) module FloatingPoint : sig From aa81d58bb0fe632a8832ec8f5a9abbd86753bf07 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Aug 2017 14:29:53 -0700 Subject: [PATCH 09/13] add sequences to ML API #1214 Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.mli | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 7b561f878..0207a53ed 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1828,6 +1828,7 @@ end (** Sequences, Strings and Regular Expressions **) module Seq : sig + (* create a sequence sort *) val mk_seq_sort : context -> Sort.sort -> Sort.sort (* test if sort is a sequence sort *) From 1e445a62d4d37009cdd537d22bff2d0826efcf1d Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 18 Aug 2017 17:31:40 -0400 Subject: [PATCH 10/13] improve error message in theory_str when an invalid term in str.to.re is encountered addresses #871 --- src/smt/theory_str.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 5642339f4..7fbc15e8a 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6223,7 +6223,8 @@ namespace smt { TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); } } else { // ! u.str.is_string(arg_str, str) - TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;); + TRACE("str", tout << "WARNING: invalid string constant in str.to.re! Cancelling." << std::endl;); + u.get_manager().raise_exception("invalid term in str.to.re, argument must be a string constant"); m_valid = false; return; } From 7a977f0106fe0ae07c90d1566a8a75e2d430f2f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Aug 2017 14:54:54 -0700 Subject: [PATCH 11/13] ensure that timeouts are distinguished from other cancel events #848 Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 2 +- src/api/api_solver.cpp | 8 ++++++++ src/solver/check_sat_result.cpp | 18 ++++++++++++++++++ src/solver/check_sat_result.h | 2 ++ src/solver/combined_solver.cpp | 4 ++-- src/util/cancel_eh.h | 10 +++++++--- src/util/event_handler.h | 14 +++++++++++++- src/util/scoped_ctrl_c.cpp | 2 +- src/util/scoped_timer.cpp | 2 +- src/util/timeout.cpp | 3 ++- 10 files changed, 55 insertions(+), 10 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 210e0a1d4..c99d3f0c8 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -142,7 +142,7 @@ namespace api { #pragma omp critical (set_interruptable) { if (m_interruptable) - (*m_interruptable)(); + (*m_interruptable)(API_INTERRUPT_EH_CALLER); m_limit.cancel(); m().limit().cancel(); } diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 7fd6d08fe..3a81080ed 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -296,10 +296,14 @@ extern "C" { result = to_solver_ref(s)->check_sat(num_assumptions, _assumptions); } catch (z3_exception & ex) { + to_solver_ref(s)->set_reason_unknown(eh); mk_c(c)->handle_exception(ex); return Z3_L_UNDEF; } } + if (result == l_undef) { + to_solver_ref(s)->set_reason_unknown(eh); + } return static_cast(result); } @@ -466,10 +470,14 @@ extern "C" { result = to_solver_ref(s)->get_consequences(_assumptions, _variables, _consequences); } catch (z3_exception & ex) { + to_solver_ref(s)->set_reason_unknown(eh); mk_c(c)->handle_exception(ex); return Z3_L_UNDEF; } } + if (result == l_undef) { + to_solver_ref(s)->set_reason_unknown(eh); + } for (unsigned i = 0; i < _consequences.size(); ++i) { to_ast_vector_ref(consequences).push_back(_consequences[i].get()); } diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp index 5a7733071..f1bedfc08 100644 --- a/src/solver/check_sat_result.cpp +++ b/src/solver/check_sat_result.cpp @@ -18,6 +18,24 @@ Notes: --*/ #include "solver/check_sat_result.h" +void check_sat_result::set_reason_unknown(event_handler& eh) { + switch (eh.caller_id()) { + case UNSET_EH_CALLER: break; + case CTRL_C_EH_CALLER: + set_reason_unknown("interrupted from keyboard"); + break; + case TIMEOUT_EH_CALLER: + set_reason_unknown("timeout"); + break; + case RESLIMIT_EH_CALLER: + set_reason_unknown("max. resource limit exceeded"); + break; + case API_INTERRUPT_EH_CALLER: + set_reason_unknown("interrupted"); + break; + } +} + simple_check_sat_result::simple_check_sat_result(ast_manager & m): m_core(m), m_proof(m) { diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h index 3079433b5..38720a5e9 100644 --- a/src/solver/check_sat_result.h +++ b/src/solver/check_sat_result.h @@ -22,6 +22,7 @@ Notes: #include "model/model.h" #include "util/lbool.h" #include "util/statistics.h" +#include "util/event_handler.h" /** \brief Abstract interface for the result of a (check-sat) like command. @@ -57,6 +58,7 @@ public: virtual proof * get_proof() = 0; virtual std::string reason_unknown() const = 0; virtual void set_reason_unknown(char const* msg) = 0; + void set_reason_unknown(event_handler& eh); virtual void get_labels(svector & r) = 0; virtual ast_manager& get_manager() const = 0; diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 744ac494a..8f37224ad 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -89,8 +89,8 @@ private: m_solver->get_manager().limit().dec_cancel(); } } - virtual void operator()() { - m_canceled = true; + virtual void operator()(event_handler_caller_t caller_id) { + m_canceled = true; m_solver->get_manager().limit().inc_cancel(); } }; diff --git a/src/util/cancel_eh.h b/src/util/cancel_eh.h index 4347a5b52..59f11b3f3 100644 --- a/src/util/cancel_eh.h +++ b/src/util/cancel_eh.h @@ -31,10 +31,14 @@ class cancel_eh : public event_handler { public: cancel_eh(T & o): m_canceled(false), m_obj(o) {} ~cancel_eh() { if (m_canceled) m_obj.dec_cancel(); } - virtual void operator()() { - m_canceled = true; - m_obj.inc_cancel(); + virtual void operator()(event_handler_caller_t caller_id) { + if (!m_canceled) { + m_caller_id = caller_id; + m_canceled = true; + m_obj.inc_cancel(); + } } + bool canceled() const { return m_canceled; } }; #endif diff --git a/src/util/event_handler.h b/src/util/event_handler.h index 4b13f9c48..2a951c3ce 100644 --- a/src/util/event_handler.h +++ b/src/util/event_handler.h @@ -19,10 +19,22 @@ Revision History: #ifndef EVENT_HANDLER_H_ #define EVENT_HANDLER_H_ +enum event_handler_caller_t { + UNSET_EH_CALLER, + CTRL_C_EH_CALLER, + TIMEOUT_EH_CALLER, + RESLIMIT_EH_CALLER, + API_INTERRUPT_EH_CALLER +}; + class event_handler { +protected: + event_handler_caller_t m_caller_id; public: + event_handler(): m_caller_id(UNSET_EH_CALLER) {} virtual ~event_handler() {} - virtual void operator()() = 0; + virtual void operator()(event_handler_caller_t caller_id) = 0; + event_handler_caller_t caller_id() const { return m_caller_id; } }; #endif diff --git a/src/util/scoped_ctrl_c.cpp b/src/util/scoped_ctrl_c.cpp index 739eca295..1cb3a03c4 100644 --- a/src/util/scoped_ctrl_c.cpp +++ b/src/util/scoped_ctrl_c.cpp @@ -24,7 +24,7 @@ scoped_ctrl_c * scoped_ctrl_c::g_obj = 0; void scoped_ctrl_c::on_ctrl_c(int) { if (g_obj->m_first) { - g_obj->m_cancel_eh(); + g_obj->m_cancel_eh(CTRL_C_EH_CALLER); if (g_obj->m_once) { g_obj->m_first = false; signal(SIGINT, on_ctrl_c); // re-install the handler diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 741523291..825b251c9 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -85,7 +85,7 @@ struct scoped_timer::imp { obj->m_first = false; } else { - obj->m_eh->operator()(); + obj->m_eh->operator()(TIMEOUT_EH_CALLER); } } #elif defined(__APPLE__) && defined(__MACH__) diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp index a82d1ec25..67995c2aa 100644 --- a/src/util/timeout.cpp +++ b/src/util/timeout.cpp @@ -32,10 +32,11 @@ void (* g_on_timeout)() = 0; class g_timeout_eh : public event_handler { public: - void operator()() { + void operator()(event_handler_caller_t caller_id) { #pragma omp critical (g_timeout_cs) { std::cout << "timeout\n"; + m_caller_id = caller_id; if (g_on_timeout) g_on_timeout(); if (g_timeout) From bc8ae21ebee8a3451c9450a7add52289dc799a16 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Aug 2017 15:14:47 -0700 Subject: [PATCH 12/13] missing parameters for OSX/Linus Signed-off-by: Nikolaj Bjorner --- src/util/scoped_timer.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 825b251c9..3991abd36 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -98,7 +98,7 @@ struct scoped_timer::imp { int e = pthread_cond_timedwait(&st->m_condition_var, &st->m_mutex, &st->m_end_time); if (e != 0 && e != ETIMEDOUT) throw default_exception("failed to start timed wait"); - st->m_eh->operator()(); + st->m_eh->operator()(TIMEOUT_EH_CALLER); pthread_mutex_unlock(&st->m_mutex); @@ -133,7 +133,7 @@ struct scoped_timer::imp { pthread_mutex_unlock(&st->m_mutex); if (e == ETIMEDOUT) - st->m_eh->operator()(); + st->m_eh->operator()(TIMEOUT_EH_CALLER); return 0; } #else From adae32f7efeb5c4bcf4777792f04e53c03e1e564 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sat, 19 Aug 2017 23:25:34 -0400 Subject: [PATCH 13/13] add re.all to NFA in theory_str --- src/smt/theory_str.cpp | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 7fbc15e8a..127409efe 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6297,9 +6297,18 @@ namespace smt { TRACE("str", tout << "range NFA: start = " << start << ", end = " << end << std::endl;); } else if (u.re.is_full(e)) { - NOT_IMPLEMENTED_YET(); - m_valid = false; - return; + // effectively the same as .* where . can be any single character + // start --e--> tmp + // tmp --e--> end + // tmp --C--> tmp for every character C + unsigned tmp = next_id(); + make_epsilon_move(start, tmp); + make_epsilon_move(tmp, end); + for (unsigned int i = 0; i < 256; ++i) { + char ch = (char)i; + make_transition(tmp, ch, tmp); + } + TRACE("str", tout << "re.all NFA: start = " << start << ", end = " << end << std::endl;); } else { TRACE("str", tout << "invalid regular expression" << std::endl;); m_valid = false;