rustproof_libsmt/backends/
z3.rs

1//! Struct and methods to interact with the Z3 solver.
2
3
4//extern crate native;
5//extern crate rustrt;
6
7//use std::io::{process, Command};
8//use native::io::file;
9///use rustrt::rtio;
10
11// for file
12/*
13use std::error::Error;
14use std::io::prelude::*;
15use std::fs::File;
16use std::os::unix::io::IntoRawFd;
17use std::path::Path;
18*/
19//f2
20
21use backends::smtlib2::SMTProc;
22use std::process::{Child, Command, Stdio};
23
24
25#[derive(Default)]
26pub struct Z3 {
27    fd: Option<Child>,
28}
29
30impl SMTProc for Z3 {
31    fn init(&mut self) {
32        let (cmd, args) = ("z3", &["-in", "-smt2"]);
33        let child = Command::new(cmd)
34                        .args(args)
35                        .stdout(Stdio::piped())
36                        .stdin(Stdio::piped())
37                        .stderr(Stdio::piped())
38                        .spawn()
39                        .expect("Failed to spawn process");
40
41        self.fd = Some(child);
42    }
43
44    fn pipe<'a>(&'a mut self) -> &'a mut Child {
45        if self.fd.is_none() {
46            self.init();
47        }
48        self.fd.as_mut().unwrap()
49    }
50}
51
52#[cfg(test)]
53mod test {
54    use backends::backend::*;
55    use backends::smtlib2::*;
56    use super::*;
57    use theories::bitvec;
58    use theories::{core, integer};
59    use logics::{lia, qf_bv};
60
61    #[test]
62    fn test_z3_int() {
63        let mut z3: Z3 = Default::default();
64        let mut solver = SMTLib2::new(Some(lia::LIA));
65        let x = solver.new_var(Some("X"), integer::Sorts::Int);
66        let y = solver.new_var(Some("Y"), integer::Sorts::Int);
67        let c = solver.new_const(integer::OpCodes::Const(10));
68        solver.assert(core::OpCodes::Cmp, &[x, c]);
69        solver.assert(integer::OpCodes::Gt, &[x, y]);
70        let result = solver.solve(&mut z3).unwrap();
71        assert_eq!(result[&x], 10);
72        assert_eq!(result[&y], 9);
73    }
74
75    #[test]
76    fn test_z3_bitvec() {
77        let mut z3: Z3 = Default::default();
78        let mut solver = SMTLib2::new(Some(qf_bv::QF_BV));
79        let x = solver.new_var(Some("X"), bitvec::Sorts::BitVector(32));
80        let c = solver.new_const(bitvec::OpCodes::Const(10, 32));
81        let c8 = solver.new_const(bitvec::OpCodes::Const(8, 32));
82        let y = solver.new_var(Some("Y"), bitvec::Sorts::BitVector(32));
83        solver.assert(core::OpCodes::Cmp, &[x, c]);
84        let x_xor_y = solver.assert(bitvec::OpCodes::BvXor, &[x, y]);
85        solver.assert(core::OpCodes::Cmp, &[x_xor_y, c8]);
86        let result = solver.solve(&mut z3).unwrap();
87        assert_eq!(result[&x], 10);
88        assert_eq!(result[&y], 2);
89    }
90
91    #[test]
92    fn test_z3_extract() {
93        let mut z3: Z3 = Default::default();
94        let mut solver = SMTLib2::new(Some(qf_bv::QF_BV));
95        let x = solver.new_var(Some("X"), bitvec::Sorts::BitVector(32));
96        let c4 = solver.new_const(bitvec::OpCodes::Const(0b100, 4));
97        let x_31_28 = solver.assert(bitvec::OpCodes::Extract(31, 28), &[x]);
98        solver.assert(core::OpCodes::Cmp, &[x_31_28, c4]);
99        let result = solver.solve(&mut z3).unwrap();
100        assert_eq!(result[&x], (0b100 << 28));
101    }
102}
rustproof_libsmt/backends/z3.rs

rustproof_libsmt/backends/
z3.rs
