Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
460f6bc0
Commit
460f6bc0
authored
Jun 03, 2013
by
François Bobot
Browse files
[SMTV2] add builtin functions from SMT-LIB theories
parent
56cfe3b2
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/printer/smtv2.ml
View file @
460f6bc0
...
...
@@ -38,15 +38,20 @@ let ident_printer =
"get-option"
;
"get-proof"
;
"get-unsat-core"
;
"get-value"
;
"pop"
;
"push"
;
"set-logic"
;
"set-info"
;
"set-option"
;
(** for security *)
"Bool"
;
"unsat"
;
"sat"
;
"true"
;
"false"
;
"select"
;
"store"
;
"unsat"
;
"sat"
;
(** SMT-LIB Theories http://www.smt-lib.org/ *)
(** SmtV2 core *)
"Bool"
;
"true"
;
"false"
;
"not"
;
"and"
;
"or"
;
"xor"
;
"distinct"
;
"ite"
;
(** arrays -- this really belongs to the driver! (esp. const) *)
"Array"
;
"select"
;
"store"
;
"const"
;
(** div and mod are builtin *)
"div"
;
"mod"
;
(** distinct is builtin in some provers *)
"distinct"
;
(** CVC4 built-in symbols *)
"concat"
;
(** Ints theory *)
"div"
;
"mod"
;
"abs"
;
(** Fixed_Size_BitVectors theory *)
"BitVec"
;
"concat"
;
"extract"
;
"bv2nat"
;
"nat2bv"
;
"bvnot"
;
"bvneg"
;
"bvand"
;
"bvor"
;
"bvand"
;
"bvmul"
;
"bvudiv"
;
"bvurem"
;
"bvshl"
;
"bvlshr"
;
"bvult"
;
(** SMTv2's Reals_Ints theory *)
"to_int"
;
"to_real"
;
"is_int"
]
in
let
san
=
sanitizer
char_to_alpha
char_to_alnumus
in
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment