rustproof_libsmt/logics/
lia.rs

1//! Module that describes LIA logic.
2//!
3//! Note that the functions and structs that are defined.
4
5use std::fmt;
6
7use theories::{integer, core};
8use backends::backend::{Logic, SMTNode};
9
10define_sorts_for_logic!(LIA_Sorts,
11                  Int -> integer::Sorts,
12                  Core -> core::Sorts
13                 );
14
15define_fns_for_logic!(LIA_Fn,
16                      IntOps -> integer::OpCodes,
17                      CoreOps -> core::OpCodes
18                     );
19
20#[derive(Clone, Copy, Debug)]
21pub struct LIA;
22
23impl fmt::Display for LIA {
24    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
25        write!(f, "{}", "LIA")
26    }
27}
28
29impl Logic for LIA {
30    type Fns = LIA_Fn;
31    type Sorts = LIA_Sorts;
32
33    fn free_var<T: AsRef<str>>(name: T, ty: LIA_Sorts) -> Self::Fns {
34        let fv = match ty {
35            LIA_Sorts::Int(_) => integer::OpCodes::FreeVar(name.as_ref().to_owned()),
36            LIA_Sorts::Core(_) => unreachable!(),
37        };
38        LIA_Fn::IntOps(fv)
39    }
40}
rustproof_libsmt/logics/lia.rs

rustproof_libsmt/logics/
lia.rs
