Hi all,

Attached a few updates to the SMTLIB printer. Disclaimer: I am actually 
allergic to OCAML so honestly I have no idea if I have made obvious mistakes. 
Especially for the datatype stuff.

It comes out all-right but its likely to do that by chance.

I'll follow up with some driver updates.

        Florian
commit 1aa2bd4081b485fbf68fdad99ecef8fb88133d89
Author: Florian Schanda <florian.scha...@altran.com>
Date:   Thu Aug 10 14:32:46 2017 +0100

    Update and re-organize reserved word list.

diff --git a/src/printer/smtv2.ml b/src/printer/smtv2.ml
index 44551e601..25e1e0f1a 100644
--- a/src/printer/smtv2.ml
+++ b/src/printer/smtv2.ml
@@ -24,33 +24,34 @@ let debug = Debug.register_info_flag "smtv2_printer"
   ~desc:"Print@ debugging@ messages@ about@ printing@ \
          the@ input@ of@ smtv2."
 
-(** SMTLIB tokens taken from CVC4: src/parser/smt2/Smt2.g *)
+(** SMTLIB tokens taken from CVC4: src/parser/smt2/{Smt2.g,smt2.cpp} *)
 let ident_printer () =
-  let bls = (*["and";" benchmark";" distinct";"exists";"false";"flet";"forall";
-     "if then else";"iff";"implies";"ite";"let";"logic";"not";"or";
-     "sat";"theory";"true";"unknown";"unsat";"xor";
-     "assumption";"axioms";"definition";"extensions";"formula";
-     "funs";"extrafuns";"extrasorts";"extrapreds";"language";
-     "notes";"preds";"sorts";"status";"theory";"Int";"Real";"Bool";
-     "Array";"U";"select";"store"]*)
-    (* smtlib2 V2 p71 *)
-    [(* Base SMT-LIB tokens *)
-      "assert"; "check-sat"; "declare-fun"; "declare-sort"; "define-fun";
-      "define-sort"; "get-value"; "get-assignment"; "get-assertions";
-      "get-proof"; "get-unsat-core"; "exit"; "ite"; "let"; "!"; "_";
-      "set-logic"; "set-info"; "get-info"; "set-option"; "get-option";
-      "push"; "pop"; "as";
-
-      (* extended commands *)
-      "declare-datatypes"; "get-model"; "echo"; "assert-rewrite";
+  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"; "declare-const";
+      "declare-funs"; "declare-preds"; "define";
       "simplify";
 
-      (* attributes *)
-
-      (* operators, including theory symbols *)
-      "and"; "distinct"; "exists"; "forall"; "is_int"; "not"; "or"; "select";
+     (* operators, including theory symbols *)
+      "ite";
+      "and"; "distinct"; "is_int"; "not"; "or"; "select";
       "store"; "to_int"; "to_real"; "xor";
 
       "div"; "mod";
@@ -59,23 +60,54 @@ let ident_printer () =
       "bvurem"; "bvshl"; "bvlshr"; "bvult"; "bvnand"; "bvnor"; "bvxor";
       "bvcomp"; "bvsub"; "bvsdiv"; "bvsrem"; "bvsmod"; "bvashr"; "bvule";
       "bvugt"; "bvuge"; "bvslt"; "bvsle"; "bvsgt"; "bvsge"; "rotate_left";
-      "rotate_right";
-
-      "cos"; "sin"; "tan"; "atan"; "pi";
-
-      (* Other stuff that Why3 seems to need *)
-      "DECIMAL"; "NUMERAL"; "par"; "STRING";
-      "unsat";"sat";
-      "Bool"; "true"; "false";
-      "Array";"const";
+      "rotate_right"; "bvredor"; "bvredand";
+
+      "sin"; "cos"; "tan"; "asin"; "acos"; "atan"; "pi";
+
+     (* 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.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"; "re.++"; "re.union"; "re.inter";
+      "re.*"; "re.+"; "re.opt"; "re.range"; "re.loop";
+
+     (* the new proposed set theory *)
+      "union"; "intersection"; "setminus"; "subset"; "member";
+      "singleton"; "insert";
+
+     (* 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"; "subset"; "union"; "default";
-
-(* floats *)
-      "RNE"; "RNA"; "RTP"; "RTN"; "RTZ"
+     (* From Z3 *)
+      "map"; "bv"; "default";
+      "difference";
       ]
   in
   let san = sanitizer char_to_alpha char_to_alnumus in
commit d8b1130163e4f0226560c6aaa91933b9cf8436be
Author: Florian Schanda <florian.scha...@altran.com>
Date:   Thu Aug 10 14:34:51 2017 +0100

    SMTLIB 2.6 support
    
    Emit new-style datatypes.

diff --git a/src/printer/smtv2.ml b/src/printer/smtv2.ml
index 60bb525d4..e0c5771cc 100644
--- a/src/printer/smtv2.ml
+++ b/src/printer/smtv2.ml
@@ -527,9 +527,13 @@ let print_constructor_decl info fmt (ls,args) =
      in
      fprintf fmt ")@]"
 
-let print_data_decl info fmt (ts,cl) =
-  fprintf fmt "@[(%a@ %a)@]"
+let print_data_names info fmt (ts,cl) =
+  fprintf fmt "(%a %i)"
     (print_ident info) ts.ts_name
+    (List.length ts.ts_args)
+
+let print_data_decl info fmt (ts,cl) =
+  fprintf fmt "(%a)"
     (print_list space (print_constructor_decl info)) cl
 
 let print_decl vc_loc cntexample args info fmt d =
@@ -538,7 +542,8 @@ let print_decl vc_loc cntexample args info fmt d =
       print_type_decl info fmt ts
   | Ddata [(ts,_)] when query_syntax info.info_syn ts.ts_name <> None -> ()
   | Ddata dl ->
-      fprintf fmt "@[(declare-datatypes ()@ (%a))@]@\n"
+      fprintf fmt "@[(declare-datatypes (%a)@ (%a))@]@\n"
+        (print_list space (print_data_names info)) dl
         (print_list space (print_data_decl info)) dl
   | Dparam ls ->
       collect_model_ls info ls;
commit aa356991b8e67c75b6a023cef7b9591d312530ec
Author: Florian Schanda <florian.scha...@altran.com>
Date:   Thu Aug 10 14:33:20 2017 +0100

    SMTLIB 2.6 support
    
    Use declare-const instead of declare-fun, if applicable.

diff --git a/src/printer/smtv2.ml b/src/printer/smtv2.ml
index 25e1e0f1a..60bb525d4 100644
--- a/src/printer/smtv2.ml
+++ b/src/printer/smtv2.ml
@@ -440,10 +440,15 @@ let print_type_decl info fmt ts =
 
 let print_param_decl info fmt ls =
   if Mid.mem ls.ls_name info.info_syn then () else
-  fprintf fmt "@[<hov 2>(declare-fun %a (%a) %a)@]@\n@\n"
-    (print_ident info) ls.ls_name
-    (print_list space (print_type info)) ls.ls_args
-    (print_type_value info) ls.ls_value
+    if (List.length ls.ls_args) > 0 then
+      fprintf fmt "@[<hov 2>(declare-fun %a (%a) %a)@]@\n@\n"
+        (print_ident info) ls.ls_name
+        (print_list space (print_type info)) ls.ls_args
+        (print_type_value info) ls.ls_value
+    else
+      fprintf fmt "@[<hov 2>(declare-const %a %a)@]@\n@\n"
+        (print_ident info) ls.ls_name
+        (print_type_value info) ls.ls_value
 
 let print_logic_decl info fmt (ls,def) =
   if Mid.mem ls.ls_name info.info_syn then () else begin
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Reply via email to