Struct uvls::smt::SmtSolver

pub struct SmtSolver {
    _proc: Child,
    stdin: BufWriter<ChildStdin>,
    stdout: Lines<BufReader<ChildStdout>>,
    cancel: CancellationToken,
}

Z3 process interface(over stdio)

A wrapper providing functions to interact with Z3.

Fields

_proc: Child

stdin: BufWriter<ChildStdin>

stdout: Lines<BufReader<ChildStdout>>

cancel: CancellationToken

Implementations

impl SmtSolver

pub async fn new( model: String, cancel: &CancellationToken, ) -> Result<Self, Box<dyn Error + Send + Sync>>

pub async fn read_block( &mut self, ) -> Result<String, Box<dyn Error + Send + Sync>>

returns the output of Z3

pub async fn check_sat(&mut self) -> Result<bool, Box<dyn Error + Send + Sync>>

checks if the current configuration loaded to Z3 is still SAT Solvable

pub async fn unsat_core( &mut self, ) -> Result<String, Box<dyn Error + Send + Sync>>

pub async fn push( &mut self, cmd: String, ) -> Result<(), Box<dyn Error + Send + Sync>>

Pushes new content to the Z3 Solver

pub async fn model(&mut self) -> Result<String, Box<dyn Error + Send + Sync>>

If SAT (must be checked beforehand) this function returns a valid model

pub async fn values( &mut self, active: String, ) -> Result<String, Box<dyn Error + Send + Sync>>

If SAT (must be checked beforehand) this function returns the values for the requested variables