Unexpected behaviour for z3_seq_4.8.14

[SebastianKuehne98]

(set-option :produce-unsat-cores true)
; 
(set-info :status unsat)
(assert (! 
 (let ((?x844 ((_ re.loop 0) re.all)))
 (= ?x844 re.all)) :named a0))
(check-sat)

(get-unsat-core)
(get-info :reason-unknown)

z3_seq_4.8.14 returns sat. But according to SMT-LIB ((re.^ 0) re.all) = str.to_re "".

(set-option :random-seed 42)
(set-option :produce-models true)
; 
(set-info :status sat)
(declare-fun tmp_reglan1 () (RegEx String))
(assert
 (let ((?x56 (str.to_re "b")))
 (let ((?x1007 (re.comp ?x56)))
 (let ((?x1008 (re.inter re.allchar ?x1007)))
 (let ((?x991 (re.diff re.allchar tmp_reglan1)))
 (= ?x991 ?x1008))))))
(check-sat)

(get-value (tmp_reglan1 ))
(get-info :reason-unknown)

z3_seq_4.8.14 returns unsat.

[NikolajBjorner]

SMTLIB does not define re.loop for only one argument. It isn't part of SMTLIB definition. z3 defines it to be lower bound 0 repetitions, upper bound infinity. Use re.^ to get the semantics you are seeking.

The second example is for @veanes

[SebastianKuehne98]

First I want to say thank you for always being so supportive! I obtained the first formula by using mkLoop(re.all,0,0) in the java api. The formula then gets "transformed" into (( re.loop 0) re.all). I don't know if this is intended, as using the same parameter twice usually does not get further "simplified", for instance mkLoop(re.all,1,1) gets "transformed" into (( re.loop 1 1) re.all). Furthermore I am sorry for all the recent requests for the java api, but would it be possible to also add the re.^ function to the java api? Thank you!

[NikolajBjorner]

the re.^ function to the java api?

This was done

[NikolajBjorner]

I now see what the problem is. The API assigns a special meaing to loop(r, 0, 0), as documented where Z3_mk_re_loop is declared:

       \brief Create a regular expression loop. The supplied regular expression \c r is repeated
       between \c lo and \c hi times. The \c lo should be below \c hi with one exception: when
       supplying the value \c hi as 0, the meaning is to repeat the argument \c r at least
       \c lo number of times, and with an unbounded upper bound.

It must have been my intent that if you want loop(r, 0, 0) you might was well have used the empty string regex.

You could make the case that the API behavior should change (this has to be a rarely used feature), but for now it explains the behavior as documented.

[SebastianKuehne98]

Thank you!