##############################################

import itertools

from time import time

##############################################
##############################################
##############################################


"""
Autoepigraph: Model-based Theorem Prover 
for Epistemic graphs for Argumenation.
25 April 2019
"""


##############################################
##############################################
##############################################


"""Format of formulae is as follows:
- an argument is represented by a letter
- a term is an argument or a Boolean combination 
of terms in prefix form with connectives being
&, v, and - symbols
- an epiatom is a triple [term,comparator,value]
where comparator is L,LE,E,GE, or G (denoting 
less than, less than or equal to, equal, greater 
than or equal, or greater than, respectively), and
value is a value in the unit interval.
- an epiformula is an epiatom or a Boolean 
combination of epiformula with connectives being
OR, AND, NOT, IMPLIES."""



##############################################
##############################################
##############################################
"""Method for testing model building. Each code x is 
for a different formula. Also, some options 
for the value set and for the atom set are given"""


def run(x):
        pi = [0,0.5,1]
        #pi = [0,0.25,0.5,0.75,1]
        #pi = [0,0.1,0.2,0.3,0.4,0.5,0.6,0.7,0.8,0.9,10]
        #atoms = ["a","b"]
        #atoms = ["a","b","c","d","e"]
        #atoms = ["a","b","c","d"]
        atoms = ["a","b","c"]
        if x == -1:
                epiformula = ["NOT",["a","E",1]]   
        if x == 0:
                epiformula = ["a","E",1] 
        if x == 1:
                epiformula = ["a + -a","LE",1]
        if x == 2:
                epiformula = ["a","GE",0]
        if x == 3:
                epiformula = [["a","G",0.5],"IMPLIES",["b","LE",0.5]]
        if x == 4:
                epiformula = [["NOT",["a","G",0.5]],"OR",["b","LE",0.5]]
        if x == 5:
                epiformula = ["-(v(a,b))","E",1]
        if x == 6:
                epiformula = ["&(-a,-b)","E",1]
        if x == 7:
                epiformula = ["&(v(a,-a),v(b,-b))","E",1]
        if x == 8:
                epiformula = ["-(-(a))","E",1]
        if x == 9:
                epiformula = ["a","E",1]
        if x == 10:
                epiformula = [[["a","G",0.5],"AND",["b","LE",0.5]],"AND",["a","LE",1]]
        if x == 20:
                epiformula = ["a + b","GE",0.9]
        if x == 40:
                epiformula = ["v(v(a,b),c)","E",0.5]
        getmodels(epiformula,pi,atoms)
   

     
##############################################
##############################################
##############################################
"""Method for testing entailment. Each code x is 
for different pair for formulae. Also, some options 
for the value set and for the atom set are given"""


def go(x):
        #t0 = time()
        #pi = [0,0.5,1]
        pi = [0,0.25,0.5,0.75,1]
        #pi = [0,0.2,0.4,0.6,0.8,1.0]
        #pi = [0,0.125,0.25,0.375,0.5,0.625,0.75,0.875,1.0]
        #pi = [0,0.1,0.2,0.3,0.4,0.5,0.6,0.7,0.8,0.9,1.0]
        #atoms = ["a","b"]
        #atoms = ["a","b","c"]
        #atoms = ["b","c","d"]
        atoms = ["a","b","c","d"]
        #atoms = ["c","d"]
        #atoms = ["a","c","d"]
        #atoms = ["a","b","c","d","e"]
        if x == 1:
                formula1 = ["a","E",1]
                formula2 = ["a","LE",1]
        if x == 2:
                formula1 = ["-(-a)","E",1]
                formula2 = ["a","E",1]
        if x == 3:
                formula1 = [["a","E",1],"AND",["b","GE",0.5]]
                formula2 = ["a","E",1]
        if x == 4:
                formula1 = ["a + -a","LE",1]
                formula2 = [["a","G",0.5],"IMPLIES",["b","LE",0.5]]
        if x == 5:
                formula1 = [["a","G",0.5],"IMPLIES",["b","LE",0.5]]
                formula2 = ["a + -a","LE",1]
        if x == 6:
                formula1 = ["a + b","LE",1]
                formula2 = [["a","G",0.5],"IMPLIES",["b","LE",0.5]]
        if x == 7:
                formula1 = [["a","G",0.5],"IMPLIES",["b","LE",0.5]]
                formula2 = ["a + b","LE",1]
        if x == 8:
                formula1 = ["a + b","LE",1] 
                formula2 = ["a","LE",1]
        if x == 9:
                formula1 = [[[["b","L",0.5],"AND",["c","G",0.5]],"AND",["d","G",0.5]],"IMPLIES",["a","G",0.5]]
                formula2 = [[["b","L",0.5],"AND",["&(c,d)","G",0.5]],"IMPLIES",["a","G",0.5]]
        if x == 10:
                formula2 = [[[["b","L",0.5],"AND",["c","G",0.5]],"AND",["d","G",0.5]],"IMPLIES",["a","G",0.5]]
                formula1 = [[["b","L",0.5],"AND",["&(c,d)","G",0.5]],"IMPLIES",["a","G",0.5]]
        if x == 11:
                formula1 = [[["c","G",0.5],"AND",["d","G",0.5]],"IMPLIES",["a","G",0.5]]
                formula2 = [["&(c,d)","G",0.5],"IMPLIES",["a","G",0.5]]
        if x == 110:
                formula2 = [[["c","G",0.5],"AND",["d","G",0.5]],"IMPLIES",["a","G",0.5]]
                formula1 = [["&(c,d)","G",0.5],"IMPLIES",["a","G",0.5]]
        if x == 12:
                formula1 = [["c","G",0.5],"AND",["d","G",0.5]]
                formula2 = ["&(c,d)","G",0.5]
        if x == 13:
                formula2 = [["c","G",0.5],"AND",["d","G",0.5]]
                formula1 = ["&(c,d)","G",0.5]
        
        if x == 20:
                formula1 = [["a","L",0.9],"AND",["a","G",0.7]]
                formula2 = [["a","G",0.7],"AND",["NOT",["a","GE",0.9]]]
        if x == 21:
                formula2 = [["a","L",0.9],"AND",["a","G",0.7]]
                formula1 = [["a","G",0.7],"AND",["NOT",["a","GE",0.9]]]
                
        if x == 30:
                formula1 = [[[["b","L",0.5],"AND",["c","G",0.5]],"AND",["d","G",0.5]],"IMPLIES",["b","G",0.5]]
                formula2 = [[["b","L",0.5],"AND",["&(c,d)","G",0.5]],"IMPLIES",["b","G",0.5]]
               
        if x == 31:
                formula2 = [[[["b","L",0.5],"AND",["c","G",0.5]],"AND",["d","G",0.5]],"IMPLIES",["b","G",0.5]]
                formula1 = [[["b","L",0.5],"AND",["&(c,d)","G",0.5]],"IMPLIES",["b","G",0.5]]
               
        if x == 40:
                formula1 = [[[["a","G",0.5],"OR",["b","G",0.5]],"OR",["c","G",0.5]],"OR",["d","G",0.5]]
                formula2 = ["v(v(v(a,b),c),d)","G",0.5]
        if x == 41:
                formula2 = [[[["a","G",0.5],"OR",["b","G",0.5]],"OR",["c","G",0.5]],"OR",["d","G",0.5]]
                formula1 = ["v(v(v(a,b),c),d)","G",0.5]
               
                
        entailment(formula1,formula2,pi,atoms)
        
##############################################
##############################################
"""Top level method for testing for entailment"""

def entailment(formula1,formula2,pi,atoms):
        models1 = getmodels(formula1,pi,atoms)
        models2 = getmodels(formula2,pi,atoms)
        print("\n")
        if subset(models1,models2):
                print(str(formula1) + "\t" + str(len(models1)))
                print("entails ")
                print(str(formula2) + "\t" + str(len(models2)))             
        else:
                print(str(formula1) + "\t" + str(len(models1)))
                print("does not entail ")
                print(str(formula2) + "\t" + str(len(models2)))             

##############################################
##############################################
"""Top level method for getting models for a formula"""


def getmodels(epiformula,pi,atoms):
        models = doEpiformula(epiformula,pi,atoms)
#        print("\nModels of "+str(epiformula)+ " are \n")
#        for model in models:
#               print("\t"+str(model))
#        print("\n")
        return models
                

##############################################
##############################################
"""Decompose epiformulae recursively to epiatoms 
via disjunction, conjunction, and negation"""

def doEpiformula(epiformula,pi,atoms):
        #print("Doing epiformula = "+str(epiformula))
        if isEpiatom(epiformula):
                models = doEpiatom(epiformula,pi,atoms)
        else:
                if epiformula[0] == "NOT":
                        submodels = doEpiformula(epiformula[1],pi,atoms)
                        models = complementation(submodels,pi,atoms)
                if epiformula[1] == "AND":
                        submodels1 = doEpiformula(epiformula[0],pi,atoms)
                        submodels2 = doEpiformula(epiformula[2],pi,atoms)
                        models = intersection(submodels1,submodels2)
                if epiformula[1] == "OR":
                        submodels1 = doEpiformula(epiformula[0],pi,atoms)
                        submodels2 = doEpiformula(epiformula[2],pi,atoms)
                        models = union(submodels1,submodels2)
                if epiformula[1] == "IMPLIES":
                        submodels1 = doEpiformula(epiformula[0],pi,atoms)
                        submodels2 = doEpiformula(epiformula[2],pi,atoms)
                        submodels3 = complementation(submodels1,pi,atoms)
                        models = union(submodels2,submodels3)
                        #print("\nComplement of "+str(epiformula[0]))
                        #for x in submodels3:
                        #    print(str(x))
        #print("\n"+str(epiformula)+ " => "+str(models))
        return models
    
##############################################
##############################################
"""Decopose epiatom via the operational rule""" 
    
def doEpiatom(epiatom,pi,atoms):
        #print("\n")
        #print("Doing epiatom = "+str(epiatom))
        opformula = epiatom[0]
        comparator = epiatom[1]
        value = epiatom[2]
        #flatatoms = []
        optuple = getoperators(opformula)
        termtuple = getterms(opformula)
        #print("\n")
        #print("Optuple = "+str(optuple))
        #print("Termtuple = "+str(termtuple))
        newvaluetuples = getvaluetuples(pi,optuple,termtuple,comparator,value)
        #print("Value tuple ="+str(newvaluetuples))
        models = [] 
        for vtuple in newvaluetuples:
                i = 0
                conjunctionmodels = []
                while i < len(termtuple):
                        submodels = doFlatatom([termtuple[i],vtuple[i]],pi,atoms)
                        #print(str(submodels))
                        conjunctionmodels.append(submodels)
                        #intersection(conjunctionmodels,submodels)
                        i = i+1
                if len(conjunctionmodels) <= 1:
                        cmodels = conjunctionmodels[0]
                        newmodels = models[:] + cmodels
                else:
                        model = conjunctionmodels.pop(0)
                        newmodels = model[:]
                        for model2 in conjunctionmodels:
                                newmodels = intersection(model2,newmodels[:])
                models = union(newmodels[:],models[:])
        #print(str(epiatom))
        #print(str(models))
        #print("\n"+str(epiatom)+ " => "+str(models))
        #for x in models:
            #print("\t"+str(x))
        return models
        
##############################################
##############################################
""" getvaluetuples is used by doEpiatom method to get the combination set"""
        
def getvaluetuples(pi,optuple,termtuple,comparator,value):
    n = len(optuple)+1
    #print("n = "+str(n))
    sums = [[]]
    for i in range(0,n):
        newsums = []
        for x in sums:
            for v in pi:
                y = x[:]
                y.append(v)
                newsums.append(y)
        sums = newsums[:]
    goodsums = []
    for x in sums:
        if correctsum(x,optuple,comparator,value):
                goodsums.append(x)
    return goodsums


def correctsum(numbers,optuple,comparator,number):
    total = numbers[0]
    i = 0
    #print("numbers = "+str(numbers))
    #print("optuple = "+str(optuple))
    while i < len(optuple):
        #print("i = "+str(i))
        if optuple[i] == "+":
            total = total + numbers[i+1]
        else:
            total = total - numbers[i+1]
        i = i+1
    if comparator == "G" and total > number:
        return True
    elif comparator == "GE" and total >= number:
        return True
    elif comparator == "E" and total == number:
        return True
    elif comparator == "LE" and total <= number:
        return True
    elif comparator == "L" and total < number:
        return True
    else:
        return False


##############################################
##############################################
"""Decompose the flatatom to set of models via the term rule"""

def doFlatatom(flatatom,pi,atoms):
        #print("Doing flatatom = "+str(flatatom))
        term = flatatom[0]
        total = flatatom[1]
        modelset = genmodels(pi,atoms)
        satisfyingmodels = []
        for model in modelset:
                #print(str(model))
                currentsum = 0
                for [world,value] in model:
                    if satisfy(world,term):
                        #print(term+"\t\t satisfied by " +str(world))
                        currentsum = currentsum + value
                        #print(currentsum)
                if currentsum == total:
                    satisfyingmodels.append(model)
        #print(str(satisfyingmodels))
        #print("\n"+str(flatatom)+ " => "+str(satisfyingmodels))
        #for x in satisfyingmodels:
        #        print(str(x))
        return satisfyingmodels


##############################################
##############################################
"""Subsidiary methods"""


def isEpiatom(epiformula):
        #print("Is epistemic atom = "+str(epiformula))
        #print(str(epiformula[1]))
        if epiformula[1] in ["L","LE","E","GE","G"]:
                return True
        else:
                return False



def removeredundant(mylist):
    newlist = []
    for x in mylist:
        if x not in newlist:
            newlist.append(x)
    return newlist
    


def complementation(submodels,pi,atoms):
        modelsetextra = genmodels(pi,atoms)
        modelset = removeredundant(modelsetextra)
        #print("\nmodelset")
        #for x in modelset:
        #    print(x)
        models = []
        for model in modelset:
                if model not in submodels:
#                        True
#                else:
                    #print("Add = "+str(model))
                    models.append(model)
        return models



def union(alist1,alist2):
    models = removeredundant(alist1+alist2)
    return models

            


def intersection(alist1,alist2):
        models = []
        for model in alist1:
                if model in alist2:
                        models.append(model)
        return models



def subset(alist,blist):
        #print(str(alist))
        #print(str(blist))
        for x in alist:
                #print(str(x))
                if not(x in blist):
                        #print("fail")
                        return False
        return True


def getoperators(opformula):
    oplist = []
    for x in opformula.split():
        if x in ["+","-"]:
            oplist.append(x)
    return oplist


def getterms(opformula):
    termlist = []
    for x in opformula.split():
        if x not in ["+","-"]:
            termlist.append(x)
    return termlist


def getvalues(comparator,value,pi):
        greaterthan = []
        lessthan = []
        for x in pi:
                if x > value:
                        greaterthan.append(x)
                elif x < value:
                        lessthan.append(x)
        values = []
        if comparator == "G":
              values = greaterthan[:]
        elif comparator == "GE":
              values = [value]+greaterthan[:]
        elif comparator == "E":
              values = [value]
        elif comparator == "LE":
              values = lessthan[:]+[value]
        elif comparator == "L":
              values = lessthan[:]
        return values
              
def genpowerset(X):
    allsets = [[]]
    for x in X:
        newsets = []
        for s in allsets:
            t = s[:]
            t.append(x)
            newsets.append(t)
        allsets = allsets+newsets
    return allsets

               
           
def sumsto(numbers,number):
    total = 0
    for k in numbers:
        total = total + k
    if total == number:
        return True
    else:
        return False

##############################################
##############################################
""" Methods for handling terms """



def satisfy(world,formula):
    #print("Trying to satisfy\t"+formula+"\t\t with world " +str(world))
    if ispositiveliteral(formula):
        if formula in world:
            #print("yes")
            return True
        else:
            return False
    elif isnegativeliteral(formula):
        if formula[1] in world:
            return False
        else:
            #print("yes")
            #print("neg literal\t"+str(formula))
            return True
    elif isconjunction(formula):
        conjuncts = getjuncts(formula)
        #print("conjuncts\t"+str(conjuncts))
        return satisfy(world,conjuncts[0]) and satisfy(world,conjuncts[1])
    elif isdisjunction(formula):
        disjuncts = getjuncts(formula)
        return satisfy(world,disjuncts[0]) or satisfy(world,disjuncts[1])
    elif isnegation(formula):
        subformula = formula[2:-1]
        return complement(satisfy(world,subformula))




def isatom(formula):
    if formula in ["-","&","v","(",")",","]:
        return False
    else:
        return True


def ispositiveliteral(formula):
    if len(formula) == 1 and isatom(formula):
        return True
    else:
        return False


def isnegativeliteral(formula):
    if formula[0] == "-" and len(formula) == 2:
        return True
    else:
        return False

def isconjunction(formula):
    if formula[0] == "&":
        return True
    else:
        return False
    

def isdisjunction(formula):
    if formula[0] == "v":
        return True
    else:
        return False

def isnegation(formula):
    if formula[0] == "-":
        return True
    else:
        return False

def complement(value):
    if value == True:
        return False
    else:
        return True

def getjuncts(formula):
    formula = formula[2:-1]
    if isatom(formula[0]):
        junct1 = formula[0]
        junct2 = formula[2:]
    else:
        i = 0
        unclosed = 0
        while unclosed != 0 or formula[i] != ",":
            #print("i = " + str(i) + "\t" + str(formula[i]))
            if formula[i] == "(":
                unclosed = unclosed+1
            elif formula[i] == ")":
                unclosed = unclosed-1
            i = i+1
        #print(str(i))
        junct1 = formula[:i]
        junct2 = formula[i+1:]
    return [junct1,junct2]
    
##############################################
##############################################
##############################################
##############################################
##############################################
##############################################
##############################################
""" The genmodels method generates the models 
for a set of restructed values and set 
of atoms"""

def genmodels(pi,atoms):
    atompowerset = genpowerset(atoms)
    n = pow(2,len(atoms))
    #print("n = "+str(n))
    sumtuples = newgensums(n,pi,1)
    models = []
    for currentsumtuple in sumtuples:
        model = []
        i = 0
        while i < len(currentsumtuple):
            world = atompowerset[i]
            value = currentsumtuple[i]
            pair = [world,value]
            model.append(pair)
            i = i+1
        #print(str(model))
        models.append(model)
    return models



def newgensums(n,pi,k):
        goodcardtuples = multisets(n,pi,k)
        combinations = []
        #print("\n")
        for x in goodcardtuples:
                #print(str(x))
                combination = []
                for i in range(1,len(x)):
                        combination = combination + values(x[i],pi[i])
                #print(str(combination))
                combinations.append(combination)
        zeroarray = getzeros(n)
        gensums = []
        #print("\n")
        for combo in combinations:
                alist = []
                for y in range(0,n):
                        alist.append(y)
                        
                indexlists = list(itertools.permutations(alist,len(combo)))
                #print(str(indexlists))
                for indexlist in indexlists:
                        #print("indexlist = "+str(indexlist))
                        perm = zeroarray[:]
                        i = 0
                        while i < len(indexlist):
                                #print("\ti = "+str(i))
                                index = indexlist[i]
                                #print("\tindex = "+str(index))
                                perm[index] = combo[i]
                                #print("\tvalue = "+str(perm[index]))
                                i = i+1
                        gensums.append(perm)
                        #print(str(perm))
        return gensums


def getzeros(n):
        alist = []
        while n > 0:
                alist.append(0)
                n = n - 1
        return alist

     

def multisets(n,pi,k):
        cardtuples = [[0]]
        for i in range(1,len(pi)):
                newcardtuples = []
                for cardtuple in cardtuples:
                        for c in range(0,n):
                                newcardtuple = cardtuple[:]
                                newcardtuple.append(c)
                                newcardtuples.append(newcardtuple)
                cardtuples = newcardtuples[:]
        goodcardtuples = []
        for x in cardtuples:
                #print("\t"+str(x))
                if computes(x,pi,k):
                        #print("\t"+str(x))
                        goodcardtuples.append(x)
        return goodcardtuples

def computes(x,pi,k):
        sum = 0
        for i in range(0,len(x)):
                product = x[i] * pi[i]
                sum = sum+product
        #print(str(sum))
        if sum == k:
                return True
        else:
                return False
        

def values(card,value):
        alist = []
        while card > 0:
                alist.append(value)
                card = card - 1
        return alist
      

###############################################################################
###############################################################################
"""Code to run time trials"""
        
def goaverage(code,cycles):
    total = 0
    for i in range(0,cycles):
        t0 = time()
        go(code)
        t1 = time()
        print(str(t1-t0))
        total = total+(t1-t0)
    average = total/cycles
    print("\nAverage " + str(average))

    
    
###############################################################################
###############################################################################

#go(41)
goaverage(41,10)
#run(-1)
#run(20)
#for x in [9,10,11,110,12,13,20,21]:
####range(1,9):
#    print("\n Code = "+str(x)+"\n")
#    go(x)

##############################################
##############################################
##############################################
##############################################
##############################################
##############################################
##############################################
##############################################
##############################################