why3/
ce_models.rs

1#[cfg(feature = "serde")]
2use serde::Deserialize;
3use serde_json::Value as Json;
4use std::fmt::{Debug, Formatter};
5
6#[cfg_attr(feature = "serde", derive(Deserialize))]
7#[cfg_attr(feature = "serde", serde(untagged))]
8pub enum Loc {
9    Span(Why3Span),
10    Other(Json),
11}
12
13#[allow(dead_code)]
14#[cfg_attr(feature = "serde", derive(Deserialize, Debug))]
15#[cfg_attr(feature = "serde", serde(rename_all = "kebab-case"))]
16pub struct Why3Span {
17    pub file_name: String,
18    pub start_line: u32,
19    pub start_char: u32,
20    pub end_line: u32,
21    pub end_char: u32,
22}
23
24impl Debug for Loc {
25    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
26        match self {
27            Loc::Span(Why3Span { file_name, start_line, start_char, end_line, end_char }) => {
28                write!(f, "[#\"{file_name}\" {start_line} {start_char} {end_line} {end_char}]")
29            }
30            _ => write!(f, "[#???]"),
31        }
32    }
33}
34
35#[derive(Debug)]
36#[cfg_attr(feature = "serde", derive(Deserialize))]
37#[cfg_attr(feature = "serde", serde(untagged))]
38pub enum Fallible<T> {
39    Ok(T),
40    Err(Json),
41}
42
43#[derive(Debug)]
44#[cfg_attr(feature = "serde", derive(Deserialize))]
45#[cfg_attr(feature = "serde", serde(untagged))]
46pub enum Model {
47    Model { answer: String, model: Vec<Fallible<Model2>> },
48    Unknown(Json),
49}
50
51#[derive(Debug)]
52#[cfg_attr(feature = "serde", derive(Deserialize))]
53pub struct Model2 {
54    pub filename: String,
55    pub model: Vec<Fallible<Model3>>,
56}
57
58#[derive(Debug)]
59#[cfg_attr(feature = "serde", derive(Deserialize))]
60pub struct Model3 {
61    pub is_vc_line: bool,
62    pub line: String,
63    pub model_elements: Vec<Fallible<ModelElem>>,
64}
65
66#[derive(Debug)]
67#[cfg_attr(feature = "serde", derive(Deserialize))]
68pub struct LSymbol {
69    pub name: String,
70    pub attrs: Vec<String>,
71    pub loc: Loc,
72}
73
74#[derive(Debug)]
75#[cfg_attr(feature = "serde", derive(Deserialize))]
76pub struct ModelElem {
77    pub attrs: Vec<String>,
78    pub kind: String,
79    pub location: Loc,
80    pub lsymbol: LSymbol,
81    pub value: Value,
82}
83
84#[derive(Debug)]
85#[cfg_attr(feature = "serde", derive(Deserialize))]
86pub struct Value {
87    pub value_concrete_term: ConcreteTerm,
88    pub value_term: Term,
89    pub value_type: Type,
90}
91
92#[cfg_attr(feature = "serde", derive(Deserialize))]
93pub enum Type {
94    #[cfg_attr(feature = "serde", serde(rename = "Tyvar"))]
95    Var(String),
96    #[cfg_attr(feature = "serde", serde(rename = "Tyapp"))]
97    App { ty_symbol: String, ty_args: Vec<Type> },
98    #[cfg_attr(feature = "serde", serde(untagged))]
99    Unknown(Json),
100}
101
102impl Debug for Type {
103    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
104        match self {
105            Type::Var(v) => write!(f, "*{v}"),
106            Type::App { ty_symbol, ty_args } => {
107                write!(f, "{ty_symbol}")?;
108                if !ty_args.is_empty() {
109                    f.debug_list().entries(ty_args).finish()?;
110                }
111                Ok(())
112            }
113            Type::Unknown(json) => write!(f, "{json}"),
114        }
115    }
116}
117
118#[derive(Debug)]
119#[cfg_attr(feature = "serde", derive(Deserialize))]
120pub struct VSymbol {
121    pub vs_name: String,
122    pub vs_type: Type,
123}
124
125#[derive(Debug)]
126#[cfg_attr(feature = "serde", derive(Deserialize))]
127pub enum TBool {
128    #[cfg_attr(feature = "serde", serde(rename = "Ttrue"))]
129    True,
130    #[cfg_attr(feature = "serde", serde(rename = "Tfalse"))]
131    False,
132}
133
134#[derive(Debug)]
135#[cfg_attr(feature = "serde", derive(Deserialize))]
136pub enum Term {
137    #[cfg_attr(feature = "serde", serde(rename = "Tvar"))]
138    Var(VSymbol),
139    #[cfg_attr(feature = "serde", serde(rename = "Tconst"))]
140    Const {
141        #[cfg_attr(feature = "serde", serde(rename = "const_type"))]
142        ty: String,
143        #[cfg_attr(feature = "serde", serde(rename = "const_value"))]
144        val: String,
145    },
146    #[cfg_attr(feature = "serde", serde(rename = "Tapp"))]
147    App {
148        #[cfg_attr(feature = "serde", serde(rename = "app_ls"))]
149        ls: String,
150        #[cfg_attr(feature = "serde", serde(rename = "app_args"))]
151        args: Vec<Term>,
152    },
153    #[cfg_attr(feature = "serde", serde(rename = "Tif"))]
154    If {
155        #[cfg_attr(feature = "serde", serde(rename = "if"))]
156        ift: Box<Term>,
157        then: Box<Term>,
158        #[cfg_attr(feature = "serde", serde(rename = "else"))]
159        elset: Box<Term>,
160    },
161    #[cfg_attr(feature = "serde", serde(rename = "Teps"))]
162    Eps {
163        #[cfg_attr(feature = "serde", serde(rename = "eps_vs"))]
164        vs: VSymbol,
165        #[cfg_attr(feature = "serde", serde(rename = "eps_t"))]
166        t: Box<Term>,
167    },
168    #[cfg_attr(feature = "serde", serde(rename = "Tfun"))]
169    Fun {
170        #[cfg_attr(feature = "serde", serde(rename = "fun_args"))]
171        args: Vec<VSymbol>,
172        #[cfg_attr(feature = "serde", serde(rename = "fun_body"))]
173        body: Box<Term>,
174    },
175    #[cfg_attr(feature = "serde", serde(rename = "Tquant"))]
176    Quant {
177        quant: String,
178        #[cfg_attr(feature = "serde", serde(rename = "quant_vs"))]
179        vs: Vec<VSymbol>,
180        #[cfg_attr(feature = "serde", serde(rename = "quant_t"))]
181        t: Box<Term>,
182    },
183    #[cfg_attr(feature = "serde", serde(rename = "Tbinop"))]
184    Binop {
185        binop: String,
186        #[cfg_attr(feature = "serde", serde(rename = "binop_t1"))]
187        t1: Box<Term>,
188        #[cfg_attr(feature = "serde", serde(rename = "binop_t2"))]
189        t2: Box<Term>,
190    },
191    #[cfg_attr(feature = "serde", serde(rename = "Tnot"))]
192    Not(Box<Term>),
193    #[cfg_attr(feature = "serde", serde(rename = "Tlet"))]
194    Let(String),
195    #[cfg_attr(feature = "serde", serde(rename = "Tcase"))]
196    Case(String),
197    #[cfg_attr(feature = "serde", serde(untagged))]
198    Bool(TBool),
199    #[cfg_attr(feature = "serde", serde(untagged))]
200    Unknown(Json),
201}
202
203#[derive(Debug)]
204#[cfg_attr(feature = "serde", derive(Deserialize))]
205pub struct BitVector {
206    pub bv_value_as_decimal: String,
207    pub bv_length: u32,
208    pub bv_verbatim: String,
209}
210
211#[derive(Debug)]
212#[cfg_attr(feature = "serde", derive(Deserialize))]
213pub struct Real {
214    pub real_value: String,
215    pub real_verbatim: String,
216}
217
218#[cfg_attr(feature = "serde", derive(Deserialize))]
219pub struct Integer {
220    pub int_value: String,
221    pub int_verbatim: String,
222}
223
224impl Integer {
225    fn try_to_u64(&self) -> Option<u64> {
226        if self.int_value != self.int_verbatim { None } else { self.int_value.parse().ok() }
227    }
228}
229
230impl Debug for Integer {
231    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
232        match self.try_to_u64() {
233            Some(n) => write!(f, "{n}"),
234            None => f
235                .debug_struct("Integer")
236                .field("value", &self.int_value)
237                .field("verbatim", &self.int_verbatim)
238                .finish(),
239        }
240    }
241}
242
243#[derive(Debug)]
244#[cfg_attr(feature = "serde", derive(Deserialize))]
245pub enum Float {
246    Infinity,
247    #[cfg_attr(feature = "serde", serde(rename = "Plus_zero"))]
248    PlusZero,
249    #[cfg_attr(feature = "serde", serde(rename = "Minus_zero"))]
250    MinusZero,
251    #[cfg_attr(feature = "serde", serde(rename = "Float_value"))]
252    Value {
253        float_hex: String,
254    },
255}
256
257#[allow(dead_code)]
258#[derive(Debug)]
259#[cfg_attr(feature = "serde", derive(Deserialize))]
260pub struct FunLitElt {
261    pub indice: ConcreteTerm,
262    pub value: ConcreteTerm,
263}
264
265#[derive(Debug)]
266#[cfg_attr(feature = "serde", derive(Deserialize))]
267#[cfg_attr(feature = "serde", serde(tag = "type", content = "val"))]
268pub enum ConcreteTerm {
269    Var(String),
270    Boolean(bool),
271    String(String),
272    Integer(Integer),
273    Real(Real),
274    BitVector(BitVector),
275    Fraction {
276        #[cfg_attr(feature = "serde", serde(rename = "frac_num"))]
277        num: Real,
278        #[cfg_attr(feature = "serde", serde(rename = "frac_denom"))]
279        denom: Real,
280        #[cfg_attr(feature = "serde", serde(rename = "frac_verbatim"))]
281        verbatim: String,
282    },
283    Float(Float),
284    #[cfg_attr(feature = "serde", serde(rename = "Apply"))]
285    App {
286        #[cfg_attr(feature = "serde", serde(rename = "app_ls"))]
287        ls: String,
288        #[cfg_attr(feature = "serde", serde(rename = "app_args"))]
289        args: Vec<ConcreteTerm>,
290    },
291    If {
292        #[cfg_attr(feature = "serde", serde(rename = "if"))]
293        ift: Box<ConcreteTerm>,
294        then: Box<ConcreteTerm>,
295        #[cfg_attr(feature = "serde", serde(rename = "else"))]
296        elset: Box<ConcreteTerm>,
297    },
298    #[cfg_attr(feature = "serde", serde(rename = "Epsilon"))]
299    Eps {
300        #[cfg_attr(feature = "serde", serde(rename = "eps_var"))]
301        var: String,
302        #[cfg_attr(feature = "serde", serde(rename = "eps_t"))]
303        t: Box<ConcreteTerm>,
304    },
305    #[cfg_attr(feature = "serde", serde(rename = "Function"))]
306    Fun {
307        #[cfg_attr(feature = "serde", serde(rename = "fun_args"))]
308        args: Vec<String>,
309        #[cfg_attr(feature = "serde", serde(rename = "fun_body"))]
310        body: Box<ConcreteTerm>,
311    },
312    Quant {
313        quant: String,
314        #[cfg_attr(feature = "serde", serde(rename = "quant_vs"))]
315        vs: Vec<String>,
316        #[cfg_attr(feature = "serde", serde(rename = "quant_t"))]
317        t: Box<ConcreteTerm>,
318    },
319    Binop {
320        binop: String,
321        #[cfg_attr(feature = "serde", serde(rename = "binop_t1"))]
322        t1: Box<ConcreteTerm>,
323        #[cfg_attr(feature = "serde", serde(rename = "binop_t2"))]
324        t2: Box<ConcreteTerm>,
325    },
326    Not(Box<ConcreteTerm>),
327    FunctionLiteral {
328        #[cfg_attr(feature = "serde", serde(rename = "funliteral_elts"))]
329        elts: Vec<FunLitElt>,
330        #[cfg_attr(feature = "serde", serde(rename = "funliteral_others"))]
331        other: Box<ConcreteTerm>,
332    },
333    Proj {
334        #[cfg_attr(feature = "serde", serde(rename = "proj_name"))]
335        name: String,
336        #[cfg_attr(feature = "serde", serde(rename = "proj_value"))]
337        value: Box<ConcreteTerm>,
338    },
339    #[cfg_attr(feature = "serde", serde(untagged))]
340    Unknown(Json),
341}
342
343#[cfg_attr(feature = "serde", derive(Deserialize, Debug))]
344pub struct Goal {
345    pub term: GoalTerm,
346    #[cfg_attr(feature = "serde", serde(alias = "prover-result"))]
347    pub prover_result: ProverResult,
348}
349
350#[derive(Debug)]
351#[cfg_attr(feature = "serde", derive(Deserialize))]
352pub struct GoalTerm {
353    pub loc: Loc,
354    #[cfg_attr(feature = "serde", serde(alias = "goal-name"))]
355    //Why3 doesn't currently use kebab-case but this might change
356    pub goal_name: String,
357    pub explanations: Vec<String>,
358}
359#[allow(dead_code)]
360#[derive(Debug)]
361#[cfg_attr(feature = "serde", derive(Deserialize))]
362pub struct ProverResult {
363    pub answer: String,
364    #[cfg_attr(feature = "serde", serde(rename = "ce-models"))]
365    pub ce_models: Vec<Model>,
366    pub time: f32,
367    pub step: i32,
368}
369
370impl ProverResult {
371    pub fn model_elems(&self) -> impl Iterator<Item = &ModelElem> {
372        self.ce_models
373            .iter()
374            .flat_map(|x| match x {
375                Model::Model { model, .. } => &**model,
376                _ => &[],
377            })
378            .flat_map(|x| match x {
379                Fallible::Ok(x) => &*x.model,
380                _ => &[],
381            })
382            .flat_map(|x| match x {
383                Fallible::Ok(x) => &*x.model_elements,
384                _ => &[],
385            })
386            .filter_map(|x| match x {
387                Fallible::Ok(x) => Some(x),
388                _ => None,
389            })
390    }
391}
why3/ce_models.rs

why3/
ce_models.rs
