rsmt2_zz/example/
print_time.rs

1//! A more involved example.
2//!
3//! This example showcases print-time user-specified information but lacks a proper discussion,
4//! because no one has asked for it yet.
5
6// Parser library.
7use std::io::Write;
8
9use crate::{common::*, parse::*};
10
11#[cfg(test)]
12use crate::example::get_solver;
13
14use self::Var::*;
15
16/// A type.
17#[derive(Debug, Clone, Copy, PartialEq)]
18enum Type {
19    /// Integers.
20    Int,
21    /// Booleans.
22    Bool,
23    /// Reals.
24    Real,
25}
26impl Type {
27    /// String representation.
28    pub fn to_str(self) -> &'static str {
29        match self {
30            Type::Int => "Int",
31            Type::Bool => "Bool",
32            Type::Real => "Real",
33        }
34    }
35}
36impl Sort2Smt for Type {
37    fn sort_to_smt2<Writer: Write>(&self, writer: &mut Writer) -> SmtRes<()> {
38        writer.write_all(self.to_str().as_bytes())?;
39        Ok(())
40    }
41}
42
43/// A symbol is a variable and an offset.
44#[derive(Debug, Clone, PartialEq)]
45pub struct Symbol<'a, 'b>(&'a Var, &'b Offset);
46
47/// An offset gives the index of current and next step.
48#[derive(Debug, Clone, Copy, PartialEq)]
49pub struct Offset(usize, usize);
50impl Offset {
51    /// Index of the current state.
52    #[inline(always)]
53    pub fn curr(&self) -> usize {
54        self.0
55    }
56    /// Index of the next state.
57    #[inline(always)]
58    pub fn next(&self) -> usize {
59        self.1
60    }
61}
62
63/// An unrolled version of something.
64#[derive(Debug, Clone, PartialEq)]
65pub struct Unrolled<'a, T>(T, &'a Offset);
66
67/// Under the hood a symbol is a string.
68pub type Sym = String;
69
70/// A variable wraps a symbol.
71#[derive(Debug, Clone, PartialEq)]
72pub enum Var {
73    /// Variable constant in time (Non-Stateful Var: NSVar).
74    NSVar(Sym),
75    /// State variable in the current step.
76    SVar0(Sym),
77    /// State variable in the next step.
78    SVar1(Sym),
79}
80impl Var {
81    /// Symbol of a variable.
82    pub fn sym(&self) -> &str {
83        match *self {
84            NSVar(ref s) => s,
85            SVar0(ref s) => s,
86            SVar1(ref s) => s,
87        }
88    }
89    /// Non-stateful variable constructor.
90    pub fn nsvar(s: &str) -> Self {
91        NSVar(s.to_string())
92    }
93    /// State variable in the current step.
94    pub fn svar0(s: &str) -> Self {
95        SVar0(s.to_string())
96    }
97    /// State variable in the next step.
98    pub fn svar1(s: &str) -> Self {
99        SVar1(s.to_string())
100    }
101
102    /// Given an offset, an S-expression can be unrolled.
103    pub fn unroll<'a, 'b>(&'a self, off: &'b Offset) -> Unrolled<'b, &'a Var> {
104        Unrolled(self, off)
105    }
106}
107
108impl<'a, V: AsRef<Var>> Expr2Smt<()> for Unrolled<'a, V> {
109    fn expr_to_smt2<Writer: Write>(&self, writer: &mut Writer, _: ()) -> SmtRes<()> {
110        self.0.as_ref().expr_to_smt2(writer, &self.1)
111    }
112}
113impl<'a> Expr2Smt<&'a Offset> for Var {
114    fn expr_to_smt2<Writer: Write>(&self, writer: &mut Writer, off: &'a Offset) -> SmtRes<()> {
115        match *self {
116            NSVar(ref sym) => write!(writer, "|{}|", sym)?,
117            // SVar at 0, we use the index of the current step.
118            SVar0(ref sym) => write!(writer, "|{}@{}|", sym, off.0)?,
119            // SVar at 1, we use the index of the next step.
120            SVar1(ref sym) => write!(writer, "|{}@{}|", sym, off.1)?,
121        }
122        Ok(())
123    }
124}
125
126impl<'a> Sym2Smt<&'a Offset> for Var {
127    fn sym_to_smt2<Writer: Write>(&self, writer: &mut Writer, off: &'a Offset) -> SmtRes<()> {
128        self.expr_to_smt2(writer, off)
129    }
130}
131impl<'a, 'b> Sym2Smt<()> for Unrolled<'a, &'b Var> {
132    fn sym_to_smt2<Writer: Write>(&self, writer: &mut Writer, _: ()) -> SmtRes<()> {
133        self.0.expr_to_smt2(writer, &self.1)
134    }
135}
136
137/// A constant.
138#[derive(Debug, Clone, PartialEq)]
139pub enum Const {
140    /// Boolean constant.
141    BConst(bool),
142    /// Integer constant.
143    IConst(isize),
144    /// Rational constant.
145    RConst(isize, usize),
146}
147
148impl Expr2Smt<()> for Const {
149    fn expr_to_smt2<Writer: Write>(&self, writer: &mut Writer, _: ()) -> SmtRes<()> {
150        match *self {
151            Const::BConst(b) => write!(writer, "{}", b)?,
152            Const::IConst(i) => {
153                let neg = i < 0;
154                if neg {
155                    write!(writer, "(- ")?
156                }
157                write!(writer, "{}", i.abs())?;
158                if neg {
159                    write!(writer, ")")?
160                }
161            }
162            Const::RConst(num, den) => {
163                let neg = num < 0;
164                if neg {
165                    write!(writer, "(- ")?
166                }
167                write!(writer, "(/ {} {})", num, den)?;
168                if neg {
169                    write!(writer, ")")?
170                }
171            }
172        }
173        Ok(())
174    }
175}
176
177/// An S-expression.
178#[derive(Debug, Clone, PartialEq)]
179pub enum SExpr {
180    /// A variable.
181    Id(Var),
182    /// A constant.
183    Val(Const),
184    /// An application of function symbol.
185    App(Sym, Vec<SExpr>),
186}
187
188impl SExpr {
189    /// Application constructor.
190    pub fn app(sym: &str, args: Vec<SExpr>) -> Self {
191        SExpr::App(sym.to_string(), args)
192    }
193    /// Given an offset, an S-expression can be unrolled.
194    pub fn unroll<'a, 'b>(&'a self, off: &'b Offset) -> Unrolled<'b, &'a SExpr> {
195        Unrolled(self, off)
196    }
197}
198
199impl<'a> Expr2Smt<&'a Offset> for SExpr {
200    fn expr_to_smt2<Writer: Write>(&self, writer: &mut Writer, off: &'a Offset) -> SmtRes<()> {
201        match *self {
202            SExpr::Id(ref var) => var.expr_to_smt2(writer, off),
203            SExpr::Val(ref cst) => cst.expr_to_smt2(writer, ()),
204            SExpr::App(ref sym, ref args) => {
205                write!(writer, "({}", sym)?;
206                for arg in args {
207                    write!(writer, " ")?;
208                    arg.expr_to_smt2(writer, off)?
209                }
210                write!(writer, ")")?;
211                Ok(())
212            }
213        }
214    }
215}
216
217impl<'a, 'b> Expr2Smt<()> for Unrolled<'a, &'b SExpr> {
218    fn expr_to_smt2<Writer: Write>(&self, writer: &mut Writer, _: ()) -> SmtRes<()> {
219        self.0.expr_to_smt2(writer, &self.1)
220    }
221}
222
223/// Empty parser structure.
224#[derive(Clone, Copy)]
225pub struct Parser;
226
227impl<'a> IdentParser<(Var, Option<usize>), Type, &'a str> for Parser {
228    fn parse_ident(self, s: &'a str) -> SmtRes<(Var, Option<usize>)> {
229        if s.len() <= 2 {
230            bail!("not one of my idents...")
231        }
232        let s = &s[1..(s.len() - 1)]; // Removing surrounding pipes.
233        let mut parts = s.split('@');
234        let id = if let Some(id) = parts.next() {
235            id.to_string()
236        } else {
237            bail!("nothing between my pipes!")
238        };
239        if let Some(index) = parts.next() {
240            use std::str::FromStr;
241            Ok((
242                Var::SVar0(id),
243                match usize::from_str(index) {
244                    Ok(index) => Some(index),
245                    Err(e) => bail!("while parsing the offset in `{}`: {}", s, e),
246                },
247            ))
248        } else {
249            Ok((Var::NSVar(id), None))
250        }
251    }
252    fn parse_type(self, s: &'a str) -> SmtRes<Type> {
253        match s {
254            "Int" => Ok(Type::Int),
255            "Bool" => Ok(Type::Bool),
256            "Real" => Ok(Type::Real),
257            _ => bail!(format!("unknown type `{}`", s)),
258        }
259    }
260}
261
262impl<'a, Br> ModelParser<(Var, Option<usize>), Type, Const, &'a mut SmtParser<Br>> for Parser
263where
264    Br: ::std::io::BufRead,
265{
266    fn parse_value(
267        self,
268        input: &'a mut SmtParser<Br>,
269        _: &(Var, Option<usize>),
270        _: &[((Var, Option<usize>), Type)],
271        _: &Type,
272    ) -> SmtRes<Const> {
273        use std::str::FromStr;
274        if let Some(b) = input.try_bool()? {
275            Ok(Const::BConst(b))
276        } else if let Some(int) = input.try_int(|int, pos| match isize::from_str(int) {
277            Ok(int) => {
278                if pos {
279                    Ok(int)
280                } else {
281                    Ok(-int)
282                }
283            }
284            Err(e) => Err(e),
285        })? {
286            Ok(Const::IConst(int))
287        } else if let Some((num, den)) =
288            input.try_rat(
289                |num, den, pos| match (isize::from_str(num), usize::from_str(den)) {
290                    (Ok(num), Ok(den)) => {
291                        if pos {
292                            Ok((num, den))
293                        } else {
294                            Ok((-num, den))
295                        }
296                    }
297                    (Err(e), _) | (_, Err(e)) => Err(format!("{}", e)),
298                },
299            )?
300        {
301            Ok(Const::RConst(num, den))
302        } else {
303            input.fail_with("unexpected value")
304        }
305    }
306}
307
308#[test]
309fn declare_non_nullary_fun() {
310    let mut solver = get_solver(Parser);
311
312    smtry!(
313      solver.declare_fun(
314        "my_fun", & [ "Int", "Real", "Bool" ], "Real"
315      ), failwith "during function declaration: {:?}"
316    );
317
318    solver.kill().expect("kill")
319}
320
321#[test]
322fn test_native() {
323    use self::SExpr::*;
324
325    let mut solver = get_solver(Parser);
326
327    let nsv_0 = Var::nsvar("non-stateful var");
328    let s_nsv_0 = Id(nsv_0.clone());
329    let nsv_1 = Var::nsvar("also non-stateful");
330    let s_nsv_1 = Id(nsv_1.clone());
331    let sv_0 = Var::svar0("stateful var");
332    let s_sv_0 = Id(sv_0.clone());
333    let sv_1 = Var::svar1("also stateful");
334    let s_sv_1 = Id(sv_1.clone());
335    let app1 = SExpr::app("not", vec![s_sv_0.clone()]);
336    let app2 = SExpr::app(">", vec![s_sv_1.clone(), Val(Const::IConst(7))]);
337    let app3 = SExpr::app(
338        "=",
339        vec![
340            Val(Const::RConst(-7, 3)),
341            SExpr::app("+", vec![s_nsv_1.clone(), Val(Const::RConst(2, 1))]),
342        ],
343    );
344    let app = SExpr::app("and", vec![s_nsv_0.clone(), app1, app2, app3]);
345    let offset1 = Offset(0, 1);
346
347    smtry!(
348      solver.declare_const_with(& nsv_0, & "Bool", & offset1),
349      failwith "declaration failed: {:?}"
350    );
351
352    smtry!(
353      solver.declare_const_with(& nsv_1, & "Real", & offset1),
354      failwith "declaration failed: {:?}"
355    );
356
357    smtry!(
358      solver.declare_const_with(& sv_0, & "Bool", & offset1),
359      failwith "declaration failed: {:?}"
360    );
361
362    smtry!(
363      solver.declare_const_with(& sv_1, & "Int", & offset1),
364      failwith "declaration failed: {:?}"
365    );
366
367    smtry!(
368      solver.assert_with(& app, & offset1),
369      failwith "assert failed: {:?}"
370    );
371
372    assert!(smtry!(
373      solver.check_sat(),
374      failwith "error in checksat: {:?}"
375    ));
376
377    let model = smtry!(
378      solver.get_model(),
379      failwith "while getting model: {:?}"
380    );
381
382    for ((var, off), _, typ, val) in model {
383        if var.sym() == "stateful var" {
384            assert_eq!(off, Some(0));
385            assert_eq!(typ, Type::Bool);
386            assert_eq!(val, Const::BConst(false))
387        } else if var.sym() == "also stateful" {
388            assert_eq!(off, Some(1));
389            assert_eq!(typ, Type::Int);
390            if let Const::IConst(val) = val {
391                assert!(val > 7)
392            } else {
393                panic!("expected variable, got {:?}", val)
394            }
395        } else if var.sym() == "non-stateful var" {
396            assert_eq!(off, None);
397            assert_eq!(typ, Type::Bool);
398            assert_eq!(val, Const::BConst(true))
399        } else if var.sym() == "also non-stateful" {
400            assert_eq!(off, None);
401            assert_eq!(typ, Type::Real);
402            if let Const::RConst(num, den) = val {
403                assert_eq!(num * 3 + (2 * 3 * den as isize), (7 * den as isize))
404            } else {
405                panic!("expected variable, got {:?}", val)
406            }
407        }
408    }
409
410    solver.kill().expect("kill")
411}
412
413#[test]
414fn test_unroll() {
415    use self::SExpr::*;
416
417    let mut solver = get_solver(Parser);
418
419    let nsv_0 = Var::nsvar("non-stateful var");
420    let s_nsv_0 = Id(nsv_0.clone());
421    let nsv_1 = Var::nsvar("also non-stateful");
422    let s_nsv_1 = Id(nsv_1.clone());
423    let sv_0 = Var::svar0("stateful var");
424    let s_sv_0 = Id(sv_0.clone());
425    let sv_1 = Var::svar1("also stateful");
426    let s_sv_1 = Id(sv_1.clone());
427    let app1 = SExpr::app("not", vec![s_sv_0.clone()]);
428    let app2 = SExpr::app(">", vec![s_sv_1.clone(), Val(Const::IConst(7))]);
429    let app3 = SExpr::app(
430        "=",
431        vec![
432            Val(Const::RConst(-7, 3)),
433            SExpr::app("+", vec![s_nsv_1.clone(), Val(Const::RConst(2, 1))]),
434        ],
435    );
436    let app = SExpr::app("and", vec![s_nsv_0.clone(), app1, app2, app3]);
437    let offset1 = Offset(0, 1);
438
439    let sym = nsv_0.unroll(&offset1);
440    smtry!(
441      solver.declare_const(& sym, & "Bool"),
442      failwith "declaration failed: {:?}"
443    );
444
445    let sym = nsv_1.unroll(&offset1);
446    smtry!(
447      solver.declare_const(& sym, & "Real"),
448      failwith "declaration failed: {:?}"
449    );
450
451    let sym = sv_0.unroll(&offset1);
452    smtry!(
453      solver.declare_const(& sym, & "Bool"),
454      failwith "declaration failed: {:?}"
455    );
456
457    let sym = sv_1.unroll(&offset1);
458    smtry!(
459      solver.declare_const(& sym, & "Int"),
460      failwith "declaration failed: {:?}"
461    );
462
463    let expr = app.unroll(&offset1);
464    smtry!(
465      solver.assert(& expr),
466      failwith "assert failed: {:?}"
467    );
468
469    assert!(smtry!(
470      solver.check_sat(),
471      failwith "error in checksat: {:?}"
472    ));
473
474    let model = smtry!(
475      solver.get_model(),
476      failwith "while getting model: {:?}"
477    );
478
479    for ((var, off), _, typ, val) in model {
480        if var.sym() == "stateful var" {
481            assert_eq!(off, Some(0));
482            assert_eq!(typ, Type::Bool);
483            assert_eq!(val, Const::BConst(false))
484        } else if var.sym() == "also stateful" {
485            assert_eq!(off, Some(1));
486            assert_eq!(typ, Type::Int);
487            if let Const::IConst(val) = val {
488                assert!(val > 7)
489            } else {
490                panic!("expected variable, got {:?}", val)
491            }
492        } else if var.sym() == "non-stateful var" {
493            assert_eq!(off, None);
494            assert_eq!(typ, Type::Bool);
495            assert_eq!(val, Const::BConst(true))
496        } else if var.sym() == "also non-stateful" {
497            assert_eq!(off, None);
498            assert_eq!(typ, Type::Real);
499            if let Const::RConst(num, den) = val {
500                assert_eq!(num * 3 + (2 * 3 * den as isize), (7 * den as isize))
501            } else {
502                panic!("expected variable, got {:?}", val)
503            }
504        }
505    }
506
507    solver.kill().expect("kill")
508}
rsmt2_zz/example/print_time.rs

rsmt2_zz/example/
print_time.rs
