From f038291293d1453ff3421c125ae97498b9f1f58b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 10 Jan 2016 12:12:56 +0000 Subject: [PATCH 01/13] Don't silently fail if ocamlfind cannot be found when building the Ocaml bindings is enabled. That is really unhelpful behaviour. Instead emit a warning. I would prefer an error message but apparently being able to build but not install the OCaml bindings is desirable. Whilst I'm here also print information about ocamlfind where it should have been mentioned. --- scripts/mk_util.py | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ed5df106b..3c4d4aab9 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -460,7 +460,7 @@ def find_ocaml_find(): print ("Testing %s..." % OCAMLFIND) r = exec_cmd([OCAMLFIND, 'printconf']) if r != 0: - OCAMLFIND='' + OCAMLFIND = '' def find_ml_lib(): global OCAML_LIB @@ -630,6 +630,7 @@ def display_help(exit_code): print(" JDK_HOME JDK installation directory (only relevant if -j or --java option is provided)") print(" JNI_HOME JNI bindings directory (only relevant if -j or --java option is provided)") print(" OCAMLC Ocaml byte-code compiler (only relevant with --ml)") + print(" OCAMLFIND Ocaml find tool (only relevant with --ml)") print(" OCAMLOPT Ocaml native compiler (only relevant with --ml)") print(" OCAML_LIB Ocaml library directory (only relevant with --ml)") print(" CSC C# Compiler (only relevant if .NET bindings are enabled)") @@ -1753,6 +1754,15 @@ class MLComponent(Component): self.stubs = "z3native_stubs" self.sub_dir = os.path.join('api', 'ml') + def _install_bindings(self): + # FIXME: Depending on global state is gross. We can't pre-compute this + # in the constructor because we haven't tested for ocamlfind yet + return OCAMLFIND != '' + + def final_info(self): + if not self._install_bindings(): + print("WARNING: Could not find ocamlfind utility. OCaml bindings will not be installed") + def mk_makefile(self, out): if is_ml_enabled(): src_dir = self.to_src_dir @@ -1832,7 +1842,7 @@ class MLComponent(Component): out.write('\n') def mk_install_deps(self, out): - if is_ml_enabled() and OCAMLFIND != '': + if is_ml_enabled() and self._install_bindings(): out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ') out.write(os.path.join(self.sub_dir, 'META ')) out.write(os.path.join(self.sub_dir, 'z3ml.cma ')) @@ -1840,7 +1850,7 @@ class MLComponent(Component): out.write(os.path.join(self.sub_dir, 'z3ml.cmxs ')) def mk_install(self, out): - if is_ml_enabled() and OCAMLFIND != '': + if is_ml_enabled() and self._install_bindings(): out.write('\t@%s install Z3 %s' % (OCAMLFIND, (os.path.join(self.sub_dir, 'META')))) for m in self.modules: @@ -1859,7 +1869,7 @@ class MLComponent(Component): out.write('\n') def mk_uninstall(self, out): - if is_ml_enabled() and OCAMLFIND != '': + if is_ml_enabled() and self._install_bindings(): out.write('\t@%s remove Z3\n' % (OCAMLFIND)) def main_component(self): @@ -2175,6 +2185,7 @@ def mk_config(): print('Java Compiler: %s' % JAVAC) if is_ml_enabled(): print('OCaml Compiler: %s' % OCAMLC) + print('OCaml Find tool: %s' % OCAMLFIND) print('OCaml Native: %s' % OCAMLOPT) print('OCaml Library: %s' % OCAML_LIB) else: @@ -2310,6 +2321,7 @@ def mk_config(): print('Java Compiler: %s' % JAVAC) if is_ml_enabled(): print('OCaml Compiler: %s' % OCAMLC) + print('OCaml Find tool: %s' % OCAMLFIND) print('OCaml Native: %s' % OCAMLOPT) print('OCaml Library: %s' % OCAML_LIB) if is_dotnet_enabled(): From cb106d71cfd805e3971bd9d5bcb50625ebbf4159 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 10 Jan 2016 13:58:11 +0000 Subject: [PATCH 02/13] Teach the OCaml bindings install rule to respect the DESTDIR makefile variable. Previously it would try to install into the system (e.g. ``/usr/lib/ocaml``) regardless of the value of DESTDIR. Unfortunately it looks like packagers who use DESTDIR to do staged installs will need to have their packages patch their user's OCaml ``ld.conf`` file manually at package install time (not ``make install`` time) with the extra path to the Z3 Ocaml package directory. We could use the ``touch`` command to create an empty ``ld.conf`` before running ``ocamlfind install`` but that adds the wrong path to ``ld.conf`` because it contains DESTDIR. --- scripts/mk_util.py | 49 ++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 47 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 3c4d4aab9..bd1496f67 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1754,11 +1754,38 @@ class MLComponent(Component): self.stubs = "z3native_stubs" self.sub_dir = os.path.join('api', 'ml') + self.destdir = "" + self.ldconf = "" + # Calling _init_ocamlfind_paths() is postponed to later because + # OCAMLFIND hasn't been checked yet. + def _install_bindings(self): # FIXME: Depending on global state is gross. We can't pre-compute this # in the constructor because we haven't tested for ocamlfind yet return OCAMLFIND != '' + def _init_ocamlfind_paths(self): + """ + Initialises self.destdir and self.ldconf + + Do not call this from the MLComponent constructor because OCAMLFIND + has not been checked at that point + """ + if self.destdir != "" and self.ldconf != "": + # Initialisation already done + return + # Use Ocamlfind to get the default destdir and ldconf path + self.destdir = check_output([OCAMLFIND, 'printconf', 'destdir']) + if self.destdir == "": + raise MKException('Failed to get OCaml destdir') + + if not os.path.isdir(self.destdir): + raise MKException('The destdir reported by {ocamlfind} ({destdir}) does not exist'.format(ocamlfind=OCAMLFIND, destdir=self.destdir)) + + self.ldconf = check_output([OCAMLFIND, 'printconf', 'ldconf']) + if self.ldconf == "": + raise MKException('Failed to get OCaml ldconf path') + def final_info(self): if not self._install_bindings(): print("WARNING: Could not find ocamlfind utility. OCaml bindings will not be installed") @@ -1851,7 +1878,21 @@ class MLComponent(Component): def mk_install(self, out): if is_ml_enabled() and self._install_bindings(): - out.write('\t@%s install Z3 %s' % (OCAMLFIND, (os.path.join(self.sub_dir, 'META')))) + self._init_ocamlfind_paths() + in_prefix = self.destdir.startswith(PREFIX) + maybe_stripped_destdir = strip_path_prefix(self.destdir, PREFIX) + # Note that when doing a staged install with DESTDIR that modifying + # OCaml's ``ld.conf`` may fail. Therefore packagers will need to + # make their packages modify it manually at package install time + # as opposed to ``make install`` time. + MakeRuleCmd.make_install_directory(out, + maybe_stripped_destdir, + in_prefix=in_prefix) + out.write('\t@{ocamlfind} install -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3 {metafile}'.format( + ldconf=self.ldconf, + ocamlfind=OCAMLFIND, + ocaml_destdir=self.destdir, + metafile=os.path.join(self.sub_dir, 'META'))) for m in self.modules: out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli') @@ -1870,7 +1911,11 @@ class MLComponent(Component): def mk_uninstall(self, out): if is_ml_enabled() and self._install_bindings(): - out.write('\t@%s remove Z3\n' % (OCAMLFIND)) + self._init_ocamlfind_paths() + out.write('\t@{ocamlfind} remove -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3\n'.format( + ldconf=self.ldconf, + ocamlfind=OCAMLFIND, + ocaml_destdir=self.destdir)) def main_component(self): return is_ml_enabled() From 01c3e02e99da5852e69c4d2fe0e4d0bb05bd268c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jan 2016 07:57:10 -0800 Subject: [PATCH 03/13] fix query for non-relational engines Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_engine_base.h | 21 ++++++++++++++++++++- src/muz/fp/dl_cmds.cpp | 8 ++++---- 2 files changed, 24 insertions(+), 5 deletions(-) diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h index e0d8680b2..f353fbf2e 100644 --- a/src/muz/base/dl_engine_base.h +++ b/src/muz/base/dl_engine_base.h @@ -44,7 +44,26 @@ namespace datalog { virtual expr_ref get_answer() = 0; virtual lbool query(expr* q) = 0; - virtual lbool query(unsigned num_rels, func_decl*const* rels) { return l_undef; } + virtual lbool query(unsigned num_rels, func_decl*const* rels) { + if (num_rels != 1) return l_undef; + expr_ref q(m); + expr_ref_vector args(m); + sort_ref_vector sorts(m); + svector names; + func_decl* r = rels[0]; + for (unsigned i = 0; i < r->get_arity(); ++i) { + args.push_back(m.mk_var(i, r->get_domain(i))); + sorts.push_back(r->get_domain(i)); + names.push_back(symbol(i)); + } + sorts.reverse(); + names.reverse(); + q = m.mk_app(r, args.size(), args.c_ptr()); + if (!args.empty()) { + q = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), q); + } + return query(q); + } virtual void reset_statistics() {} virtual void display_profile(std::ostream& out) const {} diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index f8e97d95d..2a6ff04d4 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -268,10 +268,10 @@ public: print_certificate(ctx); break; case l_undef: - if(dlctx.get_status() == datalog::BOUNDED){ - ctx.regular_stream() << "bounded\n"; - print_certificate(ctx); - break; + if (dlctx.get_status() == datalog::BOUNDED){ + ctx.regular_stream() << "bounded\n"; + print_certificate(ctx); + break; } ctx.regular_stream() << "unknown\n"; switch(dlctx.get_status()) { From db715634785fcb74c3578ddb8f33be9fcd703154 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jan 2016 09:36:01 -0800 Subject: [PATCH 04/13] fix build compiler warnings on OSX Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 164 +++++++++++++++++++----------- src/ast/rewriter/seq_rewriter.h | 1 + src/ast/seq_decl_plugin.cpp | 44 ++++++-- src/ast/seq_decl_plugin.h | 4 +- src/smt/theory_seq.cpp | 11 +- src/smt/theory_seq_empty.h | 8 +- 6 files changed, 153 insertions(+), 79 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d94e54935..8a6515f00 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -53,6 +53,7 @@ eautomaton* re2automaton::re2aut(expr* e) { SASSERT(u.is_re(e)); expr* e1, *e2; scoped_ptr a, b; + unsigned lo, hi; if (u.re.is_to_re(e, e1)) { return seq2aut(e1); } @@ -77,10 +78,21 @@ eautomaton* re2automaton::re2aut(expr* e) { return a.detach(); } else if (u.re.is_range(e)) { - + // TBD } - else if (u.re.is_loop(e)) { - + else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) { + scoped_ptr eps = eautomaton::mk_epsilon(m); + b = eautomaton::mk_epsilon(m); + while (hi > lo) { + scoped_ptr c = eautomaton::mk_concat(*a, *b); + b = eautomaton::mk_union(*eps, *c); + --hi; + } + while (lo > 0) { + b = eautomaton::mk_concat(*a, *b); + --lo; + } + return b.detach(); } #if 0 else if (u.re.is_intersect(e, e1, e2)) { @@ -210,8 +222,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_STRING_STOI: SASSERT(num_args == 1); return mk_str_stoi(args[0], result); - case OP_REGEXP_LOOP: - return BR_FAILED; case _OP_STRING_CONCAT: case _OP_STRING_PREFIX: case _OP_STRING_SUFFIX: @@ -653,6 +663,31 @@ void seq_rewriter::add_next(u_map& next, unsigned idx, expr* cond) { } } +bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) { + unsigned state = aut.init(); + uint_set visited; + eautomaton::moves mvs; + aut.get_moves_from(state, mvs, true); + while (!aut.is_final_state(state)) { + if (mvs.size() != 1) { + return false; + } + if (visited.contains(state)) { + return false; + } + visited.insert(state); + expr* t = mvs[0].t(); + if (!t) { + return false; + } + seq.push_back(m_util.str.mk_unit(t)); + state = mvs[0].dst(); + mvs.reset(); + aut.get_moves_from(state, mvs, true); + } + return mvs.empty(); +} + bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) { zstring s; ptr_vector todo; @@ -688,63 +723,78 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) { br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { scoped_ptr aut; expr_ref_vector seq(m()); - if (is_sequence(a, seq) && (aut = re2automaton(m())(b))) { - expr_ref_vector trail(m()); - u_map maps[2]; - bool select_map = false; - expr_ref ch(m()), cond(m()); - eautomaton::moves mvs; - maps[0].insert(aut->init(), m().mk_true()); - // is_accepted(a, aut) & some state in frontier is final. + if (!(aut = re2automaton(m())(b))) { + return BR_FAILED; + } - for (unsigned i = 0; i < seq.size(); ++i) { - u_map& frontier = maps[select_map]; - u_map& next = maps[!select_map]; - select_map = !select_map; - ch = seq[i].get(); - next.reset(); - u_map::iterator it = frontier.begin(), end = frontier.end(); - for (; it != end; ++it) { - mvs.reset(); - unsigned state = it->m_key; - expr* acc = it->m_value; - aut->get_moves_from(state, mvs, false); - for (unsigned j = 0; j < mvs.size(); ++j) { - eautomaton::move const& mv = mvs[j]; - if (m().is_value(mv.t()) && m().is_value(ch)) { - if (mv.t() == ch) { - add_next(next, mv.dst(), acc); - } - else { - continue; - } - } - else { - cond = m().mk_eq(mv.t(), ch); - if (!m().is_true(acc)) cond = m().mk_and(acc, cond); - add_next(next, mv.dst(), cond); - } - } - } + if (is_sequence(*aut, seq)) { + if (seq.empty()) { + result = m().mk_eq(a, m_util.str.mk_empty(m().get_sort(a))); } - u_map const& frontier = maps[select_map]; - u_map::iterator it = frontier.begin(), end = frontier.end(); - expr_ref_vector ors(m()); - for (; it != end; ++it) { - unsigned_vector states; - bool has_final = false; - aut->get_epsilon_closure(it->m_key, states); - for (unsigned i = 0; i < states.size() && !has_final; ++i) { - has_final = aut->is_final_state(states[i]); - } - if (has_final) { - ors.push_back(it->m_value); - } + else { + result = m().mk_eq(a, m_util.str.mk_concat(seq)); } - result = mk_or(ors); return BR_REWRITE_FULL; } - return BR_FAILED; + + if (!is_sequence(a, seq)) { + return BR_FAILED; + } + + expr_ref_vector trail(m()); + u_map maps[2]; + bool select_map = false; + expr_ref ch(m()), cond(m()); + eautomaton::moves mvs; + maps[0].insert(aut->init(), m().mk_true()); + // is_accepted(a, aut) & some state in frontier is final. + + for (unsigned i = 0; i < seq.size(); ++i) { + u_map& frontier = maps[select_map]; + u_map& next = maps[!select_map]; + select_map = !select_map; + ch = seq[i].get(); + next.reset(); + u_map::iterator it = frontier.begin(), end = frontier.end(); + for (; it != end; ++it) { + mvs.reset(); + unsigned state = it->m_key; + expr* acc = it->m_value; + aut->get_moves_from(state, mvs, false); + for (unsigned j = 0; j < mvs.size(); ++j) { + eautomaton::move const& mv = mvs[j]; + if (m().is_value(mv.t()) && m().is_value(ch)) { + if (mv.t() == ch) { + add_next(next, mv.dst(), acc); + } + else { + continue; + } + } + else { + cond = m().mk_eq(mv.t(), ch); + if (!m().is_true(acc)) cond = m().mk_and(acc, cond); + add_next(next, mv.dst(), cond); + } + } + } + } + u_map const& frontier = maps[select_map]; + u_map::iterator it = frontier.begin(), end = frontier.end(); + expr_ref_vector ors(m()); + for (; it != end; ++it) { + unsigned_vector states; + bool has_final = false; + aut->get_epsilon_closure(it->m_key, states); + for (unsigned i = 0; i < states.size() && !has_final; ++i) { + has_final = aut->is_final_state(states[i]); + } + if (has_final) { + ors.push_back(it->m_value); + } + } + result = mk_or(ors); + return BR_REWRITE_FULL; } br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) { return BR_FAILED; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index b9d3460aa..5d6c40fa1 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -75,6 +75,7 @@ class seq_rewriter { void add_next(u_map& next, unsigned idx, expr* cond); bool is_sequence(expr* e, expr_ref_vector& seq); + bool is_sequence(eautomaton& aut, expr_ref_vector& seq); bool is_epsilon(expr* e) const; public: diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 165e24eac..e31b168b8 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -250,7 +250,13 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do if (!is_match) { std::ostringstream strm; strm << "Sort of function '" << sig.m_name << "' "; - strm << "does not match the declared type"; + strm << "does not match the declared type. Given domain: "; + for (unsigned i = 0; i < dsz; ++i) { + strm << mk_pp(dom[i], m) << " "; + } + if (range) { + strm << " and range: " << mk_pp(range, m); + } m.raise_exception(strm.str().c_str()); } range_out = apply_binding(binding, sig.m_range); @@ -277,7 +283,19 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran if (!is_match) { std::ostringstream strm; strm << "Sort of polymorphic function '" << sig.m_name << "' "; - strm << "does not match the declared type"; + strm << "does not match the declared type. "; + strm << "\nGiven domain: "; + for (unsigned i = 0; i < dsz; ++i) { + strm << mk_pp(dom[i], m) << " "; + } + if (range) { + strm << " and range: " << mk_pp(range, m); + } + strm << "\nExpected domain: "; + for (unsigned i = 0; i < dsz; ++i) { + strm << mk_pp(sig.m_dom[i].get(), m) << " "; + } + m.raise_exception(strm.str().c_str()); } if (!range && dsz == 0) { @@ -319,7 +337,8 @@ void seq_decl_plugin::init() { parameter paramA(A); parameter paramS(strT); sort* seqA = m.mk_sort(m_family_id, SEQ_SORT, 1, ¶mA); - sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, ¶mA); + parameter paramSA(seqA); + sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, ¶mSA); sort* reT = m.mk_sort(m_family_id, RE_SORT, 1, ¶mS); sort* boolT = m.mk_bool_sort(); sort* intT = arith_util(m).mk_int(); @@ -356,7 +375,7 @@ void seq_decl_plugin::init() { m_sigs[OP_RE_CONCAT] = alloc(psig, m, "re.++", 1, 2, reAreA, reA); m_sigs[OP_RE_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA); m_sigs[OP_RE_INTERSECT] = alloc(psig, m, "re.inter", 1, 2, reAreA, reA); - m_sigs[OP_RE_LOOP] = alloc(psig, m, "re-loop", 1, 1, &reA, reA); + m_sigs[OP_RE_LOOP] = alloc(psig, m, "re.loop", 1, 1, &reA, reA); m_sigs[OP_RE_EMPTY_SET] = alloc(psig, m, "re-empty-set", 1, 0, 0, reA); m_sigs[OP_RE_FULL_SET] = alloc(psig, m, "re-full-set", 1, 0, 0, reA); m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA); @@ -367,7 +386,6 @@ void seq_decl_plugin::init() { m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT); m_sigs[OP_STRING_ITOS] = alloc(psig, m, "int.to.str", 0, 1, &intT, strT); m_sigs[OP_STRING_STOI] = alloc(psig, m, "str.to.int", 0, 1, &strT, intT); - m_sigs[OP_REGEXP_LOOP] = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments. m_sigs[_OP_STRING_CONCAT] = alloc(psig, m, "str.++", 1, 2, str2T, strT); m_sigs[_OP_STRING_LENGTH] = alloc(psig, m, "str.len", 0, 1, &strT, intT); m_sigs[_OP_STRING_STRCTN] = alloc(psig, m, "str.contains", 0, 2, str2T, boolT); @@ -472,7 +490,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_RE_OF_PRED: case OP_STRING_ITOS: case OP_STRING_STOI: - case OP_REGEXP_LOOP: match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); @@ -670,3 +687,18 @@ void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const { es.push_back(e); } } + +bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) { + if (is_loop(n)) { + app const* a = to_app(n); + SASSERT(a->get_num_args() == 1); + SASSERT(a->get_decl()->get_num_parameters() == 2); + body = a->get_arg(0); + lo = a->get_decl()->get_parameter(0).get_int(); + hi = a->get_decl()->get_parameter(1).get_int(); + return true; + } + else { + return false; + } +} diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 00ada9e86..4a94ef18f 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -63,7 +63,6 @@ enum seq_op_kind { OP_STRING_CONST, OP_STRING_ITOS, OP_STRING_STOI, - OP_REGEXP_LOOP, // TBD re-loop: integers as parameters or arguments? // internal only operators. Converted to SEQ variants. _OP_STRING_STRREPL, _OP_STRING_CONCAT, @@ -304,7 +303,7 @@ public: bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_RE_PLUS); } bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OPTION); } bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_RE_RANGE); } - bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_LOOP); } + bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_RE_LOOP); } MATCH_UNARY(is_to_re); MATCH_BINARY(is_concat); @@ -313,6 +312,7 @@ public: MATCH_UNARY(is_star); MATCH_UNARY(is_plus); MATCH_UNARY(is_opt); + bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi); }; str str; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index c1083ea25..6c27dc104 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -165,9 +165,9 @@ theory_seq::theory_seq(ast_manager& m): m_util(m), m_autil(m), m_trail_stack(*this), - m_atoms_qhead(0), m_ls(m), m_rs(m), m_lhs(m), m_rhs(m), + m_atoms_qhead(0), m_new_solution(false), m_new_propagation(false) { m_prefix = "seq.prefix.suffix"; @@ -194,7 +194,6 @@ theory_seq::~theory_seq() { final_check_status theory_seq::final_check_eh() { - context & ctx = get_context(); TRACE("seq", display(tout);); if (simplify_and_solve_eqs()) { ++m_stats.m_solve_eqs; @@ -760,7 +759,6 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) { if (l == r) { return false; } - context& ctx = get_context(); TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n";); m_new_solution = true; m_rep.update(l, r, deps); @@ -933,7 +931,6 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons } bool theory_seq::solve_nqs(unsigned i) { - bool change = false; context & ctx = get_context(); for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) { if (solve_ne(i)) { @@ -1262,7 +1259,7 @@ void theory_seq::init_model(expr_ref_vector const& es) { } void theory_seq::init_model(model_generator & mg) { - m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()); + m_factory = alloc(seq_factory, get_manager(), get_family_id()); mg.register_factory(m_factory); for (unsigned j = 0; j < m_nqs.size(); ++j) { ne const& n = m_nqs[j]; @@ -1288,7 +1285,6 @@ public: } virtual app * mk_value(model_generator & mg, ptr_vector & values) { SASSERT(values.size() == m_dependencies.size()); - ast_manager& m = mg.get_manager(); if (values.empty()) { return th.mk_value(n); } @@ -1362,7 +1358,7 @@ app* theory_seq::mk_value(app* e) { unsigned sz; if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) { unsigned v = val.get_unsigned(); - if ((0 <= v && v < 7) || (14 <= v && v < 32) || v == 127) { + if ((v < 7) || (14 <= v && v < 32) || v == 127) { result = m_util.str.mk_unit(result); } else { @@ -1817,7 +1813,6 @@ enode* theory_seq::ensure_enode(expr* e) { } static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) { - ast_manager& m = ctx.get_manager(); theory* th = ctx.get_theory(afid); if (th && ctx.e_internalized(e)) { return dynamic_cast(th); diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index 9c8f15a7a..69f8b54b7 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -26,23 +26,19 @@ namespace smt { class seq_factory : public value_factory { typedef hashtable symbol_set; ast_manager& m; - proto_model& m_model; seq_util u; symbol_set m_strings; unsigned m_next; - char m_char; std::string m_unique_delim; obj_map m_unique_sequences; expr_ref_vector m_trail; public: - seq_factory(ast_manager & m, family_id fid, proto_model & md): + seq_factory(ast_manager & m, family_id fid): value_factory(m, fid), m(m), - m_model(md), u(m), m_next(0), - m_char(0), m_unique_delim("!"), m_trail(m) { @@ -129,7 +125,7 @@ namespace smt { public: theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {} virtual void init_model(model_generator & mg) { - mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model())); + mg.register_factory(alloc(seq_factory, get_manager(), get_family_id())); } }; From 985fc509614e8959a34282c07048abed13821bd8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jan 2016 09:48:43 -0800 Subject: [PATCH 05/13] breaking regression tests: ensure that model values are of the sort of the original expression. Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_core.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 6f245d1c6..cde3aa9fd 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3126,7 +3126,7 @@ namespace smt { TRACE("arith", tout << "Truncating non-integer value. This is possible for non-linear constraints v" << v << " " << num << "\n";); num = floor(num); } - return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v))); + return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(var2expr(v)))); } // ----------------------------------- From db746e0c2f0a4ba446852cf8429cdf0ed3890b42 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jan 2016 09:52:16 -0800 Subject: [PATCH 06/13] fix more unused variable warning messages Signed-off-by: Nikolaj Bjorner --- src/api/api_fpa.cpp | 8 ++++---- src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 1 - src/ast/seq_decl_plugin.cpp | 1 - 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 90b818b4b..eaffdd226 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -943,7 +943,7 @@ extern "C" { return ""; } scoped_mpf val(mpfm); - app * a = to_app(e); +// app * a = to_app(e); bool r = plugin->is_numeral(e, val); if (!r || !mpfm.is_regular(val)) { SET_ERROR_CODE(Z3_INVALID_ARG) @@ -981,7 +981,7 @@ extern "C" { return 0; } scoped_mpf val(mpfm); - app * a = to_app(e); +// app * a = to_app(e); bool r = plugin->is_numeral(e, val); const mpz & z = mpfm.sig(val); if (!r || mpfm.is_regular(val)|| !mpzm.is_uint64(z)) { @@ -1012,7 +1012,7 @@ extern "C" { return ""; } scoped_mpf val(mpfm); - app * a = to_app(e); +// app * a = to_app(e); bool r = plugin->is_numeral(e, val); if (!r || !mpfm.is_regular(val)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1044,7 +1044,7 @@ extern "C" { return 0; } scoped_mpf val(mpfm); - app * a = to_app(e); +// app * a = to_app(e); bool r = plugin->is_numeral(e, val); if (!r || !mpfm.is_regular(val)) { SET_ERROR_CODE(Z3_INVALID_ARG); diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 102082cd5..16aef6a00 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -1171,7 +1171,6 @@ void bit_blaster_tpl::mk_carry_save_adder(unsigned sz, expr * const * a_bit template bool bit_blaster_tpl::mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { - unsigned nb = 0; unsigned case_size = 1; unsigned circuit_size = sz*sz*5; for (unsigned i = 0; case_size < circuit_size && i < sz; ++i) { diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index e31b168b8..e715ef571 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -429,7 +429,6 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter if (!parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) { m.raise_exception("invalid regex sort, parameter is not a sort"); } - sort * s = to_sort(parameters[0].get_ast()); return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters)); } case _STRING_SORT: From f093ebe44c33dcafb6f80ad27c6b58b97226447f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 12 Jan 2016 19:06:53 +0000 Subject: [PATCH 07/13] Optimization for initialization of mpf's from tiny reals. --- src/util/mpf.cpp | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 24aa253a4..899b8635b 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -245,26 +245,30 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode m_mpz_manager.set(exp, exponent); // Normalize such that 1.0 <= sig < 2.0 - if (m_mpq_manager.ge(sig, mpq(2))) { + if (m_mpq_manager.lt(sig, 1)) { + m_mpq_manager.inv(sig); + unsigned int pp = m_mpq_manager.prev_power_of_two(sig); + if (!m_mpq_manager.is_power_of_two(sig, pp)) pp++; + scoped_mpz p2(m_mpz_manager); + m_mpq_manager.power(2, pp, p2); + m_mpq_manager.div(sig, p2, sig); + m_mpz_manager.sub(exp, mpz(pp), exp); + m_mpq_manager.inv(sig); + } + else if (m_mpq_manager.ge(sig, 2)) { unsigned int pp = m_mpq_manager.prev_power_of_two(sig); scoped_mpz p2(m_mpz_manager); m_mpq_manager.power(2, pp, p2); m_mpq_manager.div(sig, p2, sig); m_mpz_manager.add(exp, mpz(pp), exp); } - SASSERT(m_mpq_manager.lt(sig, mpq(2))); - - while (m_mpq_manager.lt(sig, 1)) { - m_mpq_manager.mul(sig, 2, sig); - m_mpz_manager.dec(exp); - } - - // Check that 1.0 <= sig < 2.0 - SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2))); TRACE("mpf_dbg", tout << "Normalized: sig = " << m_mpq_manager.to_string(sig) << " exp = " << m_mpz_manager.to_string(exp) << std::endl;); + // Check that 1.0 <= sig < 2.0 + SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2))); + scoped_mpz p(m_mpq_manager); scoped_mpq t(m_mpq_manager), sq(m_mpq_manager); m_mpz_manager.power(2, sbits + 3 - 1, p); From 22fbed18ccf9b2017cf73430c42b9ca811dfbda7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jan 2016 11:18:52 -0800 Subject: [PATCH 08/13] fix regressions exposed by build Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 4 +++- src/ast/rewriter/seq_rewriter.cpp | 15 ++++++++++----- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 2670dfa9a..0626d2f3c 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -9320,8 +9320,10 @@ def Union(*args): args = _get_args(args) sz = len(args) if __debug__: - _z3_assert(sz >= 2, "At least two arguments expected.") + _z3_assert(sz > 0, "At least one argument expected.") _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") + if sz == 1: + return args[0] ctx = args[0].ctx v = (Ast * sz)() for i in range(sz): diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 8a6515f00..5a97e13c8 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -40,10 +40,9 @@ re2automaton::re2automaton(ast_manager& m): m(m), u(m) {} eautomaton* re2automaton::operator()(expr* e) { eautomaton* r = re2aut(e); if (r) { - //display_expr1 disp(m); - //r->display(std::cout, disp); + display_expr1 disp(m); r->compress(); - //r->display(std::cout, disp); + TRACE("seq", r->display(tout, disp);); } return r; } @@ -664,6 +663,7 @@ void seq_rewriter::add_next(u_map& next, unsigned idx, expr* cond) { } bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) { + seq.reset(); unsigned state = aut.init(); uint_set visited; eautomaton::moves mvs; @@ -675,6 +675,9 @@ bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) { if (visited.contains(state)) { return false; } + if (aut.is_final_state(mvs[0].src())) { + return false; + } visited.insert(state); expr* t = mvs[0].t(); if (!t) { @@ -689,6 +692,7 @@ bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) { } bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) { + seq.reset(); zstring s; ptr_vector todo; expr *e1, *e2; @@ -728,6 +732,8 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { } if (is_sequence(*aut, seq)) { + TRACE("seq", tout << seq << "\n";); + if (seq.empty()) { result = m().mk_eq(a, m_util.str.mk_empty(m().get_sort(a))); } @@ -873,8 +879,7 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) { br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) { sort* s; VERIFY(m_util.is_re(a, s)); - sort_ref seq(m_util.str.mk_seq(s), m()); - result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(seq)), a); + result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(s)), a); return BR_REWRITE1; } From 250c8d028d0f81b44e1767b20cb2f2f9bd8f9938 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 12 Jan 2016 19:38:43 +0000 Subject: [PATCH 09/13] Fix bug when configuring when building OCaml bindings is enabled when using Python2. The output from ``check_output()`` has ``unicode`` type under Python 2 but type ``str`` under Python 3. This type ended up being used inside the ``MakeRuleCmd`` class which asserts that it receives paths of type ``str``. To fix the problem under Python 2 the asserts have been made weaker by also allowing the paths to be of type ``unicode``. --- scripts/mk_util.py | 29 +++++++++++++++++++---------- 1 file changed, 19 insertions(+), 10 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index bd1496f67..3ca0012e7 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -3592,6 +3592,15 @@ class MakeRuleCmd(object): # Note: DESTDIR is to support staged installs return "$(DESTDIR)$(PREFIX)/" + @classmethod + def _is_str(cls, obj): + if sys.version_info.major > 2: + # Python 3 or newer. Strings are always unicode and of type str + return isinstance(obj, str) + else: + # Python 2. Has byte-string and unicode representation, allow both + return isinstance(obj, str) or isinstance(obj, unicode) + @classmethod def _install_root(cls, path, in_prefix, out, is_install=True): if not in_prefix: @@ -3610,9 +3619,9 @@ class MakeRuleCmd(object): @classmethod def install_files(cls, out, src_pattern, dest, in_prefix=True): assert len(dest) > 0 - assert isinstance(src_pattern, str) + assert cls._is_str(src_pattern) assert not ' ' in src_pattern - assert isinstance(dest, str) + assert cls._is_str(dest) assert not ' ' in dest assert not os.path.isabs(src_pattern) install_root = cls._install_root(dest, in_prefix, out) @@ -3625,7 +3634,7 @@ class MakeRuleCmd(object): @classmethod def remove_installed_files(cls, out, pattern, in_prefix=True): assert len(pattern) > 0 - assert isinstance(pattern, str) + assert cls._is_str(pattern) assert not ' ' in pattern install_root = cls._install_root(pattern, in_prefix, out, is_install=False) @@ -3636,7 +3645,7 @@ class MakeRuleCmd(object): @classmethod def make_install_directory(cls, out, dir, in_prefix=True): assert len(dir) > 0 - assert isinstance(dir, str) + assert cls._is_str(dir) assert not ' ' in dir install_root = cls._install_root(dir, in_prefix, out) @@ -3650,8 +3659,8 @@ class MakeRuleCmd(object): Returns True iff ``temp_path`` is a path prefix of ``target_as_abs`` """ - assert isinstance(temp_path, str) - assert isinstance(target_as_abs, str) + assert cls._is_str(temp_path) + assert cls._is_str(target_as_abs) assert len(temp_path) > 0 assert len(target_as_abs) > 0 assert os.path.isabs(temp_path) @@ -3667,8 +3676,8 @@ class MakeRuleCmd(object): @classmethod def create_relative_symbolic_link(cls, out, target, link_name): - assert isinstance(target, str) - assert isinstance(link_name, str) + assert cls._is_str(target) + assert cls._is_str(link_name) assert len(target) > 0 assert len(link_name) > 0 assert not os.path.isabs(target) @@ -3705,8 +3714,8 @@ class MakeRuleCmd(object): @classmethod def create_symbolic_link(cls, out, target, link_name): - assert isinstance(target, str) - assert isinstance(link_name, str) + assert cls._is_str(target) + assert cls._is_str(link_name) assert not os.path.isabs(target) cls.write_cmd(out, 'ln -s {target} {install_root}{link_name}'.format( From e2d54940b460ac2c4352bd596d72d4c36eb83feb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jan 2016 12:11:27 -0800 Subject: [PATCH 10/13] revert mixed integer/real handling pending fix to equality propagation Signed-off-by: Nikolaj Bjorner --- src/model/func_interp.cpp | 1 + src/smt/theory_arith_core.h | 4 ++++ src/smt/theory_arith_eq.h | 1 + 3 files changed, 6 insertions(+) diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index fb594a09f..90810f294 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -169,6 +169,7 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) { for (unsigned i = 0; i < m_arity; i++) { tout << mk_ismt2_pp(args[i], m_manager) << "\n"; } + tout << "Old: " << mk_ismt2_pp(get_entry(args)->get_result(), m_manager) << "\n"; ); SASSERT(get_entry(args) == 0); func_entry * new_entry = func_entry::mk(m_manager, m_arity, args, r); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index cde3aa9fd..64aa2b638 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -66,6 +66,9 @@ namespace smt { template bool theory_arith::is_int_expr(expr* e) { + return m_util.is_int(e); +#if 0 + Disable refined integer until equality propagation is fixed. if (m_util.is_int(e)) return true; if (is_uninterp(e)) return false; m_todo.reset(); @@ -93,6 +96,7 @@ namespace smt { } } return true; +#endif } diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index 7ed6cfe50..4a5dad34f 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -329,6 +329,7 @@ namespace smt { if (is_equal(x, y)) return; if (get_manager().get_sort(var2expr(x)) != get_manager().get_sort(var2expr(y))) { + TRACE("arith", tout << mk_pp(var2expr(x), get_manager()) << " = " << mk_pp(var2expr(y), get_manager()) << "\n";); return; } context & ctx = get_context(); From 9a6fe93e6c6124710c59278d5f4853baf13094c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jan 2016 12:42:18 -0800 Subject: [PATCH 11/13] re-enable feature that lets Z3 solver mixed integer/real constraints with additional information tha texpressions with sort real can only take integer values. Fixes regression on epsilon.smt2 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 1 + src/smt/theory_arith_core.h | 8 ++++---- src/smt/theory_arith_eq.h | 15 +++++++-------- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 703e19f1d..8ccee885a 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -547,6 +547,7 @@ namespace smt { ptr_vector m_todo; bool is_int_expr(expr* e); bool is_int(theory_var v) const { return m_data[v].m_is_int; } + bool is_int_src(theory_var v) const { return m_util.is_int(var2expr(v)); } bool is_real(theory_var v) const { return !is_int(v); } bool get_implied_old_value(theory_var v, inf_numeral & r) const; inf_numeral const & get_implied_value(theory_var v) const; diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 64aa2b638..1b1b9a1a6 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -66,9 +66,9 @@ namespace smt { template bool theory_arith::is_int_expr(expr* e) { - return m_util.is_int(e); #if 0 - Disable refined integer until equality propagation is fixed. + return m_util.is_int(e); +#else if (m_util.is_int(e)) return true; if (is_uninterp(e)) return false; m_todo.reset(); @@ -3077,7 +3077,7 @@ namespace smt { theory_var num = get_num_vars(); bool refine = false; for (theory_var v = 0; v < num; v++) { - if (is_int(v)) + if (is_int_src(v)) continue; if (!get_context().is_shared(get_enode(v))) continue; @@ -3088,7 +3088,7 @@ namespace smt { rational value = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational(); theory_var v2; if (mapping.find(value, v2)) { - SASSERT(!is_int(v2)); + SASSERT(!is_int_src(v2)); if (get_value(v) != get_value(v2)) { // v and v2 are not known to be equal. // The choice of m_epsilon is making them equal. diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index 4a5dad34f..8e1b52ee5 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -43,7 +43,7 @@ namespace smt { CTRACE("arith_bug", !lower_bound(v).is_rational(), display_var(tout, v);); SASSERT(lower_bound(v).is_rational()); numeral const & val = lower_bound(v).get_rational(); - value_sort_pair key(val, is_int(v)); + value_sort_pair key(val, is_int_src(v)); theory_var v2; if (m_fixed_var_table.find(key, v2)) { if (v2 < static_cast(get_num_vars()) && is_fixed(v2) && lower_bound(v2).get_rational() == val) { @@ -51,7 +51,7 @@ namespace smt { // The table m_fixed_var_table is not restored during backtrack. So, it may // contain invalid (key -> value) pairs. So, we must check whether v2 is really equal to val (previous test) AND it has // the same sort of v. The following test was missing in a previous version of Z3. - if (!is_equal(v, v2) && is_int(v) == is_int(v2)) { + if (!is_equal(v, v2) && is_int_src(v) == is_int_src(v2)) { antecedents ante(*this); // @@ -226,7 +226,7 @@ namespace smt { if (y == null_theory_var) { // x is an implied fixed var at k. - value_sort_pair key(k, is_int(x)); + value_sort_pair key(k, is_int_src(x)); theory_var x2; if (m_fixed_var_table.find(key, x2) && x2 < static_cast(get_num_vars()) && @@ -238,7 +238,7 @@ namespace smt { // So, we must check whether x2 is really equal to k (previous test) // AND has the same sort of x. // The following test was missing in a previous version of Z3. - is_int(x) == is_int(x2) && + is_int_src(x) == is_int_src(x2) && !is_equal(x, x2)) { antecedents ante(*this); @@ -254,7 +254,7 @@ namespace smt { } } - if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int(x) == is_int(y)) { + if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int_src(x) == is_int_src(y)) { // found equality x = y antecedents ante(*this); collect_fixed_var_justifications(r, ante); @@ -294,7 +294,7 @@ namespace smt { } if (new_eq) { - if (!is_equal(x, x2) && is_int(x) == is_int(x2)) { + if (!is_equal(x, x2) && is_int_src(x) == is_int_src(x2)) { SASSERT(y == y2 && k == k2); antecedents ante(*this); collect_fixed_var_justifications(r, ante); @@ -323,11 +323,10 @@ namespace smt { template void theory_arith::propagate_eq_to_core(theory_var x, theory_var y, antecedents& antecedents) { - // I doesn't make sense to propagate an equality (to the core) of variables of different sort. - SASSERT(is_int(x) == is_int(y)); // Ignore equality if variables are already known to be equal. if (is_equal(x, y)) return; + // I doesn't make sense to propagate an equality (to the core) of variables of different sort. if (get_manager().get_sort(var2expr(x)) != get_manager().get_sort(var2expr(y))) { TRACE("arith", tout << mk_pp(var2expr(x), get_manager()) << " = " << mk_pp(var2expr(y), get_manager()) << "\n";); return; From 9909c056f0412007e3060f6db4c9131554ad3d06 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Jan 2016 00:49:31 -0800 Subject: [PATCH 12/13] add range / loop handling for re. Fix regression reading mixed numerals reported by Trentin Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 77 ++++++++++++++++++++++--------- src/ast/rewriter/seq_rewriter.h | 33 +++++++++++-- src/ast/seq_decl_plugin.cpp | 47 ++++++++++++++++--- src/ast/seq_decl_plugin.h | 9 ++-- src/math/automata/automaton.h | 38 ++++++++++++++- src/parsers/smt2/smt2parser.cpp | 4 +- src/smt/theory_seq.cpp | 47 ++++++++++--------- src/smt/theory_seq.h | 3 +- 8 files changed, 200 insertions(+), 58 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 5a97e13c8..f30aa90b8 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -24,18 +24,35 @@ Notes: #include"uint_set.h" #include"automaton.h" #include"well_sorted.h" +#include"var_subst.h" +expr_ref sym_expr::accept(expr* e) { + ast_manager& m = m_t.get_manager(); + expr_ref result(m); + if (m_is_pred) { + var_subst subst(m); + subst(m_t, 1, &e, result); + } + else { + result = m.mk_eq(e, m_t); + } + return result; +} + +std::ostream& sym_expr::display(std::ostream& out) const { + return out << m_t; +} struct display_expr1 { ast_manager& m; display_expr1(ast_manager& m): m(m) {} - std::ostream& display(std::ostream& out, expr* e) const { - return out << mk_pp(e, m); + std::ostream& display(std::ostream& out, sym_expr* e) const { + return e->display(out); } }; -re2automaton::re2automaton(ast_manager& m): m(m), u(m) {} +re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m) {} eautomaton* re2automaton::operator()(expr* e) { eautomaton* r = re2aut(e); @@ -53,6 +70,7 @@ eautomaton* re2automaton::re2aut(expr* e) { expr* e1, *e2; scoped_ptr a, b; unsigned lo, hi; + zstring s1, s2; if (u.re.is_to_re(e, e1)) { return seq2aut(e1); } @@ -76,12 +94,27 @@ eautomaton* re2automaton::re2aut(expr* e) { a = eautomaton::mk_opt(*a); return a.detach(); } - else if (u.re.is_range(e)) { - // TBD + else if (u.re.is_range(e, e1, e2)) { + if (u.str.is_string(e1, s1) && u.str.is_string(e2, s2) && + s1.length() == 1 && s2.length() == 1) { + unsigned start = s1[0]; + unsigned stop = s2[0]; + unsigned nb = s1.num_bits(); + sort_ref s(bv.mk_sort(nb), m); + expr_ref v(m.mk_var(0, s), m); + expr_ref _start(bv.mk_numeral(start, nb), m); + expr_ref _stop(bv.mk_numeral(stop, nb), m); + expr_ref cond(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop)), m); + a = alloc(eautomaton, sm, sym_expr::mk_pred(cond)); + return a.detach(); + } + else { + TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";); + } } else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) { - scoped_ptr eps = eautomaton::mk_epsilon(m); - b = eautomaton::mk_epsilon(m); + scoped_ptr eps = eautomaton::mk_epsilon(sm); + b = eautomaton::mk_epsilon(sm); while (hi > lo) { scoped_ptr c = eautomaton::mk_concat(*a, *b); b = eautomaton::mk_union(*eps, *c); @@ -94,10 +127,12 @@ eautomaton* re2automaton::re2aut(expr* e) { return b.detach(); } #if 0 - else if (u.re.is_intersect(e, e1, e2)) { - - } else if (u.re.is_empty(e)) { + return alloc(eautomaton, m); + } + else if (u.re.is_full(e)) { + } + else if (u.re.is_intersect(e, e1, e2)) { } #endif @@ -114,10 +149,10 @@ eautomaton* re2automaton::seq2aut(expr* e) { return eautomaton::mk_concat(*a, *b); } else if (u.str.is_unit(e, e1)) { - return alloc(eautomaton, m, e1); + return alloc(eautomaton, sm, sym_expr::mk_char(m, e1)); } else if (u.str.is_empty(e)) { - return eautomaton::mk_epsilon(m); + return eautomaton::mk_epsilon(sm); } else if (u.str.is_string(e, s)) { unsigned init = 0; @@ -126,9 +161,9 @@ eautomaton* re2automaton::seq2aut(expr* e) { final.push_back(s.length()); for (unsigned k = 0; k < s.length(); ++k) { // reference count? - mvs.push_back(eautomaton::move(m, k, k+1, u.str.mk_char(s, k))); + mvs.push_back(eautomaton::move(sm, k, k+1, sym_expr::mk_char(m, u.str.mk_char(s, k)))); } - return alloc(eautomaton, m, init, final, mvs); + return alloc(eautomaton, sm, init, final, mvs); } return 0; } @@ -679,11 +714,11 @@ bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) { return false; } visited.insert(state); - expr* t = mvs[0].t(); - if (!t) { + sym_expr* t = mvs[0].t(); + if (!t || !t->is_char()) { return false; } - seq.push_back(m_util.str.mk_unit(t)); + seq.push_back(m_util.str.mk_unit(t->get_char())); state = mvs[0].dst(); mvs.reset(); aut.get_moves_from(state, mvs, true); @@ -727,7 +762,7 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) { br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { scoped_ptr aut; expr_ref_vector seq(m()); - if (!(aut = re2automaton(m())(b))) { + if (!(aut = m_re2aut(b))) { return BR_FAILED; } @@ -769,8 +804,8 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { aut->get_moves_from(state, mvs, false); for (unsigned j = 0; j < mvs.size(); ++j) { eautomaton::move const& mv = mvs[j]; - if (m().is_value(mv.t()) && m().is_value(ch)) { - if (mv.t() == ch) { + if (mv.t()->is_char() && m().is_value(mv.t()->get_char()) && m().is_value(ch)) { + if (mv.t()->get_char() == ch) { add_next(next, mv.dst(), acc); } else { @@ -778,7 +813,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { } } else { - cond = m().mk_eq(mv.t(), ch); + cond = mv.t()->accept(ch); if (!m().is_true(acc)) cond = m().mk_and(acc, cond); add_next(next, mv.dst(), cond); } diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 5d6c40fa1..77af42dee 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -26,11 +26,37 @@ Notes: #include"lbool.h" #include"automaton.h" +class sym_expr { + bool m_is_pred; + expr_ref m_t; + unsigned m_ref; + sym_expr(bool is_pred, expr_ref& t) : m_is_pred(is_pred), m_t(t), m_ref(0) {} +public: + expr_ref accept(expr* e); + static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, false, t); } + static sym_expr* mk_char(ast_manager& m, expr* t) { expr_ref tr(t, m); return alloc(sym_expr, false, tr); } + static sym_expr* mk_pred(expr_ref& t) { return alloc(sym_expr, true, t); } + void inc_ref() { ++m_ref; } + void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); } + std::ostream& display(std::ostream& out) const; + bool is_char() const { return !m_is_pred; } + bool is_pred() const { return m_is_pred; } + expr* get_char() const { SASSERT(is_char()); return m_t; } -typedef automaton eautomaton; +}; + +class sym_expr_manager { +public: + void inc_ref(sym_expr* s) { if (s) s->inc_ref(); } + void dec_ref(sym_expr* s) { if (s) s->dec_ref(); } +}; + +typedef automaton eautomaton; class re2automaton { ast_manager& m; - seq_util u; + sym_expr_manager sm; + seq_util u; + bv_util bv; eautomaton* re2aut(expr* e); eautomaton* seq2aut(expr* e); public: @@ -44,6 +70,7 @@ class re2automaton { class seq_rewriter { seq_util m_util; arith_util m_autil; + re2automaton m_re2aut; expr_ref_vector m_es, m_lhs, m_rhs; br_status mk_seq_concat(expr* a, expr* b, expr_ref& result); @@ -80,7 +107,7 @@ class seq_rewriter { public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): - m_util(m), m_autil(m), m_es(m), m_lhs(m), m_rhs(m) { + m_util(m), m_autil(m), m_re2aut(m), m_es(m), m_lhs(m), m_rhs(m) { } ast_manager & m() const { return m_util.get_manager(); } family_id get_fid() const { return m_util.get_family_id(); } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index e715ef571..66ff7116a 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -22,12 +22,46 @@ Revision History: #include "ast_pp.h" #include +static bool is_hex_digit(char ch, unsigned& d) { + if ('0' <= ch && ch <= '9') { + d = ch - '0'; + return true; + } + if ('A' <= ch && ch <= 'F') { + d = 10 + ch - 'A'; + return true; + } + return false; +} + +static bool is_escape_char(char const *& s, unsigned& result) { + unsigned d1, d2; + if (*s == '\\' && *(s + 1) == 'x' && + is_hex_digit(*(s + 2), d1) && is_hex_digit(*(s + 3), d2)) { + result = d1*16 + d2; + s += 4; + return true; + } + if (*s == '\\' && *(s + 1) == '\\') { + result = '\\'; + s += 2; + return true; + } + return false; +} + zstring::zstring(encoding enc): m_encoding(enc) {} zstring::zstring(char const* s, encoding enc): m_encoding(enc) { while (*s) { - m_buffer.push_back(*s); - ++s; + unsigned ch; + if (is_escape_char(s, ch)) { + m_buffer.push_back(ch); + } + else { + m_buffer.push_back(*s); + ++s; + } } } @@ -80,9 +114,10 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const { return result; } -static const char esc_table[32][3] = - { "\\0", "^A", "^B", "^C", "^D", "^E", "^F", "\\a", "\\b", "\\t", "\\n", "\\v", "\\f", "\\r", "^N", - "^O", "^P", "^Q", "^R", "^S", "^T", "^U", "^V","^W","^X","^Y","^Z","\\e","^\\","^]","^^","^_"}; +static const char esc_table[32][6] = + { "\\x00", "\\x01", "\\x02", "\\x03", "\\x04", "\\x05", "\\x06", "\\x07", "\\x08", "\\x09", "\\n", "\\v", "\\f", "\\r", "\\x0E", "\\x0F", + "\\x10", "\\x11", "\\x12", "\\x13", "\\x14", "\\x15", "\\x16", "\\x17", "\\x18", "\\x19", "\\x1A", "\\x1B", "\\x1C", "\\x1D", "\\x1E", "\\x1F" +}; std::string zstring::encode() const { SASSERT(m_encoding == ascii); @@ -91,7 +126,7 @@ std::string zstring::encode() const { unsigned char ch = m_buffer[i]; if (0 <= ch && ch < 32) { strm << esc_table[ch]; - } + } else if (ch == 127) { strm << "^?"; } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 4a94ef18f..e97e92962 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -98,6 +98,7 @@ public: zstring& operator=(zstring const& other); zstring replace(zstring const& src, zstring const& dst) const; unsigned num_bits() const { return (m_encoding==ascii)?8:16; } + encoding get_encoding() const { return m_encoding; } std::string encode() const; unsigned length() const { return m_buffer.size(); } unsigned operator[](unsigned i) const { return m_buffer[i]; } @@ -298,17 +299,19 @@ public: bool is_to_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); } bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_RE_CONCAT); } bool is_union(expr const* n) const { return is_app_of(n, m_fid, OP_RE_UNION); } - bool is_inter(expr const* n) const { return is_app_of(n, m_fid, OP_RE_INTERSECT); } + bool is_intersection(expr const* n) const { return is_app_of(n, m_fid, OP_RE_INTERSECT); } bool is_star(expr const* n) const { return is_app_of(n, m_fid, OP_RE_STAR); } bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_RE_PLUS); } bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OPTION); } bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_RE_RANGE); } bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_RE_LOOP); } - + bool is_empty(expr const* n) const { return is_app_of(n, m_fid, OP_RE_EMPTY_SET); } + bool is_full(expr const* n) const { return is_app_of(n, m_fid, OP_RE_FULL_SET); } MATCH_UNARY(is_to_re); MATCH_BINARY(is_concat); MATCH_BINARY(is_union); - MATCH_BINARY(is_inter); + MATCH_BINARY(is_intersection); + MATCH_BINARY(is_range); MATCH_UNARY(is_star); MATCH_UNARY(is_plus); MATCH_UNARY(is_opt); diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index e7d7c8bfb..084f3e4f8 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -151,7 +151,7 @@ public: m_final_states(other.m_final_states) {} - // create the automaton that accepts the empty string only. + // create the automaton that accepts the empty string/sequence only. static automaton* mk_epsilon(M& m) { moves mvs; unsigned_vector final; @@ -168,10 +168,24 @@ public: return alloc(automaton, m, 0, final, mvs); } + static automaton* clone(automaton const& a) { + moves mvs; + unsigned_vector final; + append_moves(0, a, mvs); + append_final(0, a, final); + return alloc(automaton, a.m, a.init(), final, mvs); + } + // create the sum of disjoint automata static automaton* mk_union(automaton const& a, automaton const& b) { SASSERT(&a.m == &b.m); M& m = a.m; + if (a.is_empty()) { + return clone(b); + } + if (b.is_empty()) { + return clone(a); + } moves mvs; unsigned_vector final; unsigned offset1 = 1; @@ -196,6 +210,10 @@ public: init = 0; mvs.push_back(move(m, 0, a.init() + offset)); } + if (a.is_empty()) { + return clone(a); + } + mvs.push_back(move(m, init, a.final_state() + offset)); append_moves(offset, a, mvs); append_final(offset, a, final); @@ -206,6 +224,19 @@ public: static automaton* mk_concat(automaton const& a, automaton const& b) { SASSERT(&a.m == &b.m); M& m = a.m; + if (a.is_empty()) { + return clone(a); + } + if (b.is_empty()) { + return clone(b); + } + if (a.is_epsilon()) { + return clone(b); + } + if (b.is_epsilon()) { + return clone(a); + } + moves mvs; unsigned_vector final; unsigned init = 0; @@ -295,6 +326,10 @@ public: // src - e -> dst - ET -> Dst1 => src - ET -> Dst1 if in_degree(dst) = 1, src != dst // Src - E -> dst - et -> dst1 => Src - et -> dst1 if out_degree(dst) = 1, src != dst // + // Some missing: + // src - et -> dst - E -> Dst1 => src - et -> Dst1 if in_degree(dst) = 1 + // Src - ET -> dst - e -> dst1 => Src - ET -> dst1 if out_degree(dst) = 1, + // void compress() { for (unsigned i = 0; i < m_delta.size(); ++i) { for (unsigned j = 0; j < m_delta[i].size(); ++j) { @@ -446,6 +481,7 @@ public: } bool is_empty() const { return m_final_states.empty(); } + bool is_epsilon() const { return m_final_states.size() == 1 && m_final_states.back() == init() && m_delta.empty(); } unsigned final_state() const { return m_final_states[0]; } bool has_single_final_sink() const { return m_final_states.size() == 1 && m_delta[final_state()].empty(); } unsigned num_states() const { return m_delta.size(); } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index b6350ed28..f23207f66 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -399,7 +399,7 @@ namespace smt2 { void check_keyword(char const * msg) { if (!curr_is_keyword()) throw parser_exception(msg); } void check_string(char const * msg) { if (!curr_is_string()) throw parser_exception(msg); } void check_int(char const * msg) { if (!curr_is_int()) throw parser_exception(msg); } - void check_int_or_float(char const * msg) { if (!curr_is_int() || !curr_is_float()) throw parser_exception(msg); } + void check_int_or_float(char const * msg) { if (!curr_is_int() && !curr_is_float()) throw parser_exception(msg); } void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); } void error(unsigned line, unsigned pos, char const * msg) { @@ -2341,7 +2341,7 @@ namespace smt2 { break; } case CPK_NUMERAL: - check_int("invalid command argument, numeral expected"); + check_int_or_float("invalid command argument, numeral expected"); m_curr_cmd->set_next_arg(m_ctx, curr_numeral()); next(); break; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 6c27dc104..50a32470e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -31,8 +31,8 @@ using namespace smt; struct display_expr { ast_manager& m; display_expr(ast_manager& m): m(m) {} - std::ostream& display(std::ostream& out, expr* e) const { - return out << mk_pp(e, m); + std::ostream& display(std::ostream& out, sym_expr* e) const { + return e->display(out); } }; @@ -169,7 +169,8 @@ theory_seq::theory_seq(ast_manager& m): m_lhs(m), m_rhs(m), m_atoms_qhead(0), m_new_solution(false), - m_new_propagation(false) { + m_new_propagation(false), + m_mk_aut(m) { m_prefix = "seq.prefix.suffix"; m_suffix = "seq.suffix.prefix"; m_contains_left = "seq.contains.left"; @@ -1176,7 +1177,9 @@ void theory_seq::display(std::ostream & out) const { for (; it != end; ++it) { out << mk_pp(it->m_key, m) << "\n"; display_expr disp(m); - it->m_value->display(out, disp); + if (it->m_value) { + it->m_value->display(out, disp); + } } } if (!m_rep.empty()) { @@ -1952,11 +1955,10 @@ void theory_seq::add_at_axiom(expr* e) { void theory_seq::propagate_step(literal lit, expr* step) { context& ctx = get_context(); SASSERT(ctx.get_assignment(lit) == l_true); - expr* re, *t, *s, *idx, *i, *j; - VERIFY(is_step(step, s, idx, re, i, j, t)); - expr_ref nth = mk_nth(s, idx); - TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(t, m) << " = " << nth << "\n";); - propagate_eq(lit, t, nth); + expr* re, *acc, *s, *idx, *i, *j; + VERIFY(is_step(step, s, idx, re, i, j, acc)); + TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(acc, m) << "\n";); + propagate_lit(0, 1, &lit, mk_literal(acc)); rational lo; rational _idx; if (lower_bound(s, lo) && lo.is_unsigned() && m_autil.is_numeral(idx, _idx) && lo >= _idx) { @@ -2250,15 +2252,14 @@ eautomaton* theory_seq::get_automaton(expr* re) { if (m_re2aut.find(re, result)) { return result; } - result = re2automaton(m)(re); + result = m_mk_aut(re); if (result) { display_expr disp(m); TRACE("seq", result->display(tout, disp);); } - if (result) { - m_automata.push_back(result); - m_trail_stack.push(push_back_vector >(m_automata)); - } + m_automata.push_back(result); + m_trail_stack.push(push_back_vector >(m_automata)); + m_re2aut.insert(re, result); m_trail_stack.push(insert_obj_map(m_re2aut, re)); return result; @@ -2281,10 +2282,11 @@ bool theory_seq::is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& idx, exp s = to_app(e)->get_arg(0); idx = to_app(e)->get_arg(1); re = to_app(e)->get_arg(2); + TRACE("seq", tout << mk_pp(re, m) << "\n";); VERIFY(m_autil.is_numeral(to_app(e)->get_arg(3), r)); SASSERT(r.is_unsigned()); i = r.get_unsigned(); - aut = m_re2aut[re]; + aut = get_automaton(re); return true; } else { @@ -2311,12 +2313,13 @@ bool theory_seq::is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, exp } } -expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, expr* t) { +expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, expr* acc) { + SASSERT(m.is_bool(acc)); expr_ref_vector args(m); args.push_back(s).push_back(idx).push_back(re); args.push_back(m_autil.mk_int(i)); args.push_back(m_autil.mk_int(j)); - args.push_back(t); + args.push_back(acc); return expr_ref(m_util.mk_skolem(m_aut_step, args.size(), args.c_ptr(), m.mk_bool_sort()), m); } @@ -2390,7 +2393,9 @@ bool theory_seq::add_accept2step(expr* acc) { for (unsigned i = 0; i < mvs.size(); ++i) { unsigned j = (i + start) % mvs.size(); eautomaton::move mv = mvs[j]; - step = mk_step(e, idx, re, src, mv.dst(), mv.t()); + expr_ref nth = mk_nth(e, idx); + expr_ref acc = mv.t()->accept(nth); + step = mk_step(e, idx, re, src, mv.dst(), acc); lits.push_back(mk_literal(step)); switch (ctx.get_assignment(lits.back())) { case l_true: @@ -2433,8 +2438,8 @@ bool theory_seq::add_accept2step(expr* acc) { bool theory_seq::add_step2accept(expr* step) { context& ctx = get_context(); SASSERT(ctx.get_assignment(step) == l_true); - expr* re, *t, *s, *idx, *i, *j; - VERIFY(is_step(step, s, idx, re, i, j, t)); + expr* re, *_acc, *s, *idx, *i, *j; + VERIFY(is_step(step, s, idx, re, i, j, _acc)); literal acc1 = mk_accept(s, idx, re, i); switch (ctx.get_assignment(acc1)) { case l_false: @@ -2508,7 +2513,7 @@ bool theory_seq::add_reject2reject(expr* rej) { bool has_undef = false; for (unsigned i = 0; i < mvs.size(); ++i) { eautomaton::move const& mv = mvs[i]; - literal eq = mk_eq(nth, mv.t(), false); + literal eq = mk_literal(mv.t()->accept(nth)); switch (ctx.get_assignment(eq)) { case l_false: case l_true: diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 927cec537..8e0b8e17e 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -278,6 +278,7 @@ namespace smt { unsigned m_atoms_qhead; bool m_new_solution; // new solution added bool m_new_propagation; // new propagation to core + re2automaton m_mk_aut; virtual final_check_status final_check_eh(); virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); } @@ -411,7 +412,7 @@ namespace smt { return is_acc_rej(m_reject, rej, s, idx, re, i, aut); } bool is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut); - expr_ref mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* t); + expr_ref mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* acc); bool is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const; bool is_step(expr* e) const; void propagate_step(literal lit, expr* n); From 57e1d4dc1ff3c62135a0a4d6628fc811dd924c44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Jan 2016 10:39:38 +0100 Subject: [PATCH 13/13] model generation with strings Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 8 +++++++- src/smt/theory_seq.cpp | 8 ++++++-- 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index f30aa90b8..439d60bbf 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -938,7 +938,6 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) { bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) { expr* a, *b; zstring s; - bool lchange = false; SASSERT(lhs.empty()); // solve from back @@ -1327,6 +1326,13 @@ bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, ex found = !rpos.contains(j) && l[i] == r[j]; } if (!found) { +#if 0 + std::cout << mk_pp(l[i], m()) << " not found in "; + for (unsigned j = 0; j < szr; ++j) { + std::cout << mk_pp(r[j], m()) << " "; + } + std::cout << "\n"; +#endif return false; } SASSERT(0 < j && j <= szr); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 50a32470e..c7fab3934 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1325,7 +1325,10 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { if (concats.size() > 1) { for (unsigned i = 0; i < concats.size(); ++i) { - sv->add_dependency(ctx.get_enode(concats[i])); + expr* e = concats[i]; + if (!m_util.str.is_string(e)) { + sv->add_dependency(ctx.get_enode(e)); + } } } else if (m_util.str.is_unit(e, e1)) { @@ -1361,7 +1364,8 @@ app* theory_seq::mk_value(app* e) { unsigned sz; if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) { unsigned v = val.get_unsigned(); - if ((v < 7) || (14 <= v && v < 32) || v == 127) { + if (false && ((v < 7) || (14 <= v && v < 32) || v == 127)) { + // disabled: use escape characters. result = m_util.str.mk_unit(result); } else {