rustproof-libsmt 0.1.0

Rust bindings for z3 as utilized by RustProof.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

use std::fmt;

use theories::{array_ex, bitvec, core};
use backends::backend::{Logic, SMTNode};

define_sorts_for_logic!(QF_AUFBV_Sorts,
                        BV -> bitvec::Sorts,
                        Core -> core::Sorts,
                        ArrayEx -> array_ex::Sorts<QF_AUFBV_Sorts, QF_AUFBV_Sorts>
                        );

define_fns_for_logic!(QF_AUFBV_Fn,
                      BVOps -> bitvec::OpCodes,
                      CoreOps -> core::OpCodes,
                      ArrayOps -> array_ex::OpCodes<QF_AUFBV_Sorts, QF_AUFBV_Sorts, QF_AUFBV_Fn>
                      );

define_logic!(QF_AUFBV,
              QF_AUFBV_Fn,
              QF_AUFBV_Sorts,
              map { QF_AUFBV_Sorts::BV(_) => bitvec::OpCodes::FreeVar,
                  QF_AUFBV_Sorts::ArrayEx(_) => array_ex::OpCodes::FreeVar
              }
              );