State graph dgml update and fixes in condition simplifier

[veanes]

Main changes:

1. added a feature to state graph dgml output to collapse and un-collapse states to view regexes inside of them in VS
2. fixed negated range constraint simplification that did not work,
   constraints of the form !('a' <= x <= 'z') were ignored by the simplifier
3. removed some dead code (regex rewrites no longer needed due to normalization)

regarding (2), as a repo, the following two concrete unsat examples did not terminate,
but are working fine with this update:
these examples are variants using ranges from to the earlier issue #5693

(declare-const s String)
(assert (let ((a!1 (re.++ (re.range "0" "9")
(re.* (re.++ (str.to_re "b") (re.range "0" "9")))))
(a!2 (re.++ (re.* (re.++ (re.range "0" "9") (str.to_re "b")))
(re.range "0" "9"))))
(str.in.re s (re.diff (re.++ a!1 a!1) (re.++ a!2 a!2)))))
(check-sat)

(reset)

(declare-fun a () String)
(assert (str.in_re a (re.union
(re.inter
(re.++ (re.++ (re.range "a" "z") (re.* (re.++ (re.range "A" "Z") (re.range "a" "z")))) (re.++ (re.range "a" "z") (re.* (re.++ (re.range "A" "Z") (re.range "a" "z")))))
(re.comp
(re.++ (re.++ (re.* (re.++ (re.range "a" "z") (re.range "A" "Z"))) (re.range "a" "z")) (re.++ (re.* (re.++ (re.range "a" "z") (re.range "A" "Z"))) (re.range "a" "z")))
)
)
(re.inter
(re.++ (re.++ (re.* (re.++ (re.range "a" "z") (re.range "A" "Z"))) (re.range "a" "z")) (re.++ (re.* (re.++ (re.range "a" "z") (re.range "A" "Z"))) (re.range "a" "z")))
(re.comp
(re.++ (re.++ (re.range "a" "z") (re.* (re.++ (re.range "A" "Z") (re.range "a" "z")))) (re.++ (re.range "a" "z") (re.* (re.++ (re.range "A" "Z") (re.range "a" "z")))))
)
)
)))
(check-sat)

[veanes]

The build failures do not seem related to the new changes in this pr.

[veanes]

The last commit fixes another nontermination bug related to normal form violations.
Loops with both lower and upper bound 0 must not be created.
This issue was detected very quickly using the updated graph viewer feature.

The repo case that is unsat and did not terminate earlier (does terminate with unsat after this commit) is this:

(declare-const s String)
(assert (str.in_re s (re.+ (re.inter (re.++ ((_ re.loop 0 3) (re.+ (str.to_re "a"))) (str.to_re "c")) (re.* (re.range "a" "b"))))))
(check-sat)

[veanes]

The last commit also avoids a nontermination, also violating normal forms, namely a loop with upper and lower bound =1 is not a loop, or else normal forms are not detected correctly and unsat cases may diverge, here is a repo (with this commit it terminates with unsat result):

(declare-const s String)
(assert (str.in_re s
(re.inter (re.++ (re.++ (re.++ re.all (str.to_re "a")) ((_ re.loop 3 3) re.allchar)) (str.to_re "b")) (re.++ (re.* (str.to_re "a")) (str.to_re "c")))
))
(check-sat)

[NikolajBjorner]

added your examples to Z3Prover/z3test@ad9236f

[NikolajBjorner]

There is a regression.
This test now times out, z3test\regressions\smt2\issue-1224.smt2

(set-option :encoding ascii)
(declare-fun X () String)
(assert (not (str.in.re X (re.* (re.range "\u{0}" "\u{FF}")))))
(check-sat)

(reset)
(set-option :encoding unicode)
(declare-fun X () String)
(assert (not (str.in.re X (re.* (re.range "\u{0}" "\u{2FFFF}")))))
(check-sat)

[veanes]

I'll look into this.
I believe there is a general issue of re-rewrites interfering with derivatives. so that a rewrite of a regex to an equivalent regex then causes a disconnect in the state-graph between a state (containing as subexpression the original regex that was rewritten), bur because there are no "epsilon" transitions in the state-graph corresponding to those rewrites, this is unknown so the states loo as different/disconnected state. I'm seeing this now with other examples as well.
This mostly affects unsat cases -- might be the case here too.

[veanes]

Ohh, In this case there is a bug due to infeasible transition in state graph because there is a transition
~(.) --> .
that makes no sense because ~(.*) is the trivial deadend []

[NikolajBjorner]

Your fix broke the first two examples from #5721. See regression test failure.

[veanes]

I found the bug in is_char_const_range had messed up the params with a stupid mistake, earlier overwritten a param e1 that was assumed to be untouched. will fix now.
Also fixed another related bug that caused a variant of 1224 to diverge, will add a new example to that in the pr for this fix. I'll try to make sure that the other examples pass before making a PR, --- what an annoying "evil circle" of regressions, but very useful tests in finding these bugs actually!!!