rustproof_libsmt/logics/
qf_aufbv.rs

1use std::fmt;
2
3use theories::{array_ex, bitvec, core};
4use backends::backend::{Logic, SMTNode};
5
6define_sorts_for_logic!(QF_AUFBV_Sorts,
7                        BV -> bitvec::Sorts,
8                        Core -> core::Sorts,
9                        ArrayEx -> array_ex::Sorts<QF_AUFBV_Sorts, QF_AUFBV_Sorts>
10                        );
11
12define_fns_for_logic!(QF_AUFBV_Fn,
13                      BVOps -> bitvec::OpCodes,
14                      CoreOps -> core::OpCodes,
15                      ArrayOps -> array_ex::OpCodes<QF_AUFBV_Sorts, QF_AUFBV_Sorts, QF_AUFBV_Fn>
16                      );
17
18define_logic!(QF_AUFBV,
19              QF_AUFBV_Fn,
20              QF_AUFBV_Sorts,
21              map { QF_AUFBV_Sorts::BV(_) => bitvec::OpCodes::FreeVar,
22                  QF_AUFBV_Sorts::ArrayEx(_) => array_ex::OpCodes::FreeVar
23              }
24              );