Commit f9e2170a authored by Sylvain Dailler's avatar Sylvain Dailler

Q217-025 Allow parsing for reference in counterexamples

Parsing reference was forgotten in commit for Q217-025. This solves the
problem with a new token MK_ANYTHING.

* src/driver/parse_smtv2_model_lexer.mll
(parse): Added lexing for all remaining mk*___ record constructs.

* src/driver/parse_smtv2_model_parser.mly
(smt_term): An smt_term can be a reference to a smt_term. It means it can
be (Mk_anything smt_term).

Change-Id: Ib529fee83d16d09266e526ca5fb3c65526addff5
parent ac4f6321
......@@ -19,6 +19,7 @@ let space = [' ''\t''\n''\r']
let num = ['0'-'9']+
let opt_num = ['0'-'9']*
let dec_num = num"."num
let name = (['a'-'z']*'_'*['0'-'9']*)*
rule token = parse
| '\n'
......@@ -65,6 +66,7 @@ rule token = parse
match n with
| "" -> MK_SPLIT_DISCRS ("mk___split_discrs",0)
| n -> MK_SPLIT_DISCRS ("mk____split_discrs"^n, int_of_string n) }
| "mk" name "___" { MK_ANYTHING } (* encapsulate mk_int_ref etc (other refs) *)
| "(_ bv"(num as bv_value)" "num")" { BITVECTOR_VALUE bv_value }
| "(_ BitVec "num")" { BITVECTOR_TYPE }
| num as integer
......
......@@ -40,6 +40,7 @@
%token <string * string> DEC_STR
%token <string * string> MINUS_DEC_STR
%token LPAREN RPAREN
%token MK_ANYTHING
%token <string * int> MK_REP
%token <string * int> MK_SPLIT_FIELD
%token <string * int> MK_T
......@@ -83,7 +84,7 @@ tname:
| MK_SPLIT_FIELD { fst $1 }
| MK_T { fst $1 }
| MK_SPLIT_DISCRS { fst $1 }
| MK_ANYTHING { "" } (* ignore text on this keyword for the moment *)
smt_term:
| name { Smt2_model_defs.Variable $1 }
......@@ -110,6 +111,7 @@ smt_term:
{ Smt2_model_defs.Record (snd $2, List.rev $4) }
| LPAREN MK_SPLIT_DISCRS SPACE list_smt_term RPAREN
{ Smt2_model_defs.Discr (snd $2, List.rev $4) }
| LPAREN MK_ANYTHING ps smt_term RPAREN { $4 } (* ad hoc for refs *)
(* Particular case for functions that are defined as an equality:
define-fun f ((a int) (b int)) (= a b) *)
| LPAREN EQUAL ps list_smt_term RPAREN { Smt2_model_defs.Other "" }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment