Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 72a2b3e0 authored by Sylvain Dailler's avatar Sylvain Dailler

Merge branch 'master' into itp.

Main change is the type of json value which I changed in master and did
not follow in ITP. Now record are not sent as List. They are maps as in
master. This is quite a big change as json_util completely changes.
parents 376cf77b 084a4108
......@@ -161,8 +161,8 @@ LIBGENERATED = src/util/config.ml \
src/parser/parser.mli src/parser/parser.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
src/driver/driver_lexer.ml \
src/driver/parse_smtv2_model_parser.mli src/driver/parse_smtv2_model_parser.ml \
src/driver/parse_smtv2_model_lexer.ml \
src/driver/parse_smtv2_model_parser.mli src/driver/parse_smtv2_model_parser.ml \
src/driver/parse_smtv2_model_lexer.ml \
src/session/compress.ml src/session/xml.ml \
src/session/strategy_parser.ml \
lib/ocaml/why3__BigInt_compat.ml
......@@ -178,8 +178,10 @@ LIB_CORE = ident ty term pattern decl theory \
task pretty dterm env trans printer model_parser
LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection \
parse_smtv2_model_parser parse_smtv2_model_lexer parse_smtv2_model
whyconf autodetection \
smt2_model_defs parse_smtv2_model_parser \
collect_data_model parse_smtv2_model_lexer parse_smtv2_model \
parse_smtv2_model
LIB_MLW = ity expr dexpr pdecl pmodule
......@@ -201,7 +203,8 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
args_wrapper case \
eliminate_literal
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 smtv2_cvc_ce coq\
pvs isabelle \
simplify gappa cvc3 yices mathematica
LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
......
......@@ -15,7 +15,7 @@ prelude "(set-logic AUFBVDTLIRA)"
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2-cvc-ce.drv"
import "smt-libv2-bv.gen"
import "discrimination.gen"
......
(* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
prelude ";;; generated by SMT-LIB2 driver"
(*
Note: we do not insert any command "set-logic" because its
interpretation is specific to provers
prelude "(set-logic AUFNIRA)"
A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
NIRA : NonLinear Integer Reals Arithmetic
*)
printer "smtv2_cvc_ce"
filename "%f-%t-%g.smt2"
invalid "^sat$"
unknown "^\\(unknown\\|Fail\\)$" ""
time "why3cpulimit time : %s s"
valid "^unsat$"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "encoding:ignore_polymorphism_ls" predicate (=)
meta "encoding : kept" type int
end
theory algebra.OrderedUnitaryCommutativeRing
remove allprops
end
theory algebra.Field
remove allprops
end
theory algebra.OrderedField
remove allprops
end
theory int.Int
prelude ";;; SMT-LIB2: integer arithmetic"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function ( * ) "(* %1 %2)"
syntax function (-_) "(- %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove allprops
end
theory int.Abs
syntax function abs "(abs %1)"
remove allprops
end
theory int.MinMax
syntax function min "(ite (< %1 %2) %1 %2)"
syntax function max "(ite (< %1 %2) %2 %1)"
remove allprops
end
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove allprops
end
theory int.Div2
remove allprops
end
theory int.ComputerDivision
(* really, you should use bitvectors here, but... *)
end
theory real.Real
prelude ";;; SMT-LIB2: real arithmetic"
meta "encoding : kept" type real
syntax function zero "0.0"
syntax function one "1.0"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function ( * ) "(* %1 %2)"
syntax function (/) "(/ %1 %2)"
syntax function (-_) "(- %1)"
syntax function inv "(/ 1.0 %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove allprops
end
theory real.Abs
syntax function abs "(ite (>= %1 0.0) %1 (- %1))"
remove allprops
end
theory real.MinMax
syntax function min "(ite (< %1 %2) %1 %2)"
syntax function max "(ite (< %1 %2) %2 %1)"
remove allprops
end
theory real.FromInt
syntax function from_int "(to_real %1)"
remove allprops
end
theory real.Truncate
syntax function truncate "(ite (>= %1 0.0)
(to_int %1)
(- (to_int (- %1))))"
syntax function floor "(to_int %1)"
syntax function ceil "(- 1 (to_int (- 1.0 %1)))"
remove allprops
end
theory Bool
meta "encoding : kept" type bool
meta "eliminate_algebraic" "no_inversion"
syntax type bool "Bool"
syntax function True "true"
syntax function False "false"
remove allprops
end
theory bool.Bool
syntax function andb "(and %1 %2)"
syntax function orb "(or %1 %2)"
syntax function xorb "(xor %1 %2)"
syntax function notb "(not %1)"
syntax function implb "(=> %1 %2)"
remove allprops
end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding : lskept" function ite
meta "encoding:ignore_polymorphism_ls" function ite
remove allprops
end
theory map.Map
syntax type map "(Array %1 %2)"
meta "encoding:ignore_polymorphism_ts" type map
syntax function get "(select %1 %2)"
syntax function set "(store %1 %2 %3)"
meta "encoding : lskept" function get
meta "encoding : lskept" function set
meta "encoding:ignore_polymorphism_ls" function get
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function set
meta "encoding:ignore_polymorphism_ls" function ([<-])
meta "encoding:ignore_polymorphism_pr" prop Select_eq
meta "encoding:ignore_polymorphism_pr" prop Select_neq
remove allprops
end
theory map.Const
meta "encoding : lskept" function const
(* syntax function const "(const[%t0] %1)" *)
end
......@@ -30,17 +30,23 @@ let debug = Debug.register_info_flag "model_parser"
type model_value =
| Integer of string
| Decimal of (string * string)
| Boolean of bool
| Array of model_array
| Record of model_record
| Bitvector of string
| Unparsed of string
and arr_index = {
arr_index_key : model_value;
arr_index_key : string; (* Even array indices can exceed MAX_INT with Z3 *)
arr_index_value : model_value;
}
and model_array = {
arr_others : model_value;
arr_indices : arr_index list;
}
and model_record = {
discrs : model_value list;
fields : model_value list;
}
let array_create_constant ~value =
{
......@@ -61,37 +67,69 @@ let array_add_element ~array ~index ~value =
arr_indices = arr_index::array.arr_indices;
}
let rec print_indices fmt indices =
match indices with
| [] -> ()
| index::tail ->
fprintf fmt "%a => " print_model_value index.arr_index_key;
print_model_value fmt index.arr_index_value;
fprintf fmt ", ";
print_indices fmt tail
and
print_array fmt arr =
fprintf fmt "(";
print_indices fmt arr.arr_indices;
fprintf fmt "others => ";
print_model_value fmt arr.arr_others;
fprintf fmt ")"
and
print_model_value_sanit sanit_print fmt value =
(* Prints model value. *)
let rec convert_model_value value : Json_base.json =
match value with
| Integer s -> sanit_print fmt s
| Integer s ->
let m = Mstr.add "type" (Json_base.String "Integer") Stdlib.Mstr.empty in
let m = Mstr.add "val" (Json_base.String s) m in
Json_base.Record m
| Decimal (int_part, fract_part) ->
sanit_print fmt (int_part^"."^fract_part)
| Unparsed s -> sanit_print fmt s
let m = Mstr.add "type" (Json_base.String "Float") Stdlib.Mstr.empty in
let m = Mstr.add "val" (Json_base.String (int_part^"."^fract_part)) 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
Json_base.Record m
| Bitvector v ->
let m = Mstr.add "type" (Json_base.String "Bv") Stdlib.Mstr.empty in
let m = Mstr.add "val" (Json_base.String v) m in
Json_base.Record m
| Boolean b ->
let m = Mstr.add "type" (Json_base.String "Boolean") Stdlib.Mstr.empty in
let m = Mstr.add "val" (Json_base.Bool b) m in
Json_base.Record m
| Array a ->
print_array str_formatter a;
sanit_print fmt (flush_str_formatter ())
| Bitvector v -> sanit_print fmt v
and
print_model_value fmt value =
print_model_value_sanit (fun fmt s -> fprintf fmt "%s" s) fmt value
let l = convert_array a in
let m = Mstr.add "type" (Json_base.String "Array") Stdlib.Mstr.empty in
let m = Mstr.add "val" (Json_base.List l) m in
Json_base.Record m
| Record r ->
convert_record r
and convert_array a =
let m_others =
Mstr.add "others" (convert_model_value a.arr_others) Stdlib.Mstr.empty in
convert_indices a.arr_indices @ [Json_base.Record m_others]
and convert_indices indices =
match indices with
| [] -> []
| index :: tail ->
let m = Mstr.add "indice" (Json_base.String index.arr_index_key) Stdlib.Mstr.empty in
let m = Mstr.add "value" (convert_model_value index.arr_index_value) m in
Json_base.Record m :: convert_indices tail
and convert_record r =
let m = Mstr.add "type" (Json_base.String "Record") Stdlib.Mstr.empty in
let fields = convert_fields r.fields in
let discrs = convert_discrs r.discrs in
let m_field_discr = Mstr.add "Field" fields Stdlib.Mstr.empty in
let m_field_discr = Mstr.add "Discr" discrs m_field_discr in
let m = Mstr.add "val" (Json_base.Record m_field_discr) m in
Json_base.Record m
and convert_fields fields =
Json_base.List (List.map convert_model_value fields)
and convert_discrs discrs =
Json_base.List (List.map convert_model_value discrs)
let print_model_value_sanit fmt v =
let v = convert_model_value v in
Json_base.print_json fmt v
let print_model_value = print_model_value_sanit
(*
***************************************************************
......@@ -324,7 +362,7 @@ let interleave_with_source
*)
let print_model_element_json me_name_to_str fmt me =
let print_value fmt =
fprintf fmt "%a" (print_model_value_sanit Json_base.string) me.me_value in
fprintf fmt "%a" print_model_value_sanit me.me_value in
let print_kind fmt =
match me.me_name.men_kind with
| Result -> fprintf fmt "%a" Json_base.string "result"
......
......@@ -17,17 +17,23 @@
type model_value =
| Integer of string
| Decimal of (string * string)
| Boolean of bool
| Array of model_array
| Record of model_record
| Bitvector of string
| Unparsed of string
and arr_index = {
arr_index_key : model_value;
arr_index_key : string;
arr_index_value : model_value;
}
and model_array = {
arr_others : model_value;
arr_indices : arr_index list;
}
and model_record ={
discrs : model_value list;
fields : model_value list;
}
val array_create_constant :
value : model_value ->
......@@ -36,7 +42,7 @@ val array_create_constant :
val array_add_element :
array : model_array ->
index : model_value ->
index : string ->
value : model_value ->
model_array
(** Adds an element to the array.
......
open Stdlib
open Smt2_model_defs
open Strings
exception Not_value
(* Adds all referenced cvc4 variables found in the term t to table *)
let rec get_variables_term (table: correspondence_table) t =
match t with
| Variable _ | Function_Local_Variable _ | Boolean _ | Integer _
| Decimal _ | Other _ | Bitvector _ -> table
| Array a ->
get_variables_array table a
| Ite (t1, t2, t3, t4) ->
let table = get_variables_term table t1 in
let table = get_variables_term table t2 in
let table = get_variables_term table t3 in
let table = get_variables_term table t4 in
table
| Cvc4_Variable cvc ->
if Mstr.mem cvc table then
table
else
Mstr.add cvc (false, Noelement) table
| Record (_, l) ->
List.fold_left (fun table t -> get_variables_term table t) table l
| Discr (_, l) ->
List.fold_left (fun table t -> get_variables_term table t) table l
| To_array t ->
get_variables_term table t
and get_variables_array table a =
match a with
| Const t ->
let table = get_variables_term table t in
table
| Store (a, t1, t2) ->
let table = get_variables_array table a in
let table = get_variables_term table t1 in
get_variables_term table t2
let get_all_var (table: correspondence_table) =
Mstr.fold (fun _key element table ->
match element with
| _, Noelement -> table
| _, Function (_, t) -> get_variables_term table t
| _, Term t -> get_variables_term table t) table table
(* Return true if key is s suffixed with a number *)
(* We should change the code of this function (Str still forbidden) *)
let is_prefix_num key s =
if (String.length s >= String.length key) || String.length s = 0 then
false
else
try
let b = ref (has_prefix s key) in
for i = String.length s to String.length key - 1 do
b := !b && (String.get key i <= '9') && (String.get key i >= '0')
done;
!b
with
| _ -> false
(* Add all variables referenced in the model to the table *)
let add_all_cvc s table t =
Mstr.fold (fun key _element acc ->
if is_prefix_num key s then
try
if snd (Mstr.find key acc) = Noelement then
Mstr.add key t acc
else acc
with Not_found -> acc
else
acc) table table
exception Bad_variable
(* Get the "radical" of a variable *)
let remove_end_num s =
let n = ref (String.length s - 1) in
while String.get s !n <= '9' && String.get s !n >= '0' && !n >= 0 do
n := !n - 1
done;
try
String.sub s 0 (!n + 1)
with
| _ -> s
(* Add the variables that can be deduced from ITE to the table of variables *)
let add_vars_to_table table value =
let rec add_vars_to_table (table: correspondence_table) value =
let t = match (snd value) with
| Term t -> t
| Function (_, t) -> t
| Noelement -> raise Bad_variable in
match t with
| Ite (Cvc4_Variable cvc, Function_Local_Variable _x, t1, t2) ->
begin
let table = Mstr.add cvc (false, Term t1) table in
add_vars_to_table table (false, Term t2)
end
| Ite (Function_Local_Variable _x, Cvc4_Variable cvc, t1, t2) ->
begin
let table = Mstr.add cvc (false, Term t1) table in
add_vars_to_table table (false, Term t2)
end
| Ite (t, Function_Local_Variable _x, Cvc4_Variable cvc, t2) ->
begin
let table = Mstr.add cvc (false, Term t) table in
add_vars_to_table table (false, Term t2)
end
| Ite (Function_Local_Variable _x, t, Cvc4_Variable cvc, t2) ->
begin
let table = Mstr.add cvc (false, Term t) table in
add_vars_to_table table (false, Term t2)
end
| Ite (_, _, _, _) -> table
| _ -> table
in
add_vars_to_table table value
let rec refine_definition table t =
match t with
| Term t -> Term (refine_function table t)
| Function (vars, t) -> Function (vars, refine_function table t)
| Noelement -> Noelement
and refine_array table a =
match a with
| Const t ->
let t = refine_function table t in
Const t
| Store (a, t1, t2) ->
let a = refine_array table a in
let t1 = refine_function table t1 in
let t2 = refine_function table t2 in
Store (a, t1, t2)
(* This function takes the table of assigned variables and a term and replace
the variables with the constant associated with them in the table. If their
value is not a constant yet, recursively apply on these variables and update
their value. *)
and refine_function table term =
match term with
| Integer _ | Decimal _ | Other _ | Bitvector _ | Boolean _ -> term
| Cvc4_Variable v ->
begin
try (
let (b, t) = Mstr.find v table in
let t = match t with
| Term t -> t
| Function (_vars, t) -> t
| Noelement -> raise Not_value
in
if b then
t
else
let table = refine_variable_value table v (b, Term t) in
let t = match (snd (Mstr.find v table)) with
| Term t -> t
| Function (_vars, t) -> t
| Noelement -> raise Not_value in
t
) with
| Not_found -> term
| Not_value -> term
end
| Function_Local_Variable _ -> term
| Variable _ -> term
| Ite (t1, t2, t3, t4) ->
let t1 = refine_function table t1 in
let t2 = refine_function table t2 in
let t3 = refine_function table t3 in
let t4 = refine_function table t4 in
Ite (t1, t2, t3, t4)
| Array a ->
Array (refine_array table a)
| Record (n, l) ->
Record (n, List.map (fun x -> refine_function table x) l)
| Discr (n, l) ->
Discr (n, List.map (fun x -> refine_function table x) l)
| To_array t ->
To_array (refine_function table t)
and refine_variable_value (table: correspondence_table) key v =
let (b, t) = v in
if b then
table
else
let tv = refine_definition table t in
Mstr.add key (true, tv) table
(* Conversion to value referenced as defined in model_parser.
We assume that array indices fit into an integer *)
let convert_to_indice t =
match t with
| Integer i -> i
| _ -> raise Not_value
let rec convert_array_value (a: array) : Model_parser.model_array =
let array_indices = ref [] in
let rec create_array_value a =
match a with