rsmt2 0.16.2

Wrapper for SMT-LIB 2 compliant 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

//! https://github.com/kino-mc/rsmt2/issues/33

mod issue_33 {

    #[test]
    fn multiline_sexpr() {
        let input = "(\n\
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real\n\
      (ite (and (= x!0 1.0) (= x!1 (- (/ 3.0 4.0)))) (- (/ 4.0 3.0))\n\
      (ite (and (= x!0 1.0) (= x!1 (/ 3.0 4.0))) (/ 4.0 3.0)\n\
      0.0)))\n\
)";

        let mut parser = rsmt2::parse::SmtParser::new(input.as_bytes());
        match parser.get_model(false, ()) {
            Ok(m) => {
                assert_eq!(m.len(), 1);
                let (id, params, out, body) = &m[0];
                assert_eq!(id, "/0");
                let mut params = params.into_iter();
                assert_eq!(params.next(), Some(&("x!0".into(), "Real".into())));
                assert_eq!(params.next(), Some(&("x!1".into(), "Real".into())));
                assert_eq!(params.next(), None);
                assert_eq!(out, "Real");
                assert_eq!(
                    body,
                    "\
                    (ite (and (= x!0 1.0) (= x!1 (- (/ 3.0 4.0)))) (- (/ 4.0 3.0))\n\
                    (ite (and (= x!0 1.0) (= x!1 (/ 3.0 4.0))) (/ 4.0 3.0)\n\
                    0.0))\
                "
                )
            }
            Err(e) => {
                println!("Error : {:#?}", e);
                panic!("error")
            }
        }
    }

    #[test]
    fn multiline_sexpr_with_comment() {
        let input = "(
  (define-fun x1 () Real
      (/ 1.0 4.0))
  (define-fun x0 () Real
      (/ 1.0 2.0))
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real
      (ite (and (= x!0 1.0) (= x!1 (- (/ 3.0 4.0)))) (- (/ 4.0 3.0))
      (ite (and (= x!0 1.0) (= x!1 (/ 3.0 4.0))) (/ 4.0 3.0) ; a comment
      0.0)))
)";

        let mut parser = rsmt2::parse::SmtParser::new(input.as_bytes());
        match parser.get_model(false, ()) {
            Ok(_) => (),
            Err(e) => {
                println!("Error : {:#?}", e);
                panic!("error")
            }
        }
    }

    #[test]
    fn multiline_sexpr_with_quoted_ident() {
        let input = "(
  (define-fun x1 () Real
      (/ 1.0 4.0))
  (define-fun x0 () Real
      (/ 1.0 2.0))
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real
      (ite (and (= x!0 1.0) (= x!1 (- (/ 3.0 4.0)))) (- (/ 4.0 3.0))
      (ite (and (= x!0 1.0) (= x!1 (/ 3.0 4.0))) (/ 4.0 | some multiline
      ident|)
      0.0)))
)";

        let mut parser = rsmt2::parse::SmtParser::new(input.as_bytes());
        match parser.get_model(false, ()) {
            Ok(_) => (),
            Err(e) => {
                println!("Error : {:#?}", e);
                panic!("error")
            }
        }
    }

    #[test]
    fn just_id() {
        let input = "(
  (define-fun x1 () Real
      x2
  )
)";

        let mut parser = rsmt2::parse::SmtParser::new(input.as_bytes());
        match parser.get_model(false, ()) {
            Ok(_) => (),
            Err(e) => {
                println!("Error : {:#?}", e);
                panic!("error")
            }
        }
    }
}