API for accessing an element of a sequence

[LeventErkok]

As discussed here: https://stackoverflow.com/questions/46696982/how-do-you-extract-an-element-as-the-base-type-from-a-seq-type-in-z3

Is there an API (both at SMT-Lib and from other interfaces) to access the element at a given index of a sequence?

I can imagine one issue with this API: What if the index is out-of-bounds. Perhaps that's the reason this function doesn't exist? Maybe the user can be required to provide a default if that is the case.

[NikolajBjorner]

There isn't an API. The API builds on the string proposal for SMT-LIB2 and extends minimally with a unit constructor and allows general sequences. There is a workaround as follows:

Introduce a function nth: (Seq A) Int -> A
Then add the axiom unit(nth(s,j)) = at(s,j) or at(s,j) = empty
for every occurrence of at(s,j), or alternatively add a quantifier with pattern { at(s,j) .

[LeventErkok]

@NikolajBjorner I was under the impression that users aren't allowed to define polymorphic functions in benchmarks. So, nth has to be declared for each monomorphic sequence instance needed; is that correct?

[NikolajBjorner]

Correct, polymorphic function declarations / definitions are not (yet) available.

[LeventErkok]

Thanks.. Doesn't seem very effective though, I'm getting unknown for the following rather innocuous query:

(define-sort ISeq () (Seq Int))
(define-const x ISeq (seq.unit 5))
(define-const y ISeq (seq.unit 6))

(declare-fun ISeq.nth (ISeq Int) Int)
(assert (forall ((s ISeq) (i Int))
           (! (or (= (seq.unit (ISeq.nth s i)) (seq.at s i))
                  (= (as seq.empty ISeq)       (seq.at s i)))
           :pattern (seq.at s i)
           :pattern (ISeq.nth s i)
           )))
(assert (<= (ISeq.nth x 0) (ISeq.nth y 0)))
(check-sat)

Should I use a different set of patterns?

[NikolajBjorner]

likely because Z3 doesn't know that the quantifiers are satisfiable.

[LeventErkok]

OK, I'll close this ticket since at this time it's more of a curiosity.

For reference, I found at least two references where people axiomatized lists with that operation built in:

• http://www.kroening.com/smt-lib-lsm.pdf
• http://smt2012.loria.fr/paper11.pdf (by you!)

Would be nice if this was incorporated directly into the sequence theory, which I presume would make it work more friendly with the necessary axiomatization?

[NikolajBjorner]

Granted, it is a valid point

[LeventErkok]

I'm going to reopen this ticket, as it's popping up quite often. No urgency, but a nice-to-have.

[LeventErkok]

@NikolajBjorner

Looks like you added support for nth in:

834cf96

I'm closing this ticket. Thanks!

[OrenGitHub]

Posted an update answer in stack overflow about nth.