Question: Sequence logic

[LeventErkok]

I've tried using vampire with --input_syntax smtlib2 for an SMTLib benchmark containing a sequence problem (https://microsoft.github.io/z3guide/docs/theories/Sequences/)

Vampire complained:

User error: Unrecognized term identifier 'Seq' in top-level expression <snip>

I'm most likely being naive here and I shouldn't expect vampire to understand sequence logic as supported by z3/cvc5 I suppose. But wanted to double check.

Assuming this is indeed not supported, is there a way to use vampire for quantified problems over list-like data-structures? Any examples/documentation regarding this would be appreciated.

[MichaelRawson]

I have no idea, but I've never seen code that handled it and git grep Seq turned up nothing relevant. So let's say "no" unless anyone else knows better.

is there a way to use vampire for quantified problems over list-like data-structures?

Yes, you can use Vampire's support for datatypes to define a list. Look at the inductive benchmarks, like this one about lists of natural numbers.

If you want polymorphic lists, @mezpusz is the expert and has some benchmarks somewhere.

[LeventErkok]

Thanks!

I tried that benchmark, and vampire (freshly built) timed-out after 60s on it. Should I have waited longer?

[MichaelRawson]

Those benchmarks do require inductive reasoning, which is not turned on by default - so Vampire will be trying very hard to prove something that isn't provable. I just meant to provide an example of the syntax so that you can adapt it to your own problems.

[LeventErkok]

Thanks!