Skip to content

Instantly share code, notes, and snippets.

@kyleheadley kyleheadley/usez3.rs
Created Nov 11, 2017

Embed
What would you like to do?
Use pipes to communicate with z3 in rust
#![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); }
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.