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/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)

Also available in: Unified diff