Biddy  1.7.3
An academic Binary Decision Diagrams package
biddyInOut.c File Reference

File biddyInOut.c contains various parsers and generators. More...

#include "biddyInt.h"

Go to the source code of this file.

Functions

Biddy_String Biddy_Managed_Eval0 (Biddy_Manager MNG, Biddy_String s)
 Function Biddy_Managed_Eval0 evaluates raw format. More...
 
Biddy_Edge Biddy_Managed_Eval1x (Biddy_Manager MNG, Biddy_String s, Biddy_LookupFunction lf)
 Function Biddy_Managed_Eval1x evaluates prefix AND-OR-EXOR-NOT format. More...
 
Biddy_Edge Biddy_Managed_Eval2 (Biddy_Manager MNG, Biddy_String boolFunc)
 Function Biddy_Managed_Eval2 evaluates infix &|^~>< format. More...
 
void Biddy_Managed_ReadVerilogFile (Biddy_Manager MNG, const char filename[], Biddy_String prefix)
 Function Biddy_Managed_ReadVerilogFile reads Verilog file and creates variables for all primary inputs and Boolean functions for all primary outputs. More...
 
void Biddy_Managed_PrintfBDD (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_PrintfBDD writes raw format using printf. More...
 
void Biddy_Managed_WriteBDD (Biddy_Manager MNG, const char filename[], Biddy_Edge f, Biddy_String label)
 Function Biddy_Managed_WriteBDD writes raw format using fprintf. More...
 
void Biddy_Managed_PrintfTable (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_PrintfTable writes truth table using printf. More...
 
void Biddy_Managed_WriteTable (Biddy_Manager MNG, const char filename[], Biddy_Edge f)
 Function Biddy_Managed_WriteTable writes truth table using fprintf. More...
 
void Biddy_Managed_PrintfSOP (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_PrintfSOP writes SOP using printf. More...
 
void Biddy_Managed_WriteSOP (Biddy_Manager MNG, const char filename[], Biddy_Edge f)
 Function Biddy_Managed_WriteSOP writes SOP using fprintf. More...
 
unsigned int Biddy_Managed_WriteDot (Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], int id, Biddy_Boolean cudd)
 Function Biddy_Managed_WriteDot writes dot/graphviz format using fprintf. More...
 
unsigned int Biddy_Managed_WriteBddview (Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], Biddy_XY *table)
 Function Biddy_Managed_WriteBDDView writes bddview format using fprintf. More...
 

Detailed Description

File biddyInOut.c contains various parsers and generators.

Description

PackageName [Biddy]
Synopsis    [Biddy provides data structures and algorithms for the
             representation and manipulation of Boolean functions with
             ROBDDs, 0-sup-BDDs, and TZBDDs. A hash table is used for quick
             search of nodes. Complement edges decreases the number of
             nodes. An automatic garbage collection with a system age is
             implemented. Variable swapping and sifting are implemented.]

FileName    [biddyInOut.c]
Revision    [$Revision: 320 $]
Date        [$Date: 2017-10-01 12:02:23 +0200 (ned, 01 okt 2017) $]
Authors     [Robert Meolic (robert.meolic@um.si),
             Ales Casar (ales@homemade.net),
             Jan Kraner (jankristian.kraner@student.um.si),
             Ziga Kobale (ziga.kobale@student.um.si),
             Volodymyr Mihav (mihaw.wolodymyr@gmail.com),
             David Kebo Houngninou (dhoungninou@smu.edu)]

Copyright

Copyright (C) 2006, 2017 UM FERI, Koroska cesta 46, SI-2000 Maribor, Slovenia

Biddy is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

Biddy is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.

More info

See also: biddy.h, biddyInt.h

Definition in file biddyInOut.c.

Function Documentation

Biddy_String Biddy_Managed_Eval0 ( Biddy_Manager  MNG,
Biddy_String  s 
)

Function Biddy_Managed_Eval0 evaluates raw format.

Description

First word is a name. It is followed by raw format. Function return name of the formula.

Side effects

All variables should already exists in the correct ordering! Not reentrant.

More info

Macro Biddy_Eval0(s) is defined for use with anonymous manager.

Definition at line 241 of file biddyInOut.c.

Biddy_Edge Biddy_Managed_Eval1x ( Biddy_Manager  MNG,
Biddy_String  s,
Biddy_LookupFunction  lf 
)

Function Biddy_Managed_Eval1x evaluates prefix AND-OR-EXOR-NOT format.

Description

Parameter lf is a lookup function in the user-defined cache table.

Side effects

Not reentrant.

More info

Macro Biddy_Eval1x(s,lf) is defined for use with anonymous manager. Macros Biddy_Managed_Eval1(s) and Biddy_Eval1(s) are defined for use without searching in the user-defined cache.

Definition at line 318 of file biddyInOut.c.

Biddy_Edge Biddy_Managed_Eval2 ( Biddy_Manager  MNG,
Biddy_String  boolFunc 
)

Function Biddy_Managed_Eval2 evaluates infix &|^~>< format.

Description

Boolean constants are '0' and '1'. Parenthesis are implemented. Operators' priority is implemented. Formula Tree is suported (global table, only). Operators '*' and '+' are also allowed for conjunction/disjunction.

Side effects

Variable names must be one letter a-zA-Z optionally followed by int number.

More info

Original author: Volodymyr Mihav (mihaw.nosp@m..wol.nosp@m.odymy.nosp@m.r@gm.nosp@m.ail.c.nosp@m.om) Original implementation of this function is on https://github.com/sungmaster/liBDD. Macro Biddy_Eval2(boolFunc) is defined for use with anonymous manager.

Definition at line 417 of file biddyInOut.c.

void Biddy_Managed_ReadVerilogFile ( Biddy_Manager  MNG,
const char  filename[],
Biddy_String  prefix 
)

Function Biddy_Managed_ReadVerilogFile reads Verilog file and creates variables for all primary inputs and Boolean functions for all primary outputs.

Description

If (prefix != NULL) then the created BDD variables and formulae will get it.

Side effects

More info

Original author: David Kebo Houngninou, Southern Methodist University Original implementation of this function is on https://github.com/davidkebo/verilog-parser Macro Biddy_ReadVerilogFile(filename,prefix) is defined for use with anonymous manager.

Definition at line 610 of file biddyInOut.c.

void Biddy_Managed_PrintfBDD ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_PrintfBDD writes raw format using printf.

Description

This function is intended for writing to an output channel via macro which overrides the meaning of standard printf calls. For writing raw format into the file, use Biddy_Managed_WriteBDD.

Side effects

More info

Macro Biddy_PrintfBDD(f) is defined for use with anonymous manager.

Definition at line 711 of file biddyInOut.c.

void Biddy_Managed_WriteBDD ( Biddy_Manager  MNG,
const char  filename[],
Biddy_Edge  f,
Biddy_String  label 
)

Function Biddy_Managed_WriteBDD writes raw format using fprintf.

Description

Side effects

More info

Macro Biddy_WriteBDD(f) is defined for use with anonymous manager.

Definition at line 741 of file biddyInOut.c.

void Biddy_Managed_PrintfTable ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_PrintfTable writes truth table using printf.

Description

This function is intended for writing to an output channel via macro which overrides the meaning of standard printf calls. For writing truth table into the file, use Biddy_Managed_WriteTable.

Side effects

More info

Thanks to Jan Kraner (jankr.nosp@m.isti.nosp@m.an.kr.nosp@m.aner.nosp@m.@stud.nosp@m.ent..nosp@m.um.si) and Ziga Kobale (ziga..nosp@m.koba.nosp@m.le@st.nosp@m.uden.nosp@m.t.um..nosp@m.si). Macro Biddy_PrintfTable(f) is defined for use with anonymous manager.

Definition at line 788 of file biddyInOut.c.

void Biddy_Managed_WriteTable ( Biddy_Manager  MNG,
const char  filename[],
Biddy_Edge  f 
)

Function Biddy_Managed_WriteTable writes truth table using fprintf.

Description

Side effects

More info

Thanks to Jan Kraner (jankr.nosp@m.isti.nosp@m.an.kr.nosp@m.aner.nosp@m.@stud.nosp@m.ent..nosp@m.um.si) and Ziga Kobale (ziga..nosp@m.koba.nosp@m.le@st.nosp@m.uden.nosp@m.t.um..nosp@m.si). Macro Biddy_WriteTable(f) is defined for use with anonymous manager.

Definition at line 896 of file biddyInOut.c.

void Biddy_Managed_PrintfSOP ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_PrintfSOP writes SOP using printf.

Description

Side effects

More info

Definition at line 918 of file biddyInOut.c.

void Biddy_Managed_WriteSOP ( Biddy_Manager  MNG,
const char  filename[],
Biddy_Edge  f 
)

Function Biddy_Managed_WriteSOP writes SOP using fprintf.

Description

Side effects

More info

Definition at line 996 of file biddyInOut.c.

unsigned int Biddy_Managed_WriteDot ( Biddy_Manager  MNG,
const char  filename[],
Biddy_Edge  f,
const char  label[],
int  id,
Biddy_Boolean  cudd 
)

Function Biddy_Managed_WriteDot writes dot/graphviz format using fprintf.

Description

Output dot format. Two approaches are implemented. The CUDD-like implementation is copyied from CUDD 3.0.

Side effects

If (id != -1) then id is used instead of <...> for variable names. If (filename == NULL) then output is to stdout. Function resets all variables value.

More info

Macro Biddy_WriteDot(filename,f,label) is defined for use with anonymous manager.

Definition at line 1111 of file biddyInOut.c.

unsigned int Biddy_Managed_WriteBddview ( Biddy_Manager  MNG,
const char  filename[],
Biddy_Edge  f,
const char  label[],
Biddy_XY table 
)

Function Biddy_Managed_WriteBDDView writes bddview format using fprintf.

Description

Output bddview format.

Side effects

Parameter table is optional, if not NULL then it must contain node names and coordinates. If (filename == NULL) then output is to stdout.

More info

Macro Biddy_WriteBddview(filename,f,label) is defined for use with anonymous manager.

Definition at line 1330 of file biddyInOut.c.