Commit 24de6436 authored by Sylvain Dailler's avatar Sylvain Dailler

Adding fractions counterexamples.

parent 42700759
ce/real.mlw ModelReal test1 : Unknown (other)
Counter-example model:File real.mlw:
Line 5:
x = {"type" : "Fraction" ,
"val" : "1\/4" }
ce/real.mlw ModelReal test2 : Unknown (other)
Counter-example model:File real.mlw:
Line 7:
......
......@@ -38,6 +38,7 @@ type float_type =
type model_value =
| Integer of string
| Decimal of (string * string)
| Fraction of (string * string)
| Float of float_type
| Boolean of bool
| Array of model_array
......@@ -114,6 +115,10 @@ let rec convert_model_value value : Json_base.json =
let m = Mstr.add "type" (Json_base.String "Decimal") Stdlib.Mstr.empty in
let m = Mstr.add "val" (Json_base.String (int_part^"."^fract_part)) m in
Json_base.Record m
| Fraction (num, den) ->
let m = Mstr.add "type" (Json_base.String "Fraction") Stdlib.Mstr.empty in
let m = Mstr.add "val" (Json_base.String (num^"/"^den)) m in
Json_base.Record m
| Unparsed s ->
let m = Mstr.add "type" (Json_base.String "Unparsed") Stdlib.Mstr.empty in
let m = Mstr.add "val" (Json_base.String s) m in
......@@ -204,6 +209,7 @@ and print_model_value_human fmt (v: model_value) =
match v with
| Integer s -> fprintf fmt "%s" s
| Decimal (s1,s2) -> fprintf fmt "%s" (s1 ^ "." ^ s2)
| Fraction (s1, s2) -> fprintf fmt "%s" (s1 ^ "/" ^ s2)
| Float f -> print_float_human fmt f
| Boolean b -> fprintf fmt "%b" b
| Array arr -> print_array_human fmt arr
......
......@@ -26,6 +26,7 @@ type float_type =
type model_value =
| Integer of string
| Decimal of (string * string)
| Fraction of (string * string)
| Float of float_type
| Boolean of bool
| Array of model_array
......
......@@ -19,7 +19,7 @@ exception Not_value
let rec get_variables_term (table: correspondence_table) t =
match t with
| Variable _ | Function_Local_Variable _ | Boolean _ | Integer _
| Decimal _ | Float _ | Other _ | Bitvector _ -> table
| Decimal _ | Fraction _ | Float _ | Other _ | Bitvector _ -> table
| Array a ->
get_variables_array table a
| Ite (t1, t2, t3, t4) ->
......@@ -153,7 +153,8 @@ and refine_array table a =
their value. *)
and refine_function table term =
match term with
| Integer _ | Decimal _ | Float _ | Other _ | Bitvector _ | Boolean _ -> term
| Integer _ | Decimal _ | Float _ | Fraction _
| Other _ | Bitvector _ | Boolean _ -> term
| Cvc4_Variable v ->
begin
try (
......@@ -238,6 +239,7 @@ and convert_to_model_value (t: term): Model_parser.model_value =
match t with
| Integer i -> Model_parser.Integer i
| Decimal (d1, d2) -> Model_parser.Decimal (d1, d2)
| Fraction (s1, s2) -> Model_parser.Fraction (s1, s2)
| Float f -> Model_parser.Float (convert_float f)
| Bitvector bv -> Model_parser.Bitvector bv
| Boolean b -> Model_parser.Boolean b
......
......@@ -42,6 +42,7 @@ rule token = parse
| ";;" { read_string (Buffer.create 17) lexbuf }
| '=' { EQUAL }
| '_' { UNDERSCORE }
| '/' { DIV }
| "as-array" { AS_ARRAY }
| "ite" { ITE }
| "define-fun" { DEFINE_FUN }
......
......@@ -33,6 +33,7 @@
%token TRUE FALSE
%token LET
%token AND LE GE NOT
%token DIV
%token <Smt2_model_defs.float_type> FLOAT_VALUE
%token <string> COMMENT
%token <string> BITVECTOR_VALUE
......@@ -92,6 +93,7 @@ smt_term:
| name { Smt2_model_defs.Variable $1 }
| integer { Smt2_model_defs.Integer $1 }
| decimal { Smt2_model_defs.Decimal $1 }
| fraction { Smt2_model_defs.Fraction $1 }
| array { Smt2_model_defs.Array $1 }
| bitvector { Smt2_model_defs.Bitvector $1 }
| boolean { Smt2_model_defs.Boolean $1 }
......@@ -206,6 +208,10 @@ decimal:
| LPAREN ps MINUS_DEC_STR ps RPAREN
{ $3 }
fraction:
| LPAREN ps DIV ps integer ps integer ps RPAREN
{ ($5, $7) }
(* Example:
(_ bv2048 16) *)
bitvector:
......
......@@ -28,6 +28,7 @@ type array =
and term =
| Integer of string
| Decimal of (string * string)
| Fraction of (string * string)
| Float of float_type
| Other of string
| Array of array
......@@ -72,6 +73,7 @@ and print_term fmt t =
match t with
| Integer s -> Format.fprintf fmt "Integer: %s" s
| Decimal (s1, s2) -> Format.fprintf fmt "Decimal: %s . %s" s1 s2
| Fraction (s1, s2) -> Format.fprintf fmt "Fraction: %s / %s" s1 s2
| Float f -> Format.fprintf fmt "Float: %a" print_float f
| Other s -> Format.fprintf fmt "Other: %s" s
| Array a -> Format.fprintf fmt "Array: %a" print_array a
......@@ -143,7 +145,7 @@ and make_local vars_lists t =
let t3 = make_local vars_lists t3 in
let t4 = make_local vars_lists t4 in
Ite (t1, t2, t3, t4)
| Integer _ | Decimal _ | Float _ | Other _ -> t
| Integer _ | Decimal _ | Fraction _ | Float _ | Other _ -> t
| Bitvector _ -> t
| Cvc4_Variable _ -> raise Bad_local_variable
| Boolean _ -> t
......@@ -178,7 +180,8 @@ let build_record_discr lgen =
let rec subst var value t =
match t with
| Integer _ | Decimal _ | Float _ | Other _ | Bitvector _ | Boolean _ ->
| Integer _ | Decimal _ | Fraction _ | Float _
| Other _ | Bitvector _ | Boolean _ ->
t
| Array a -> Array (subst_array var value a)
| Cvc4_Variable _ -> raise Bad_local_variable
......
......@@ -28,6 +28,7 @@ type array =
and term =
| Integer of string
| Decimal of (string * string)
| Fraction of (string * string)
| Float of float_type
| Other of string
| Array of array
......
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