Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by Lélio Brun over 1 year ago

reformatting

View differences:

src/tools/zustre/zustre_data.ml
1 1 
let ctx = ref (Z3.mk_context [])
2 

  		




  2
  3
  
    
let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx)


  		




  3
  4
  
    

  		




  
  5
  
    
let const_sorts : (Lustre_types.ident, Z3.Sort.sort) Hashtbl.t =


  		




  
  6
  
    
  Hashtbl.create 13


  		




  4
  7
  
    

  		




  5
  
  
    
let const_sorts : (Lustre_types.ident, Z3.Sort.sort) Hashtbl.t = Hashtbl.create 13


  		




  6
  
  
    
let const_tags : (Lustre_types.ident, Z3.Sort.sort) Hashtbl.t = Hashtbl.create 13


  		




  7
  
  
    
let sort_elems : (Z3.Sort.sort, Lustre_types.ident list) Hashtbl.t = Hashtbl.create 13


  		




  
  8
  
    
let const_tags : (Lustre_types.ident, Z3.Sort.sort) Hashtbl.t =


  		




  
  9
  
    
  Hashtbl.create 13


  		




  8
  10
  
    

  		




  
  11
  
    
let sort_elems : (Z3.Sort.sort, Lustre_types.ident list) Hashtbl.t =


  		




  
  12
  
    
  Hashtbl.create 13


  		




  9
  13
  
    

  		




  10
  
  
    
let decls: (Lustre_types.ident, Z3.FuncDecl.func_decl) Hashtbl.t = Hashtbl.create 13


  		




  
  14
  
    
let decls : (Lustre_types.ident, Z3.FuncDecl.func_decl) Hashtbl.t =


  		




  
  15
  
    
  Hashtbl.create 13


  		




  11
  16
  
    

  		




  12
  17
  
    
let debug = ref false


  		




  13
  
  
    
let timeout = ref 10000 (* default : 10 s = 10 000 ms *)


  		




  
  18
  
    

  		




  
  19
  
    
let timeout = ref 10000


  		




  
  20
  
    
(* default : 10 s = 10 000 ms *)


  		




  14
  21
  
    

  		




  15
  22
  
    
(* Local Variables: *)


  		




  16
  23
  
    
(* compile-command:"make -C ../.." *)


  		












Also available in:  Unified diff