Project

General

Profile

Revision f19eb2fd

View differences:

ex3.smt2
1 1
; COUNTER
2
(declare_var COUNTER.init Int)
3
(declare_var COUNTER.incr Int)
4
(declare_var COUNTER.X Bool)
5
(declare_var COUNTER.reset Bool)
6
(declare_var COUNTER.C Int)
7
(declare_var COUNTER.COUNTER.__COUNTER_1_c Int)
8
(declare_var COUNTER.COUNTER.__COUNTER_1_x Int)
9
(declare_var COUNTER.PC Int)
10
(declare-rel COUNTER_reset (Int Int Bool Bool Int Int))
2
(declare-var COUNTER.init Int)
3
(declare-var COUNTER.incr Int)
4
(declare-var COUNTER.X Bool)
5
(declare-var COUNTER.reset Bool)
6
(declare-var COUNTER.C Int)
7
(declare-var COUNTER.COUNTER.__COUNTER_1_c Int)
8
(declare-var COUNTER.COUNTER.__COUNTER_1_x Int)
9
(declare-var COUNTER.PC Int)
10
(declare-rel COUNTER_init (Int Int Bool Bool Int Int))
11 11
(declare-rel COUNTER_step (Int Int Bool Bool Int Int Int))
12 12

  
13 13
(rule (=> 
......
29 29
))
30 30

  
31 31
; speed
32
(declare_var speed.beacon Bool)
33
(declare_var speed.second Bool)
34
(declare_var speed.late Bool)
35
(declare_var speed.early Bool)
36
(declare_var speed.speed.__speed_3_c Bool)
37
(declare_var speed.speed.__speed_6_c Bool)
38
(declare_var speed.ni_4.COUNTER.__COUNTER_1_c Int)
39
(declare_var speed.speed.__speed_3_x Bool)
40
(declare_var speed.speed.__speed_6_x Bool)
41
(declare_var speed.ni_4.COUNTER.__COUNTER_1_x Int)
42
(declare_var speed.__speed_1 Bool)
43
(declare_var speed.__speed_2 Bool)
44
(declare_var speed.__speed_4 Bool)
45
(declare_var speed.__speed_5 Bool)
46
(declare_var speed.__speed_7 Bool)
47
(declare_var speed.__speed_8 Bool)
48
(declare_var speed.diff Int)
49
(declare_var speed.incr Int)
50
(declare-rel speed_reset (Bool Bool Bool Bool Bool Bool Int))
32
(declare-var speed.beacon Bool)
33
(declare-var speed.second Bool)
34
(declare-var speed.late Bool)
35
(declare-var speed.early Bool)
36
(declare-var speed.speed.__speed_3_c Bool)
37
(declare-var speed.speed.__speed_6_c Bool)
38
(declare-var speed.ni_4.COUNTER.__COUNTER_1_c Int)
39
(declare-var speed.speed.__speed_3_x Bool)
40
(declare-var speed.speed.__speed_6_x Bool)
41
(declare-var speed.ni_4.COUNTER.__COUNTER_1_x Int)
42
(declare-var speed.__speed_1 Bool)
43
(declare-var speed.__speed_2 Bool)
44
(declare-var speed.__speed_4 Bool)
45
(declare-var speed.__speed_5 Bool)
46
(declare-var speed.__speed_7 Bool)
47
(declare-var speed.__speed_8 Bool)
48
(declare-var speed.diff Int)
49
(declare-var speed.incr Int)
50
(declare-rel speed_init (Bool Bool Bool Bool Bool Bool Int))
51 51
(declare-rel speed_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Int))
52 52

  
53 53
(rule (=> 
......
89 89
))
90 90

  
91 91
; top
92
(declare_var top.beacon Bool)
93
(declare_var top.second Bool)
94
(declare_var top.OK Bool)
95
(declare_var top.top.__top_1_c Bool)
96
(declare_var top.ni_1.speed.__speed_3_c Bool)
97
(declare_var top.ni_1.speed.__speed_6_c Bool)
98
(declare_var top.ni_1.ni_4.COUNTER.__COUNTER_1_c Int)
99
(declare_var top.top.__top_1_x Bool)
100
(declare_var top.ni_1.speed.__speed_3_x Bool)
101
(declare_var top.ni_1.speed.__speed_6_x Bool)
102
(declare_var top.ni_1.ni_4.COUNTER.__COUNTER_1_x Int)
103
(declare_var top.early Bool)
104
(declare_var top.late Bool)
105
(declare-rel top_reset (Bool Bool Bool Bool Bool Bool Int))
92
(declare-var top.beacon Bool)
93
(declare-var top.second Bool)
94
(declare-var top.OK Bool)
95
(declare-var top.top.__top_1_c Bool)
96
(declare-var top.ni_1.speed.__speed_3_c Bool)
97
(declare-var top.ni_1.speed.__speed_6_c Bool)
98
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_c Int)
99
(declare-var top.top.__top_1_x Bool)
100
(declare-var top.ni_1.speed.__speed_3_x Bool)
101
(declare-var top.ni_1.speed.__speed_6_x Bool)
102
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_x Int)
103
(declare-var top.early Bool)
104
(declare-var top.late Bool)
105
(declare-rel top_init (Bool Bool Bool Bool Bool Bool Int))
106 106
(declare-rel top_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Bool Int))
107 107

  
108 108
(rule (=> 
src/horn_backend.ml
4 4
open Machine_code
5 5

  
6 6

  
7
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
7
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
8 8
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
9 9

  
10 10
let pp_type fmt t =
......
21 21
    
22 22

  
23 23
let pp_decl_var fmt id = 
24
  Format.fprintf fmt "(declare_var %s %a)"
24
  Format.fprintf fmt "(declare-var %s %a)"
25 25
    id.var_id
26 26
    pp_type id.var_type
27 27

  
......
186 186
     (Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs 
187 187
    )
188 188

  
189
let pp_machine_reset (m: machine_t) self fmt inst =
189
let pp_machine_init (m: machine_t) self fmt inst =
190 190
  let (node, static) = List.assoc inst m.minstances in
191 191
  fprintf fmt "(%a %a%t%s->%s)"
192
    pp_machine_reset_name (node_name node)
192
    pp_machine_init_name (node_name node)
193 193
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
194 194
    (Utils.pp_final_char_if_non_empty " " static)
195 195
    self inst
......
206 206
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
207 207
  match instr with 
208 208
  | MReset i ->
209
    pp_machine_reset m self fmt i
209
    pp_machine_init m self fmt i
210 210
  | MLocalAssign (i,v) ->
211 211
    pp_assign
212 212
      m self (pp_horn_var m) fmt
......
249 249
   Format.pp_print_newline fmt ();
250 250
   (* Declaring predicate *)
251 251
   Format.fprintf fmt "(declare-rel %a (%a))@."
252
     pp_machine_reset_name m.mname.node_id
252
     pp_machine_init_name m.mname.node_id
253 253
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m));
254 254
   
255 255
   Format.fprintf fmt "(declare-rel %a (%a))@."

Also available in: Unified diff