Struct Z3

pub struct Z3 { /* private fields */ }

Trait Implementations

impl Default for Z3

fn default() -> Z3

Returns the “default value” for a type.

impl SMTProc for Z3

fn init(&mut self)

Function to initialize the solver. This includes spawning a process and keeping the process pipe open for read and write. The function takes &mut self as an argument to allow configuration during initialization.

fn pipe<'a>(&'a mut self) -> &'a mut Child

Return a mutable reference to the process pipe.

fn write<T: AsRef<str>>(&mut self, s: T) -> Result<(), String>

fn read(&mut self) -> String

fn read_checksat_output(&mut self) -> String

fn read_getmodel_output(&mut self) -> String