Trait SMTProc

Source

pub trait SMTProc {
    // Required methods
    fn init(&mut self);
    fn pipe<'a>(&'a mut self) -> &'a mut Child;

    // Provided methods
    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 { ... }
}

Expand description

Trait that needs to be implemented in order to support a new solver. SMTProc is short for “SMT Process”.

To support a new solver that accepts input in the standard SMTLIB2 format, it is sufficient to implement this trait for the struct. This trait describes method needed to spawn, and communicate (read / write) with the solver.

read and write methods are implemented by deafult and needs to be changed only if the mode of communication is different (other than process pipes), or if some custom functionality is required for the specific solver.

Required Methods§

Source

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.

Source