#!/usr/bin/env python3
# ----------------------------------
#
# 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, 2018 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_dot = {
    "~"   : "&not;",
    "&"   : "&and;",
    "|"   : "&or;",
    "->"  : "&rarr;",
    "<=>" : "&harr;"
    }

op_trans_txt = {
    "~"   : "~",
    "&"   : "&",
    "|"   : "|",
    "->"  : "->",
    "<=>" : "<=>"
    }

op_trans_tex = {
    "~"   : "\lnot{}",
    "&"   : "\land{}",
    "|"   : "\lor{}",
    "->"  : "\limpl{}",
    "<=>" : "\lequiv{}"
    }

op_pref = {
    "const": 6,
    "atom" : 6,
    "~"    : 5,
    "&"    : 4,
    "|"    : 3,
    "->"   : 2,
    "<=>"  : 1
    }


op_trans = op_trans_dot

neg_const = {
    "$true"  : "$false",
    "$false" : "$true"
    }


def PropFormulaSetPrintStyle(style="default"):
    global op_trans

    if style=="tex":
        op_trans = op_trans_tex
    elif style=="txt":
        op_trans = op_trans_txt
    elif style=="default" or style=="dot":
        op_trans = op_trans_dot
    else:
        raise Exception("Wrong Argument to PropFormula.set_style()")


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 __str2__(self):
        """
        Return a printable representation of the formula with nearly
        full parentheses (negated atoms are not parenthesized).
        """
        if self.type=="const" or self.type=="atom":
            return self.arg1
        elif self.type  == "~":
            if self.arg1.type == "atom":
                return op_trans["~"]+self.arg1.__str2__()
            else:
                return "("+op_trans["~"]+self.arg1.__str2__()+")"
        else:
            # "type" is a binary operator
            return "("+self.arg1.__str2__()+op_trans[self.type]+self.arg2.__str2__()+")"

    def __str3__(self):
        """
        Return a printable representation of the formula with
        full parentheses.
        """
        if self.type=="const" or self.type=="atom":
            return self.arg1
        elif self.type  == "~":
            return "("+op_trans["~"]+self.arg1.__str3__()+")"
        else:
            # "type" is a binary operator
            return "("+self.arg1.__str3__()+op_trans[self.type]+self.arg2.__str3__()+")"


    def __str__(self):
        """
        Return a printable representation of the formula with reduced
        parentheses (bracked ->, <=>, and as necessary to reflect
        structure). Associative parts may fake associativity ;-)
        """
        if self.type=="const" or self.type=="atom":
            return self.arg1
        elif self.type  == "~":
            if op_pref[self.arg1.type] < op_pref["~"]:
                return op_trans["~"]+"("+str(self.arg1)+")"
            else:
                return op_trans["~"]+str(self.arg1)
        else:
            # "type" is a binary operator
            if self.arg1.type in ["->", "<=>"] or\
               op_pref[self.type] > op_pref[self.arg1.type]:
                arg1 = "("+str(self.arg1)+")"
            else:
                arg1 = str(self.arg1)

            if self.arg2.type in ["->", "<=>"] or\
               op_pref[self.type] > op_pref[self.arg2.type]:
                arg2 = "("+str(self.arg2)+")"
            else:
                arg2 = str(self.arg2)

            return arg1+op_trans[self.type]+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 hasOp(self, op):
        if self.type=="const" or self.type=="atom":
            return False
        elif self.type == op:
            return True
        elif self.type == "~":
            return self.arg1.hasOp(op)
        else:
            return self.arg1.hasOp(op) or self.arg2.hasOp(op)


    def isNNF(self):
        if self.type=="const" or self.type=="atom":
            return True
        elif self.type in ["->", "<=>"]:
            return False
        elif self.type == "~":
            return selfarg1.type=="const" or self.arg1.type=="atom"
        else:
            return self.arg1.isNNF() and self.arg2.isNNF()


    def elimFirstEquiv(self):
        """
        Return changed formula or None.
        """
        if self.type=="const" or self.type=="atom":
            return None
        elif self.type == "<=>":
            return PropFormula("&",
                               PropFormula("->",
                                           self.arg1,
                                           self.arg2),
                               PropFormula("->",
                                           self.arg2,
                                           self.arg1))
        elif self.type == "~":
            sub1 = self.arg1.elimFirstEquiv()
            if sub1:
                return PropFormula("~",
                                   self.arg1.elimFirstEquiv())
            else:
                return None
        else:
            sub1 = self.arg1.elimFirstEquiv()
            if not sub1:
                sub1 = self.arg1
                sub2 = self.arg2.elimFirstEquiv()
                if not sub2:
                   return None
            else:
                sub2 = self.arg2

            return PropFormula(self.type,
                               sub1, sub2)

    def elimFirstImpl(self):
        """
        Return changed formula or None.
        """
        if self.type=="const" or self.type=="atom":
            return None
        elif self.type == "->":
            return PropFormula("|",
                               PropFormula("~",
                                           self.arg1),
                               self.arg2)
        elif self.type == "~":
            sub1 = self.arg1.elimFirstImpl()
            if sub1:
                return PropFormula("~",
                                   self.arg1.elimFirstImpl())
            return None
        else:
            sub1 = self.arg1.elimFirstImpl()
            if not sub1:
                sub1 = self.arg1
                sub2 = self.arg2.elimFirstImpl()
                if not sub2:
                   return None
            else:
                sub2 = self.arg2

            return PropFormula(self.type,
                               sub1, sub2)


    def elimEquiv(self):
        if self.type=="const" or self.type=="atom":
            return self
        elif self.type == "<=>":
            return PropFormula("&",
                               PropFormula("->",
                                           self.arg1.elimEquiv(),
                                           self.arg2.elimEquiv()),
                               PropFormula("->",
                                           self.arg2.elimEquiv(),
                                           self.arg1.elimEquiv()))

        elif self.type == "~":
            return PropFormula("~",
                               self.arg1.elimEquiv())
        else:
            return PropFormula(self.type,
                               self.arg1.elimEquiv(),
                               self.arg2.elimEquiv())


    def elimImpl(self):
        if self.type=="const" or self.type=="atom":
            return self
        elif self.type == "<=>":
            raise Exception("elimEquiv() expects formula without <=>")
        elif self.type == "->":
            return PropFormula("|",
                               PropFormula("~",
                                           self.arg1.elimImpl()),
                               self.arg2.elimImpl())
        elif self.type == "~":
            return PropFormula("~",
                               self.arg1.elimImpl())
        else:
            return PropFormula(self.type,
                               self.arg1.elimImpl(),
                               self.arg2.elimImpl())





    def shiftNeg(self):
        if self.type=="const" or self.type=="atom":
            return self
        if self.type == "~":
            if self.arg1.type == "atom":
                return self
            elif self.arg1.type == "const":
                return PropFormula("const", neg_prop[self.arg1.arg1])
            elif self.arg1.type == "~":
                return self.arg1.arg1.shiftNeg()
            elif self.arg1.type == "&":
                arg11 = self.arg1.arg1.negation()
                arg12 = self.arg1.arg2.negation()
                return PropFormula("|", arg11.shiftNeg(), arg12.shiftNeg())
            elif self.arg1.type == "|":
                arg11 = self.arg1.arg1.negation()
                arg12 = self.arg1.arg2.negation()
                return PropFormula("&", arg11.shiftNeg(), arg12.shiftNeg())
            else:
                print("Wrong:", self, self.arg1, self.arg1.type)
                raise Exception("shiftNeg(): Wrong argument type"+self.arg1.type)
        else:
            return PropFormula(self.type,
                               self.arg1.shiftNeg(),
                               self.arg2.shiftNeg())

    def distributeOr(self):
        if self.type=="const" or self.type=="atom" or self.type == "~":
            return self
        else:
            arg1 = self.arg1.distributeOr()
            arg2 = self.arg2.distributeOr()
            if self.type == "|":
                if arg1.type == "&":
                    dis1 = PropFormula("|", arg1.arg1, arg2)
                    dis2 = PropFormula("|", arg1.arg2, arg2)
                    return PropFormula("&", dis1, dis2).distributeOr()
                elif arg2.type =="&":
                    dis1 = PropFormula("|", arg1, arg2.arg1)
                    dis2 = PropFormula("|", arg1, arg2.arg2)
                    return PropFormula("&", dis1, dis2).distributeOr()
                else:
                    return PropFormula("|", arg1, arg2)
            elif self.type=="&":
                return PropFormula("&", arg1, arg2)
            else:
                print("Wrong:", self, self.arg1, self.arg1.type)
                raise Exception("distributeOrNeg(): Wrong argument type"+self.type)


def parseBaseForm(lexer):
    """
    Parse a propositional formula. This simply tests for the
    different possibilities in the grammar and does a recursive
    descent. It does do associativity and precedence.
    """
    if lexer.TestTok(Token.OpenPar):
        lexer.AcceptTok(Token.OpenPar)
        res = parseForm(lexer)
        lexer.AcceptTok(Token.ClosePar)
    elif  lexer.TestLit(["$true", "$false"]):
        res = PropFormula("const", lexer.LookLit())
        lexer.Next()
    elif lexer.TestTok(Token.IdentLower):
        res = PropFormula("atom", lexer.LookLit())
        lexer.Next()
    elif lexer.TestTok(Token.Negation):
        lexer.Next()
        res = parseBaseForm(lexer)
        res =  PropFormula("~", res)
    else:
        lexer.CheckTok([Token.DefFunctor, Token.OpenPar,
                        Token.IdentLower, Token.Negation])
    return res

def parseAndForm(lexer):
    f1 = parseBaseForm(lexer)
    while lexer.TestTok(Token.And):
        lexer.Next()
        f2 = parseBaseForm(lexer)
        f1 = PropFormula("&", f1, f2)
    return f1

def parseOrForm(lexer):
    f1 = parseAndForm(lexer)
    while lexer.TestTok(Token.Or):
        lexer.Next()
        f2 = parseAndForm(lexer)
        f1 = PropFormula("|", f1, f2)
    return f1

def parseImplForm(lexer):
    f1 = parseOrForm(lexer)
    while lexer.TestTok(Token.Implies):
        lexer.Next()
        f2 = parseOrForm(lexer)
        f1 = PropFormula("->", f1, f2)
    return f1

def parseForm(lexer):
    f1 = parseImplForm(lexer)
    while lexer.TestTok(Token.Equiv):
        lexer.Next()
        f2 = parseImplForm(lexer)
        f1 = PropFormula("<=>", f1, f2)
    return f1



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))"
        self.example2 = "p1|p2|p3   (p1 | p2 & ~(p3<=>~~p4))"

    def testParser(self):
        print("Parser 1")
        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 testParser2(self):
        print("Parser 2")
        lex  = Lexer(self.example1)
        expr1 = parseForm(lex)
        print(expr1)

        expr2 = parseForm(lex)
        print(expr2)

        expr3 = parseForm(lex)
        print(expr3)

        expr4 = parseForm(lex)
        print(expr4)

        lex  = Lexer(self.example2)
        expr1 = parseForm(lex)
        print(expr1)

        expr2 = parseForm(lex)
        print(expr2)


    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()