Commit 8db8a6d5 authored by MARCHE Claude's avatar MARCHE Claude Committed by David Hauzar

Preliminary support for model from CVC4

parent 6fe88dfc
prelude "(set-logic AUFBVNIRA)"
prelude "(set-logic ALL_SUPPORTED)"
(** A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
......
module M
use import int.Int
constant x "model" : int
constant y "model" : int
goal g : x + y >= 0
goal h : forall z "model". x+z >= 0
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="50" memlimit="1000"/>
<file name="../cvc4-models.mlw" expanded="true">
<theory name="M" sum="62207797bdc32ae2764dd3e964f5e9e2" expanded="true">
<goal name="g" expanded="true">
<proof prover="0"><result status="unknown" time="0.02"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -75,6 +75,7 @@ let print_ident fmt id =
type info = {
info_syn : syntax_map;
info_converters : converter_map;
mutable info_model : term list;
}
(** type *)
......@@ -264,15 +265,23 @@ let print_prop_decl info fmt k pr f = match k with
| Some loc -> fprintf fmt " @[;; %a@]@\n"
Loc.gen_report_position loc);
fprintf fmt " @[(not@ %a))@]@\n" (print_fmla info) f;
fprintf fmt "@[(check-sat)@]@\n"
fprintf fmt "@[(check-sat)@]@\n";
if info.info_model != [] then
fprintf fmt "@[(get-value (%a))@]@\n"
(Pp.print_list Pp.space (print_term info)) info.info_model
| Plemma| Pskip -> assert false
let model_label = Ident.create_label "model"
let print_decl info fmt d = match d.d_node with
| Dtype ts ->
print_type_decl info fmt ts
| Ddata _ -> unsupportedDecl d
"smtv2 : algebraic type are not supported"
| Dparam ls ->
if ls.ls_args = [] &&
Slab.mem model_label ls.ls_name.id_label then
info.info_model <- (t_app ls [] ls.ls_value) :: info.info_model;
print_param_decl info fmt ls
| Dlogic dl ->
print_list nothing (print_logic_decl info) fmt dl
......@@ -283,14 +292,24 @@ let print_decl info fmt d = match d.d_node with
print_prop_decl info fmt k pr f
let print_decls =
let print_decl (sm, cm) fmt d =
try print_decl {info_syn = sm; info_converters = cm} fmt d; (sm, cm), []
let print_decl (sm, cm, model) fmt d =
try let info = {info_syn = sm; info_converters = cm; info_model = model} in
print_decl info fmt d; (sm, cm, info.info_model), []
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
Discriminate.on_syntax_map (fun sm ->
Printer.on_converter_map (fun cm ->
Trans.fold print_decl ((sm, cm),[])))
Trans.fold print_decl ((sm, cm, []),[])))
(*
let print_decl (sm,model) fmt d =
try let info = {info_syn = sm; info_model = model} in
print_decl info fmt d; (sm, info.info_model), []
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
Discriminate.on_syntax_map (fun sm -> Trans.fold print_decl ((sm,[]),[]))
Preliminary support for model from CVC4 *)
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
......
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