rustproof_libsmt/logics/
qf_bv.rs

1//! Module that describes QF_BV (closed quatifier-free formulas built over
2//! FixedSizeBitVector) logic.
3//!
4//! Note that the functions and structs that are defined.
5
6use std::fmt;
7
8use theories::{bitvec, core};
9use backends::backend::{Logic, SMTNode};
10
11define_sorts_for_logic!(QF_BV_Sorts,
12                  BV -> bitvec::Sorts,
13                  Core -> core::Sorts
14                 );
15
16define_fns_for_logic!(QF_BV_Fn,
17                      BVOps -> bitvec::OpCodes,
18                      CoreOps -> core::OpCodes
19                     );
20
21define_logic!(QF_BV,
22              QF_BV_Fn,
23              QF_BV_Sorts,
24              map {
25                  QF_BV_Sorts::BV(_) => bitvec::OpCodes::FreeVar
26              }
27             );