Revision efc2cd2f
Added by Pierre-Loïc Garoche almost 5 years ago
| src/tools/zustre/zustre_common.ml | ||
|---|---|---|
| 194 | 194 |
|
| 195 | 195 |
(* Used to print boolean constants *) |
| 196 | 196 |
let horn_tag_to_expr t = |
| 197 |
if t = Corelang.tag_true then
|
|
| 197 |
if t = tag_true then |
|
| 198 | 198 |
Z3.Boolean.mk_true !ctx |
| 199 |
else if t = Corelang.tag_false then
|
|
| 199 |
else if t = tag_false then |
|
| 200 | 200 |
Z3.Boolean.mk_false !ctx |
| 201 | 201 |
else |
| 202 | 202 |
(* Finding the associated sort *) |
| ... | ... | |
| 215 | 215 |
let rec horn_const_to_expr c = |
| 216 | 216 |
match c with |
| 217 | 217 |
| Const_int i -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i |
| 218 |
| Const_real (_,_,s) -> Z3.Arithmetic.Real.mk_numeral_s !ctx s
|
|
| 218 |
| Const_real r -> Z3.Arithmetic.Real.mk_numeral_s !ctx (Real.to_string r)
|
|
| 219 | 219 |
| Const_tag t -> horn_tag_to_expr t |
| 220 | 220 |
| _ -> assert false |
| 221 | 221 |
|
| ... | ... | |
| 350 | 350 |
(val_to_expr v1) |
| 351 | 351 |
(val_to_expr v2) |
| 352 | 352 |
|
| 353 |
| "int_to_real", [v1] -> |
|
| 354 |
Z3.Arithmetic.Integer.mk_int2real |
|
| 355 |
!ctx |
|
| 356 |
(val_to_expr v1) |
|
| 353 | 357 |
|
| 354 | 358 |
|
| 355 | 359 |
(* | _, [v1; v2] -> Z3.Boolean.mk_and |
Also available in: Unified diff
[seal] more progress on seal extract