Project

General

Profile

« Previous | Next » 

Revision 3e209698

Added by Pierre-Loïc Garoche almost 9 years ago

First fully working version of horn backend.

Has to be called with "-horn -node main_node"

The test script compute the smt2 file and calls z3 on them.

View differences:

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

Also available in: Unified diff