Use pipes to communicate with z3 in rust

usez3.rs

#![allow(unused)]
use std::error::Error;
use std::io::prelude::*;
use std::process::{Command, Stdio};
use std::str;

fn main() {
    let process = match Command::new("z3")
    // use any z3 language with another .arg() here
    .arg("-in")
    .stdin(Stdio::piped())
    .stdout(Stdio::piped())
    .spawn() {
        Err(why) => panic!("couldn't spawn z3: {}", why.description()),
        Ok(process) => process,
    };

    let mut z3in = process.stdin.unwrap();
    let mut z3out = process.stdout.unwrap();
    let mut read_result;

    write!(z3in,"
        (declare-const a Bool)
        (declare-const b Bool)
        (declare-const c Bool)
        (assert (or a b c))
        (assert (not a))
        (assert (not b))
        (push)
        (assert (not c))
        (check-sat)
    ");
    let mut buff  = [0;100];
    read_result = z3out.read(&mut buff);
    assert_eq!(&buff[0..5], b"unsat");
    println!("{}", str::from_utf8(&buff[0..5]).unwrap());
    // This hangs if available data is a multiple of buffer length
    // Instead, spawn a new process that reads from z3out and writes to a channel
    while let Ok(s) = read_result { if s < buff.len() { break }; read_result = z3out.read(&mut buff); }
    z3in.write(b"
        (pop)
        (check-sat)
    ");
    let mut buff  = [0;100];
    read_result = z3out.read(&mut buff);
    assert_eq!(&buff[0..3], b"sat");
    println!("{}", str::from_utf8(&buff[0..3]).unwrap());
    while let Ok(s) = read_result { if s < buff.len() { break }; read_result = z3out.read(&mut buff); }

}