rustproof_libsmt/logics/
qf_abv.rs

1use std::fmt;
2
3use theories::{array_ex, bitvec, core};
4use backends::backend::{Logic, SMTNode};
5
6define_sorts_for_logic!(QF_ABV_Sorts,
7                        BV -> bitvec::Sorts,
8                        Core -> core::Sorts,
9                        ArrayEx -> array_ex::Sorts<QF_ABV_Sorts, QF_ABV_Sorts>
10                        );
11
12define_fns_for_logic!(QF_ABV_Fn,
13                      BVOps -> bitvec::OpCodes,
14                      CoreOps -> core::OpCodes,
15                      ArrayOps -> array_ex::OpCodes<QF_ABV_Sorts, QF_ABV_Sorts, QF_ABV_Fn>
16                      );
17
18define_logic!(QF_ABV,
19              QF_ABV_Fn,
20              QF_ABV_Sorts,
21              map { QF_ABV_Sorts::BV(_) => bitvec::OpCodes::FreeVar,
22              QF_ABV_Sorts::ArrayEx(_) => array_ex::OpCodes::FreeVar
23              }
24              );
25
26
27// Helper methods that help in contruction of array and bitvector types.
28pub fn array_sort<T: Into<QF_ABV_Sorts>, P: Into<QF_ABV_Sorts>>(idx: T, data: P) -> QF_ABV_Sorts {
29    QF_ABV_Sorts::ArrayEx(array_ex::Sorts::new(idx.into(), data.into()))
30}
31
32pub fn bv_sort(size: usize) -> QF_ABV_Sorts {
33    QF_ABV_Sorts::BV(bitvec::Sorts::BitVector(size))
34}
35
36pub fn bv_const(val: u64, size: usize) -> QF_ABV_Fn {
37    QF_ABV_Fn::BVOps(bitvec::OpCodes::Const(val, size))
38}
39
40pub fn array_const<T, P, Q>(idx_ty: T, val_ty: P, val: Q) -> QF_ABV_Fn
41    where T: Into<QF_ABV_Sorts>,
42          P: Into<QF_ABV_Sorts>,
43          Q: Into<QF_ABV_Fn>
44{
45    let arr_ty = array_ex::Sorts::Array(Box::new(idx_ty.into()), Box::new(val_ty.into()));
46    let arr_const = array_ex::OpCodes::Const(arr_ty, Box::new(val.into()));
47    QF_ABV_Fn::ArrayOps(arr_const)
48}
rustproof_libsmt/logics/qf_abv.rs

rustproof_libsmt/logics/
qf_abv.rs
