smtlib-lowlevel 0.1.4

A low-level API for interacting with SMT solvers
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
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150

use crate::parse::{ParseError, Parser, Token};

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct Numeral(pub String);
impl std::fmt::Display for Numeral {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}
impl SmtlibParse for Numeral {
    fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
        tokens.nth(offset) == Token::Numeral
    }
    fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
        Ok(Self(tokens.expect(Token::Numeral)?.into()))
    }
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct Decimal(pub String);
impl std::fmt::Display for Decimal {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}
impl SmtlibParse for Decimal {
    fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
        tokens.nth(offset) == Token::Decimal
    }
    fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
        Ok(Self(tokens.expect(Token::Decimal)?.into()))
    }
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct Symbol(pub String);
impl std::fmt::Display for Symbol {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}
impl SmtlibParse for Symbol {
    fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
        tokens.nth(offset) == Token::Symbol
    }
    fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
        Ok(Self(tokens.expect(Token::Symbol)?.into()))
    }
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct Hexadecimal(pub String);
impl std::fmt::Display for Hexadecimal {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}
impl SmtlibParse for Hexadecimal {
    fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
        tokens.nth(offset) == Token::Hexadecimal
    }
    fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
        Ok(Self(tokens.expect(Token::Hexadecimal)?.into()))
    }
}
impl Hexadecimal {
    pub fn parse(&self) -> Result<i64, std::num::ParseIntError> {
        i64::from_str_radix(&self.0[2..], 16)
    }
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct Binary(pub String);
impl std::fmt::Display for Binary {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}
impl SmtlibParse for Binary {
    fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
        tokens.nth(offset) == Token::Binary
    }
    fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
        Ok(Self(tokens.expect(Token::Binary)?.into()))
    }
}
impl Binary {
    pub fn parse(&self) -> Result<i64, std::num::ParseIntError> {
        i64::from_str_radix(&self.0[2..], 2)
    }
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct Reserved(pub String);
impl std::fmt::Display for Reserved {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}
impl SmtlibParse for Reserved {
    fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
        tokens.nth(offset) == Token::Reserved
    }
    fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
        Ok(Self(tokens.expect(Token::Reserved)?.into()))
    }
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct Keyword(pub String);
impl std::fmt::Display for Keyword {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{}", self.0)
    }
}
impl SmtlibParse for Keyword {
    fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
        tokens.nth(offset) == Token::Keyword
    }
    fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
        Ok(Self(tokens.expect(Token::Keyword)?.into()))
    }
}

pub type BValue = bool;

pub(crate) trait SmtlibParse: Sized {
    fn is_start_of(offset: usize, tokens: &mut Parser) -> bool;
    fn parse(tokens: &mut Parser) -> Result<Self, ParseError>;
}

impl SmtlibParse for String {
    fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
        tokens.nth(offset) == Token::String
    }

    fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
        Ok(tokens.expect(Token::String)?.into())
    }
}
impl SmtlibParse for bool {
    fn is_start_of(_offset: usize, _tokens: &mut Parser) -> bool {
        todo!()
    }

    fn parse(_tokens: &mut Parser) -> Result<Self, ParseError> {
        todo!()
    }
}