From 52207cd30ad2da120f6d880c32dbade66010a007 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 28 Nov 2022 15:24:23 +0100
Subject: [PATCH] [printer] Add a new printer for VNN-LIB format.
The printer for the SMT-LIB format produces not useful stuff.
---
config/drivers/discrimination.gen | 1 -
config/drivers/vnnlib.gen | 19 +-
src/dataset.ml | 10 +-
src/printers/smtv2_vnnlib.ml | 1128 +++++++++++++++++++++++++++++
src/printers/vnnlib.ml | 954 ++++--------------------
5 files changed, 1289 insertions(+), 823 deletions(-)
create mode 100644 src/printers/smtv2_vnnlib.ml
diff --git a/config/drivers/discrimination.gen b/config/drivers/discrimination.gen
index 519eab6..3c7c30c 100644
--- a/config/drivers/discrimination.gen
+++ b/config/drivers/discrimination.gen
@@ -4,4 +4,3 @@ theory BuiltIn
meta "select_lsinst_default" "local"
meta "select_kept_default" "all"
end
-
diff --git a/config/drivers/vnnlib.gen b/config/drivers/vnnlib.gen
index 8c73915..90d83f1 100644
--- a/config/drivers/vnnlib.gen
+++ b/config/drivers/vnnlib.gen
@@ -24,30 +24,16 @@
prelude ";;; produced by VNN-LIB driver"
-printer "smtv2.6_vnnlib"
+printer "vnnlib"
import "discrimination.gen"
filename "%f-%t-%g.vnnlib"
-transformation "inline_trivial"
+transformation "introduce_premises"
transformation "eliminate_builtin"
-transformation "detect_polymorphism"
-transformation "eliminate_definition_conditionally"
-transformation "eliminate_inductive"
-transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
-transformation "eliminate_epsilon"
transformation "simplify_formula"
-(* Prepare for counter-example query: get rid of some quantifiers
- (makes it possible to query model values of the variables in
- premises) and introduce counter-example projections. Note: does
- nothing if meta get_counterexmp is not set *)
-transformation "prepare_for_counterexmp"
-
-transformation "discriminate_if_poly"
-transformation "encoding_smt_if_poly"
-
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
@@ -55,7 +41,6 @@ theory BuiltIn
meta "encoding:kept" type int
meta "encoding:ignore_polymorphism_ls" predicate (=)
- meta "supports_smt_get_info_unknown_reason" ""
end
theory int.Int
diff --git a/src/dataset.ml b/src/dataset.ml
index fe30f49..f02efd8 100644
--- a/src/dataset.ml
+++ b/src/dataset.ml
@@ -248,7 +248,7 @@ let add_axioms ?eps ~clip th task input value =
let ls_ge = Theory.(ns_find_ls th.th_export [ Ident.op_infix ">=" ]) in
let pr_ge =
Decl.create_prsymbol
- (Ident.id_fresh (Fmt.str "axiom_%s_ge" input.Term.ls_name.id_string))
+ (Ident.id_fresh (Fmt.str "axiom_ge_%s" input.Term.ls_name.id_string))
in
let t_ge =
let value = value -. eps in
@@ -261,7 +261,7 @@ let add_axioms ?eps ~clip th task input value =
let ls_le = Theory.(ns_find_ls th.th_export [ Ident.op_infix "<=" ]) in
let pr_le =
Decl.create_prsymbol
- (Ident.id_fresh (Fmt.str "axiom_%s_le" input.Term.ls_name.id_string))
+ (Ident.id_fresh (Fmt.str "axiom_le_%s" input.Term.ls_name.id_string))
in
let t_le =
let value = value +. eps in
@@ -302,7 +302,7 @@ let add_output_decl ~id predicate_kind ~outputs ~record th task =
let goal_pr =
let id =
Ident.id_fresh
- (Fmt.str "%s_record_%d_Y_%s"
+ (Fmt.str "%s_record%d_y%s"
(string_of_predicate_kind predicate_kind)
id label)
in
@@ -327,11 +327,11 @@ let tasks_of_nn_csv_predicate env
let task = Task.use_export None th_real in
(* Add input declarations. *)
let inputs, task =
- add_decls ~id:(Fmt.str "X_%d") task predicate.model.Language.nb_inputs
+ add_decls ~id:(Fmt.str "x%d") task predicate.model.Language.nb_inputs
in
(* Add output declarations. *)
let outputs, task =
- add_decls ~id:(Fmt.str "Y_%d") task predicate.model.Language.nb_outputs
+ add_decls ~id:(Fmt.str "y%d") task predicate.model.Language.nb_outputs
in
let tasks =
List.foldi dataset ~init:[] ~f:(fun id tasks record ->
diff --git a/src/printers/smtv2_vnnlib.ml b/src/printers/smtv2_vnnlib.ml
new file mode 100644
index 0000000..83af6d6
--- /dev/null
+++ b/src/printers/smtv2_vnnlib.ml
@@ -0,0 +1,1128 @@
+(********************************************************************)
+(* *)
+(* The Why3 Verification Platform / The Why3 Development Team *)
+(* Copyright 2010-2022 -- Inria - CNRS - Paris-Saclay University *)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
+
+(** SMT v2 printer with some extensions *)
+
+open Format
+open Why3
+
+[@@@warning "-9"]
+
+open Pp
+open Wstdlib
+open Ident
+open Ty
+open Term
+open Decl
+open Printer
+open Cntexmp_printer
+
+let debug =
+ Debug.register_info_flag "smtv2_printer"
+ ~desc:"Print@ debugging@ messages@ about@ printing@ the@ input@ of@ smtv2."
+
+let debug_incremental =
+ Debug.register_info_flag "force_incremental"
+ ~desc:"Force@ incremental@ mode@ for@ smtv2@ provers"
+
+(** SMTLIB tokens taken from CVC4: src/parser/smt2/{Smt2.g,smt2.cpp} *)
+let ident_printer () =
+ let bls =
+ [
+ (* Base SMT-LIB commands, see page 43 *)
+ "assert";
+ "check-sat";
+ "check-sat-assuming";
+ "declare-const";
+ "declare-datatype";
+ "declare-datatypes";
+ "declare-fun";
+ "declare-sort";
+ "define-fun";
+ "define-fun-rec";
+ "define-funs-rec";
+ "define-sort";
+ "echo";
+ "exit";
+ "get-assignment";
+ "get-assertions";
+ "get-info";
+ "get-model";
+ "get-option";
+ "get-proof";
+ "get-unsat-assumptions";
+ "get-unsat-core";
+ "get-value";
+ "pop";
+ "push";
+ "reset";
+ "reset-assertions";
+ "set-info";
+ "set-logic";
+ "set-option";
+ (* Base SMT-LIB tokens, see page 22*)
+ "BINARY";
+ "DECIMAL";
+ "HEXADECIMAL";
+ "NUMERAL";
+ "STRING";
+ "_";
+ "!";
+ "as";
+ "let";
+ "exists";
+ "forall";
+ "match";
+ "par";
+ (* extended commands *)
+ "assert-rewrite";
+ "assert-reduction";
+ "assert-propagation";
+ "declare-sorts";
+ "declare-funs";
+ "declare-preds";
+ "define";
+ "simplify";
+ (* operators, including theory symbols *)
+ "=";
+ "=>";
+ "+";
+ "-";
+ "*";
+ "^";
+ "<";
+ "<=";
+ ">";
+ ">=";
+ "ite";
+ "and";
+ "distinct";
+ "is_int";
+ "not";
+ "or";
+ "select";
+ "store";
+ "to_int";
+ "to_real";
+ "xor";
+ "/";
+ "div";
+ "mod";
+ "rem";
+ "concat";
+ "bvnot";
+ "bvand";
+ "bvor";
+ "bvneg";
+ "bvadd";
+ "bvmul";
+ "bvudiv";
+ "bvurem";
+ "bvshl";
+ "bvlshr";
+ "bvult";
+ "bvnand";
+ "bvnor";
+ "bvxor";
+ "bvxnor";
+ "bvcomp";
+ "bvsub";
+ "bvsdiv";
+ "bvsrem";
+ "bvsmod";
+ "bvashr";
+ "bvule";
+ "bvugt";
+ "bvuge";
+ "bvslt";
+ "bvsle";
+ "bvsgt";
+ "bvsge";
+ "rotate_left";
+ "rotate_right";
+ "bvredor";
+ "bvredand";
+ "bv2nat";
+ "sqrt";
+ "sin";
+ "cos";
+ "tan";
+ "asin";
+ "acos";
+ "atan";
+ "pi";
+ "exp";
+ "csc";
+ "sec";
+ "cot";
+ "arcsin";
+ "arccos";
+ "arctan";
+ "arccsc";
+ "arcsec";
+ "arccot";
+ (* the new floating point theory - updated to the 2014-05-27 standard *)
+ "FloatingPoint";
+ "fp";
+ "Float16";
+ "Float32";
+ "Float64";
+ "Float128";
+ "RoundingMode";
+ "roundNearestTiesToEven";
+ "RNE";
+ "roundNearestTiesToAway";
+ "RNA";
+ "roundTowardPositive";
+ "RTP";
+ "roundTowardNegative";
+ "RTN";
+ "roundTowardZero";
+ "RTZ";
+ "NaN";
+ "+oo";
+ "-oo";
+ "+zero";
+ "-zero";
+ "fp.abs";
+ "fp.neg";
+ "fp.add";
+ "fp.sub";
+ "fp.mul";
+ "fp.div";
+ "fp.fma";
+ "fp.sqrt";
+ "fp.rem";
+ "fp.roundToIntegral";
+ "fp.min";
+ "fp.max";
+ "fp.leq";
+ "fp.lt";
+ "fp.geq";
+ "fp.gt";
+ "fp.eq";
+ "fp.isNormal";
+ "fp.isSubnormal";
+ "fp.isZero";
+ "fp.isInfinite";
+ "fp.isNaN";
+ "fp.isNegative";
+ "fp.isPositive";
+ "to_fp";
+ "to_fp_unsigned";
+ "fp.to_ubv";
+ "fp.to_sbv";
+ "fp.to_real";
+ (* the new proposed string theory *)
+ "String";
+ "str.<";
+ "str.<=";
+ "str.++";
+ "str.len";
+ "str.substr";
+ "str.contains";
+ "str.at";
+ "str.indexof";
+ "str.prefixof";
+ "str.suffixof";
+ "int.to.str";
+ "str.to.int";
+ "u16.to.str";
+ "str.to.u16";
+ "u32.to.str";
+ "str.to.u32";
+ "str.in.re";
+ "str.to.re";
+ "str.replace";
+ "str.tolower";
+ "str.toupper";
+ "str.rev";
+ "str.from_code";
+ "str.is_digit";
+ "str.from_int";
+ "str.to_int";
+ "str.in_re";
+ "str.to_code";
+ "str.replace_all";
+ "int.to.str";
+ "str.to.int";
+ "str.code";
+ "str.replaceall";
+ "re.++";
+ "re.union";
+ "re.inter";
+ "re.*";
+ "re.+";
+ "re.opt";
+ "re.range";
+ "re.loop";
+ "re.comp";
+ "re.diff";
+ (* the new proposed set theory *)
+ "union";
+ "intersection";
+ "setminus";
+ "subset";
+ "member";
+ "singleton";
+ "insert";
+ "card";
+ "complement";
+ "join";
+ "product";
+ "transpose";
+ "tclosure";
+ (* built-in sorts *)
+ "Bool";
+ "Int";
+ "Real";
+ "BitVec";
+ "Array";
+ (* Other stuff that Why3 seems to need *)
+ "unsat";
+ "sat";
+ "true";
+ "false";
+ "const";
+ "abs";
+ "BitVec";
+ "extract";
+ "bv2nat";
+ "nat2bv";
+ (* From Z3 *)
+ "map";
+ "bv";
+ "default";
+ "difference";
+ (* From CVC4 *)
+ "char";
+ "choose";
+ (* Counterexamples specific keywords *)
+ "lambda";
+ "LAMBDA";
+ "model";
+ (* various stuff from "sed -n -e 's/^.*addOperator.*\"\([^\"]*\)\".*/\1/p'
+ src/parser/smt2/smt2.cpp" *)
+ "inst-closure";
+ "dt.size";
+ "sep";
+ "pto";
+ "wand";
+ "emp";
+ "fmf.card";
+ "fmf.card.val";
+ ]
+ in
+ let san = sanitizer char_to_alpha char_to_alnumus in
+ create_ident_printer bls ~sanitizer:san
+
+type version =
+ | V20
+ | V26
+ | V26Par
+
+type info = {
+ info_syn : syntax_map;
+ info_rliteral : syntax_map;
+ mutable info_model : S.t;
+ mutable info_in_goal : bool;
+ info_vc_term : vc_term_info;
+ info_printer : ident_printer;
+ mutable list_projs : Ident.ident Mstr.t;
+ mutable list_field_def : Ident.ident Mstr.t;
+ info_version : version;
+ meta_model_projection : Sls.t;
+ meta_record_def : Sls.t;
+ mutable list_records : field_info list Mstr.t;
+ (* For algebraic type counterexamples: constructors with no arguments can be
+ misunderstood for variables *)
+ mutable noarg_constructors : string list;
+ info_cntexample_need_push : bool;
+ info_cntexample : bool;
+ info_incremental : bool;
+ info_set_incremental : bool;
+ info_supports_reason_unknown : bool;
+ mutable info_labels : Sattr.t Mstr.t;
+ mutable incr_list_axioms : (prsymbol * term) list;
+ mutable incr_list_ldecls : (lsymbol * vsymbol list * term) list;
+}
+
+let debug_print_term message t =
+ let form = Debug.get_debug_formatter () in
+ Debug.dprintf debug message;
+ if Debug.test_flag debug then Pretty.print_term form t;
+ Debug.dprintf debug "@."
+
+let print_ident info fmt id =
+ pp_print_string fmt (id_unique info.info_printer id)
+
+(** type *)
+
+let print_tv info fmt tv =
+ pp_print_string fmt (id_unique info.info_printer tv.tv_name)
+
+(** print `(par ...)` around the given body to print *)
+let print_par info
+ (* body *)
+ (* Format.kdprintf *) print_body fmt tvs =
+ if Ty.Stv.is_empty tvs
+ then print_body fmt
+ else if info.info_version = V26Par
+ then
+ Format.fprintf fmt "(par (%a)@ %t)"
+ (print_iter1 Ty.Stv.iter pp_print_space (print_tv info))
+ tvs print_body
+ else unsupported "smt: polymorphism must be encoded"
+(* body *)
+
+let rec print_type info fmt ty =
+ match ty.ty_node with
+ | Tyvar s -> (
+ match info.info_version with
+ | V20 -> unsupported "smtv2: you must encode type polymorphism"
+ | V26 | V26Par -> print_tv info fmt s)
+ | Tyapp (ts, l) -> (
+ match (query_syntax info.info_syn ts.ts_name, l) with
+ | Some s, _ -> syntax_arguments s (print_type info) fmt l
+ | None, [] -> print_ident info fmt ts.ts_name
+ | None, _ ->
+ fprintf fmt "(%a %a)" (print_ident info) ts.ts_name
+ (print_list space (print_type info))
+ l)
+
+let print_type info fmt ty =
+ try print_type info fmt ty
+ with Unsupported s -> raise (UnsupportedType (ty, s))
+
+let print_type_value info fmt = function
+ | None -> pp_print_string fmt "Bool"
+ | Some ty -> print_type info fmt ty
+
+(** var *)
+let forget_var info v = forget_id info.info_printer v.vs_name
+
+let print_var info fmt { vs_name = id } =
+ let n = id_unique info.info_printer id in
+ pp_print_string fmt n
+
+let print_typed_var info fmt vs =
+ fprintf fmt "(%a %a)" (print_var info) vs (print_type info) vs.vs_ty
+
+let print_var_list info fmt vsl = print_list space (print_var info) fmt vsl
+
+let print_typed_var_list info fmt vsl =
+ print_list space (print_typed_var info) fmt vsl
+
+let collect_model_ls info ls =
+ if Sls.mem ls info.meta_model_projection
+ then
+ info.list_projs <-
+ Mstr.add
+ (sprintf "%a" (print_ident info) ls.ls_name)
+ ls.ls_name info.list_projs;
+ if Sls.mem ls info.meta_record_def
+ then
+ info.list_field_def <-
+ Mstr.add
+ (sprintf "%a" (print_ident info) ls.ls_name)
+ ls.ls_name info.list_field_def;
+ if ls.ls_args = [] && relevant_for_counterexample ls.ls_name
+ then
+ let t = t_app ls [] ls.ls_value in
+ info.info_model <-
+ add_model_element
+ (t_attr_set ?loc:ls.ls_name.id_loc ls.ls_name.id_attrs t)
+ info.info_model
+
+let number_format =
+ {
+ Number.long_int_support = `Default;
+ Number.negative_int_support = `Default;
+ Number.dec_int_support = `Default;
+ Number.hex_int_support = `Unsupported;
+ Number.oct_int_support = `Unsupported;
+ Number.bin_int_support = `Unsupported;
+ Number.negative_real_support = `Default;
+ Number.dec_real_support = `Default;
+ Number.hex_real_support = `Unsupported;
+ Number.frac_real_support =
+ `Custom
+ ( (fun fmt i -> fprintf fmt "%s.0" i),
+ fun fmt i n -> fprintf fmt "(/ %s.0 %s.0)" i n );
+ }
+
+let escape c =
+ match c with
+ | '\\' -> "\\x5C"
+ | '\"' -> "\\x22"
+ | '\032' .. '\126' -> Format.sprintf "%c" c
+ | '\000' .. '\031' | '\127' .. '\255' ->
+ Format.sprintf "\\x%02X" (Char.code c)
+
+(* can the type of a value be derived from the type of the arguments? *)
+let unambig_fs version fs =
+ let rec lookup v ty =
+ match ty.ty_node with
+ | Tyvar u when tv_equal u v -> true
+ | _ -> ty_any (lookup v) ty
+ in
+ let lookup v = List.exists (lookup v) fs.ls_args in
+ let rec inspect ty =
+ match ty.ty_node with
+ | Tyvar u when not (lookup u) -> false
+ | _ -> ty_all inspect ty
+ in
+ match version with
+ | V20 | V26 -> true
+ | V26Par -> inspect (Opt.get fs.ls_value)
+
+(** expr *)
+let rec print_term info fmt t =
+ debug_print_term "Printing term: " t;
+ if check_for_counterexample t
+ then info.info_model <- add_model_element t info.info_model;
+
+ check_enter_vc_term t info.info_in_goal info.info_vc_term;
+
+ let () =
+ match t.t_node with
+ | Tconst c -> (
+ let ts =
+ match t.t_ty with
+ | Some { ty_node = Tyapp (ts, []) } -> ts
+ | _ -> assert false (* impossible *)
+ in
+ (* look for syntax literal ts in driver *)
+ match (query_syntax info.info_rliteral ts.ts_name, c) with
+ | Some st, Constant.ConstInt c -> syntax_range_literal st fmt c
+ | Some st, Constant.ConstReal c ->
+ let fp = match ts.ts_def with Float fp -> fp | _ -> assert false in
+ syntax_float_literal st fp fmt c
+ | _, Constant.ConstStr _ | None, _ ->
+ Constant.print number_format escape fmt c
+ (* TODO/FIXME: we must assert here that the type is either ty_int or
+ ty_real, otherwise it makes no sense to print the literal. Do we ensure
+ that preserved literal types are exactly those that have a dedicated
+ syntax? *))
+ | Tvar v -> print_var info fmt v
+ | Tapp (ls, tl) -> (
+ match query_syntax info.info_syn ls.ls_name with
+ | Some s ->
+ syntax_arguments_typed s (print_term info) (print_type info) t fmt tl
+ | None -> (
+ match tl with
+ (* for cvc3 wich doesn't accept (toto ) *)
+ | [] ->
+ let str_ls = sprintf "%a" (print_ident info) ls.ls_name in
+ let cur_var = info.info_labels in
+ let new_var = update_info_labels str_ls cur_var t ls in
+ let () = info.info_labels <- new_var in
+ let vc_term_info = info.info_vc_term in
+ (if vc_term_info.vc_inside
+ then
+ match vc_term_info.vc_loc with
+ | None -> ()
+ | Some loc ->
+ let attrs =
+ (* match vc_term_info.vc_func_name with | None -> *)
+ ls.ls_name.id_attrs
+ (* | Some _ -> model_trace_for_postcondition
+ ~attrs:ls.ls_name.id_attrs info.info_vc_term *)
+ in
+ let _t_check_pos = t_attr_set ~loc attrs t in
+ (* TODO: temporarily disable collecting variables inside the term
+ triggering VC *)
+ (*info.info_model <- add_model_element t_check_pos
+ info.info_model;*)
+ ());
+ if unambig_fs info.info_version ls
+ then fprintf fmt "@[%a@]" (print_ident info) ls.ls_name
+ else
+ fprintf fmt "@[(as %a %a)@]" (print_ident info) ls.ls_name
+ (print_type info) (t_type t)
+ | _ ->
+ if unambig_fs info.info_version ls
+ then
+ fprintf fmt "@[<hv2>(%a@ %a)@]" (print_ident info) ls.ls_name
+ (print_list space (print_term info))
+ tl
+ else
+ fprintf fmt "@[<hv2>((as %a@ %a)@ %a)@]" (print_ident info)
+ ls.ls_name (print_type info) (t_type t)
+ (print_list space (print_term info))
+ tl))
+ | Tlet (t1, tb) ->
+ let v, t2 = t_open_bound tb in
+ fprintf fmt "@[<hv2>(let ((%a %a))@ %a)@]" (print_var info) v
+ (print_term info) t1 (print_term info) t2;
+ forget_var info v
+ | Tif (f1, t1, t2) ->
+ fprintf fmt "@[<hv2>(ite %a@ %a@ %a)@]" (print_fmla info) f1
+ (print_term info) t1 (print_term info) t2
+ | Tcase (t, bl) -> (
+ let ty = t_type t in
+ match ty.ty_node with
+ | Tyapp (ts, _) when ts_equal ts ts_bool ->
+ print_boolean_branches info t print_term fmt bl
+ | _ -> (
+ match t.t_node with
+ | Tvar v -> print_branches info v print_term fmt bl
+ | _ ->
+ let subject = create_vsymbol (id_fresh "subject") (t_type t) in
+ fprintf fmt "@[<hv2>(let ((%a @[%a@]))@ %a)@]" (print_var info)
+ subject (print_term info) t
+ (print_branches info subject print_term)
+ bl;
+ forget_var info subject))
+ | Teps _ -> unsupportedTerm t "smtv2: you must eliminate epsilon"
+ | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
+ in
+
+ check_exit_vc_term t info.info_in_goal info.info_vc_term
+
+and print_fmla info fmt f =
+ debug_print_term "Printing formula: " f;
+ if check_for_counterexample f
+ then info.info_model <- add_model_element f info.info_model;
+
+ check_enter_vc_term f info.info_in_goal info.info_vc_term;
+
+ let () =
+ match f.t_node with
+ | Tapp ({ ls_name = id }, []) -> print_ident info fmt id
+ | Tapp (ls, tl) -> (
+ match query_syntax info.info_syn ls.ls_name with
+ | Some s ->
+ syntax_arguments_typed s (print_term info) (print_type info) f fmt tl
+ | None -> (
+ match tl with
+ (* for cvc3 wich doesn't accept (toto ) *)
+ | [] -> print_ident info fmt ls.ls_name
+ | _ ->
+ fprintf fmt "@[<hv2>(%a@ %a)@]" (print_ident info) ls.ls_name
+ (print_list space (print_term info))
+ tl))
+ | Tquant (q, fq) ->
+ let q = match q with Tforall -> "forall" | Texists -> "exists" in
+ let vl, tl, f = t_open_quant fq in
+ (* TODO trigger dépend des capacités du prover : 2 printers?
+ smtwithtriggers/smtstrict *)
+ if tl = []
+ then
+ fprintf fmt "@[<hv2>(%s @[<h>(%a)@]@ %a)@]" q
+ (print_typed_var_list info)
+ vl (print_fmla info) f
+ else
+ fprintf fmt "@[<hv2>(%s @[<h>(%a)@]@ (! %a %a))@]" q
+ (print_typed_var_list info)
+ vl (print_fmla info) f (print_triggers info) tl;
+ List.iter (forget_var info) vl
+ | Tbinop (Tand, f1, f2) ->
+ fprintf fmt "@[<hv2>(and@ %a@ %a)@]" (print_fmla info) f1
+ (print_fmla info) f2
+ | Tbinop (Tor, f1, f2) ->
+ fprintf fmt "@[<hv2>(or@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info)
+ f2
+ | Tbinop (Timplies, f1, f2) ->
+ fprintf fmt "@[<hv2>(=>@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info)
+ f2
+ | Tbinop (Tiff, f1, f2) ->
+ fprintf fmt "@[<hv2>(=@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info)
+ f2
+ | Tnot f -> fprintf fmt "@[<hv2>(not@ %a)@]" (print_fmla info) f
+ | Ttrue -> pp_print_string fmt "true"
+ | Tfalse -> pp_print_string fmt "false"
+ | Tif (f1, f2, f3) ->
+ fprintf fmt "@[<hv2>(ite %a@ %a@ %a)@]" (print_fmla info) f1
+ (print_fmla info) f2 (print_fmla info) f3
+ | Tlet (t1, tb) ->
+ let v, f2 = t_open_bound tb in
+ fprintf fmt "@[<hv2>(let ((%a %a))@ %a)@]" (print_var info) v
+ (print_term info) t1 (print_fmla info) f2;
+ forget_var info v
+ | Tcase (t, bl) -> (
+ let ty = t_type t in
+ match ty.ty_node with
+ | Tyapp (ts, _) when ts_equal ts ts_bool ->
+ print_boolean_branches info t print_fmla fmt bl
+ | _ -> (
+ match t.t_node with
+ | Tvar v -> print_branches info v print_fmla fmt bl
+ | _ ->
+ let subject = create_vsymbol (id_fresh "subject") (t_type t) in
+ fprintf fmt "@[<hv2>(let ((%a @[%a@]))@ %a)@]" (print_var info)
+ subject (print_term info) t
+ (print_branches info subject print_fmla)
+ bl;
+ forget_var info subject))
+ | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
+ in
+
+ check_exit_vc_term f info.info_in_goal info.info_vc_term
+
+and print_boolean_branches info subject pr fmt bl =
+ let error () =
+ unsupportedTerm subject
+ "smtv2: bad pattern-matching on Boolean (compile_match missing?)"
+ in
+ match bl with
+ | [ br1; br2 ] -> (
+ let p1, t1 = t_open_branch br1 in
+ let _p2, t2 = t_open_branch br2 in
+ match p1.pat_node with
+ | Papp (cs, _) ->
+ let csname = if ls_equal cs fs_bool_true then "true" else "false" in
+ fprintf fmt "@[<hv2>(ite (= %a %s) %a %a)@]" (print_term info) subject
+ csname (pr info) t1 (pr info) t2
+ | _ -> error ())
+ | _ -> error ()
+
+and print_branches info subject pr fmt bl =
+ match bl with
+ | [] -> assert false
+ | br :: bl -> (
+ let p, t = t_open_branch br in
+ let error () =
+ unsupportedPattern p "smtv2: you must compile nested pattern-matching"
+ in
+ match p.pat_node with
+ | Pwild -> pr info fmt t
+ | Papp (cs, args) ->
+ let args =
+ List.map (function { pat_node = Pvar v } -> v | _ -> error ()) args
+ in
+ if bl = []
+ then print_branch info subject pr fmt (cs, args, t)
+ else
+ (match info.info_version with
+ | V20 | V26 (* It should be the same than V26Par but it was different *)
+ ->
+ fprintf fmt "@[<hv2>(ite (is-%a %a) %a %a)@]"
+ | V26Par -> fprintf fmt "@[<hv2>(ite ((_ is %a) %a) %a %a)@]")
+ (print_ident info) cs.ls_name (print_var info) subject
+ (print_branch info subject pr)
+ (cs, args, t)
+ (print_branches info subject pr)
+ bl
+ | _ -> error ())
+
+and print_branch info subject pr fmt (cs, vars, t) =
+ if vars = []
+ then pr info fmt t
+ else
+ let tvs = t_freevars Mvs.empty t in
+ if List.for_all (fun v -> not (Mvs.mem v tvs)) vars
+ then pr info fmt t
+ else
+ let i = ref 0 in
+ let pr_proj fmt v =
+ incr i;
+ if Mvs.mem v tvs
+ then
+ fprintf fmt "(%a (%a_proj_%d %a))" (print_var info) v
+ (print_ident info) cs.ls_name !i (print_var info) subject
+ in
+ fprintf fmt "@[<hv2>(let (%a) %a)@]" (print_list space pr_proj) vars
+ (pr info) t
+
+and print_expr info fmt =
+ TermTF.t_select (print_term info fmt) (print_fmla info fmt)
+
+and print_trigger info fmt e = print_expr info fmt e
+
+and print_triggers info fmt = function
+ | [] -> ()
+ | a :: l ->
+ fprintf fmt ":pattern (%a) %a"
+ (print_list space (print_trigger info))
+ a (print_triggers info) l
+
+let print_type_decl info fmt ts =
+ if is_alias_type_def ts.ts_def
+ then ()
+ else if Mid.mem ts.ts_name info.info_syn
+ then ()
+ else
+ fprintf fmt "(declare-sort %a %i)@\n@\n" (print_ident info) ts.ts_name
+ (List.length ts.ts_args)
+
+let print_param_decl info fmt ls =
+ if Mid.mem ls.ls_name info.info_syn
+ then ()
+ else
+ match ls.ls_args with
+ (* only in SMTLIB 2.5 | [] -> fprintf fmt "@[<hov 2>(declare-const %a
+ %a)@]@\n@\n" (print_ident info) ls.ls_name (print_type_value info)
+ ls.ls_value *)
+ | _ ->
+ let tvs = Term.ls_ty_freevars ls in
+ fprintf fmt ";; %s@\n@[<v2>(declare-fun %a %a)@]@\n@\n"
+ ls.ls_name.id_string (print_ident info) ls.ls_name
+ (print_par info (fun fmt ->
+ Format.fprintf fmt "(%a) %a"
+ (print_list space (print_type info))
+ ls.ls_args (print_type_value info) ls.ls_value))
+ tvs
+
+let rec has_quantification f =
+ match f.t_node with
+ | Tquant _ | Teps _ -> true
+ | _ -> Term.t_any has_quantification f
+
+let print_logic_decl_aux flag info fmt (ls, def) =
+ if not (Mid.mem ls.ls_name info.info_syn)
+ then (
+ collect_model_ls info ls;
+ let vsl, expr = Decl.open_ls_defn def in
+ if info.info_incremental && has_quantification expr
+ then (
+ fprintf fmt ";; %s@\n@[<hov2>(declare-fun %a (%a) %a)@]@\n@\n"
+ ls.ls_name.id_string (print_ident info) ls.ls_name
+ (print_list space (print_type info))
+ (List.map (fun vs -> vs.vs_ty) vsl)
+ (print_type_value info) ls.ls_value;
+ info.incr_list_ldecls <- (ls, vsl, expr) :: info.incr_list_ldecls)
+ else
+ let tvs = Term.ls_ty_freevars ls in
+ fprintf fmt ";; %s@\n@[<v2>(define-fun%s %a %a)@]@\n@\n"
+ ls.ls_name.id_string flag (print_ident info) ls.ls_name
+ (print_par info (fun fmt ->
+ Format.fprintf fmt "@[<h>(%a) %a@]@ %a"
+ (print_typed_var_list info)
+ vsl (print_type_value info) ls.ls_value (print_expr info) expr))
+ tvs;
+ List.iter (forget_var info) vsl)
+
+let print_logic_decl = print_logic_decl_aux ""
+
+let print_rec_logic_decl info fmt = function
+ | [] -> ()
+ | [ ld ] -> print_logic_decl_aux "-rec" info fmt ld
+ | l ->
+ let l =
+ List.map
+ (fun (ls, def) ->
+ let vsl, expr = Decl.open_ls_defn def in
+ (ls, vsl, expr))
+ l
+ in
+ let print_decl fmt (ls, vsl, _) =
+ if Mid.mem ls.ls_name info.info_syn
+ then ()
+ else (
+ collect_model_ls info ls;
+ let tvs = Term.ls_ty_freevars ls in
+ fprintf fmt "@[<hov 2>(%a %a)@]@\n@\n" (print_ident info) ls.ls_name
+ (print_par info (fun fmt ->
+ Format.fprintf fmt "(%a) %a"
+ (print_typed_var_list info)
+ vsl (print_type_value info) ls.ls_value))
+ tvs)
+ in
+ let print_term fmt (ls, _, expr) =
+ if Mid.mem ls.ls_name info.info_syn
+ then ()
+ else fprintf fmt "@[<hov 2>%a@]" (print_expr info) expr
+ in
+ fprintf fmt "@[<hov 2>(define-funs-rec (%a) (%a))@]@\n@\n"
+ (print_list nothing print_decl)
+ l
+ (print_list nothing print_term)
+ l;
+ List.iter (fun (_, vsl, _) -> List.iter (forget_var info) vsl) l
+
+let print_info_model info =
+ (* Prints the content of info.info_model *)
+ let info_model = info.info_model in
+ if (not (S.is_empty info_model)) && info.info_cntexample
+ then (
+ let model_map =
+ S.fold
+ (fun f acc ->
+ let s = asprintf "%a" (print_fmla info) f in
+ Mstr.add s f acc)
+ info_model Mstr.empty
+ in
+
+ (* Printing model has modification of info.info_model as undesirable
+ side-effect. Revert it back. *)
+ info.info_model <- info_model;
+ model_map)
+ else Mstr.empty
+
+(* TODO factor out print_prop ? *)
+let print_prop info fmt (pr, f) =
+ let tvs = Term.t_ty_freevars Ty.Stv.empty f in
+ fprintf fmt ";; %s@\n@[<hov 2>(assert@ %a)@]@\n@\n"
+ pr.pr_name.id_string (* FIXME? collisions *)
+ (print_par info (fun fmt -> print_fmla info fmt f))
+ tvs
+
+let add_check_sat info fmt =
+ if info.info_cntexample && info.info_cntexample_need_push
+ then fprintf fmt "@[(push)@]@\n";
+ fprintf fmt "@[(check-sat)@]@\n";
+ if info.info_supports_reason_unknown
+ then fprintf fmt "@[(get-info :reason-unknown)@]@\n";
+ if info.info_cntexample then fprintf fmt "@[(get-model)@]@\n@\n"
+
+let print_ldecl_axiom info fmt (ls, vls, t) =
+ fprintf fmt ";; %s@\n" ls.ls_name.id_string;
+ fprintf fmt
+ "@[<hv2>(assert@ @[<hv2>(forall @[(%a)@]@ @[<hv2>(= @[<h>(%a %a)@]@ \
+ %a)@])@])@]@\n\
+ @\n"
+ (print_typed_var_list info)
+ vls (print_ident info) ls.ls_name (print_var_list info) vls
+ (print_expr info) t
+
+(* TODO if the property doesnt begin with quantifier, then we print it first.
+ Else, we print it afterwards. *)
+let print_incremental_axiom info fmt =
+ List.iter (print_prop info fmt) info.incr_list_axioms;
+ List.iter (print_ldecl_axiom info fmt) info.incr_list_ldecls;
+ add_check_sat info fmt
+
+let print_prop_decl vc_loc vc_attrs printing_info info fmt k pr f =
+ match k with
+ | Paxiom ->
+ if info.info_incremental && has_quantification f
+ then info.incr_list_axioms <- (pr, f) :: info.incr_list_axioms
+ else print_prop info fmt (pr, f)
+ | Pgoal ->
+ let tvs = Term.t_ty_freevars Ty.Stv.empty f in
+ if not (Ty.Stv.is_empty tvs)
+ then unsupported "smt: monomorphise goal must be applied";
+ fprintf fmt ";; Goal %s@\n" pr.pr_name.id_string;
+ (match pr.pr_name.id_loc with
+ | None -> ()
+ | Some loc -> fprintf fmt ";; %a@\n" Loc.gen_report_position loc);
+ info.info_in_goal <- true;
+ fprintf fmt "@[(assert@\n";
+ fprintf fmt " @[(not@ %a))@]@\n@\n" (print_fmla info) f;
+ info.info_in_goal <- false;
+ add_check_sat info fmt;
+
+ (* If in incremental mode, we empty the list of axioms we stored *)
+ if info.info_incremental then print_incremental_axiom info fmt;
+
+ let model_list = print_info_model info in
+
+ printing_info :=
+ Some
+ {
+ vc_term_loc = vc_loc;
+ vc_term_attrs = vc_attrs;
+ queried_terms = model_list;
+ list_projections = info.list_projs;
+ list_fields = info.list_field_def;
+ Printer.list_records = info.list_records;
+ noarg_constructors = info.noarg_constructors;
+ set_str = info.info_labels;
+ }
+ | Plemma -> assert false
+
+let print_constructor_decl info fmt (ls, args) =
+ let field_names =
+ match args with
+ | [] ->
+ fprintf fmt "(%a)" (print_ident info) ls.ls_name;
+ let cons_name = sprintf "%a" (print_ident info) ls.ls_name in
+ info.noarg_constructors <- cons_name :: info.noarg_constructors;
+ []
+ | _ ->
+ fprintf fmt "@[(%a@ " (print_ident info) ls.ls_name;
+ let field_names, _ =
+ List.fold_left2
+ (fun (acc, i) ty pr ->
+ let field_name =
+ match pr with
+ | Some pr ->
+ let field_name = sprintf "%a" (print_ident info) pr.ls_name in
+ fprintf fmt "(%s" field_name;
+ let field_trace =
+ try
+ let attr =
+ Sattr.choose
+ (Sattr.filter
+ (fun l ->
+ Strings.has_prefix "model_trace:" l.attr_string)
+ pr.ls_name.id_attrs)
+ in
+ Strings.remove_prefix "model_trace:" attr.attr_string
+ with Not_found -> ""
+ in
+ { field_name; field_trace; field_ident = Some pr.ls_name }
+ | None ->
+ let field_name =
+ sprintf "%a_proj_%d" (print_ident info) ls.ls_name i
+ in
+ (* FIXME: is it possible to generate 2 same value with _proj_
+ inside it ? Need sanitizing and uniquifying ? *)
+ fprintf fmt "(%s" field_name;
+ { field_name; field_trace = ""; field_ident = None }
+ in
+ fprintf fmt " %a)" (print_type info) ty;
+ (field_name :: acc, succ i))
+ ([], 1) ls.ls_args args
+ in
+ fprintf fmt ")@]";
+ List.rev field_names
+ in
+
+ if Strings.has_suffix "'mk" ls.ls_name.id_string
+ then
+ info.list_records <-
+ Mstr.add
+ (sprintf "%a" (print_ident info) ls.ls_name)
+ field_names info.list_records
+
+let print_data_decl info fmt (ts, cl) =
+ fprintf fmt "@[(%a@ %a)@]" (print_ident info) ts.ts_name
+ (print_list space (print_constructor_decl info))
+ cl
+
+let print_data_def info fmt (ts, cl) =
+ if ts.ts_args <> []
+ then
+ let args = List.map (fun arg -> arg.tv_name) ts.ts_args in
+ fprintf fmt "@[(par (%a) (%a))@]"
+ (print_list space (print_ident info))
+ args
+ (print_list space (print_constructor_decl info))
+ cl
+ else
+ fprintf fmt "@[(%a)@]" (print_list space (print_constructor_decl info)) cl
+
+let print_sort_decl info fmt (ts, _) =
+ fprintf fmt "@[(%a %d)@]" (print_ident info) ts.ts_name
+ (List.length ts.ts_args)
+
+let print_decl vc_loc vc_attrs printing_info info fmt d =
+ match d.d_node with
+ | Dtype ts -> print_type_decl info fmt ts
+ | Ddata [ (ts, _) ] when query_syntax info.info_syn ts.ts_name <> None -> ()
+ | Ddata dl -> (
+ match info.info_version with
+ | V20 ->
+ fprintf fmt "@[<v2>(declare-datatypes ()@ (%a))@]@\n@\n"
+ (print_list space (print_data_decl info))
+ dl
+ | V26 | V26Par ->
+ fprintf fmt "@[<v2>(declare-datatypes (%a)@ (%a))@]@\n@\n"
+ (print_list space (print_sort_decl info))
+ dl
+ (print_list space (print_data_def info))
+ dl)
+ | Dparam ls ->
+ collect_model_ls info ls;
+ print_param_decl info fmt ls
+ | Dlogic dl -> (
+ match info.info_version with
+ | V20 | V26 -> print_list nothing (print_logic_decl info) fmt dl
+ | V26Par -> (
+ match dl with
+ | [ ((s, _) as dl) ] when not (Sid.mem s.ls_name (get_decl_syms d)) ->
+ print_logic_decl info fmt dl
+ | dl -> print_rec_logic_decl info fmt dl))
+ | Dind _ -> unsupportedDecl d "smtv2: inductive definitions are not supported"
+ | Dprop (k, pr, f) ->
+ if Mid.mem pr.pr_name info.info_syn
+ then ()
+ else print_prop_decl vc_loc vc_attrs printing_info info fmt k pr f
+
+let set_produce_models fmt info =
+ if info.info_cntexample
+ then fprintf fmt "(set-option :produce-models true)@\n"
+
+let set_incremental fmt info =
+ if info.info_set_incremental
+ then fprintf fmt "(set-option :incremental true)@\n"
+
+let meta_counterexmp_need_push =
+ Theory.register_meta_excl "counterexample_need_smtlib_push"
+ [ Theory.MTstring ] ~desc:"Internal@ use@ only"
+
+let meta_incremental =
+ Theory.register_meta_excl "meta_incremental" [ Theory.MTstring ]
+ ~desc:"Internal@ use@ only"
+
+let meta_supports_reason_unknown =
+ Theory.register_meta_excl "supports_smt_get_info_unknown_reason"
+ [ Theory.MTstring ] ~desc:"Internal@ use@ only"
+
+let print_task version args ?old:_ fmt task =
+ let cntexample = Driver.get_counterexmp task in
+ let incremental =
+ let incr_meta = Task.find_meta_tds task meta_incremental in
+ not (Theory.Stdecl.is_empty incr_meta.Task.tds_set)
+ in
+ let incremental = Debug.test_flag debug_incremental || incremental in
+ let need_push =
+ let need_push_meta = Task.find_meta_tds task meta_counterexmp_need_push in
+ not (Theory.Stdecl.is_empty need_push_meta.Task.tds_set)
+ in
+ let supports_reason_unknown =
+ let m = Task.find_meta_tds task meta_supports_reason_unknown in
+ not (Theory.Stdecl.is_empty m.Task.tds_set)
+ in
+ let vc_loc = Intro_vc_vars_counterexmp.get_location_of_vc task in
+ let vc_attrs = (Task.task_goal_fmla task).t_attrs in
+ let vc_info = { vc_inside = false; vc_loc = None; vc_func_name = None } in
+ let info =
+ {
+ info_syn = Discriminate.get_syntax_map task;
+ info_rliteral = Printer.get_rliteral_map task;
+ info_model = S.empty;
+ info_in_goal = false;
+ info_vc_term = vc_info;
+ info_printer = ident_printer ();
+ list_projs = Mstr.empty;
+ list_field_def = Mstr.empty;
+ info_version = version;
+ meta_model_projection = Task.on_tagged_ls Theory.meta_projection task;
+ meta_record_def = Task.on_tagged_ls Theory.meta_record task;
+ list_records = Mstr.empty;
+ noarg_constructors = [];
+ info_cntexample_need_push = need_push;
+ info_cntexample = cntexample;
+ info_incremental = incremental;
+ info_labels = Mstr.empty;
+ (* info_set_incremental add the incremental option to the header. It is
+ not needed for some provers *)
+ info_set_incremental = (not need_push) && incremental;
+ info_supports_reason_unknown = supports_reason_unknown;
+ incr_list_axioms = [];
+ incr_list_ldecls = [];
+ }
+ in
+ print_prelude fmt args.prelude;
+ set_produce_models fmt info;
+ set_incremental fmt info;
+ print_th_prelude task fmt args.th_prelude;
+ let rec print_decls = function
+ | Some t -> (
+ print_decls t.Task.task_prev;
+ match t.Task.task_decl.Theory.td_node with
+ | Theory.Decl d -> (
+ try print_decl vc_loc vc_attrs args.printing_info info fmt d
+ with Unsupported s -> raise (UnsupportedDecl (d, s)))
+ | _ -> ())
+ | None -> ()
+ in
+ print_decls task;
+ pp_print_flush fmt ()
+
+let init () =
+ register_printer "smtv2_vnnlib" (print_task V20)
+ ~desc:"Printer@ for@ the@ SMTlib@ version@ 2@ format.";
+ register_printer "smtv2.6_vnnlib" (print_task V26)
+ ~desc:"Printer@ for@ the@ SMTlib@ version@ 2.6@ format."
diff --git a/src/printers/vnnlib.ml b/src/printers/vnnlib.ml
index 83af6d6..6329d4b 100644
--- a/src/printers/vnnlib.ml
+++ b/src/printers/vnnlib.ml
@@ -1,38 +1,27 @@
-(********************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2022 -- Inria - CNRS - Paris-Saclay University *)
-(* *)
-(* 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. *)
-(* *)
-(********************************************************************)
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(* Copyright (C) 2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* You can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
-(** SMT v2 printer with some extensions *)
-
-open Format
open Why3
-[@@@warning "-9"]
-
-open Pp
-open Wstdlib
-open Ident
-open Ty
-open Term
-open Decl
-open Printer
-open Cntexmp_printer
-
-let debug =
- Debug.register_info_flag "smtv2_printer"
- ~desc:"Print@ debugging@ messages@ about@ printing@ the@ input@ of@ smtv2."
-
-let debug_incremental =
- Debug.register_info_flag "force_incremental"
- ~desc:"Force@ incremental@ mode@ for@ smtv2@ provers"
-
(** SMTLIB tokens taken from CVC4: src/parser/smt2/{Smt2.g,smt2.cpp} *)
let ident_printer () =
let bls =
@@ -321,127 +310,23 @@ let ident_printer () =
"fmf.card.val";
]
in
- let san = sanitizer char_to_alpha char_to_alnumus in
- create_ident_printer bls ~sanitizer:san
-
-type version =
- | V20
- | V26
- | V26Par
+ let sanitizer = Ident.(sanitizer char_to_alpha char_to_alnumus) in
+ Ident.create_ident_printer bls ~sanitizer
+
+type relops = {
+ le : Term.lsymbol;
+ ge : Term.lsymbol;
+ lt : Term.lsymbol;
+ gt : Term.lsymbol;
+}
type info = {
- info_syn : syntax_map;
- info_rliteral : syntax_map;
- mutable info_model : S.t;
- mutable info_in_goal : bool;
- info_vc_term : vc_term_info;
- info_printer : ident_printer;
- mutable list_projs : Ident.ident Mstr.t;
- mutable list_field_def : Ident.ident Mstr.t;
- info_version : version;
- meta_model_projection : Sls.t;
- meta_record_def : Sls.t;
- mutable list_records : field_info list Mstr.t;
- (* For algebraic type counterexamples: constructors with no arguments can be
- misunderstood for variables *)
- mutable noarg_constructors : string list;
- info_cntexample_need_push : bool;
- info_cntexample : bool;
- info_incremental : bool;
- info_set_incremental : bool;
- info_supports_reason_unknown : bool;
- mutable info_labels : Sattr.t Mstr.t;
- mutable incr_list_axioms : (prsymbol * term) list;
- mutable incr_list_ldecls : (lsymbol * vsymbol list * term) list;
+ ls_rel_real : relops;
+ info_printer : Ident.ident_printer;
+ info_syn : Printer.syntax_map;
+ variables : string Term.Hls.t;
}
-let debug_print_term message t =
- let form = Debug.get_debug_formatter () in
- Debug.dprintf debug message;
- if Debug.test_flag debug then Pretty.print_term form t;
- Debug.dprintf debug "@."
-
-let print_ident info fmt id =
- pp_print_string fmt (id_unique info.info_printer id)
-
-(** type *)
-
-let print_tv info fmt tv =
- pp_print_string fmt (id_unique info.info_printer tv.tv_name)
-
-(** print `(par ...)` around the given body to print *)
-let print_par info
- (* body *)
- (* Format.kdprintf *) print_body fmt tvs =
- if Ty.Stv.is_empty tvs
- then print_body fmt
- else if info.info_version = V26Par
- then
- Format.fprintf fmt "(par (%a)@ %t)"
- (print_iter1 Ty.Stv.iter pp_print_space (print_tv info))
- tvs print_body
- else unsupported "smt: polymorphism must be encoded"
-(* body *)
-
-let rec print_type info fmt ty =
- match ty.ty_node with
- | Tyvar s -> (
- match info.info_version with
- | V20 -> unsupported "smtv2: you must encode type polymorphism"
- | V26 | V26Par -> print_tv info fmt s)
- | Tyapp (ts, l) -> (
- match (query_syntax info.info_syn ts.ts_name, l) with
- | Some s, _ -> syntax_arguments s (print_type info) fmt l
- | None, [] -> print_ident info fmt ts.ts_name
- | None, _ ->
- fprintf fmt "(%a %a)" (print_ident info) ts.ts_name
- (print_list space (print_type info))
- l)
-
-let print_type info fmt ty =
- try print_type info fmt ty
- with Unsupported s -> raise (UnsupportedType (ty, s))
-
-let print_type_value info fmt = function
- | None -> pp_print_string fmt "Bool"
- | Some ty -> print_type info fmt ty
-
-(** var *)
-let forget_var info v = forget_id info.info_printer v.vs_name
-
-let print_var info fmt { vs_name = id } =
- let n = id_unique info.info_printer id in
- pp_print_string fmt n
-
-let print_typed_var info fmt vs =
- fprintf fmt "(%a %a)" (print_var info) vs (print_type info) vs.vs_ty
-
-let print_var_list info fmt vsl = print_list space (print_var info) fmt vsl
-
-let print_typed_var_list info fmt vsl =
- print_list space (print_typed_var info) fmt vsl
-
-let collect_model_ls info ls =
- if Sls.mem ls info.meta_model_projection
- then
- info.list_projs <-
- Mstr.add
- (sprintf "%a" (print_ident info) ls.ls_name)
- ls.ls_name info.list_projs;
- if Sls.mem ls info.meta_record_def
- then
- info.list_field_def <-
- Mstr.add
- (sprintf "%a" (print_ident info) ls.ls_name)
- ls.ls_name info.list_field_def;
- if ls.ls_args = [] && relevant_for_counterexample ls.ls_name
- then
- let t = t_app ls [] ls.ls_value in
- info.info_model <-
- add_model_element
- (t_attr_set ?loc:ls.ls_name.id_loc ls.ls_name.id_attrs t)
- info.info_model
-
let number_format =
{
Number.long_int_support = `Default;
@@ -455,674 +340,143 @@ let number_format =
Number.hex_real_support = `Unsupported;
Number.frac_real_support =
`Custom
- ( (fun fmt i -> fprintf fmt "%s.0" i),
- fun fmt i n -> fprintf fmt "(/ %s.0 %s.0)" i n );
+ ( (fun fmt i -> Fmt.pf fmt "%s.0" i),
+ fun fmt i n -> Fmt.pf fmt "(/ %s.0 %s.0)" i n );
}
-let escape c =
- match c with
- | '\\' -> "\\x5C"
- | '\"' -> "\\x22"
- | '\032' .. '\126' -> Format.sprintf "%c" c
- | '\000' .. '\031' | '\127' .. '\255' ->
- Format.sprintf "\\x%02X" (Char.code c)
-
-(* can the type of a value be derived from the type of the arguments? *)
-let unambig_fs version fs =
- let rec lookup v ty =
- match ty.ty_node with
- | Tyvar u when tv_equal u v -> true
- | _ -> ty_any (lookup v) ty
- in
- let lookup v = List.exists (lookup v) fs.ls_args in
- let rec inspect ty =
- match ty.ty_node with
- | Tyvar u when not (lookup u) -> false
- | _ -> ty_all inspect ty
- in
- match version with
- | V20 | V26 -> true
- | V26Par -> inspect (Opt.get fs.ls_value)
-
-(** expr *)
-let rec print_term info fmt t =
- debug_print_term "Printing term: " t;
- if check_for_counterexample t
- then info.info_model <- add_model_element t info.info_model;
-
- check_enter_vc_term t info.info_in_goal info.info_vc_term;
-
- let () =
- match t.t_node with
- | Tconst c -> (
- let ts =
- match t.t_ty with
- | Some { ty_node = Tyapp (ts, []) } -> ts
- | _ -> assert false (* impossible *)
- in
- (* look for syntax literal ts in driver *)
- match (query_syntax info.info_rliteral ts.ts_name, c) with
- | Some st, Constant.ConstInt c -> syntax_range_literal st fmt c
- | Some st, Constant.ConstReal c ->
- let fp = match ts.ts_def with Float fp -> fp | _ -> assert false in
- syntax_float_literal st fp fmt c
- | _, Constant.ConstStr _ | None, _ ->
- Constant.print number_format escape fmt c
- (* TODO/FIXME: we must assert here that the type is either ty_int or
- ty_real, otherwise it makes no sense to print the literal. Do we ensure
- that preserved literal types are exactly those that have a dedicated
- syntax? *))
- | Tvar v -> print_var info fmt v
- | Tapp (ls, tl) -> (
- match query_syntax info.info_syn ls.ls_name with
- | Some s ->
- syntax_arguments_typed s (print_term info) (print_type info) t fmt tl
- | None -> (
- match tl with
- (* for cvc3 wich doesn't accept (toto ) *)
- | [] ->
- let str_ls = sprintf "%a" (print_ident info) ls.ls_name in
- let cur_var = info.info_labels in
- let new_var = update_info_labels str_ls cur_var t ls in
- let () = info.info_labels <- new_var in
- let vc_term_info = info.info_vc_term in
- (if vc_term_info.vc_inside
- then
- match vc_term_info.vc_loc with
- | None -> ()
- | Some loc ->
- let attrs =
- (* match vc_term_info.vc_func_name with | None -> *)
- ls.ls_name.id_attrs
- (* | Some _ -> model_trace_for_postcondition
- ~attrs:ls.ls_name.id_attrs info.info_vc_term *)
- in
- let _t_check_pos = t_attr_set ~loc attrs t in
- (* TODO: temporarily disable collecting variables inside the term
- triggering VC *)
- (*info.info_model <- add_model_element t_check_pos
- info.info_model;*)
- ());
- if unambig_fs info.info_version ls
- then fprintf fmt "@[%a@]" (print_ident info) ls.ls_name
- else
- fprintf fmt "@[(as %a %a)@]" (print_ident info) ls.ls_name
- (print_type info) (t_type t)
- | _ ->
- if unambig_fs info.info_version ls
- then
- fprintf fmt "@[<hv2>(%a@ %a)@]" (print_ident info) ls.ls_name
- (print_list space (print_term info))
- tl
- else
- fprintf fmt "@[<hv2>((as %a@ %a)@ %a)@]" (print_ident info)
- ls.ls_name (print_type info) (t_type t)
- (print_list space (print_term info))
- tl))
- | Tlet (t1, tb) ->
- let v, t2 = t_open_bound tb in
- fprintf fmt "@[<hv2>(let ((%a %a))@ %a)@]" (print_var info) v
- (print_term info) t1 (print_term info) t2;
- forget_var info v
- | Tif (f1, t1, t2) ->
- fprintf fmt "@[<hv2>(ite %a@ %a@ %a)@]" (print_fmla info) f1
- (print_term info) t1 (print_term info) t2
- | Tcase (t, bl) -> (
- let ty = t_type t in
- match ty.ty_node with
- | Tyapp (ts, _) when ts_equal ts ts_bool ->
- print_boolean_branches info t print_term fmt bl
- | _ -> (
- match t.t_node with
- | Tvar v -> print_branches info v print_term fmt bl
- | _ ->
- let subject = create_vsymbol (id_fresh "subject") (t_type t) in
- fprintf fmt "@[<hv2>(let ((%a @[%a@]))@ %a)@]" (print_var info)
- subject (print_term info) t
- (print_branches info subject print_term)
- bl;
- forget_var info subject))
- | Teps _ -> unsupportedTerm t "smtv2: you must eliminate epsilon"
- | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
- in
-
- check_exit_vc_term t info.info_in_goal info.info_vc_term
-
-and print_fmla info fmt f =
- debug_print_term "Printing formula: " f;
- if check_for_counterexample f
- then info.info_model <- add_model_element f info.info_model;
-
- check_enter_vc_term f info.info_in_goal info.info_vc_term;
-
- let () =
- match f.t_node with
- | Tapp ({ ls_name = id }, []) -> print_ident info fmt id
- | Tapp (ls, tl) -> (
- match query_syntax info.info_syn ls.ls_name with
- | Some s ->
- syntax_arguments_typed s (print_term info) (print_type info) f fmt tl
- | None -> (
- match tl with
- (* for cvc3 wich doesn't accept (toto ) *)
- | [] -> print_ident info fmt ls.ls_name
- | _ ->
- fprintf fmt "@[<hv2>(%a@ %a)@]" (print_ident info) ls.ls_name
- (print_list space (print_term info))
- tl))
- | Tquant (q, fq) ->
- let q = match q with Tforall -> "forall" | Texists -> "exists" in
- let vl, tl, f = t_open_quant fq in
- (* TODO trigger dépend des capacités du prover : 2 printers?
- smtwithtriggers/smtstrict *)
- if tl = []
- then
- fprintf fmt "@[<hv2>(%s @[<h>(%a)@]@ %a)@]" q
- (print_typed_var_list info)
- vl (print_fmla info) f
- else
- fprintf fmt "@[<hv2>(%s @[<h>(%a)@]@ (! %a %a))@]" q
- (print_typed_var_list info)
- vl (print_fmla info) f (print_triggers info) tl;
- List.iter (forget_var info) vl
- | Tbinop (Tand, f1, f2) ->
- fprintf fmt "@[<hv2>(and@ %a@ %a)@]" (print_fmla info) f1
- (print_fmla info) f2
- | Tbinop (Tor, f1, f2) ->
- fprintf fmt "@[<hv2>(or@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info)
- f2
- | Tbinop (Timplies, f1, f2) ->
- fprintf fmt "@[<hv2>(=>@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info)
- f2
- | Tbinop (Tiff, f1, f2) ->
- fprintf fmt "@[<hv2>(=@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info)
- f2
- | Tnot f -> fprintf fmt "@[<hv2>(not@ %a)@]" (print_fmla info) f
- | Ttrue -> pp_print_string fmt "true"
- | Tfalse -> pp_print_string fmt "false"
- | Tif (f1, f2, f3) ->
- fprintf fmt "@[<hv2>(ite %a@ %a@ %a)@]" (print_fmla info) f1
- (print_fmla info) f2 (print_fmla info) f3
- | Tlet (t1, tb) ->
- let v, f2 = t_open_bound tb in
- fprintf fmt "@[<hv2>(let ((%a %a))@ %a)@]" (print_var info) v
- (print_term info) t1 (print_fmla info) f2;
- forget_var info v
- | Tcase (t, bl) -> (
- let ty = t_type t in
- match ty.ty_node with
- | Tyapp (ts, _) when ts_equal ts ts_bool ->
- print_boolean_branches info t print_fmla fmt bl
- | _ -> (
- match t.t_node with
- | Tvar v -> print_branches info v print_fmla fmt bl
- | _ ->
- let subject = create_vsymbol (id_fresh "subject") (t_type t) in
- fprintf fmt "@[<hv2>(let ((%a @[%a@]))@ %a)@]" (print_var info)
- subject (print_term info) t
- (print_branches info subject print_fmla)
- bl;
- forget_var info subject))
- | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
- in
+let print_ident info fmt id =
+ Fmt.string fmt (Ident.id_unique info.info_printer id)
- check_exit_vc_term f info.info_in_goal info.info_vc_term
+let rec print_type info fmt ty =
+ match ty.Ty.ty_node with
+ | Tyvar _ -> Printer.unsupportedType ty "Unknown type variable"
+ | Tyapp (ts, tyl) -> (
+ match (Printer.query_syntax info.info_syn ts.ts_name, tyl) with
+ | Some s, _ -> Printer.syntax_arguments s (print_type info) fmt tyl
+ | None, [] -> print_ident info fmt ts.ts_name
+ | None, _ ->
+ Fmt.pf fmt "(%a %a)" (print_ident info) ts.ts_name
+ (Pp.print_list Pp.space (print_type info))
+ tyl)
-and print_boolean_branches info subject pr fmt bl =
- let error () =
- unsupportedTerm subject
- "smtv2: bad pattern-matching on Boolean (compile_match missing?)"
- in
- match bl with
- | [ br1; br2 ] -> (
- let p1, t1 = t_open_branch br1 in
- let _p2, t2 = t_open_branch br2 in
- match p1.pat_node with
- | Papp (cs, _) ->
- let csname = if ls_equal cs fs_bool_true then "true" else "false" in
- fprintf fmt "@[<hv2>(ite (= %a %s) %a %a)@]" (print_term info) subject
- csname (pr info) t1 (pr info) t2
- | _ -> error ())
- | _ -> error ()
+let print_type_value info fmt = function
+ | None -> Fmt.string fmt "Bool"
+ | Some ty -> print_type info fmt ty
-and print_branches info subject pr fmt bl =
- match bl with
- | [] -> assert false
- | br :: bl -> (
- let p, t = t_open_branch br in
- let error () =
- unsupportedPattern p "smtv2: you must compile nested pattern-matching"
+let rec print_term info fmt t =
+ match t.Term.t_node with
+ | Tconst c -> Constant.(print number_format unsupported_escape) fmt c
+ | Tbinop (Tand, t1, t2) ->
+ Fmt.pf fmt "@[<hv2>(and@ %a@ %a)@]" (print_term info) t1 (print_term info)
+ t2
+ | Tbinop (Tor, t1, t2) ->
+ Fmt.pf fmt "@[<hv2>(or@ %a@ %a)@]" (print_term info) t1 (print_term info) t2
+ | Tapp ({ ls_name = id; _ }, []) -> print_ident info fmt id
+ | Tapp (ls, tl) -> (
+ match Printer.query_syntax info.info_syn ls.ls_name with
+ | Some s -> Printer.syntax_arguments s (print_term info) fmt tl
+ | None -> Printer.unsupportedTerm t "Unknown logic symbol(s)")
+ | _ -> ()
+
+let print_axiom info fmt (pr, t) =
+ Fmt.pf fmt ";; %s@\n" pr.Decl.pr_name.id_string;
+ Fmt.pf fmt "@[(assert %a)@]@\n@\n" (print_term info) t
+
+let print_goal info fmt (pr, t) =
+ Fmt.pf fmt ";; Goal %s@\n" pr.Decl.pr_name.id_string;
+ Fmt.pf fmt "@[<hov 2>(assert@ %a)@]@\n" (print_term info) t
+
+let rec negate_term info t =
+ match t.Term.t_node with
+ | Tbinop (Tand, t1, t2) ->
+ Term.t_or (negate_term info t1) (negate_term info t2)
+ | Tbinop (Tor, t1, t2) ->
+ Term.t_and (negate_term info t1) (negate_term info t2)
+ | Tapp (ls, [ t1; t2 ]) ->
+ let tt = [ t1; t2 ] in
+ (* Negate real relational symbols. *)
+ let ls_neg =
+ if Term.ls_equal ls info.ls_rel_real.le
+ then info.ls_rel_real.gt
+ else if Term.ls_equal ls info.ls_rel_real.ge
+ then info.ls_rel_real.lt
+ else if Term.ls_equal ls info.ls_rel_real.lt
+ then info.ls_rel_real.ge
+ else if Term.ls_equal ls info.ls_rel_real.gt
+ then info.ls_rel_real.le
+ else ls
in
- match p.pat_node with
- | Pwild -> pr info fmt t
- | Papp (cs, args) ->
- let args =
- List.map (function { pat_node = Pvar v } -> v | _ -> error ()) args
- in
- if bl = []
- then print_branch info subject pr fmt (cs, args, t)
- else
- (match info.info_version with
- | V20 | V26 (* It should be the same than V26Par but it was different *)
- ->
- fprintf fmt "@[<hv2>(ite (is-%a %a) %a %a)@]"
- | V26Par -> fprintf fmt "@[<hv2>(ite ((_ is %a) %a) %a %a)@]")
- (print_ident info) cs.ls_name (print_var info) subject
- (print_branch info subject pr)
- (cs, args, t)
- (print_branches info subject pr)
- bl
- | _ -> error ())
-
-and print_branch info subject pr fmt (cs, vars, t) =
- if vars = []
- then pr info fmt t
- else
- let tvs = t_freevars Mvs.empty t in
- if List.for_all (fun v -> not (Mvs.mem v tvs)) vars
- then pr info fmt t
- else
- let i = ref 0 in
- let pr_proj fmt v =
- incr i;
- if Mvs.mem v tvs
- then
- fprintf fmt "(%a (%a_proj_%d %a))" (print_var info) v
- (print_ident info) cs.ls_name !i (print_var info) subject
- in
- fprintf fmt "@[<hv2>(let (%a) %a)@]" (print_list space pr_proj) vars
- (pr info) t
-
-and print_expr info fmt =
- TermTF.t_select (print_term info fmt) (print_fmla info fmt)
-
-and print_trigger info fmt e = print_expr info fmt e
-
-and print_triggers info fmt = function
- | [] -> ()
- | a :: l ->
- fprintf fmt ":pattern (%a) %a"
- (print_list space (print_trigger info))
- a (print_triggers info) l
-
-let print_type_decl info fmt ts =
- if is_alias_type_def ts.ts_def
- then ()
- else if Mid.mem ts.ts_name info.info_syn
- then ()
- else
- fprintf fmt "(declare-sort %a %i)@\n@\n" (print_ident info) ts.ts_name
- (List.length ts.ts_args)
+ if Term.ls_equal ls_neg ls
+ then Printer.unsupportedTerm t "Cannot negate such term"
+ else Term.ps_app ls_neg tt
+ | _ -> Printer.unsupportedTerm t "Cannot negate such term"
+
+let print_prop_decl info fmt prop_kind pr t =
+ match prop_kind with
+ | Decl.Plemma -> assert false
+ | Decl.Paxiom -> print_axiom info fmt (pr, t)
+ | Decl.Pgoal ->
+ let negated_term = negate_term info t in
+ print_goal info fmt (pr, negated_term)
let print_param_decl info fmt ls =
- if Mid.mem ls.ls_name info.info_syn
+ if Ident.Mid.mem ls.Term.ls_name info.info_syn
then ()
else
match ls.ls_args with
- (* only in SMTLIB 2.5 | [] -> fprintf fmt "@[<hov 2>(declare-const %a
- %a)@]@\n@\n" (print_ident info) ls.ls_name (print_type_value info)
- ls.ls_value *)
- | _ ->
- let tvs = Term.ls_ty_freevars ls in
- fprintf fmt ";; %s@\n@[<v2>(declare-fun %a %a)@]@\n@\n"
- ls.ls_name.id_string (print_ident info) ls.ls_name
- (print_par info (fun fmt ->
- Format.fprintf fmt "(%a) %a"
- (print_list space (print_type info))
- ls.ls_args (print_type_value info) ls.ls_value))
- tvs
-
-let rec has_quantification f =
- match f.t_node with
- | Tquant _ | Teps _ -> true
- | _ -> Term.t_any has_quantification f
-
-let print_logic_decl_aux flag info fmt (ls, def) =
- if not (Mid.mem ls.ls_name info.info_syn)
- then (
- collect_model_ls info ls;
- let vsl, expr = Decl.open_ls_defn def in
- if info.info_incremental && has_quantification expr
- then (
- fprintf fmt ";; %s@\n@[<hov2>(declare-fun %a (%a) %a)@]@\n@\n"
- ls.ls_name.id_string (print_ident info) ls.ls_name
- (print_list space (print_type info))
- (List.map (fun vs -> vs.vs_ty) vsl)
- (print_type_value info) ls.ls_value;
- info.incr_list_ldecls <- (ls, vsl, expr) :: info.incr_list_ldecls)
- else
- let tvs = Term.ls_ty_freevars ls in
- fprintf fmt ";; %s@\n@[<v2>(define-fun%s %a %a)@]@\n@\n"
- ls.ls_name.id_string flag (print_ident info) ls.ls_name
- (print_par info (fun fmt ->
- Format.fprintf fmt "@[<h>(%a) %a@]@ %a"
- (print_typed_var_list info)
- vsl (print_type_value info) ls.ls_value (print_expr info) expr))
- tvs;
- List.iter (forget_var info) vsl)
-
-let print_logic_decl = print_logic_decl_aux ""
-
-let print_rec_logic_decl info fmt = function
- | [] -> ()
- | [ ld ] -> print_logic_decl_aux "-rec" info fmt ld
- | l ->
- let l =
- List.map
- (fun (ls, def) ->
- let vsl, expr = Decl.open_ls_defn def in
- (ls, vsl, expr))
- l
- in
- let print_decl fmt (ls, vsl, _) =
- if Mid.mem ls.ls_name info.info_syn
- then ()
- else (
- collect_model_ls info ls;
- let tvs = Term.ls_ty_freevars ls in
- fprintf fmt "@[<hov 2>(%a %a)@]@\n@\n" (print_ident info) ls.ls_name
- (print_par info (fun fmt ->
- Format.fprintf fmt "(%a) %a"
- (print_typed_var_list info)
- vsl (print_type_value info) ls.ls_value))
- tvs)
- in
- let print_term fmt (ls, _, expr) =
- if Mid.mem ls.ls_name info.info_syn
- then ()
- else fprintf fmt "@[<hov 2>%a@]" (print_expr info) expr
- in
- fprintf fmt "@[<hov 2>(define-funs-rec (%a) (%a))@]@\n@\n"
- (print_list nothing print_decl)
- l
- (print_list nothing print_term)
- l;
- List.iter (fun (_, vsl, _) -> List.iter (forget_var info) vsl) l
-
-let print_info_model info =
- (* Prints the content of info.info_model *)
- let info_model = info.info_model in
- if (not (S.is_empty info_model)) && info.info_cntexample
- then (
- let model_map =
- S.fold
- (fun f acc ->
- let s = asprintf "%a" (print_fmla info) f in
- Mstr.add s f acc)
- info_model Mstr.empty
- in
-
- (* Printing model has modification of info.info_model as undesirable
- side-effect. Revert it back. *)
- info.info_model <- info_model;
- model_map)
- else Mstr.empty
-
-(* TODO factor out print_prop ? *)
-let print_prop info fmt (pr, f) =
- let tvs = Term.t_ty_freevars Ty.Stv.empty f in
- fprintf fmt ";; %s@\n@[<hov 2>(assert@ %a)@]@\n@\n"
- pr.pr_name.id_string (* FIXME? collisions *)
- (print_par info (fun fmt -> print_fmla info fmt f))
- tvs
-
-let add_check_sat info fmt =
- if info.info_cntexample && info.info_cntexample_need_push
- then fprintf fmt "@[(push)@]@\n";
- fprintf fmt "@[(check-sat)@]@\n";
- if info.info_supports_reason_unknown
- then fprintf fmt "@[(get-info :reason-unknown)@]@\n";
- if info.info_cntexample then fprintf fmt "@[(get-model)@]@\n@\n"
-
-let print_ldecl_axiom info fmt (ls, vls, t) =
- fprintf fmt ";; %s@\n" ls.ls_name.id_string;
- fprintf fmt
- "@[<hv2>(assert@ @[<hv2>(forall @[(%a)@]@ @[<hv2>(= @[<h>(%a %a)@]@ \
- %a)@])@])@]@\n\
- @\n"
- (print_typed_var_list info)
- vls (print_ident info) ls.ls_name (print_var_list info) vls
- (print_expr info) t
-
-(* TODO if the property doesnt begin with quantifier, then we print it first.
- Else, we print it afterwards. *)
-let print_incremental_axiom info fmt =
- List.iter (print_prop info fmt) info.incr_list_axioms;
- List.iter (print_ldecl_axiom info fmt) info.incr_list_ldecls;
- add_check_sat info fmt
-
-let print_prop_decl vc_loc vc_attrs printing_info info fmt k pr f =
- match k with
- | Paxiom ->
- if info.info_incremental && has_quantification f
- then info.incr_list_axioms <- (pr, f) :: info.incr_list_axioms
- else print_prop info fmt (pr, f)
- | Pgoal ->
- let tvs = Term.t_ty_freevars Ty.Stv.empty f in
- if not (Ty.Stv.is_empty tvs)
- then unsupported "smt: monomorphise goal must be applied";
- fprintf fmt ";; Goal %s@\n" pr.pr_name.id_string;
- (match pr.pr_name.id_loc with
- | None -> ()
- | Some loc -> fprintf fmt ";; %a@\n" Loc.gen_report_position loc);
- info.info_in_goal <- true;
- fprintf fmt "@[(assert@\n";
- fprintf fmt " @[(not@ %a))@]@\n@\n" (print_fmla info) f;
- info.info_in_goal <- false;
- add_check_sat info fmt;
-
- (* If in incremental mode, we empty the list of axioms we stored *)
- if info.info_incremental then print_incremental_axiom info fmt;
-
- let model_list = print_info_model info in
-
- printing_info :=
- Some
- {
- vc_term_loc = vc_loc;
- vc_term_attrs = vc_attrs;
- queried_terms = model_list;
- list_projections = info.list_projs;
- list_fields = info.list_field_def;
- Printer.list_records = info.list_records;
- noarg_constructors = info.noarg_constructors;
- set_str = info.info_labels;
- }
- | Plemma -> assert false
-
-let print_constructor_decl info fmt (ls, args) =
- let field_names =
- match args with
| [] ->
- fprintf fmt "(%a)" (print_ident info) ls.ls_name;
- let cons_name = sprintf "%a" (print_ident info) ls.ls_name in
- info.noarg_constructors <- cons_name :: info.noarg_constructors;
- []
- | _ ->
- fprintf fmt "@[(%a@ " (print_ident info) ls.ls_name;
- let field_names, _ =
- List.fold_left2
- (fun (acc, i) ty pr ->
- let field_name =
- match pr with
- | Some pr ->
- let field_name = sprintf "%a" (print_ident info) pr.ls_name in
- fprintf fmt "(%s" field_name;
- let field_trace =
- try
- let attr =
- Sattr.choose
- (Sattr.filter
- (fun l ->
- Strings.has_prefix "model_trace:" l.attr_string)
- pr.ls_name.id_attrs)
- in
- Strings.remove_prefix "model_trace:" attr.attr_string
- with Not_found -> ""
- in
- { field_name; field_trace; field_ident = Some pr.ls_name }
- | None ->
- let field_name =
- sprintf "%a_proj_%d" (print_ident info) ls.ls_name i
- in
- (* FIXME: is it possible to generate 2 same value with _proj_
- inside it ? Need sanitizing and uniquifying ? *)
- fprintf fmt "(%s" field_name;
- { field_name; field_trace = ""; field_ident = None }
- in
- fprintf fmt " %a)" (print_type info) ty;
- (field_name :: acc, succ i))
- ([], 1) ls.ls_args args
- in
- fprintf fmt ")@]";
- List.rev field_names
+ Fmt.pf fmt ";; %s@\n" ls.ls_name.id_string;
+ Fmt.pf fmt "@[(declare-const %a %a)@]@\n@\n" (print_ident info) ls.ls_name
+ (print_type_value info) ls.ls_value
+ | _ -> Printer.unsupported "Function declaration"
+
+let print_decl info fmt d =
+ match d.Decl.d_node with
+ | Dtype _ -> ()
+ | Ddata _ -> ()
+ | Dlogic _ -> ()
+ | Dind _ -> ()
+ | Dparam ls -> print_param_decl info fmt ls
+ | Dprop (k, pr, f) -> print_prop_decl info fmt k pr f
+
+let rec print_tdecl info fmt task =
+ match task with
+ | None -> ()
+ | Some { Task.task_prev; task_decl; _ } -> (
+ print_tdecl info fmt task_prev;
+ match task_decl.Theory.td_node with
+ | Use _ | Clone _ -> ()
+ | Meta (meta, l) when Theory.meta_equal meta Utils.meta_input -> (
+ match l with
+ | [ MAls ls; MAint i ] -> Term.Hls.add info.variables ls (Fmt.str "x%i" i)
+ | _ -> assert false)
+ | Meta (meta, l) when Theory.meta_equal meta Utils.meta_output -> (
+ match l with
+ | [ MAls ls; MAint i ] -> Term.Hls.add info.variables ls (Fmt.str "y%i" i)
+ | _ -> assert false)
+ | Meta _ -> ()
+ | Decl d -> print_decl info fmt d)
+
+let print_task args ?old:_ fmt task =
+ let ls_rel_real =
+ let th = Env.read_theory args.Printer.env [ "real" ] "Real" in
+ let le = Theory.ns_find_ls th.th_export [ Ident.op_infix "<=" ] in
+ let lt = Theory.ns_find_ls th.th_export [ Ident.op_infix "<" ] in
+ let ge = Theory.ns_find_ls th.th_export [ Ident.op_infix ">=" ] in
+ let gt = Theory.ns_find_ls th.th_export [ Ident.op_infix ">" ] in
+ { le; ge; lt; gt }
in
-
- if Strings.has_suffix "'mk" ls.ls_name.id_string
- then
- info.list_records <-
- Mstr.add
- (sprintf "%a" (print_ident info) ls.ls_name)
- field_names info.list_records
-
-let print_data_decl info fmt (ts, cl) =
- fprintf fmt "@[(%a@ %a)@]" (print_ident info) ts.ts_name
- (print_list space (print_constructor_decl info))
- cl
-
-let print_data_def info fmt (ts, cl) =
- if ts.ts_args <> []
- then
- let args = List.map (fun arg -> arg.tv_name) ts.ts_args in
- fprintf fmt "@[(par (%a) (%a))@]"
- (print_list space (print_ident info))
- args
- (print_list space (print_constructor_decl info))
- cl
- else
- fprintf fmt "@[(%a)@]" (print_list space (print_constructor_decl info)) cl
-
-let print_sort_decl info fmt (ts, _) =
- fprintf fmt "@[(%a %d)@]" (print_ident info) ts.ts_name
- (List.length ts.ts_args)
-
-let print_decl vc_loc vc_attrs printing_info info fmt d =
- match d.d_node with
- | Dtype ts -> print_type_decl info fmt ts
- | Ddata [ (ts, _) ] when query_syntax info.info_syn ts.ts_name <> None -> ()
- | Ddata dl -> (
- match info.info_version with
- | V20 ->
- fprintf fmt "@[<v2>(declare-datatypes ()@ (%a))@]@\n@\n"
- (print_list space (print_data_decl info))
- dl
- | V26 | V26Par ->
- fprintf fmt "@[<v2>(declare-datatypes (%a)@ (%a))@]@\n@\n"
- (print_list space (print_sort_decl info))
- dl
- (print_list space (print_data_def info))
- dl)
- | Dparam ls ->
- collect_model_ls info ls;
- print_param_decl info fmt ls
- | Dlogic dl -> (
- match info.info_version with
- | V20 | V26 -> print_list nothing (print_logic_decl info) fmt dl
- | V26Par -> (
- match dl with
- | [ ((s, _) as dl) ] when not (Sid.mem s.ls_name (get_decl_syms d)) ->
- print_logic_decl info fmt dl
- | dl -> print_rec_logic_decl info fmt dl))
- | Dind _ -> unsupportedDecl d "smtv2: inductive definitions are not supported"
- | Dprop (k, pr, f) ->
- if Mid.mem pr.pr_name info.info_syn
- then ()
- else print_prop_decl vc_loc vc_attrs printing_info info fmt k pr f
-
-let set_produce_models fmt info =
- if info.info_cntexample
- then fprintf fmt "(set-option :produce-models true)@\n"
-
-let set_incremental fmt info =
- if info.info_set_incremental
- then fprintf fmt "(set-option :incremental true)@\n"
-
-let meta_counterexmp_need_push =
- Theory.register_meta_excl "counterexample_need_smtlib_push"
- [ Theory.MTstring ] ~desc:"Internal@ use@ only"
-
-let meta_incremental =
- Theory.register_meta_excl "meta_incremental" [ Theory.MTstring ]
- ~desc:"Internal@ use@ only"
-
-let meta_supports_reason_unknown =
- Theory.register_meta_excl "supports_smt_get_info_unknown_reason"
- [ Theory.MTstring ] ~desc:"Internal@ use@ only"
-
-let print_task version args ?old:_ fmt task =
- let cntexample = Driver.get_counterexmp task in
- let incremental =
- let incr_meta = Task.find_meta_tds task meta_incremental in
- not (Theory.Stdecl.is_empty incr_meta.Task.tds_set)
- in
- let incremental = Debug.test_flag debug_incremental || incremental in
- let need_push =
- let need_push_meta = Task.find_meta_tds task meta_counterexmp_need_push in
- not (Theory.Stdecl.is_empty need_push_meta.Task.tds_set)
- in
- let supports_reason_unknown =
- let m = Task.find_meta_tds task meta_supports_reason_unknown in
- not (Theory.Stdecl.is_empty m.Task.tds_set)
- in
- let vc_loc = Intro_vc_vars_counterexmp.get_location_of_vc task in
- let vc_attrs = (Task.task_goal_fmla task).t_attrs in
- let vc_info = { vc_inside = false; vc_loc = None; vc_func_name = None } in
let info =
{
- info_syn = Discriminate.get_syntax_map task;
- info_rliteral = Printer.get_rliteral_map task;
- info_model = S.empty;
- info_in_goal = false;
- info_vc_term = vc_info;
+ ls_rel_real;
info_printer = ident_printer ();
- list_projs = Mstr.empty;
- list_field_def = Mstr.empty;
- info_version = version;
- meta_model_projection = Task.on_tagged_ls Theory.meta_projection task;
- meta_record_def = Task.on_tagged_ls Theory.meta_record task;
- list_records = Mstr.empty;
- noarg_constructors = [];
- info_cntexample_need_push = need_push;
- info_cntexample = cntexample;
- info_incremental = incremental;
- info_labels = Mstr.empty;
- (* info_set_incremental add the incremental option to the header. It is
- not needed for some provers *)
- info_set_incremental = (not need_push) && incremental;
- info_supports_reason_unknown = supports_reason_unknown;
- incr_list_axioms = [];
- incr_list_ldecls = [];
+ info_syn = Discriminate.get_syntax_map task;
+ variables = Term.Hls.create 10;
}
in
- print_prelude fmt args.prelude;
- set_produce_models fmt info;
- set_incremental fmt info;
- print_th_prelude task fmt args.th_prelude;
- let rec print_decls = function
- | Some t -> (
- print_decls t.Task.task_prev;
- match t.Task.task_decl.Theory.td_node with
- | Theory.Decl d -> (
- try print_decl vc_loc vc_attrs args.printing_info info fmt d
- with Unsupported s -> raise (UnsupportedDecl (d, s)))
- | _ -> ())
- | None -> ()
- in
- print_decls task;
- pp_print_flush fmt ()
+ Printer.print_prelude fmt args.Printer.prelude;
+ print_tdecl info fmt task
let init () =
- register_printer "smtv2_vnnlib" (print_task V20)
- ~desc:"Printer@ for@ the@ SMTlib@ version@ 2@ format.";
- register_printer "smtv2.6_vnnlib" (print_task V26)
- ~desc:"Printer@ for@ the@ SMTlib@ version@ 2.6@ format."
+ Printer.register_printer ~desc:"Printer@ for@ the@ VNN-LIB@ format." "vnnlib"
+ print_task
--
GitLab