# Copyright (c) 1996 by Raymond Hettinger.  All Rights Reserved.
BEGIN{
        split( "1 1 2 1 2 2 3 1 2 2 3 2 3 3 4", BITS );
        SORTTYPE = 0
        for( i=1, input="" ; i<ARGC ; i++ ){
                input = input ARGV[i] " "
                ARGV[i] = ""
        }
        input = tolower( substr(input,1,length(input)-1) )

        varcnt = 0
        slptr = 0
        delete varlist

        # goal: transform to a stack language from:
        # ?        concl: prem THEREFORE prop
        # ?               | prop
        # ?       prem -> prop COMMA prop
        # ?            | prop
        #        prop -> impl EQL impl         :  EQL
        #             |  impl                  :
        #        impl |  expr IMP expr         :  IMP
        #             |  expr IMPBY expr       :  IMPBY
        #             |  expr                  :
        #        expr -> term OR term          :  OR
        #             |  term XOR term         :  XOR
        #             |  term NOR term         :  NOR
        #             |  term                  :
        #        term -> fact AND fact         :  AND
        #             |  fact NAND fact        :  NAND
        #             |  fact                  :
        #        fact -> LPAR prop RPAR        :
        #             |  TRUE                  :  TRUE
        #             |  FALSE                 :  FALSE
        #             |  ID                    :  IDidnum
        #             |  NOT expr              :  NOT

        lex()
        prop()
        if( ! test("end") ) error( "Expected end of prop" )
        emit("end")

        evalFree()
        simplify()
        done()
}

function prop(){
        impl()
        if( test("eql") ){
                impl()
                emit("xor");
                emit("not");
        }
}

function impl(          op ){
        expr()
        while( 1 ){
                if( test("imp") ){
                        emit("not")
                        expr()
                        emit("or")
                }else if( test("impby") ){
                        expr()
                        emit("not")
                        emit("or")
                }else
                        break
        }
}

function expr(){
        term()
        while( 1 ){
                if( test("or") ){
                        term()
                        emit("or")
                }else if( test("nor") ){
                        term()
                        emit("or")
                        emit("not")
                }else if( test("xor") ){
                        term()
                        emit("xor")
                }else
                        break
        }
}

function term(){
        fact()
        while( 1 ){
                if( test("and") ){
                        emit("not")
                        fact()
                        emit("not")
                        emit("or")
                        emit("not")
                }else if( test("nand") ){
                        emit("not")
                        fact()
                        emit("not")
                        emit("or")
                }else if( tok=="true" || tok=="false" || tok=="lpar" || tok=="id" || tok=="not" ){
                        emit("not")
                        fact()
                        emit("not")
                        emit("or")
                        emit("not")
                        continue
                }else
                        break
        }
}

function fact(){
        if( test("true") ){
                emit("false")
                emit("not")
        }else if( test("false") )
                emit("false")
        else if( test("lpar") ){
                prop()
                if( ! test("rpar") )
                        error( "Unbalanced parenthesis" )
        }else if( test("not") ){
                fact()
                emit("not")
        }else if( test("id") )
                emit("id" lasttokval )
        else
                error( "Expected a factor" )
}

function error( txt ){
        print txt
        print "Parse error encountered at " tok, tokval
        exit(1)
}

function emit( txt ){
        slang[ slptr++ ] = txt
}

function test( txt ){
        if( txt == tok ){
                lasttokval = tokval
                lex()
                return 1
        }
        return 0
}

function lex(                varname ){ #Gbl: input, varlist, idname, varcnt
        sub( /^[ ]+/, "", input )
        if( length(input) == 0 ){ tok = "end" ; return }
        else if( match(input, /^((<-)|(impby))/) )      tok ="impby"
        else if( match(input, /^((->)|(imp))/) )        tok ="imp"
        else if( match(input, /^([\\+\\|]|(or))/) )     tok ="or"
        else if( match(input, /^([\\*&]|(and))/) )      tok ="and"
        else if( match(input, /^([-~!]|(not))/) )       tok = "not"
        else if( match(input, /^([1]|(true))/) )        tok ="true"
        else if( match(input, /^([0]|(false))/) )       tok ="false"
        else if( match(input, /^\(/) )                  tok ="lpar"
        else if( match(input, /^\)/) )                  tok ="rpar"
        else if( match(input, /^((eql)|(==))/) )        tok ="eql"
        else if( match(input, /^nand/) )                tok ="nand"
        else if( match(input, /^nor/) )                 tok ="nor"
        else if( match(input, /^((xor)|\^)/) )          tok ="xor"
        else if( match(input, /^[A-Za-z][A-Za-z0-9]*/) ){
                varname = substr(input,RSTART,RLENGTH); tok ="id"
                if( ! (varname in varlist) ){
                        varlist[ varname ] = ++varcnt
                        idname[ varcnt ] = varname
                }
                tokval = varlist[varname]
        }else{
                print "Lex error >>>" input "<<<:"
                exit(2)
        }
        input = substr(input,RLENGTH+1,length(input)-RLENGTH)
}

function evalFree(               s, p, r ){  # Used varcnt
        for( p=1 ; p<=varcnt ; p++ )
                printf "%-4s", idname[p]
        printf "\n"
        for( p=1 ; p<=varcnt ; p++ )
                printf "--- "
        printf "\n"

        for( taut=1, s=0 ; s < 2^varcnt ; s++ ){
                for( p=varcnt ; p ; p-- ){
                        val[ "id" varcnt-p+1 ] = and(s,shiftl(1,p-1)) ? 1 : 0
                        printf "%01d   ", val["id" varcnt-p+1]
                }

                r = evalBound()
                printf "|   %01d\n", r
                taut *= r
                if( r==0 )
                        fstate[nfs++] = s
                else
                        tstate[nts++] = s
        }
        return taut
}

function evalBound(            sp, pc, stmt, i, v ){  # uses slang[] and val[]
        for( pc=0, st=0 ; pc<slptr-1 ; pc++ ){
                stmt = slang[pc]
                if( stmt ~ /^id/ )            {  st = st + st + val[ stmt ] }
                else if( stmt == "false" )    {  st = st + st }
                else if( stmt == "not" )      {  st = xor(st,1) }
                else if( stmt == "or" )       {  st = or( shiftr(st,1), and(st,1) ) }
                else if( stmt == "xor" )      {  st = xor( shiftr(st,1), and(st,1) ) }
                else                          {  error( "Undefined action " stmt ) }
        }
        return and(st,1)
}

function simplify(){
        printf "Simplified:  "
        ns = nfs + nts
        for( s=0 ; s<ns ; s++ )
                arr[ numbits(s) " " s ]
        SORTTYPE = 2
        for( elem in arr ){
                split( elem, field )
                pmask = field[2]+0
                mbits = field[1]+0
                for( vseq=0 ; vseq<2^mbits ; vseq++ ){
                           for( b=1, v=vseq, pval=0 ; v ; b+=b ){
                                if( and(b,pmask) ){
                                        if( and(v,1) ){
                                                pval += b
                                        }
                                        v = shiftr(v,1)
                                }
                           }
                           check_pattern(pmask,pval)
                }
        }
}

function check_pattern(pmask,pval,              i ){
        for( i=0, fstate[nfs+0]=pval ; and(fstate[i],pmask) != pval ; i++ ){
                ;
        }
        if( i<nfs ){ return
        }
        for( i=0 ; i<nts ; i++ )
                if( and(tstate[i],pmask) == pval )
                        if( marked[i] == 0 ){
                                out[ pmask " " pval ]
                                marked[i] = 1
                                if( ++nms == nts ){
                                        return();
                                }
                        }
}

function done(                  x, f, i ){
        for( x in out ){
                if( ++pass > 1 ) printf "OR "
                split( x, f )
                for( i=varcnt ; i ; i-- ){
                        if( and(f[1],(shiftl(1,i-1))) == 0 ) continue
                        if( and(f[2],(shiftl(1,i-1))) == 0 ) printf "~"
                        printf( "%s ", idname[varcnt-i+1] )
                }
        }
        if( nfs && nts==0 ) print "Always FALSE"
        if( nfs==0 && nts ) print "Always TRUE"
}

function numbits( word,         bits ){
        for( ; word > 15 ; word=shiftr(word,4) ){
                bits += BITS[ and(word,15) ]
        }
        return bits + BITS[ word ]
}