[printer] Add a new printer for VNN-LIB format.

The printer for the SMT-LIB format produces not useful stuff.

config/drivers/discrimination.gen

@@ -4,4 +4,3 @@ theory BuiltIn
   meta "select_lsinst_default" "local"
   meta "select_kept_default" "all"
 end
-

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

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 ->