Up  

Module Aiger

module Aiger: sig .. end
An OCaml library for AIGER files
type lit
type for literals
type var
type for variables
val aiger_false : lit
val aiger_true : lit
val sign : lit -> bool
val strip : lit -> lit
val aiger_not : lit -> lit
val var2lit : var -> lit
val var2int : var -> int
val lit2var : lit -> var
val lit2int : lit -> int
val int2lit : int -> lit
val int2var : int -> var
module Symbol: sig .. end
module SymbolMap: Map.S  with type key = Symbol.t
module LitMap: Map.S  with type key = lit
type t = {
   maxvar : int;
   num_inputs : int;
   num_latches : int;
   num_outputs : int;
   num_ands : int;
   inputs : lit list;
   latches : (lit * lit) list;
   outputs : lit list;
   ands : (lit * lit * lit) list;
   comments : string list;
   symbols : lit SymbolMap.t;
   abstract : Symbol.t LitMap.t;
} 
val read : Pervasives.in_channel -> t
val read_from_file : string -> t
val write : t -> Pervasives.out_channel -> unit
val write_to_file : t -> string -> unit
val empty : t
val new_var : t -> t * var
val add_input : t -> lit -> Symbol.t -> t
add_latch aiger lit next name
val add_latch : t -> lit -> lit -> Symbol.t -> t
val add_output : t -> lit -> Symbol.t -> t
add_and aiger lhs rhs0 rhs1
val add_and : t -> lit -> lit -> lit -> t
val add_comment : t -> string -> t
val hide : t -> Symbol.t -> t
remove an output
val nth_input : t -> int -> lit
val nth_output : t -> int -> lit
val nth_latch : t -> int -> lit * lit
val lit2string : t -> lit -> string
These function may raise Not_found
val lit2symbol : t -> lit -> Symbol.t
val symbol2lit : t -> Symbol.t -> lit
val name_to_literals : t -> string -> lit array
Give an array containing all the literals encoding the given name. For example, for an integer "i" encoded on two bits, name_to_literals a "i" will return the literals corresponding to "i<0>" and "i<1>".
val size_symbol : t -> string -> int
Gives the number of literal encoding the variable with the given name.
val names : t -> string list
List of names used as symbols.
val inputs : t -> string list
val outputs : t -> string list
val latches : t -> string list
type tag =
| Constant of bool
| Input of lit
| Latch of (lit * lit)
| And of (lit * lit * lit) 
val lit2tag : t -> lit -> tag
val compose : t -> t -> t
Merge 2 aiger files where symbols with the same name are merged. They are identified by their name in the comments.