Symbool is a program for manipulating boolean expressions symbolically.

Input

The input consists of a series of boolean  expressions assigned to symbols:

    sym = expr;

A symbol is any string of alphanumerical characters. The symbols 1 and 0 represent true and false, respectively. An expression consists of symbols, sub-expressions enclosed in parentheses, and operators. The operators are:

expr1 + expr2 OR true iff either expr1 or expr2  is true
expr1 expr2 AND true iff both expr1 and expr2 are true
expr1 ^ expr2 XOR true iff either expr1 or expr2 is true, but not both
expr'1 negation true iff expr is false
expr > sym1, sym2,... differentiation true iff expr depends on  sym1, sym2,...
expr < sym1, sym2,... integration true iff expr does not depend on  sym1, sym2,...
expr1 : sym = expr2 constraint expr1  with  expr2  substituted for  sym

Output

The output can be printed in different representations:

  1. Minimized Sum of Product (SOP) form.

  2. Factored form.

  3. Reduced Ordered Binary Decision Diagram (BDD) form.

  4. Exclusive-OR Normal Form (XNF).

Example 1

With the input program,

    f = a(b + c);
    g = f + b;
    h = g c;
    a = e + d;  

the output in SOP form is

    a = d + e
    f = b d + b e + c d + c e
    g = b + c d + c e
    h = b c + c d + c e.

Example 2

With the input program,

    f = a(b + c);
    g = f + d';

the output in BDD form is

    bdd f
        if a
            if b
                1
            else if !b
                c
            endif b
        else if !a
            0
        endif a
    bdd g
        if a
            if b
                1
            else if !b
                if c
                    1
                else if !c
                    !d
                endif c
            endif b
        else if !a
            !d
        endif a
 

Example 3

With the input program,

    f = a (b' + c);
    g = alpha ^ beta x1 ^ gamma x2 ^ delta x1 x2;
    alpha = (f > a);
    beta  = (f : b = alpha);
    gamma = (f < c);
    delta = alpha + beta + gamma;

the output expression for g  in factored form is

    g = a x1 x2' + b (a (c x2 + x1) + c' (a' x1' + x2')).
 

Copyright © 2005, Marc Riedel, California Institute of Technology
Back to  Online Interface
Back to  Home Page