`.ys` file support for finite fields?

[RyanGlScott]

I am experimenting with Yices 2.7.0's new support for finite fields. My understanding is that Yices supports parsing two syntaxes: the syntax used in .ys files, and the SMT-LIB syntax used in .smt2 files. There are examples of finite fields' SMT-LIB syntax in the yices2 repo, but I could not find any examples of finite fields' .ys syntax. Does Yices support finite fields in .ys files at all? I found some code in the .ys pretty-printer code here which suggests that perhaps they are supported, but if I try writing a .ys file like this:

(define u::(finitefield 5))

Then Yices rejects it:

$ yices test.ys
test.ys: syntax error (line 1, column 13)

[ahmed-irfan]

Finite fields aren't supported in the native .ys language — only via SMT-LIB (.smt2) and the C API.

[RyanGlScott]

Thanks! Out of curiosity, is the omission of finite fields in the native .ys language intentional, or is it something that just hasn't been implemented yet? I ask since I maintain a tool that supports generating queries in both Yices syntaxes, so I'm wondering if I will need to add a special case for the SMT-LIB syntax that isn't present in the .ys syntax.

[karthiknukala]

I'd like to add support for this (and other deviations between SMTLIB and the Yices language) to Yices2.

We've been a little sloppy with maintaining the correspondence/common feature set but there's been recent interest in finite field arithmetic support in internal tools that similarly use the Yices language, so this should be made available.