parse_smtv2_model_parser.mly 6.33 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

David Hauzar's avatar
David Hauzar committed
12
%{
13
open Smt2_model_defs
David Hauzar's avatar
David Hauzar committed
14 15
%}

16
%start <Smt2_model_defs.definition Wstdlib.Mstr.t> output
David Hauzar's avatar
David Hauzar committed
17
%token <string> ATOM
18
%token MODEL
David Hauzar's avatar
David Hauzar committed
19 20 21
%token STORE
%token CONST
%token AS
22 23 24 25 26 27 28 29 30 31 32 33 34
%token DEFINE_FUN
%token DECLARE_FUN
%token DECLARE_SORT
%token DECLARE_DATATYPES
%token FORALL
%token UNDERSCORE
%token AS_ARRAY
%token EQUAL
%token ITE
%token LAMBDA
%token ARRAY_LAMBDA
%token TRUE FALSE
%token LET
35
%token AND LE GE NOT
36
%token DIV
37
%token <Model_parser.float_type> FLOAT_VALUE
38
%token <string> COMMENT
39
%token <string> BITVECTOR_VALUE
40
%token <string> BITVECTOR_EXTRACT
41
%token <string> INT_TO_BV
42
%token BITVECTOR_TYPE
43
%token <string * string> FLOAT_TYPE
44
%token <string> INT_STR
David Hauzar's avatar
David Hauzar committed
45
%token <string> MINUS_INT_STR
46 47
%token <string * string> DEC_STR
%token <string * string> MINUS_DEC_STR
David Hauzar's avatar
David Hauzar committed
48 49 50 51
%token LPAREN RPAREN
%token EOF
%%

52

David Hauzar's avatar
David Hauzar committed
53
output:
54
| EOF { Wstdlib.Mstr.empty }
55
| LPAREN MODEL RPAREN { Wstdlib.Mstr.empty }
56
| LPAREN MODEL list_decls RPAREN { $3 }
David Hauzar's avatar
David Hauzar committed
57

58
list_decls:
59 60
| LPAREN decl RPAREN { add_element $2 Wstdlib.Mstr.empty}
| LPAREN decl RPAREN list_decls { add_element $2 $4 }
61
| COMMENT list_decls  { $2 } (* Lines beginning with ';' are ignored *)
David Hauzar's avatar
David Hauzar committed
62

63 64 65 66 67 68 69
(* Examples:
"(define-fun to_rep ((_ufmt_1 enum_t)) Int 0)"
"(declare-sort enum_t 0)"
"(declare-datatypes () ((tuple0 (Tuple0))
))"
*)
decl:
70
| DEFINE_FUN name LPAREN args_lists RPAREN
71
    ireturn_type smt_term
72 73
    { let t = make_local $4 $7 in
        Some ($2, (Function ($4, t))) }
74 75 76
| DECLARE_SORT isort_def { None }
| DECLARE_DATATYPES idata_def { None }
(* z3 declare function *)
77
| DECLARE_FUN name LPAREN args_lists RPAREN ireturn_type { None }
78
| FORALL LPAREN args_lists RPAREN smt_term { None } (* z3 cardinality *)
79 80

smt_term:
81 82 83 84 85 86 87
| name      { Variable $1         }
| integer   { Sval (Integer $1)   }
| decimal   { Sval (Decimal $1)   }
| fraction  { Sval (Fraction $1)  }
| array     { Array $1            }
| bitvector { Sval (Bitvector $1) }
| boolean   { Sval (Boolean $1)   }
88
(* z3 sometimes answer with boolean expressions for some reason ? *)
89 90
| boolean_expression { Sval (Other "") }
| FLOAT_VALUE { Sval (Float $1) }
91
(* ite (= ?a ?b) ?c ?d *)
92 93
| LPAREN ITE pair_equal smt_term smt_term RPAREN
    {  match $3 with
94 95
    | None -> Sval (Other "")
    | Some (t1, t2) -> Ite (t1, t2, $4, $5) }
96
(* No parsable value are applications. *)
97 98
| application { $1 }

99 100
(* Particular case for functions that are defined as an equality:
   define-fun f ((a int) (b int)) (= a b) *)
101
| LPAREN EQUAL list_smt_term RPAREN { Sval (Other "") }
102
| LPAREN LET LPAREN list_let RPAREN smt_term RPAREN
103
    { substitute $4 $6 }
104
(* z3 specific constructor *)
105
| LPAREN UNDERSCORE AS_ARRAY name RPAREN
106
    { To_array (Variable $4) }
107 108 109 110 111


(* value of let are not used *)
list_let:
| { [] }
112
| LPAREN name smt_term RPAREN list_let { ($2, $3) :: $5 }
113 114 115 116
(* TODO not efficient *)

(* Condition of an if-then-else. We are only interested in equality case *)
pair_equal:
117 118
| LPAREN AND list_pair_equal RPAREN { None }
| LPAREN EQUAL smt_term smt_term RPAREN { Some ($3, $4) }
119 120
| application { None }
| name { None }
121
(* ITE containing boolean expressions cannot be dealt with for counterex *)
122
| LPAREN NOT smt_term RPAREN { None }
123 124 125

list_pair_equal:
| { }
126
| pair_equal list_pair_equal { }
127 128 129

list_smt_term:
| smt_term { [$1] }
130
| list_smt_term smt_term { $2 :: $1}
131 132

application:
133 134
| LPAREN name list_smt_term RPAREN { Apply ($2, List.rev $3) }
| LPAREN binop smt_term smt_term RPAREN { Apply ($2, [$3;$4]) }
135 136
(* This should not happen in relevant part of the model *)
| LPAREN INT_TO_BV smt_term RPAREN {
137
  Apply ($2, [$3]) }
138

MARCHE Claude's avatar
MARCHE Claude committed
139 140 141 142 143

binop:
| LE { "<=" }
| GE { ">=" }

David Hauzar's avatar
David Hauzar committed
144

145
array:
146 147 148
| LPAREN
    LPAREN AS CONST ireturn_type
    RPAREN smt_term
149
  RPAREN{ Const $7 }
150 151
| LPAREN
    STORE array smt_term smt_term
152
  RPAREN { Store ($3, $4, $5) }
153 154
| LPAREN
    STORE name smt_term smt_term
155
  RPAREN { Store (Array_var $3, $4, $5) }
156 157 158
(* When array is of type int -> bool, Cvc4 returns something that looks like:
   (ARRAY_LAMBDA (LAMBDA ((BOUND_VARIABLE_1162 Int)) false)) *)
| LPAREN
159 160 161
    ARRAY_LAMBDA
    LPAREN LAMBDA LPAREN args_lists RPAREN smt_term
  RPAREN RPAREN
162
    { Const $8 }
163 164 165

args_lists:
| { [] }
166
| LPAREN args RPAREN args_lists { $2 :: $4 }
167 168 169
(* TODO This is inefficient and should be done in a left recursive way *)

args:
170
| name ireturn_type { $1, $2 }
171 172

name:
David Hauzar's avatar
David Hauzar committed
173
| ATOM { $1 }
174 175
(* Should not happen in relevant part of the model (ad hoc) *)
| BITVECTOR_TYPE { "" }
176
| BITVECTOR_EXTRACT { $1 }
177
| FLOAT_TYPE { "" }
David Hauzar's avatar
David Hauzar committed
178

179 180 181
(* Z3 specific boolean expression. This should maybe be used in the future as
   it may give some information on the counterexample. *)
boolean_expression:
182 183 184
| LPAREN FORALL LPAREN args_lists RPAREN smt_term RPAREN {  }
| LPAREN NOT smt_term RPAREN { }
| LPAREN AND list_smt_term RPAREN { }
185

186
integer:
David Hauzar's avatar
David Hauzar committed
187
| INT_STR { $1 }
188 189
| LPAREN MINUS_INT_STR RPAREN
    { $2 }
David Hauzar's avatar
David Hauzar committed
190

191 192
decimal:
| DEC_STR { $1 }
193 194
| LPAREN MINUS_DEC_STR RPAREN
    { $2 }
195

196
fraction:
197 198
| LPAREN DIV integer integer RPAREN
    { ($3, $4) }
199
(* Integer from z3 can be written 1.0 *)
200 201 202
| LPAREN DIV decimal decimal RPAREN
    { let (num, numdot) = $3 in
      let (dec, decdot) = $4 in
203 204 205 206 207 208
      if numdot = "0" && decdot = "0" then
        (num, dec)
      else
        (* Should not happen. If it does, change the parsing *)
        assert (false)
    }
209

210 211 212 213 214
(* Example:
   (_ bv2048 16) *)
bitvector:
| BITVECTOR_VALUE
    { $1 }
215 216 217 218 219 220 221 222

boolean:
| TRUE  { true  }
| FALSE { false }

(* BEGIN IGNORED TYPES *)
(* Types are badly parsed (for future use) but never saved *)
ireturn_type:
223
| name { Some $1 }
224
| LPAREN idata_type RPAREN { None }
225 226

isort_def:
227
| name integer { }
228 229

idata_def:
230 231
| LPAREN RPAREN LPAREN LPAREN idata_type RPAREN RPAREN { }
| LPAREN RPAREN LPAREN LPAREN RPAREN RPAREN { }
232 233

ilist_app:
234 235
| name { }
| name ilist_app { }
236
| LPAREN idata_type RPAREN { }
237
| LPAREN idata_type RPAREN ilist_app { }
238 239

idata_type:
240 241
| name { }
| name ilist_app { }
242
(* END IGNORED TYPES *)