search

oeb25 / smtlib-rs

A high-level API for interacting with SMT solvers.
https://crates.io/crates/smtlib
18 stars 8 forks source link

Feature request: SyGuS input format #2

Open Sicheng-Pan opened 10 months ago

Sicheng-Pan commented 10 months ago

Hi!

Since CVC5 has a Syntax-Guided-Synthesis (SyGuS) engine, it would be really nice if it could be used in Rust! Currently the SyGuS input format is closely modeled after the smtlib format (link here), may I ask if there is any plan to support it in this library?

oeb25 commented 8 months ago

Hey! There's currently no plan to add this, as I didn't know of SyGuS till now 😉

I'm no opposed to it at all, but I'm not really in a place where I would know how to build the API, since I can't quite tell how it relates to SMT-LIB and where it differs.

The way this crate is designed (specifically smtlib-lowlevel) is by generating a bunch of code from a version of the SMT-LIB specification in TOML: see this. So there might be two approaches:

  1. We extend the specification with the constructs of SyGuS, so they become a core part of the smtlib-lowlevel API.
  2. We reuse the existing infrastructure for generating code and apply it to the SyGuS specification, and build a new sygus-lowlevel crate and work from there.

I think I'm leaning more towards trying the second approach, since it allows us to explore the SyGuS API in a more focused manner, without having to worry about compatibility with smtlib. It might also be better so that we don't introduce non-smtlib API's into smtlib.

Let me know what you think of this!

And to be clear, I don't personally have much need for this ATM, so I wont be spending too much time looking into SyGuS, but if we can come up with a neat way of reusing as much of the infrastructure of smtlib-lowlevel I see no reason not to support this!

Sicheng-Pan commented 7 months ago

May I ask if the smt-lib toml is manually transcribed from this pdf specification? If so I believe that it is should be relatively straightforward to do the same on the SyGus specification. I could do the work, but if possible please elaborate a bit on how the toml format works, and I would really appreciate that!

The second approach seems better to me as well. But still, it seems that the syntax of smt-lib and sygus have a lot in common (literal, symbol, sort, term, etc.), so it may be desirable to reuse many of the content in the smt-lib toml.

oeb25 commented 7 months ago

May I ask if the smt-lib toml is manually transcribed from this pdf specification?

Yes! That's right. I remember I tried to do some automatic extraction using pdf2text or something, but I honestly forgot if I ended up using that or manually transcribing it.

So yes, I think that doing the same for the SyGus spec would be potentially quite easy. One thing to note about the TOML spec, is that it's very ad-hoc and so is the generator, which is to say that some changes might be necessary to both the existing spec and the generator when adding the SyGus spec, but I believe that it potentially would be beneficial for the project.

For that reason I can't quite tell you how the format works, since I don't remember 😅 But it should be quite possible to "re-engineer" it from looking at the implementation here a long with the spec here.

As you might see in the implementation there are some specification details, that perhaps should have been derived from the spec and not hardcoded into the generator. If the same infrastructure were to be used with SyGus, we would have to be sure that that is moved out, or, if we are lucky, they share the same hardcoded stuff 😉

If you want to have a look at some of the parts, perhaps writing up a draft of the SyGus spec in TOML, it would be interesting how far we could push the current generator!