# HG changeset patch # User Eugen Sawin # Date 1310946938 -7200 # Node ID e4720232cf410f1a8d6fe92104681798e543aa95 # Parent b27fbffacec9711acd0a35a739a01327ecc3bb37 Added zip instead of py. diff -r b27fbffacec9 -r e4720232cf41 downloads/sml.py --- a/downloads/sml.py Mon Jul 18 01:54:27 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,447 +0,0 @@ -""" -Name: sml - Simple Modal Logic Lib. -Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax. -Author: Eugen Sawin -""" - -TMP_DIMACS = "dimacs~" -TMP_SOLUTION = "solution~" - -def main(): - # edit your formulae here - p = Variable("p") - q = Variable("q") - r = Variable("r") - s = Variable("s") - formula1 = Imp(Eq(p, q), r) - formula2 = Not(Or(p, q)) - formula3 = Not(Not(p)) - formula4 = Imp(Box(Imp(Diamond(p), p)), Box(Imp(p, Box(p)))) - formula5 = Imp(And(Or(p, q), r), Not(s)) - formula6 = And(Or(p, Or(q, Not(s))), And(Or(r, Not(s)), Or(Not(p), s))) - formula = formula6 # choose your formula here - - args = parse_arguments() - if (args.formula): - scanner = Scanner(TOKENS) - parser = Parser(SYNTAX, scanner) - (accepted, out, tree_nodes) = parser.parse(args.formula) - if not accepted: - print EXCUSE - return - tree = SyntaxTree(out, tree_nodes) - formula = tree.root - - original = formula - print "formula: \t\t\t%s [%i]" % (formula, formula.depth()) - formula = expand_imp_eq(formula) - print "expanded -> and <->: \t\t%s [%i]" % (formula, formula.depth()) - formula = de_morgan(formula) - print "reduced ~: \t\t\t%s [%i]" % (formula, formula.depth()) - formula = reduce_iter(formula) - print "reduced iterated modalities: \t%s [%i]" % (formula, formula.depth()) - formula = reduce_iter(dist_mod((formula))) - print "distributed modalities+: \t%s [%i]" % (formula, formula.depth()) - formula = mcnf(formula) - print "alpha mcnf: \t\t\t%s [%i]" % (formula, formula.depth()) - #cnf_formula = cnf(original) - #print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth()) - - if not args.dimacs: - dimacs_file = TMP_DIMACS - else: - dimacs_file = args.dimacs - solution = sat_test(original, dimacs_file) - if solution: - print "satisfiable: \t\t\t%s " % (", ".join([str(s) for s in solution])) - else: - print "not satisfiable" - -from subprocess import call, PIPE - -def sat_test(formula, dimacs_file): - out, variables = dimacs(formula) - with open(dimacs_file, "w") as f: - f.write(out) - call(["minisat2", "-verb=0", dimacs_file, TMP_SOLUTION], stdout=PIPE) - with open(TMP_SOLUTION) as f: - solved, assignment = f.readlines() - solved = solved[0] == "S" - if solved: - positive = set() - for a in assignment.split(): - neg = a[0] == "-" - if not neg: - positive.add(int(a)) - solution = [] - for v, n in variables.iteritems(): - if n in positive: - solution.append(Variable(v)) - else: - solution.append(Not(Variable(v))) - return solution - -def dimacs(formula): - def clausify(f): - if f.id == AND: - c1 = clausify(f.values[0]) - c2 = clausify(f.values[1]) - if c1: - clauses.append(clausify(f.values[0])) - if c2: - clauses.append(clausify(f.values[1])) - if f.id == OR: - clause = [] - clause.extend(clausify(f.values[0])) - clause.extend(clausify(f.values[1])) - return clause - if f.id == NOT: - return ["-" + clausify(f.values[0])] - if f.id == VARIABLE: - if f.values[0] in variables: - n = variables[f.values[0]] - else: - n = len(variables) + 1 - variables[f.values[0]] = n - return str(n) - - variables = {} - clauses = [] - clausify(formula) - out = "c DIMACS CNF input file generated by sml\n" - out += "c Author: Eugen Sawin \n" - out += "p cnf %i %i\n" % (len(variables), len(clauses)) - out += " 0\n".join([" ".join(c) for c in clauses]) + " 0\n" - return out, variables - -def values(fun, f): - return [fun(v) for v in f.values] - -def expand_imp_eq(formula): - expmap = {IMP: lambda (a, b): Or(Not(a), b), - EQ: lambda (a, b): And(Or(Not(a), b), Or(a, Not(b)))} - if not isinstance(formula, Operator): - return formula - if formula.id in expmap: - return expmap[formula.id](values(expand_imp_eq, formula)) - return formula.__class__(*values(expand_imp_eq, formula)) - -def de_morgan(formula): - negmap = {AND: lambda (a, b): Or(negate(a), negate(b)), - OR: lambda (a, b): And(negate(a), negate(b)), - BOX: lambda (a,): Diamond(negate(a)), - DIAMOND: lambda (a,): Box(negate(a)), - VARIABLE: lambda (a,): Not(Variable(a)), - NOT: lambda (a,): a} - def negate(f): - return negmap[f.id](f.values) - if not isinstance(formula, Operator): - return formula - if formula.id == NOT: - return negate(formula.values[0]) - return formula.__class__(*values(de_morgan, formula)) - -def reduce_iter(formula): - redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND))) - if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator): - return formula - ids = (formula.id, formula.values[0].id) - if ids in redset: - return reduce_iter(formula.values[0]) - return formula.__class__(*values(reduce_iter, formula)) - -def dist_mod(formula): - distmap = {(BOX, AND): lambda (a, b): And(Box(a), Box(b)), - (DIAMOND, OR): lambda (a, b): Or(Diamond(a), Diamond(b)), - (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box)) - and Or(Box(a), Box(b)) or Box(Or(a, b)), - (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond)) - and And(Diamond(a), Diamond(b)) or Diamond(And(a, b))} - if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator): - return formula - ids = (formula.id, formula.values[0].id) - if ids in distmap: - return distmap[ids](values(dist_mod, formula.values[0])) - return formula.__class__(*values(dist_mod, formula)) - -def mcnf(formula): - if formula.id == OR: - conj_id = int(formula.values[1].id == AND) - return And(Or(formula.values[conj_id].values[0], formula.values[1 - conj_id]), - Or(formula.values[conj_id].values[1], formula.values[1 - conj_id])); - return formula - -def cnf(formula): - def part(f): - for v in f.values: - if v.id != VARIABLE: - sub_formulae.append(v) - part(v) - - def conjunct(f): - if len(bicon): - return And(f, conjunct(bicon.pop())) - return f - - sub_formulae = [formula] - part(formula) - sub_formulae.reverse() - known = {} - bicon = [] - for s in sub_formulae: - for i, v in enumerate(s.values): - if v in known: - s.values[i] = known[v] - bicon.append(Eq(Variable("x" + str(len(bicon))), s)) - known[s] = bicon[-1].values[0] - return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula])))))) - -""" The Parser - Do NOT look below this line! """ -import re - -NOT = "~" -AND = "&" -OR = "|" -IMP = "->" -EQ = "<->" -BOX = "[]" -DIAMOND = "<>" -VARIABLE = "VAR" -LB = "(" -RB = ")" - -class Operator(object): - def __init__(self, id, arity, *values): - self.id = id - self.arity = arity - self.values = list(values) - def depth(self): - if self.arity == 0: - return 0 - if self.id in (BOX, DIAMOND): - return 1 + self.values[0].depth() - if self.id == NOT: - return self.values[0].depth() - return max(self.values[0].depth(), self.values[1].depth()) - def __eq__(self, other): - return self.id == other.id and self.values == other.values # commutative types not considered yet - def __str__(self): - out = self.id - if self.arity == 0: - out = str(self.values[0]) - if self.arity == 1: - out = self.id + str(self.values[0]) - elif self.arity == 2: - out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")" - return out - -class Not(Operator): - arity = 1 - def __init__(self, *values): - Operator.__init__(self, NOT, Not.arity, *values) - def __call__(self): - pass - -class And(Operator): - arity = 2 - def __init__(self, *values): - Operator.__init__(self, AND, And.arity, *values) - -class Or(Operator): - arity = 2 - def __init__(self, *values): - Operator.__init__(self, OR, Or.arity, *values) - -class Imp(Operator): - arity = 2 - def __init__(self, *values): - Operator.__init__(self, IMP, Imp.arity, *values) - -class Eq(Operator): - arity = 2 - def __init__(self, *values): - Operator.__init__(self, EQ, Eq.arity, *values) - -class Box(Operator): - arity = 1 - def __init__(self, *values): - Operator.__init__(self, BOX, Box.arity, *values) - -class Diamond(Operator): - arity = 1 - def __init__(self, *values): - Operator.__init__(self, DIAMOND, Diamond.arity, *values) - -class Variable(Operator): - arity = 0 - def __init__(self, *values): - Operator.__init__(self, VARIABLE, Variable.arity, *values) - -class Lb(Operator): - arity = -1 - def __init__(self, *values): - Operator.__init__(self, LB, Lb.arity, *values) - -class Rb(Operator): - arity = -1 - def __init__(self, *values): - Operator.__init__(self, RB, Rb.arity, *values) - -class Formula(object): - def __init__(self): - pass - -TOKENS = {re.compile("\("): Lb, - re.compile("\)"): Rb, - re.compile("~"): Not, - re.compile("&"): And, - re.compile("\|"): Or, - re.compile("->"): Imp, - re.compile("<->"): Eq, - re.compile("\[\]"): Box, - re.compile("<>"): Diamond, - re.compile("[a-z]+"): Variable} - -class Scanner(object): - def __init__(self, tokens, source=None): - self.tokens = tokens - self.reset(source) - def next(self): - while self.i < len(self.source): - re.purge() - for p, token in self.tokens.iteritems(): - m = p.match(self.source[self.i:]) - if m: - self.i += m.end(0) - value = m.group(0) - return (token, value) - self.i += 1 - return (None, None) - def reset(self, source): - self.i = 0 - self.source = source - -S = Formula -A = "A" -#0 S: (Variable,), -#1 S: (Not, S), -#2 S: (Lb, A, Rb), -#3 S: (Box, S), -#4 S: (Diamond, S), -#5 A: (S, And, S), -#6 A: (S, Or, S), -#7 A: (S, Imp, S), -#8 A: (S, Eq, S) -SYNTAX = ((Variable,), - (Not, S), - (Lb, A, Rb), - (Box, S), - (Diamond, S), - (S, And, S), - (S, Or, S), - (S, Imp, S), - (S, Eq, S)) - -class Parser(object): - def __init__(self, syntax, scanner): - self.syntax = syntax - self.scanner = scanner - def parse(self, source): - table = {(S, Variable): 0, - (S, Not): 1, - (S, Lb): 2, - (S, Box): 3, - (S, Diamond): 4, - (A, S, And): 5, - (A, S, Or): 6, - (A, S, Imp): 7, - (A, S, Eq): 8, - (A, Variable, And): 5, - (A, Variable, Or): 6, - (A, Variable, Imp): 7, - (A, Variable, Eq): 8, - (A, Not, Variable, And): 5, - (A, Not, Variable, Or): 6, - (A, Not, Variable, Imp): 7, - (A, Not, Variable, Eq): 8} - stack = [S] - tree_nodes = [] - tree = None - out = [] - self.scanner.reset(source) - (token, value) = self.scanner.next() - (lookahead, la_value) = self.scanner.next() - (lookahead2, la2_value) = self.scanner.next() - accepted = True - while token and len(stack): - top = stack[-1] - if top == token: - tree_nodes.append((token, value)) - stack.pop() - #tree_nodes.append((stack.pop(), value)) - (token, value) = (lookahead, la_value) - (lookahead, la_value) = (lookahead2, la2_value) - #(lookahead, _) = self.scanner.next() - (lookahead2, la2_value) = self.scanner.next() - else: - action = None - if (top, token) in table: - action = table[(top, token)] - elif (top, token, lookahead) in table: - action = table[(top, token, lookahead)] - elif (top, token, lookahead, lookahead2) in table: - action = table[(top, token, lookahead, lookahead2)] - if action is None: - accepted = False - break - - out.append(action) - stack.pop() - stack.extend(reversed(self.syntax[action])) - accepted = accepted and not len(stack) - return (accepted, out, tree_nodes) - -class SyntaxTree(object): - def __init__(self, seq, tree_nodes): - seq.reverse() - tree_nodes.reverse() - self.root = self.compile(seq, tree_nodes)[0] - def compile(self, seq, tree_nodes): - stack = [] - while len(seq): - s = seq.pop() - if s == 0: - c, v = tree_nodes.pop() - while c != Variable: - c, v = tree_nodes.pop() - stack.append(Variable(v)) - elif s == 1: - stack.append(Not(self.compile(seq, tree_nodes))) - elif s == 2: - stack.extend(self.compile(seq, tree_nodes)) - elif s == 3: - stack.append(Box(self.compile(seq, tree_nodes))) - elif s == 4: - stack.append(Diamond(self.compile(seq, tree_nodes))) - elif s == 5: - stack.append(And(self.compile(seq, tree_nodes))) - elif s == 6: - stack.append(Or(self.compile(seq, tree_nodes))) - elif s == 7: - stack.append(Imp(self.compile(seq, tree_nodes))) - elif s == 8: - stack.append(Eq(self.compile(seq, tree_nodes))) - return stack - -from argparse import ArgumentParser - -def parse_arguments(): - 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.") - parser.add_argument("-f", "--formula", help="provide your own formula here, or better don't") - parser.add_argument("-d", "--dimacs", help="output file for the CNF DIMACS output") - return parser.parse_args() - -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""" - -if __name__ == "__main__": - main() diff -r b27fbffacec9 -r e4720232cf41 downloads/sml.zip Binary file downloads/sml.zip has changed