BDDC is a tool for manipulating logical formula. It is based on a Binary Decision Diagram library, that means that each formula is internally tranformed into a canonical form. In particular, if the formula (resp its negation) is a tautologie, BDDC will transform it into the "always true formula" (resp. the "always false formula").

All classical operators are provided. Moreover the tool provides a "functional-like" language that allows the user to define his (her) own logical operators.

• Description
  • Basic features
  • Advanced features
• Lexical aspects
• Commands
  • quit
  • help
  • exec "command-file"
  • syntax
  • list
  • exp;
  • ident := exp ;
  • ident( identlist) := exp;
  • print ident
  • size exp;
  • [dnf, cnf, reed] exp;
  • set [dnf, cnf, reed]
• Logical expressions
  • Boolean operators
    • false
    • true
    • ident
    • not exp
    • exp or exp
    • exp and exp
    • exp xor exp
    • exp => exp
    • exp = exp
    • ite(exp,exp,exp)
    • forall identlist exp
    • exist identlist exp
    • # (exp-list)
    • nor exp-list
    • xor (exp-list)
  • Control operators
    • compare(exp,exp)
    • implies(exp,exp)
    • cuts(exp,exp)
    • if exp then exp else exp
    • let ident := exp in exp
  • Bdd decomposition
    • root(exp)
    • high(exp)
    • low(exp)
    • root(exp-list)
    • supp(exp)
  • Simplification modulo care-set
    • restrict(exp,exp)
    • constrain(exp,exp)
  • Priorities
• Appendix
  • Notes on BDD size
  • Notes on identifiers
  • Notes on user-defined functions
  • Notes on Shannon decomposition
  • Notes on output format
• Examples
  • Programming the negation
  • Finding an implicant in a bdd
  • Programming the union
• References

This document was translated from L^AT_EX by H^EV^EA.