Any example of how to use this to communicate with an existing solver? (Z3, CVC4?)

[Lukas-Dresel]

Hey, first of all thanks for making this :)

I'm trying to use an existing SMTLIB solver (z3 + extra functionality) to check constraints created in Rust and I took a look at this. However, I've only started using Rust about a week ago and so I'm still a little lost on how best to understand APIs from the source and things like that and was wondering if you could provide a minimal example for how to instantiate a Client with an existing solver and give it a simple constraint to solve.

I guess, more concretely, I'm a little overwhelmed by the large number of generic traits and which of them I have to implement my own types for that implement the necessary traits vs. which are already contained. E.g. The Logic trait seems like there should be an enum contained for most of the known Logics (e.g. QF_AUFBV) or such, but I can't seem to find it. Similarly, for the bool_sort and cst_true and cst_false parameters I have to pass to Client, do I have to implement known sorts (bool, BV, Array, etc.) myself or am I missing an existing implementation somewhere?

Thanks for any help in advance :)

• Lukas

[Lukas-Dresel]

Similarly, I tried my hand at bootstrapping this myself, however got a little confused by the meaning of some of the types, e.g. I attempted to implement my own Bool sort like this, however here the generic <F> of the Sort is not quite clear to me, similarly what the value of the sort entry should be. Intuitively I'd expect to pass either a Sort name (like "Bool") or something alike, which is why the generic isn't quite obvious to me.

    let bool_sort = smt2::GroundSort{
        sort: true,
        parameters: Vec::new()
    };

[Lukas-Dresel]

I did find your rchc project and am going through that to get a better understanding, just asking in case you have any quick tips :)

[timothee-haudebourg]

Hey, I'll admit this library lacks documentation. I've been working on it a while back to build the rchc solver you found. Beware that, as mentioned in the README, only a portion of the SMT2-LIB language is currently supported. However if you find it useful, I can take some time to add whatever language feature you need. To be completely honest, I was still discovering Rust myself at the time, and would have done things differently today. But still, I can try to help you with what is there today.

As you have guessed from the numerous type parameters, this is a rather abstract implementation. For instance, there is no enum listing all the different logics, it is instead expected that you provide your own type enumerating all the logics handled by your implementation. Similarly, you can provide your own internal representation of constants (e.g. true, false, etc) sorts (e.g. bool, etc) and functions (e.g. and, or, etc) using the corresponding type parameters (C, S and F respectively). Here is an example of one possible way to define such types:

pub enum Constant {
  True,
  False
}

pub enum Sort {
  Bool,
  List
}

impl smt2::client::Sort for Sort {
  fn arity(&self) -> usize {
    match self {
      Self::Bool => 0,
      Self::List => 1
    }
  }
}

do I have to implement known sorts

Unfortunately yes. As far as I remember, no "basic" sorts are defined in the SMT2-LIB specification (apart from booleans maybe?). And even if there was, you would still need to provide your own definition since the sort type S is a parameter. That is why the client constructors expects you to provide the boolean sort type along with the two constants true and false.

what the value of the sort entry should be

You probably don't want to deal with GroundSort directly. This type is used to represent "instantiated" sorts whose parameters are known. This is the difference between List (a sort, of arity 1) and (List Bool) (a ground sort). Here is another example:

let bool_sort = Sort::Bool;

let ground_bool_sort = smt2::GroundSort{
        sort: Sort::Bool,
        parameters: Vec::new() // the `Bool` sort is of arity 0, there are no parameters.
};

let list_sort = Sort::List;

let ground_bool_list_sort = smt2::GroundSort{
        sort: Sort::List,
        parameters: vec![ground_bool_sort]
};

I hope this is somewhat helpful. I'll try to find some time to improve the API and documentation if you still want to use this library.