seq issues - running

[NikolajBjorner]

accumulated issues for seq

[NikolajBjorner]

an instance involving nth

(set-option :rewriter.eq2ineq true)
(declare-fun z () Int)
(declare-fun b () (Seq Int))
(declare-fun y () Int)
(declare-fun a () (Seq Int))
(declare-fun x () Int)
(assert (and (= 1 z) (distinct (seq.nth b x) (seq.nth a z)) (= (seq.nth b y) (seq.nth b 1))))
(assert (> x 0))
(assert (> z 0))
(check-sat)

[NikolajBjorner]

Solution unsoundness:

[556] % cvc5 -q --strings-exp small.smt2
unsat
[557] % z3release model_validate=true small.smt2
sat
(error "line 3 column 10: an invalid model was generated")
[558] % cat small.smt2
(declare-fun a () String)
(assert (str.in_re (str.++ a "AA") (re.++ (re.* (str.to_re "B")) (str.to_re (str.substr (str.++ "B" a) (str.len a) (str.len a))))))
(check-sat)
[559] % 

@veanes - this is so far the only remaining regex bug in this thread.

[NikolajBjorner]

(declare-fun z () (Seq Bool))
(assert (not (seq.nth (as seq.empty (Seq Bool)) 0)))
(assert (seq.nth (seq.extract z 1 (- (seq.len z) 1)) 0))
(check-sat)

[zhendongsu]

Invalid model:

[543] % z3release model_validate=true small.smt2
sat
(error "line 3 column 10: an invalid model was generated")
(
  (define-fun a () String
    "B")
)
[544] % 
[544] % cat small.smt2
(declare-fun a () String)
(assert (= (= a "") (str.in_re a (re.range "A" a))))
(check-sat)
(get-model)
[545] % 

[zhendongsu]

Refutation unsoundness:

[534] % z3release small.smt2
unsat
sat
[535] % cat small.smt2
(declare-fun a () String)
(assert (str.in_re (str.replace (str.++ a "B") "B" "A") (re.* (re.+ (re.range "A" (str.replace "A" (str.++ a "B") ""))))))
(check-sat)
(reset)
(define-fun a () String "")
(assert (str.in_re (str.replace (str.++ a "B") "B" "A") (re.* (re.+ (re.range "A" (str.replace "A" (str.++ a "B") ""))))))
(check-sat)
[536] % 

[zhendongsu]

Refutation unsoundness (might be related to #5591 (comment), but simpler):

[562] % z3release small.smt2
unsat
[563] % cvc5 -q small.smt2
sat
[564] % cat small.smt2
(declare-fun a () String)
(assert (str.in_re "A" (re.range "A" (str.replace "A" (str.++ a "B") ""))))
(check-sat)
[565] % 

[zhendongsu]

Another refutation unsoundness instance:

[520] % z3release small.smt2
unsat
[521] % cvc5 -q small.smt2
sat
[522] % cat small.smt2
(declare-fun a () String)
(assert (str.in_re a (re.inter (re.range a "B") (str.to_re "A"))))
(check-sat)
[523] %

[zhendongsu]

Another likely related refutation unsoundness instance:

[517] % z3release small.smt2
unsat
[518] % cvc5 -q small.smt2
sat
[519] % cat small.smt2
(declare-fun a () String)
(assert (str.in_re a (re.inter (re.opt (re.range a a)) (str.to_re "A"))))
(check-sat)
[520] % 

[zhendongsu]

Invalid model (possibly related to the other instances also involving re.range):

[568] % z3release model_validate=true small.smt2
sat
(error "line 3 column 10: an invalid model was generated")
(
  (define-fun a () String
    "A")
)
[569] % cat small.smt2
(declare-fun a () String)
(assert (not (str.in_re a (re.range a a))))
(check-sat)
(get-model)
[570] % 

[zhendongsu]

Another invalid model instance:

[540] % z3release model_validate=true small.smt2
sat
(error "line 4 column 10: an invalid model was generated")
(
  (define-fun a () String
    "BC")
)
[541] % cat small.smt2
(declare-fun a () String)
(assert (= (str.len a) 2))
(assert (not (str.in_re (str.at a 0) (re.range "A" (str.at a 1)))))
(check-sat)
(get-model)
[542] %