Project

General

Profile

« Previous | Next » 

Revision 3d1f9d9f

Added by LĂ©lio Brun over 2 years ago

more agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)

View differences:

src/spec_common.mli
2 2
open Lustre_types
3 3
open Spec_types
4 4

  
5
val type_of_l_value : 'a expression_t -> Types.t
5
val type_of_value : Machine_code_types.value_t expression_t -> Types.t
6 6

  
7 7
val mk_conditional_tr : 'a -> 'a formula_t -> 'a formula_t -> 'a formula_t
8 8

  

Also available in: Unified diff