#!/usr/bin/env python2.7
# ----------------------------------
#
# Module prop_expr.py

"""
This module implements propositional formulas according to the
following grammar:

<expr> ::= <atom>
       | '(' <unop> <expr> ')'
       | '(' <expr> <binop> <expr> ')'

<atom>       ::= <IdentLower>
<unop>       ::= '~'
<binop>      ::= '&' | '|' | '->' | '<=>'
<IdentLower> ::= [a-z][_a-z0-9A-Z]*

Note that the formula output now has been hacked to use pretty html
entities for the logical symnols for display with GraphViz/dot. 


Example expressions are:
========================
p1
(~p2)
(p->(p->p))
(p&((~p)<=>q))


Copyright 2010-2011 Stephan Schulz, schulz@eprover.org

This program 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.

This program 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., 59 Temple Place, Suite 330, Boston,
MA  02111-1307 USA 

The original copyright holder can be contacted as

Stephan Schulz
Auf der Altenburg 7
70376 Stuttgart
Germany
Email: schulz@eprover.org
"""

import unittest
import sys
import getopt
from lexer import Lexer, Token


def genInterpretations(props):
    """
    Generate a list of all interpretations for the given set of
    propositional variables.
    """
    if len(props) == 0:
        return [{}]
    prop = props.pop()
    tmp = genInterpretations(props)
    res = []
    for i in tmp:
        pos = dict(i)
        pos[prop] = True
        res.append(pos)
        neg = dict(i)
        neg[prop] = False
        res.append(neg)
    return res


op_trans = {
    "&" : "&and;",
    "|" : "&or;",
    "->": "&rarr;",
    "<=>" : "&harr;"
    }

   
class PropFormula(object):
    """
    A class to represent propositional formulas. A formula can be
    either a propositional constant (in which case the type is
    "const"), an atomic proposition (in which case the type is
    "atom"), or be a composite formula, in which case the type the
    operator, and the object carries one or two subformulas.
    """
        
    def __init__(self, type, arg1=None, arg2=None):
        """
        Initialize the formula.
        """
        self.type = type
        self.arg1 = arg1
        self.arg2 = arg2

    def __str__(self):
        """        
        Return a printable representation of the formula.
        """
        if self.type=="const" or self.type=="atom":
            return self.arg1
        elif self.type  == "~":
            return "("+"&not;"+str(self.arg1)+")"
        else:
            # "type" is a binary operator
            return "("+str(self.arg1)+op_trans[self.type]+str(self.arg2)+")"

    def __repr__(self):
        """        
        Return a printable representation of the formula.
        """
        return self.__str__()
            
    def evaluate(self, var_valuation):
        """
        Evaluate the expression. var_valuation must be a Pyton
        dictionary that contains a truth value for every variable
        in expression. If not, the program terminates with an
        error. We use the Python True and False constants as truth
        values. 
        
        Evaluation is done by simple recursions. Expressions of type
        "const" and "atom" are evaluated directly or with respect to the
        valuation given. Other expressions are recursively evaluated,
        then the operator is applied to the result.
        """
        if self.type=="atom":
            return var_valuation[self.arg1]
        elif self.type == "const":
            if self.arg1 == "$true":
                return True
            else:
                return False
        elif self.type  == "~":
            value1 = self.arg1.evaluate(var_valuation)
            return not value1
        else:
            value1 = self.arg1.evaluate(var_valuation)
            value2 = self.arg2.evaluate(var_valuation)
            if self.type == "&":            
                return value1 and value2
            elif self.type == "|":
                return value1 or value2
            elif self.type == "->":
                return (not value1) or value2
            else:
                return value1 == value2

    def getProps(self):
        """
        Return all propositional variables from formula.
        """
        if self.type=="atom":                
            return set([self.arg1])
        elif self.type == "const":
            return set()
        elif self.type  == "~":
            return self.arg1.getProps()
        else:
            props1 = self.arg1.getProps()
            props2 = self.arg2.getProps()
            return props1|props2

    def isTautology(self):
        """
        Return True if and only if the formula is a tautology.
        """
        vars = self.getProps()
        ints = genInterpretations(vars)
        
        for i in ints:
            if self.evaluate(i) == False:
                return False
        return True

    def isAtom(self):
        """
        Return True if the formula is atomic (including constant
        propsitions).
        """
        return self.type in ["const", "atom"]

    def isLiteral(self):
        """
        Return True if the formula is an atom or a negated atom.
        """
        if self.isAtom():
            return True
        if self.type == "~" and self.arg1.isAtom():
            return True
        return False
        

    def equal(self, other):
        """
        Return true if self is structurally equal to other.
        """
        if self.type != other.type:
            return False
        if self.type in ["const", "atom"]:
            return self.arg1==other.arg1
        if not self.arg1.equal(other.arg1):
            return False
        if self.arg2 == None and other.arg2 == None:
            return True
        if self.arg2 == None:
            return False
        if other.arg2 == None:
            return False
        return self.arg2.equal(other.arg2)


    def negation(self):
        """
        Return the negaton of self. Recycles self.
        """
        return PropFormula("~", self)

    def isComplement(self, other):
        """
        Return True if self = ~other or other = ~self.
        """
        if self.type == "~" and self.arg1.equal(other):
            return True
        if other.type == "~" and other.arg1.equal(self):
            return True
        return False    

    def isAlpha(self):
        """
        Return true if formula is an alpha-formula, false otherwise.
        """
        if self.type == "~" and self.arg1.type == "~":
            return True
        elif self.type == "&":
            return True
        elif self.type == "<=>":
            return True
        elif self.type == "~" and self.arg1.type == "|":
            return True
        elif self.type == "~" and self.arg1.type == "->":
            return True
        else:
            return False
   
    def isBeta(self):
        """
        Return true if formula is a beta-formula, false otherwise.
        """
        if self.type == "~" and self.arg1.type == "&":
            return True
        elif self.type == "~" and self.arg1.type == "<=>":
            return True
        elif self.type == "|":
            return True
        elif self.type == "->":
            return True
        else:
            return False

    def alphaSplit(self):
        """
        Check if self is an alpha-formula. If yes, return a list with
        the alpha-subformulae, a otherwise return None.
        """
        if self.type == "~" and self.arg1.type == "~":
            return [self.arg1.arg1]
        elif self.type == "&":
            return [self.arg1, self.arg2]
        elif self.type == "<=>":
            return [PropFormula("->", self.arg1, self.arg2),
                    PropFormula("->", self.arg2, self.arg1)]
        elif self.type == "~" and self.arg1.type == "|":
            return [self.arg1.arg1.negation(), \
                    self.arg1.arg2.negation()]
        elif self.type == "~" and self.arg1.type == "->":
            return [self.arg1.arg1, \
                    self.arg1.arg2.negation()]
        else:
            return None
        
    
    def betaSplit(self):
        """
        Check if self is an beta-formula. If yes, return a list with
        the beta-subformulae, a otherwise return None.
        """
        if self.type == "~" and self.arg1.type == "&":
            return [self.arg1.arg1.negation(), \
                    self.arg1.arg2.negation()]
        if self.type == "~" and self.arg1.type == "<=>":
            return [PropFormula("&",
                                self.arg1.arg1,
                                self.arg1.arg2.negation()),
                    PropFormula("&",
                                self.arg1.arg1.negation(),
                                self.arg1.arg2)]
        elif self.type == "|":
            return [self.arg1, self.arg2]
        elif self.type == "->":
            return [self.arg1.negation(), self.arg2]
        else:
            return None
        
    
     

def parseFormula(lexer):
    """
    Parse a propositional formula. This simply tests for the
    different possibilities in the grammar and does a recursive
    descent. 
    """
    if lexer.TestLit(["$true", "$false"]):
        res = PropFormula("const", lexer.LookLit())
        lexer.Next()
    elif lexer.TestTok(Token.IdentLower):
        res = PropFormula("atom", lexer.LookLit())
        lexer.Next()
    else:
        lexer.AcceptTok(Token.OpenPar)
        if lexer.TestTok(Token.Negation):
            op = "~"
            lexer.Next()
            arg1 = parseFormula(lexer)
            arg2 = None
        else:
            arg1 = parseFormula(lexer)
            lexer.CheckTok([Token.Or, Token.And, Token.Implies, Token.Equiv])
            op = lexer.LookLit()
            lexer.Next()
            arg2 = parseFormula(lexer)
        lexer.AcceptTok(Token.ClosePar)
        res = PropFormula(op, arg1, arg2)
    return res


class TestFormula(unittest.TestCase):
    """
    Test the lexer functions.
    """
    def setUp(self):
        print
        self.example1 = "p1 (~p2) (p->(p->p)) (p&((~p)<=>q))"

    def testParser(self):
        lex  = Lexer(self.example1)
        expr1 = parseFormula(lex)
        print expr1

        expr2 = parseFormula(lex)
        print expr2

        expr3 = parseFormula(lex)
        print expr3

        expr4 = parseFormula(lex)
        print expr4

    def doEval(self, expr, valuation, result):
        """
        Print and evaluate a single expresstion.
        """
        val = expr.evaluate(valuation)
        print "The value of", expr, "under", valuation, "is", val
        self.assertEqual(expr.evaluate(valuation), result)
        

    def testEval(self):
        lex  = Lexer(self.example1)
        expr1 = parseFormula(lex)
        expr2 = parseFormula(lex)
        expr3 = parseFormula(lex)
        expr4 = parseFormula(lex)

        valuation = {"p":True, "q":False, "p1":True, "p2":False}

        self.doEval(expr1, valuation, True) 
        self.doEval(expr2, valuation, True)
        self.doEval(expr3, valuation, True)
        self.doEval(expr4, valuation, True)

        valuation = {"p":False, "q":False, "p1":False, "p2":False}

        self.doEval(expr1, valuation, False) 
        self.doEval(expr2, valuation, True)
        self.doEval(expr3, valuation, True)
        self.doEval(expr4, valuation, False)

    def testGetProps(self):
        lex  = Lexer(self.example1)
        expr1 = parseFormula(lex)
        expr2 = parseFormula(lex)
        expr3 = parseFormula(lex)
        expr4 = parseFormula(lex)

        p = expr1.getProps()
        self.assertEqual(p, set(["p1"]))
        print p

        p = expr2.getProps()
        self.assertEqual(p, set(["p2"]))
        print p
        
        p = expr3.getProps()
        self.assertEqual(p, set(["p"]))
        print p

        p = expr4.getProps()
        self.assertEqual(p, set(["p", "q"]))
        print p

    def testGenInt(self):
        props = set(["a", "b", "c"])
        interpretations = genInterpretations(props)
        print interpretations

        self.assertEqual(len(interpretations),8)

    def testInt(self):
        lex  = Lexer(self.example1)
        expr1 = parseFormula(lex)
        expr2 = parseFormula(lex)
        expr3 = parseFormula(lex)
        expr4 = parseFormula(lex)

        print expr1.isTautology()
        print expr2.isTautology()
        print expr3.isTautology()
        print expr4.isTautology()

    def testOps(self):
        lex = Lexer("p1 (~p1) (p1->p1) (~(p1->p1))")
        f1 = parseFormula(lex)
        f2 = parseFormula(lex)
        f3 = parseFormula(lex)
        f4 = parseFormula(lex)
        self.assert_(f1.isAtom())
        self.assert_(f1.isLiteral())
        self.assert_(f1.isComplement(f2))
        self.assert_(f2.isComplement(f1))
        self.assert_(f3.isComplement(f4))
        self.assert_(f3.equal(f4.arg1))
        self.assert_(not f3.isAtom())
        self.assert_(not f4.isAtom())
        self.assert_(not f4.isLiteral())
        print f3, "alpha:",
        print f3.alphaSplit()
        print f3, "beta:",
        print f3.betaSplit()
        print f4, "alpha:",
        print f4.alphaSplit()
        print f4, "beta:",
        print f4.betaSplit()
                
            

if __name__ == '__main__':
    unittest.main()