smtlib-lowlevel 0.1.5

A low-level API for interacting with SMT solvers
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

use std::ffi::OsStr;

use super::{Backend, BinaryBackend};

pub struct Cvc5Binary {
    bin: BinaryBackend,
}

impl Cvc5Binary {
    pub fn new(cvc5: impl AsRef<OsStr>) -> Result<Self, std::io::Error> {
        Ok(Cvc5Binary {
            bin: BinaryBackend::new(cvc5, |cmd| {
                cmd.args(["--lang", "smt2"])
                    .args(["--produce-models"])
                    .args(["--incremental"]);
            })?,
        })
    }
}

impl Backend for Cvc5Binary {
    fn exec(&mut self, cmd: &crate::Command) -> Result<String, crate::Error> {
        self.bin.exec(cmd).map(Into::into)
    }
}