Project

General

Profile

Revision cd6efd9b

View differences:

ex3.smt2
121 121
  (top_step top.beacon top.second top.OK top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
122 122
))
123 123

  
124
; Collecting semantics with main node top
124
; Collecting semantics for node top
125 125

  
126 126
(declare-rel MAIN (Bool Bool Bool Int Bool))
127 127
; Initial set
......
135 135
))
136 136

  
137 137
; Inductive def
138
(declare-var dummy Bool)
139 138
(rule (=> 
140
  (and (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c dummy)
139
  (and (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.OK)
141 140
       (top_step top.beacon top.second top.OK top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
142 141
  )
143 142
  (MAIN top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x top.OK)
......
147 146
(declare-rel ERR ())
148 147
(rule (=> 
149 148
  (and (not (= top.OK true))
150
       (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c))
149
       (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.OK))
151 150
  ERR))
152 151
(query ERR)
src/horn_backend.ml
11 11
  match (Types.repr t).Types.tdesc with
12 12
  | Types.Tbool           -> Format.fprintf fmt "Bool"
13 13
  | Types.Tint            -> Format.fprintf fmt "Int"
14
  | Types.Treal           -> Format.fprintf fmt "Real"
14 15
  | Types.Tclock _
15 16
  | Types.Tarray _
16 17
  | Types.Tstatic _
......
314 315
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
315 316

  
316 317
    Format.fprintf fmt "; Inductive def@.";
317
    Format.fprintf fmt "(declare-var dummy Bool)@.";
318 318
    Format.fprintf fmt 
319
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a dummy)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a)@]@.))@.@."
319
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a)@]@.))@.@."
320 320
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
321 321
      node
322 322
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
src/main_lustre_compiler.ml
255 255
      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
256 256
    end
257 257
    | "horn" -> begin
258
      let fmt = Format.std_formatter in
258
      let source_file = basename ^ ".smt2" in (* Could be changed *)
259
      let source_out = open_out source_file in
260
      let fmt = formatter_of_out_channel source_out in
259 261
      Horn_backend.translate fmt basename normalized_prog machine_code
260 262
    end
261 263
    | _ -> assert false
test/test-compile.sh
11 11
#   echo main:$main
12 12
#   echo opts:$opts
13 13
    if [ "$main" != "" ]; then
14
	$LUSTREC -d build -verbose 0 $opts -node $main ../$file;
14
	$LUSTREC -horn -d build -verbose 0 $opts -node $main ../$file;
15 15
    else
16
	$LUSTREC -d build -verbose 0 $opts ../$file
16
	$LUSTREC -horn -d build -verbose 0 $opts ../$file 
17 17
    fi
18 18
    if [ $? -ne 0 ]; then 
19 19
      rlustrec="INVALID"; 
20 20
    else 
21 21
      rlustrec="VALID" 
22 22
    fi
23
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null
23
    echo z3 `basename $file .lus`.smt2 | grep unsat 
24
    z3 `basename $file .lus`.smt2 | grep unsat > /dev/null
24 25
    if [ $? -ne 0 ]; then
25
      rgcc="INVALID";
26
      rz3="INVALID";
26 27
    else
27
      rgcc="VALID"
28
      rz3="VALID"
28 29
    fi    
29
    echo "lustrec ($rlustrec),gcc ($rgcc),diff with ref ($rdiff),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep INVALID
30
    echo "lustrec -horn ($rlustrec),z3 ($rz3),diff with ref ($rdiff),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep INVALID
30 31
# awk 'BEGIN { FS = "\" " } ; { printf "%-20s %-40s\n", $1, $2, $3}' 
31 32
done < ../tests_ok.list
test/tests_ok.list
894 894
./src/kind_fmcad08/protocol/swimmingpool_2.lus,top
895 895
./src/kind_fmcad08/protocol/rtp_1.lus,top
896 896
./src/kind_fmcad08/protocol/swimmingpool_7.lus,top
897
./src/arrays_arnaud/arrays.lus,,-check-access
898
./src/arrays_arnaud/RelOpMatrix.lus
899
./src/arrays_arnaud/access1.lus,,-check-access
900
./src/arrays_arnaud/generic1.lus
901
./src/arrays_arnaud/generic2.lus
902
./src/arrays_arnaud/generic3.lus,top,-dynamic -check-access
903
./src/clocks/clocks1.lus
904
./src/clocks/clocks2.lus
905
./src/clocks/oversampling0.lus

Also available in: Unified diff