get-value

[aep]

how would you go about implementing get-value? considered that solvers output it very differently

[AdrienChampion]

I'm not sure what you mean, get-value is already implemented as the get_values function.

Currently only z3 is supported so the fact that solver outputs differ is not a problem. In any case, when support for more solver is added the solver configuration should take care of that problem.

Does that answer your question or did I misunderstand something?

[aep]

i'm probably just confused by how the api works. it looked like you still need to implement a parser for each solver yourself, which would make this crate kind of pointless.

[AdrienChampion]

You should probably read the documentation.

You need to provide parsers for your expressions/values/types, since rsmt2 does not force you to use a particular structure for those. The point is that rsmt2 handles everything around expressions, which includes solver-specific syntax and SMT-LIB 2 keywords for assertion, model parsing and so on.

[aep]

yes, you repeated what the docs said, no idea what that means, but anyway

[AdrienChampion]

Your expression structure needs to implement the ...2Smt traits so that rsmt2 knows how to print them. This allows you to declare symbols and assert expressions. Then, if you want to retrieve values, you will also need to provide a way to parse expressions/values.

Both aspects are discussed in the documentation on a simple example that shows the whole process and explains it on a simple expression structure. If you do not find this example understandable, feel free to let me know what is not clear so that I can improve it.

Maybe you were expecting rsmt2 to provide an expression structures for you to build your formulas, and use that to interact with the solver? In that case rsmt2 is one level of abstraction too low for you I'm afraid, but we can talk about this; I could provide a crate above this one with a built-in expression structure.

[aep]

Your expression structure

right. nowhere in the documentation does it explain what that that actually is. It just assumes that's a thing you want and goes on about how to implement whatever it is.

But an smt solver doesn't have structures, it's just statements.

Maybe you were expecting rsmt2 to provide an expression structures for you to build your formulas,

no, i expected the opposite: just an interface to smt2.

[AdrienChampion]

rsmt2 is based on the SMT-LIB 2 standard, for more details see the standard itself.

Expressions are what you use to build formulae. If you want to interact with an SMT solver, you need to build formulas so that you can assert them (and symbols so that you can declare them). Either you use SMT2 text files, in which case the expressions are just strings, or you use (for instance) z3's API to build expressions using its own expression structure.

Maybe I can help you if you answer this question. Say you want to use rsmt2 to assert (and a (not a)) and then do a check-sat. What do you expect to have to write to do this?

[aep]

well the example in the main docs page is pretty straight forward for that

use rsmt2::Solver ;
let mut solver = Solver::default(()) ? ;

solver.declare_const("a", "Bool") ? ;
solver.assert("(and a (not a)))" ? ;

let is_sat = solver.check_sat() ? ;
assert! { ! is_sat }

it becomes really confusing once you want to use get-value, where i expected a similar plain api, but instead have to build whatever an expression structure is

[AdrienChampion]

I see, the documentation is a bit rough and assumes quite a lot of familiarity with the SMT-LIB 2 standard. In particular, there is no illustration on how to use get_values, which seems to be a significant part of the problem you have.

But thanks to your feedback, I added one such example. It is not merged yet (waiting for CI) but will be shortly. In the mean time, you can check it out here:

https://github.com/AdrienChampion/rsmt2/blob/cvc4/src/parse.rs#L24-L76

It continues the example you reference above where the expressions are represented as strings. I think you comments point out a lack of documentation in the parse traits, I will work on this shortly.

In any case, using strings to build expressions is not at all the typical use case here. It's perfectly fine, but in a big model-checker it is not an option for many reasons. Hence, the traits and functions in this crate are designed to (hopefully) handle complex use-cases, and might seem more complicated than needed for you. For instance, expression printing/parsing can take Info to print/parse the same expression differently depending on the context. This can be extremely useful in specific cases, but makes the API more daunting than it needs to be.

Now, it might be worth providing another API for "simpler" use cases, where traits and functions are less confusing. We can talk about it if that would be useful to you.

In any case, thank you again for your feedback!

[aep]

great, thanks.