Struct Z3Subprocess 

pub(crate) struct Z3Subprocess {
    child: Child,
    stdin: Option<ChildStdin>,
    stdout: BufReader<ChildStdout>,
    stderr: Arc<Mutex<Vec<u8>>>,
    stderr_reader: Option<JoinHandle<()>>,
    request_id: usize,
}

Fields

child: Child

stdin: Option<ChildStdin>

stdout: BufReader<ChildStdout>

stderr: Arc<Mutex<Vec<u8>>>

stderr_reader: Option<JoinHandle<()>>

request_id: usize

Implementations

impl Z3Subprocess

pub(crate) fn new() -> Result<Self>

fn request(&mut self, commands: &str) -> Result<Response>

fn execute(&mut self, commands: &str) -> Result<()>

pub(crate) fn check_sat(&mut self, setup: &str) -> Result<SatStatus, Z3Error>

Check satisfiability (setup is a string that is sent to Z3 to be done before the check)

pub(crate) fn apply( &mut self, setup: &str, tactic: &str, ) -> Result<Vec<Vec<Sexp>>, Z3Error>

Apply a tactic (as a string) under a context (setup), returning the parsed formulas in each resulting goal.

pub(crate) fn scoped<R, E>( &mut self, setup: &str, f: impl FnOnce(&mut Self) -> Result<R, E>, ) -> Result<R, E>

where E: From<Z3Error> + From<Error>,

pub(crate) fn reset(&mut self, declarations: &str) -> Result<()>

fn take_stderr(&self) -> String

Trait Implementations

impl Drop for Z3Subprocess

fn drop(&mut self)

Executes the destructor for this type.

fn pin_drop(self: Pin<&mut Self>)

🔬This is a nightly-only experimental API. (pin_ergonomics)

Execute the destructor for this type, but different to Drop::drop, it requires self to be pinned.