CristalCaveGem » LustreC

let translate fmt basename prog machines =

  List.iter (print_machine machines fmt) (List.rev machines);

  main_print machines fmt

    let traces : (ident * expr) list=

      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in

      let filtered =

      in

      let content = List.map snd filtered in

      (* Elements are supposed to be a pair (tuple): variable, expression *)

      List.map (fun (p, v) ->

	let machine = match p with | [] -> m | (_,m')::_ -> m' in

	let traces = List.assoc machine machines_traces in

	  (* We take the expression associated to variable v in the trace info *)

	  p, List.assoc v.var_id traces

	  (* We keep the variable as is: we create an expression v *)

	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)

      ) (compute_mems m)

    in

    let memories_next = (* We remove the topest pre in each expression *)

      List.map

	memories_old

    in

(* Local Variables: *)

(* End: *)

	(Clocks.clock_list_of_clock expr.expr_clock) in

    let new_def =

      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)

(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)

   and [opt] is true *)

	with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in

      let expr = substitute_expr diff_vars defs eq.eq_rhs in

      let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in

    annot_loc = Location.dummy_loc

  }

    popd > /dev/null

	# Cheching witness

    pushd $build > /dev/null

    popd > /dev/null

    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"

    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then

    # Checking horn backend

    if [ "$main" != "" ]; then

    else

    fi

    if [ $? -ne 0 ]; then

        rlustrec="INVALID";