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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109

//! Backends are concrete solvers which can be communicated with using the
//! SMT-LIB language.
//!
//! This module contains the solver which are supported out-of-the-box by
//! `smtlib`. Each backend is feature gated, which means that a feature must be
//! enabled to use the backend.
//!
//! ## Backends
//!
//! - **[`Z3Binary`]**: A [Z3](https://github.com/Z3Prover/z3) backend using the binary CLI interface.
//!     - **Enabled by feature:** `z3`
//! - **[`Z3Static`]**: A [Z3](https://github.com/Z3Prover/z3) backend using the [`z3-sys` crate](https://github.com/prove-rs/z3.rs).
//!     - **Enabled by feature:** `z3-static`
//! - **[`Cvc5Binary`]**: A [cvc5](https://cvc5.github.io/) backend using the binary CLI interface.
//!     - **Enabled by feature:** `cvc5`

use std::{
    io::{BufRead, BufReader, Write},
    process::{Child, ChildStdin, ChildStdout},
};

#[cfg(feature = "cvc5")]
mod cvc5;
#[cfg(feature = "cvc5")]
pub use cvc5::*;

#[cfg(feature = "z3")]
mod z3_binary;
use logos::Lexer;
#[cfg(feature = "z3")]
pub use z3_binary::*;

#[cfg(feature = "z3-static")]
mod z3_static;
#[cfg(feature = "z3-static")]
pub use z3_static::*;

use crate::parse::Token;

/// The [`Backend`] trait is used to interact with SMT solver using the SMT-LIB language.
///
/// For more details read the [`backend`](crate::backend) module documentation.
pub trait Backend {
    fn exec(&mut self, cmd: &crate::Command) -> Result<String, crate::Error>;
}

#[cfg(feature = "async")]
/// The [`AsyncBackend`] trait is used to interact with SMT solver using the SMT-LIB language.
///
/// For more details read the [`backend`](crate::backend) module documentation.
#[async_trait::async_trait(?Send)]
pub trait AsyncBackend {
    async fn exec(&mut self, cmd: &crate::Command) -> Result<String, crate::Error>;
}

struct BinaryBackend {
    #[allow(unused)]
    child: Child,
    stdin: ChildStdin,
    stdout: BufReader<ChildStdout>,
    buf: String,
}

impl BinaryBackend {
    pub(crate) fn new(
        program: impl AsRef<std::ffi::OsStr>,
        init: impl FnOnce(&mut std::process::Command),
    ) -> Result<Self, std::io::Error> {
        use std::process::{Command, Stdio};

        let mut cmd = Command::new(program);
        init(&mut cmd);
        let mut child = cmd.stdin(Stdio::piped()).stdout(Stdio::piped()).spawn()?;
        let stdin = child.stdin.take().unwrap();
        let stdout = BufReader::new(child.stdout.take().unwrap());

        Ok(BinaryBackend {
            child,
            stdin,
            stdout,
            buf: String::new(),
        })
    }
    pub(crate) fn exec(&mut self, cmd: &crate::Command) -> Result<&str, crate::Error> {
        // println!("> {cmd}");
        writeln!(self.stdin, "{cmd}")?;
        self.stdin.flush()?;

        self.buf.clear();
        loop {
            let n = self.stdout.read_line(&mut self.buf)?;
            if n == 0 {
                continue;
            }
            if Lexer::new(self.buf.as_str())
                .map(|tok| tok.unwrap_or(Token::Error))
                .fold(0i32, |acc, tok| match tok {
                    Token::LParen => acc + 1,
                    Token::RParen => acc - 1,
                    _ => acc,
                })
                != 0
            {
                continue;
            }
            return Ok(&self.buf);
        }
    }
}