Consolidated bugs in string logics 2

[muchang]

(smt.arith.solver=6) Soundness bug on QF_S formula. smt.arith.solver=6 seems to be wrong.

[556] % z3release smt.arith.solver=6 small.smt2
sat
[557] % z3release smt.arith.solver=2 small.smt2
unsat
[558] % 
[558] % cat small.smt2
(declare-fun a () String)
(declare-fun var_9 () String)
(assert (str.in_re (str.++ "z" var_9) (re.* (str.to_re "z"))))
(assert (str.in_re (str.++ "a" var_9) (re.+ (re.range "a" "u"))))
(assert (str.in_re (str.++ "a" a) (re.opt (re.range "a" "u"))))
(assert (not (str.in_re (str.++ "a" a "za" var_9) (re.opt (re.++ (str.to_re "a") (re.* (str.to_re "z")) (str.to_re "a"))))))
(check-sat)
[559] %

Commit: 7708874

[muchang]

Invalid model bug on QF_S formula.

[554] % z3release model_validate=true small.smt2
sat
(error "line 6 column 10: an invalid model was generated")
(model 
 (define-fun b () String
  "")
 (define-fun a () String
  "\x00")
 (define-fun c () String
  "\x00")
)
[555] % 
[555] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(assert (str.in_re (str.substr a 0 (str.len b)) (re.opt (str.to_re "A"))))
(assert (= 0 (str.len (str.substr a (str.len b) (str.len c)))))
(check-sat)
(get-model)
[556] %

Commit: 7708874

[muchang]

Z3 solution soundness bug on QF_S formula

[596] % z3release small.smt2
sat
[597] % z3release rewriter.flat=false small.smt2
unsat
[598] %
[598] % cat small.smt2
(declare-const a String)
(declare-const b String)
(declare-const c String)
(declare-const d String)
(declare-const e String)
(declare-const f Bool)
(assert (= f (and (= "sqs" a))))
(declare-const g Bool)
(assert (= g (and (= c "aws") (= e "") (= b "111144448888") (str.in_re d (re.++ (str.to_re "ab") (str.to_re "bb") (re.* re.allchar) (str.to_re "b"))))))
(declare-const h Bool)
(assert (= h (and f g)))
(declare-const k Bool)
(assert (= k true h))
(declare-const i Bool)
(assert (= i (not k)))
(declare-const j Bool)
(assert (= j (= "" a)))
(declare-const l Bool)
(assert (= l (and (= c "aws") (= b "111144448888") (str.in_re d (re.++ (str.to_re "a")  (re.* re.allchar) (str.to_re "b") (re.* re.allchar) (str.to_re "b"))))))
(declare-const m Bool)
(assert (= m l))
(declare-const n Bool)
(assert (= n m))
(assert (not n))
(assert (not (str.contains e ":")))
(check-sat)
[599] %

OS: Ubuntu 18.04
Commit: 2d52367

[muchang]

Invalid model on QF_S formula with regex

[532] % z3release small.smt2
sat
(model 
 (define-fun f () String
  "\x00")
 (define-fun i () String
  "\x00")
 (define-fun c () String
  "\x00")
 (define-fun d () String
  "\x00")
 (define-fun T4_6 () String
  "")
 (define-fun e () Int
  0)
 (define-fun g () Bool
  false)
 (define-fun b () String
  "\x00\x00")
 (define-fun h () Bool
  true)
 (define-fun a () String
  "")
)
unsat
[533] % 
[533] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun e () Int)
(declare-fun f () String)
(declare-fun T4_6 () String)
(declare-fun g () Bool)
(declare-fun h () Bool)
(declare-fun i () String)
(assert (ite g (and (distinct e 0) (distinct (str.substr a 6 0)
 (str.++ (str.substr b 4 (str.len f)))) (not (str.in_re (str.substr d 8
 (str.len T4_6)) (re.++ (str.to_re "_") (re.++ (str.to_re "_") (re.++
 (str.to_re "u") (re.++ (str.to_re "t") (re.++ (str.to_re "m") (re.++
 (str.to_re "a") (re.union (str.to_re "=") (re.++ (re.++ (str.to_re
 "6") (re.++ (str.to_re "8") (re.++ (str.to_re "8"))))))))))))))) (not
 (str.in_re (str.substr a 6 0) (re.++ (str.to_re "u") (str.to_re "m"))))))
(assert (distinct h (= (str.substr b (str.len f) (str.len (str.substr c 0 (str.len (str.substr d 0 (str.len i)))))) "")))
(assert h)
(assert (= b (str.++ f i)))
(assert (distinct d (str.++ T4_6 i)))
(check-sat)
(get-model)
(reset)
 (define-fun f () String
  "\x00")
 (define-fun i () String
  "\x00")
 (define-fun c () String
  "\x00")
 (define-fun d () String
  "\x00")
 (define-fun T4_6 () String
  "")
 (define-fun e () Int
  0)
 (define-fun g () Bool
  false)
 (define-fun b () String
  "\x00\x00")
 (define-fun h () Bool
  true)
 (define-fun a () String
  "")
(assert (ite g (and (distinct e 0) (distinct (str.substr a 6 0)
 (str.++ (str.substr b 4 (str.len f)))) (not (str.in_re (str.substr d 8
 (str.len T4_6)) (re.++ (str.to_re "_") (re.++ (str.to_re "_") (re.++
 (str.to_re "u") (re.++ (str.to_re "t") (re.++ (str.to_re "m") (re.++
 (str.to_re "a") (re.union (str.to_re "=") (re.++ (re.++ (str.to_re
 "6") (re.++ (str.to_re "8") (re.++ (str.to_re "8"))))))))))))))) (not
 (str.in_re (str.substr a 6 0) (re.++ (str.to_re "u") (str.to_re "m"))))))
(assert (distinct h (= (str.substr b (str.len f) (str.len (str.substr c 0 (str.len (str.substr d 0 (str.len i)))))) "")))
(assert h)
(assert (= b (str.++ f i)))
(assert (distinct d (str.++ T4_6 i)))
(check-sat)
[534] % 

OS: Ubuntu 18.04
Commit: 2d52367

[muchang]

Invalid model on QF_S formula with str.in_re and str.to_re

[542] % z3release model_validate=true small.smt2
sat
(error "line 5 column 10: an invalid model was generated")
(model 
 (define-fun b () String
  "")
 (define-fun a () String
  "\x00")
)
[543] % 
[543] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (str.in_re (str.substr a 0 (str.len b)) (re.opt (str.to_re "t"))))
(assert (distinct b ""))
(check-sat)
(get-model)
[544] %

OS: Ubuntu 18.04
Commit: 1e6d2fb

[muchang]

It seems z3seq misses support for replace_all or some rewrites.

[545] % z3release small.smt2
unknown
[546] % z3release smt.string_solver=z3str3 small.smt2
sat
[547] % cvc4 -q small.smt2
sat
[548] % 
[548] % cat small.smt2
(assert (= (str.replace_all "" "" "") ""))
(check-sat)
[549] %

OS: Ubuntu 18.04
Commit: 1e6d2fb

[muchang]

z3 solution soundness bug (model validation doesn't catch the returned invalid model)

[623] % z3release smt.string_solver=z3str3 small.smt2
unsat
[624] % cvc4 --strings-exp -q small.smt2
unsat
[625] %
[625] % z3release small.smt2
sat
[626] %
[626] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Bool)
(declare-fun h () String)
(declare-fun i () Bool)
(declare-fun j () String)
(declare-fun k () Bool)
(declare-fun l () Bool)
(declare-fun m () String)
(declare-fun n () Bool)
(declare-fun o () String)
(assert (distinct l (distinct f 0)))
(assert
 (ite (= g n)
 (and (= f (+ e 7))
  (distinct m (str.++ j (str.substr a 5 0)))
  (= e (str.len (str.substr b 0 (str.len h))))
  (not (str.in_re (str.substr b 4 (str.len h))
     (re.union (str.to_re "_") (str.to_re "u")))))
 (str.in_re (str.substr a 8 0) (str.to_re ""))))
(assert (= (distinct c (= d k)) (> 0 f)))
(assert (not i))
(assert (= b (str.++ h o)))
(assert (= c (= i n) d (= k n)))
(assert (distinct g (= l n)))
(check-sat)
[627] %

Commit: 2572440

[muchang]

z3 arith.solver=6 performance regression vs. arith.solver=2 on QF_S formula

[511] % time z3-4.8.8 smt.arith.solver=2 small.smt2 
sat
real  0m0.267s
user  0m0.026s
sys   0m0.006s
[512] % time z3-4.8.8 smt.arith.solver=6 small.smt2 
sat
real  0m0.823s
user  0m0.050s
sys   0m0.006s
[513] % 
[513] % time z3release smt.arith.solver=2 small.smt2 
sat
real  0m0.365s
user  0m0.161s
sys   0m0.004s
[514] % time z3release smt.arith.solver=6 small.smt2 
sat
real  1m50.083s
user  1m31.441s
sys   0m0.161s
[515] % 
[515] % cat small.smt2 
(set-logic ALL)
(declare-fun s () String)
(assert (distinct s "AA"))
(assert (> (str.indexof s "A" 20) 0))
(check-sat)
[516] %

OS: Ubuntu 18.04
Commit: 6cc52e0

[muchang]

Z3seq performance issue on QF_S formula with regex
For this formula, both CVC4 and Z3str give results quickly (less than 1 second), while Z3seq (both mt.arith.solver=2 and 6) gives results in more than 10 seconds.

[562] % time cvc4 -q small.smt2
sat
real  0m0.321s
user  0m0.027s
sys   0m0.006s
[563] % 
[563] % time z3release smt.string_solver=z3str3 small.smt2
sat
real  0m0.043s
user  0m0.020s
sys   0m0.000s
[564] % time z3release smt.arith.solver=6 small.smt2
sat
real  0m17.801s
user  0m17.036s
sys   0m0.028s
[565] % time z3release smt.arith.solver=2 small.smt2
sat
real  0m10.240s
user  0m8.797s
sys   0m0.047s
[566] % 
[566] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun e () String)
(assert (= b "\x20\x2d\x20\x3c\x61\x20\x68\x72\x65\x66\x3d\x5c\x22\x6d\x6f\x64\x5f\x70\x6c\x75\x67\x69\x6e\x73\x2e\x70\x68\x70\x3f\x61\x63\x74\x69\x6f\x6e\x3d\x69\x6e\x73\x74\x61\x6c\x6c\x26\x70\x6c\x75\x67\x69\x6e\x5f\x66\x69\x6c\x65\x3d"))
(assert (= c (str.++ a b)))
(assert (distinct d "\x22\x3e\x49\x6e\x73\x74\x61\x6c\x6c\x3c\x2f\x61\x3e\x20\x5c\x6e"))
(assert (= e (str.++ c d)))
(assert (str.in_re e (re.++ (re.opt re.allchar) (str.to_re "\x5c\x3c\x53\x43\x52\x49\x50\x54") (re.opt re.all))))
(check-sat)
[567] %

OS: Ubuntu 18.04
Commit: 6cc52e0

[muchang]

Z3seq performance issue on QF_S formula with str.replace

[554] % time cvc4 small.smt2
unsat
real  0m0.058s
user  0m0.009s
sys   0m0.000s
[555] % 
[555] % timeout -s 9 30 z3release small.smt2
Killed
[556] % 
[556] % cat small.smt2
(set-logic QF_S)
(declare-const x String)
(assert (distinct (str.replace (str.replace x "B" x) x "A") (str.replace (str.replace x "B" "A") x "A")))
(check-sat)
[557] %

Commit: fb6e7e1

[NikolajBjorner]

Z3seq performance issue on QF_S formula with regex
(assert (= b "\u{20}\u{2d}\u{20}\u{3c}\u{61}\u{20}\u{68}\u{72}\u{65}\u{66}\u{3d}\u{5c}\u{22}\u{6d}\u{6f}\u{64}\u{5f}\u{70}\u{6c}\u{75}\u{67}\u{69}\u{6e}\u{73}\u{2e}\u{70}\u{68}\u{70}\u{3f}\u{61}\u{63}\u{74}\u{69}\u{6f}\u{6e}\u{3d}\u{69}\u{6e}\u{73}\u{74}\u{61}\u{6c}\u{6c}\u{26}\u{70}\u{6c}\u{75}\u{67}\u{69}\u{6e}\u{5f}\u{66}\u{69}\u{6c}\u{65}\u{3d}"))
(assert (= c (str.++ a b)))
(assert (distinct d "\u{22}\u{3e}\u{49}\u{6e}\u{73}\u{74}\u{61}\u{6c}\u{6c}\u{3c}\u{2f}\u{61}\u{3e}\u{20}\u{5c}\u{6e}"))
(assert (= e (str.++ c d)))
(assert (str.in_re e (re.++ (re.opt re.allchar) (str.to_re "\u{5c}\u{3c}\u{53}\u{43}\u{52}\u{49}\u{50}\u{54}") (re.opt re.all))))
(check-sat)
OS: Ubuntu 18.04
Commit: 6cc52e0

@veanes @cdstanford - this example exercises regex membership queries where the regex solver is very slow.

[NikolajBjorner]

created separate bug for performance.