Commit 1ea2eba1 authored by Florian Schanda's avatar Florian Schanda Committed by Guillaume Melquiond
Browse files

Update and re-organize reserved word list.

parent c8b94e09
......@@ -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
......
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