mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

pp support for regex expressions is more-or-less standard syntax

Browse source
This commit is contained in:
Margus Veanes 2020-08-13 12:40:35 -07:00
parent 9729db16a2
commit 2c33bd6faf
3 changed files with 203 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/seq_regex.cpp
View file

@ -791,6 +791,10 @@ namespace smt {
STRACE("seq_regex_brief", tout << "(MAX SIZE REACHED) ";);
return false;
}
STRACE("seq_regex", tout << "Updating state graph for regex "
<< mk_pp(r, m) << ") ";);
if (!m_state_graph.is_seen(r_id))
STRACE("state_graph", tout << std::endl << "state(" << r_id << ") = " << re().pp(r) << std::endl;);
// Add state
m_state_graph.add_state(r_id);
STRACE("state_graph", tout << "regex(" << r_id << ") = " << mk_pp(r, m) << std::endl;);
@ -811,7 +815,10 @@ namespace smt {
for (auto const& dr: derivatives) {
unsigned dr_id = get_state_id(dr);
STRACE("seq_regex_verbose", tout
<< " traversing deriv: " << dr_id << " " << std::endl;);
<< std::endl << " traversing deriv: " << dr_id << " ";);
if (!m_state_graph.is_seen(dr_id))
STRACE("state_graph", tout << "state(" << dr_id << ") = " << re().pp(dr) << std::endl;);
// Add state
m_state_graph.add_state(dr_id);
STRACE("state_graph", tout << "regex(" << dr_id << ") = " << mk_pp(dr, m) << std::endl;);
bool maybecycle = can_be_in_cycle(r, dr);