sawine@12: """
sawine@13: Name: sml - Simple Modal Logic Lib.
sawine@17: Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax.
sawine@12: Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
sawine@12: """
sawine@12: 
sawine@26: TMP_DIMACS = "dimacs~"
sawine@26: TMP_SOLUTION = "solution~"
sawine@26: 
sawine@12: def main():
sawine@15:     # edit your formulae here
sawine@23:     p = Variable("p")
sawine@23:     q = Variable("q")
sawine@23:     r = Variable("r") 
sawine@23:     s = Variable("s")
sawine@23:     formula1 = Imp(Eq(p, q), r)
sawine@23:     formula2 = Not(Or(p, q))
sawine@23:     formula3 = Not(Not(p))
sawine@23:     formula4 = Imp(Box(Imp(Diamond(p), p)), Box(Imp(p, Box(p))))
sawine@23:     formula5 = Imp(And(Or(p, q), r), Not(s))
sawine@25:     formula6 = And(Or(p, Or(q, Not(s))), And(Or(r, Not(s)), Or(Not(p), s)))
sawine@25:     formula = formula6 # choose your formula here
sawine@12: 
sawine@25:     args = parse_arguments()   
sawine@12:     if (args.formula):
sawine@12:         scanner = Scanner(TOKENS)
sawine@12:         parser = Parser(SYNTAX, scanner)
sawine@12:         (accepted, out, tree_nodes) = parser.parse(args.formula)
sawine@12:         if not accepted:
sawine@12:             print EXCUSE 
sawine@12:             return
sawine@12:         tree = SyntaxTree(out, tree_nodes) 
sawine@12:         formula = tree.root
sawine@12:    
sawine@22:     original = formula
sawine@22:     print "formula: \t\t\t%s [%i]" % (formula, formula.depth())
sawine@20:     formula = expand_imp_eq(formula)
sawine@22:     print "expanded -> and <->: \t\t%s [%i]" % (formula, formula.depth()) 
sawine@20:     formula = de_morgan(formula)
sawine@22:     print "reduced ~: \t\t\t%s [%i]" % (formula, formula.depth()) 
sawine@20:     formula = reduce_iter(formula)
sawine@22:     print "reduced iterated modalities: \t%s [%i]" % (formula, formula.depth()) 
sawine@20:     formula = reduce_iter(dist_mod((formula)))
sawine@22:     print "distributed modalities+: \t%s [%i]" % (formula, formula.depth()) 
sawine@21:     formula = mcnf(formula)
sawine@22:     print "alpha mcnf: \t\t\t%s [%i]" % (formula, formula.depth())
sawine@26:     #cnf_formula = cnf(original)
sawine@26:     #print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())
sawine@26:     
sawine@26:     if not args.dimacs:
sawine@26:         dimacs_file = TMP_DIMACS
sawine@26:     else:
sawine@26:         dimacs_file = args.dimacs
sawine@26:     solution = sat_test(original, dimacs_file)
sawine@26:     if solution:
sawine@26:         print "satisfiable: \t\t\t%s " % (", ".join([str(s) for s in solution]))
sawine@26:     else:
sawine@26:         print "not satisfiable"
sawine@26:     
sawine@26: from subprocess import call, PIPE
sawine@19: 
sawine@26: def sat_test(formula, dimacs_file):
sawine@26:     out, variables = dimacs(formula)
sawine@26:     with open(dimacs_file, "w") as f:
sawine@26:         f.write(out) 
sawine@26:     call(["minisat2", "-verb=0", dimacs_file, TMP_SOLUTION], stdout=PIPE)
sawine@26:     with open(TMP_SOLUTION) as f:
sawine@26:         solved, assignment = f.readlines()  
sawine@26:     solved = solved[0] == "S"      
sawine@26:     if solved:
sawine@26:         positive = set() 
sawine@26:         for a in assignment.split():           
sawine@26:             neg = a[0] == "-"
sawine@26:             if not neg:
sawine@26:                 positive.add(int(a))       
sawine@26:         solution = []
sawine@26:         for v, n in variables.iteritems():           
sawine@26:             if n in positive:              
sawine@26:                 solution.append(Variable(v))
sawine@26:             else:
sawine@26:                 solution.append(Not(Variable(v)))
sawine@26:         return solution
sawine@25: 
sawine@25: def dimacs(formula):
sawine@25:     def clausify(f):        
sawine@25:         if f.id == AND:    
sawine@25:             c1 = clausify(f.values[0])   
sawine@25:             c2 = clausify(f.values[1])   
sawine@25:             if c1:
sawine@25:                 clauses.append(clausify(f.values[0]))  
sawine@25:             if c2:
sawine@25:                 clauses.append(clausify(f.values[1]))              
sawine@25:         if f.id == OR:
sawine@25:             clause = []         
sawine@25:             clause.extend(clausify(f.values[0]))
sawine@25:             clause.extend(clausify(f.values[1]))            
sawine@25:             return clause
sawine@25:         if f.id == NOT:
sawine@25:             return ["-" + clausify(f.values[0])]
sawine@25:         if f.id == VARIABLE:
sawine@25:             if f.values[0] in variables:
sawine@25:                 n = variables[f.values[0]]
sawine@25:             else:
sawine@25:                 n = len(variables) + 1
sawine@25:                 variables[f.values[0]] = n
sawine@25:             return str(n)
sawine@25:       
sawine@25:     variables = {}
sawine@25:     clauses = []
sawine@25:     clausify(formula)
sawine@25:     out = "c DIMACS CNF input file generated by sml\n"
sawine@25:     out += "c Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>\n"
sawine@25:     out += "p cnf %i %i\n" % (len(variables), len(clauses))    
sawine@25:     out += " 0\n".join([" ".join(c) for c in clauses]) + " 0\n"
sawine@26:     return out, variables
sawine@25: 
sawine@19: def values(fun, f):  
sawine@19:     return [fun(v) for v in f.values] 
sawine@12: 
sawine@14: def expand_imp_eq(formula):  
sawine@23:     expmap = {IMP: lambda (a, b): Or(Not(a), b),
sawine@23:               EQ: lambda (a, b): And(Or(Not(a), b), Or(a, Not(b)))}   
sawine@20:     if not isinstance(formula, Operator):   
sawine@12:         return formula
sawine@20:     if formula.id in expmap:
sawine@20:         return expmap[formula.id](values(expand_imp_eq, formula))   
sawine@23:     return formula.__class__(*values(expand_imp_eq, formula))
sawine@14: 
sawine@20: def de_morgan(formula):    
sawine@23:     negmap = {AND: lambda (a, b): Or(negate(a), negate(b)),
sawine@23:               OR: lambda (a, b): And(negate(a), negate(b)),
sawine@23:               BOX: lambda (a,): Diamond(negate(a)),
sawine@23:               DIAMOND: lambda (a,): Box(negate(a)),
sawine@23:               VARIABLE: lambda (a,): Not(Variable(a)),
sawine@19:               NOT: lambda (a,): a}    
sawine@14:     def negate(f):
sawine@20:         return negmap[f.id](f.values)
sawine@14:     if not isinstance(formula, Operator):
sawine@18:         return formula  
sawine@14:     if formula.id == NOT:
sawine@14:         return negate(formula.values[0])
sawine@23:     return formula.__class__(*values(de_morgan, formula))
sawine@18: 
sawine@18: def reduce_iter(formula):  
sawine@18:     redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))
sawine@18:     if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
sawine@18:         return formula
sawine@18:     ids = (formula.id, formula.values[0].id)
sawine@18:     if ids in redset:
sawine@18:         return reduce_iter(formula.values[0])
sawine@23:     return formula.__class__(*values(reduce_iter, formula))
sawine@19: 
sawine@20: def dist_mod(formula):    
sawine@23:     distmap = {(BOX, AND): lambda (a, b): And(Box(a), Box(b)),
sawine@23:                (DIAMOND, OR): lambda (a, b): Or(Diamond(a), Diamond(b)),
sawine@19:                (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))               
sawine@23:                and Or(Box(a), Box(b)) or Box(Or(a, b)),
sawine@19:                (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))
sawine@23:                and And(Diamond(a), Diamond(b)) or Diamond(And(a, b))}   
sawine@19:     if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
sawine@19:         return formula
sawine@19:     ids = (formula.id, formula.values[0].id)
sawine@19:     if ids in distmap:
sawine@24:         return distmap[ids](values(dist_mod, formula.values[0]))
sawine@23:     return formula.__class__(*values(dist_mod, formula))    
sawine@21: 
sawine@21: def mcnf(formula):
sawine@21:     if formula.id == OR:
sawine@21:         conj_id = int(formula.values[1].id == AND) 
sawine@23:         return And(Or(formula.values[conj_id].values[0], formula.values[1 - conj_id]), 
sawine@23:                     Or(formula.values[conj_id].values[1], formula.values[1 - conj_id]));
sawine@22:     return formula
sawine@22: 
sawine@22: def cnf(formula):      
sawine@22:     def part(f):
sawine@22:         for v in f.values:
sawine@22:             if v.id != VARIABLE:
sawine@22:                 sub_formulae.append(v)
sawine@25:                 part(v) 
sawine@25: 
sawine@25:     def conjunct(f):
sawine@25:         if len(bicon):
sawine@25:             return And(f, conjunct(bicon.pop()))
sawine@25:         return f
sawine@25: 
sawine@22:     sub_formulae = [formula]
sawine@22:     part(formula)
sawine@22:     sub_formulae.reverse() 
sawine@22:     known = {}
sawine@22:     bicon = []
sawine@22:     for s in sub_formulae:       
sawine@22:         for i, v in enumerate(s.values):
sawine@22:             if v in known:
sawine@22:                 s.values[i] = known[v]
sawine@23:         bicon.append(Eq(Variable("x" + str(len(bicon))), s))
sawine@25:         known[s] = bicon[-1].values[0]     
sawine@22:     return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula]))))))
sawine@22: 
sawine@22: """ The Parser - Do NOT look below this line! """ 
sawine@23: import re
sawine@22: 
sawine@12: NOT = "~"
sawine@12: AND = "&"
sawine@12: OR = "|"
sawine@12: IMP = "->"
sawine@12: EQ = "<->"
sawine@12: BOX = "[]"
sawine@12: DIAMOND = "<>"
sawine@14: VARIABLE = "VAR"
sawine@12: LB = "("
sawine@12: RB = ")"
sawine@12: 
sawine@12: class Operator(object):
sawine@23:     def __init__(self, id, arity, *values):
sawine@12:         self.id = id         
sawine@12:         self.arity = arity
sawine@23:         self.values = list(values)
sawine@20:     def depth(self):       
sawine@20:         if self.arity == 0:
sawine@20:             return 0
sawine@20:         if self.id in (BOX, DIAMOND):
sawine@20:             return 1 + self.values[0].depth()
sawine@20:         if self.id == NOT:           
sawine@23:             return self.values[0].depth()       
sawine@20:         return max(self.values[0].depth(), self.values[1].depth())
sawine@22:     def __eq__(self, other):
sawine@22:         return self.id == other.id and self.values == other.values # commutative types not considered yet
sawine@12:     def __str__(self):
sawine@12:         out = self.id
sawine@12:         if self.arity == 0:
sawine@20:             out = str(self.values[0])           
sawine@12:         if self.arity == 1:
sawine@12:             out = self.id + str(self.values[0])
sawine@12:         elif self.arity  == 2:          
sawine@12:             out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"
sawine@12:         return out
sawine@12: 
sawine@12: class Not(Operator):
sawine@12:     arity = 1
sawine@23:     def __init__(self, *values):
sawine@23:         Operator.__init__(self, NOT, Not.arity, *values)       
sawine@12:     def __call__(self):
sawine@12:         pass
sawine@12: 
sawine@12: class And(Operator):
sawine@12:     arity = 2
sawine@23:     def __init__(self, *values):
sawine@23:         Operator.__init__(self, AND, And.arity, *values)
sawine@12:        
sawine@12: class Or(Operator):
sawine@12:     arity = 2
sawine@23:     def __init__(self, *values):
sawine@23:         Operator.__init__(self, OR, Or.arity, *values)       
sawine@12: 
sawine@12: class Imp(Operator):
sawine@12:     arity = 2
sawine@23:     def __init__(self, *values):
sawine@23:         Operator.__init__(self, IMP, Imp.arity, *values)
sawine@12:     
sawine@12: class Eq(Operator):
sawine@12:     arity = 2
sawine@23:     def __init__(self, *values):
sawine@23:         Operator.__init__(self, EQ, Eq.arity, *values)
sawine@12:     
sawine@12: class Box(Operator):
sawine@12:     arity = 1
sawine@23:     def __init__(self, *values):
sawine@23:         Operator.__init__(self, BOX, Box.arity, *values)
sawine@12: 
sawine@12: class Diamond(Operator):
sawine@12:     arity = 1
sawine@23:     def __init__(self, *values):
sawine@23:         Operator.__init__(self, DIAMOND, Diamond.arity, *values)
sawine@12:     
sawine@12: class Variable(Operator):
sawine@12:     arity = 0
sawine@23:     def __init__(self, *values):
sawine@23:         Operator.__init__(self, VARIABLE, Variable.arity, *values)   
sawine@12: 
sawine@12: class Lb(Operator):
sawine@12:     arity = -1
sawine@23:     def __init__(self, *values):
sawine@23:         Operator.__init__(self, LB, Lb.arity, *values)
sawine@12: 
sawine@12: class Rb(Operator):
sawine@12:     arity = -1
sawine@23:     def __init__(self, *values):
sawine@23:         Operator.__init__(self, RB, Rb.arity, *values)
sawine@12: 
sawine@12: class Formula(object):
sawine@12:     def __init__(self):
sawine@12:         pass 
sawine@12: 
sawine@12: TOKENS = {re.compile("\("): Lb,
sawine@12:           re.compile("\)"): Rb,
sawine@12:           re.compile("~"): Not,
sawine@12:           re.compile("&"): And,
sawine@12:           re.compile("\|"): Or,
sawine@12:           re.compile("->"): Imp,
sawine@12:           re.compile("<->"): Eq,
sawine@12:           re.compile("\[\]"): Box,
sawine@12:           re.compile("<>"): Diamond,
sawine@12:           re.compile("[a-z]+"): Variable}
sawine@12:          
sawine@12: class Scanner(object):
sawine@12:     def __init__(self, tokens, source=None):
sawine@12:         self.tokens = tokens
sawine@12:         self.reset(source)
sawine@12:     def next(self):         
sawine@12:         while self.i < len(self.source):
sawine@12:             re.purge()
sawine@12:             for p, token in self.tokens.iteritems():
sawine@12:                 m = p.match(self.source[self.i:])               
sawine@12:                 if m:                  
sawine@12:                     self.i += m.end(0)
sawine@12:                     value = m.group(0)  
sawine@12:                     return (token, value)
sawine@12:             self.i += 1
sawine@12:         return (None, None)
sawine@12:     def reset(self, source):
sawine@12:         self.i = 0
sawine@12:         self.source = source
sawine@12: 
sawine@12: S = Formula
sawine@12: A = "A"
sawine@12: #0 S: (Variable,),
sawine@12: #1 S: (Not, S),
sawine@12: #2 S: (Lb, A, Rb),
sawine@12: #3 S: (Box, S),
sawine@12: #4 S: (Diamond, S),
sawine@12: #5 A: (S, And, S),
sawine@12: #6 A: (S, Or, S),
sawine@12: #7 A: (S, Imp, S),
sawine@12: #8 A: (S, Eq, S)
sawine@12: SYNTAX = ((Variable,),
sawine@12:           (Not, S),
sawine@12:           (Lb, A, Rb),
sawine@12:           (Box, S),
sawine@12:           (Diamond, S),
sawine@12:           (S, And, S),
sawine@12:           (S, Or, S),
sawine@12:           (S, Imp, S),
sawine@12:           (S, Eq, S))
sawine@12: 
sawine@12: class Parser(object):
sawine@12:     def __init__(self, syntax, scanner):
sawine@12:         self.syntax = syntax
sawine@12:         self.scanner = scanner
sawine@12:     def parse(self, source):
sawine@12:         table = {(S, Variable): 0,
sawine@12:                  (S, Not): 1,
sawine@12:                  (S, Lb): 2,
sawine@12:                  (S, Box): 3,
sawine@12:                  (S, Diamond): 4,
sawine@12:                  (A, S, And): 5,
sawine@12:                  (A, S, Or): 6,
sawine@12:                  (A, S, Imp): 7,
sawine@12:                  (A, S, Eq): 8,
sawine@12:                  (A, Variable, And): 5,
sawine@12:                  (A, Variable, Or): 6,
sawine@12:                  (A, Variable, Imp): 7,
sawine@12:                  (A, Variable, Eq): 8,
sawine@12:                  (A, Not, Variable, And): 5,
sawine@12:                  (A, Not, Variable, Or): 6,
sawine@12:                  (A, Not, Variable, Imp): 7,
sawine@12:                  (A, Not, Variable, Eq): 8}
sawine@12:         stack = [S]
sawine@12:         tree_nodes = []
sawine@12:         tree = None
sawine@12:         out = []
sawine@12:         self.scanner.reset(source)
sawine@12:         (token, value) = self.scanner.next()
sawine@12:         (lookahead, la_value) = self.scanner.next()
sawine@12:         (lookahead2, la2_value) = self.scanner.next()
sawine@12:         accepted = True 
sawine@12:         while token and len(stack): 
sawine@12:             top = stack[-1]               
sawine@12:             if top == token:
sawine@12:                 tree_nodes.append((token, value))
sawine@12:                 stack.pop()
sawine@12:                 #tree_nodes.append((stack.pop(), value))
sawine@12:                 (token, value) = (lookahead, la_value)
sawine@12:                 (lookahead, la_value) = (lookahead2, la2_value)
sawine@12:                 #(lookahead, _) = self.scanner.next()
sawine@12:                 (lookahead2, la2_value) = self.scanner.next()
sawine@12:             else:
sawine@12:                 action = None
sawine@12:                 if (top, token) in table:
sawine@12:                     action = table[(top, token)]
sawine@12:                 elif (top, token, lookahead) in table:
sawine@12:                     action = table[(top, token, lookahead)]  
sawine@12:                 elif (top, token, lookahead, lookahead2) in table:
sawine@12:                     action = table[(top, token, lookahead, lookahead2)]    
sawine@12:                 if action is None:
sawine@12:                     accepted = False
sawine@12:                     break
sawine@12:                 
sawine@12:                 out.append(action)
sawine@12:                 stack.pop()
sawine@12:                 stack.extend(reversed(self.syntax[action]))
sawine@12:         accepted = accepted and not len(stack)
sawine@12:         return (accepted, out, tree_nodes) 
sawine@12: 
sawine@12: class SyntaxTree(object):
sawine@12:     def __init__(self, seq, tree_nodes):
sawine@12:         seq.reverse()
sawine@12:         tree_nodes.reverse()      
sawine@12:         self.root = self.compile(seq, tree_nodes)[0]       
sawine@12:     def compile(self, seq, tree_nodes):
sawine@12:         stack = []     
sawine@12:         while len(seq):           
sawine@12:             s = seq.pop()
sawine@12:             if s == 0:
sawine@12:                 c, v = tree_nodes.pop()
sawine@12:                 while c != Variable:
sawine@12:                     c, v = tree_nodes.pop()
sawine@12:                 stack.append(Variable(v))
sawine@12:             elif s == 1:
sawine@12:                 stack.append(Not(self.compile(seq, tree_nodes)))
sawine@12:             elif s == 2:
sawine@12:                 stack.extend(self.compile(seq, tree_nodes))
sawine@12:             elif s == 3:
sawine@12:                 stack.append(Box(self.compile(seq, tree_nodes)))
sawine@12:             elif s == 4:
sawine@12:                 stack.append(Diamond(self.compile(seq, tree_nodes)))
sawine@12:             elif s == 5:
sawine@12:                 stack.append(And(self.compile(seq, tree_nodes)))
sawine@12:             elif s == 6:
sawine@12:                 stack.append(Or(self.compile(seq, tree_nodes)))
sawine@12:             elif s == 7:
sawine@12:                 stack.append(Imp(self.compile(seq, tree_nodes)))
sawine@12:             elif s == 8:
sawine@12:                 stack.append(Eq(self.compile(seq, tree_nodes)))       
sawine@12:         return stack   
sawine@12: 
sawine@12: from argparse import ArgumentParser
sawine@12: 
sawine@12: def parse_arguments():
sawine@22:     parser = ArgumentParser(description="Tries to parse simple modal logic syntax and reduces the formula. Edit your formula directly in the code file for best results.")
sawine@22:     parser.add_argument("-f", "--formula", help="provide your own formula here, or better don't") 
sawine@25:     parser.add_argument("-d", "--dimacs", help="output file for the CNF DIMACS output")
sawine@12:     return parser.parse_args()
sawine@12:  
sawine@20: EXCUSE = """The formula was not accepted by me, because I do not like you. It is not personal. I seem to have some issues with formulae with inner nesting and I generally suffer from my hasty implementation. I would like to thank you for your coorporation by providing the formula within the code file itself. Thank you. ~The Parser"""
sawine@12: 
sawine@12: if __name__ == "__main__":
sawine@12:     main()