Add ability to create Cnf object from string of Boolean formula

README.md

@@ -98,3 +98,25 @@ Then, the solution can be queried for variable assignments by using it
 like a dictionary. Note that Variable objects are used, not strings.
 
 (This very example can be found in the examples directory)
+
+Parsing Boolean expressions
+---------------------------
+
+It is also possible to create a Cnf object directly, without first creating ``Variable`` objects:
+
+    from satispy import CnfFromString
+    from satispy.solver import Minisat
+
+    exp, symbols = CnfFromString.create("v1 & v2 | v3")
+
+    solver = Minisat()
+
+    solution = solver.solve(exp)
+
+    if solution.success:
+        print "Found a solution:"
+        for symbol_name in symbols.keys():
+            print "%s is %s" % (symbol_name, solution[symbols[symbol_name]])
+    else:
+        print "The expression cannot be satisfied"
+

satispy/cnf.py

@@ -231,5 +231,128 @@ def __eq__(self, other):
     def __hash__(self):
         return hash(self.dis)
 
+
+class CnfFromString(Cnf):
+    def __init__(self):
+        pass
+
+    @staticmethod
+    def create(string):
+        output_queue, symbols = CnfFromString.string_to_rpn(string)
+        return CnfFromString.execute_rpn(output_queue), symbols
+
+    @staticmethod
+    def string_to_rpn(string):
+        # Convert string to RPN using the railroad-shunt algorithm 
+
+        symbols = {} # list of 'Variable' objects; keys are strings used as names in input
+        current_token = ''
+
+        output_queue = []
+        stack = []
+
+        for i in range(0, len(string)):
+            ch = string[i]
+            operator_char = (ch in ["-", "&", "|", "^", ">", " ", "(", ")"])
+
+            # reached end of variable-name token
+            if current_token and operator_char:
+                if current_token not in symbols.keys():
+                    symbols[current_token] = Variable(current_token)
+
+                output_queue.append(symbols[current_token])
+                current_token = ''
+
+            elif current_token and i == len(string)-1:
+
+                if not operator_char:
+                    current_token += ch
+
+                if current_token not in symbols.keys():
+                    symbols[current_token] = Variable(current_token)
+
+                output_queue.append(symbols[current_token])
+                current_token = ''
+
+
+            if ch in ["-", "&", "|", "^", '>']:
+
+                # don't let unary '-' operator pop a binary operator from the stack
+                # give parens a high precedence
+                if stack and ch != "-" and stack[-1] != '(':
+                    output_queue.append(stack.pop())
+
+                    # if popped a minus, pop again?
+                    if output_queue[-1] == "-" and stack and stack[-1] != '(':
+                        output_queue.append(stack.pop())
+
+                if ch == ">" and string[i+1] != ">":
+                    print "Error: single '>' is not allowed"
+                    return
+                if ch == ">" and string[i+1] == ">":
+                    stack.append(ch)
+                    i += 1
+                else:
+                    stack.append(ch)
+
+            if ch == "(":
+                stack.append("(")
+
+            if ch == ")":
+                while True:                
+                    next_operator = stack.pop()
+                    if next_operator == "(":
+                        break
+                    output_queue.append(next_operator)
+
+            if  ch not in ["-", "&", "|", "^", '>', "(", ")", " "]:
+                current_token += ch
+
+        while stack:
+            output_queue.append(stack.pop())
+
+        return output_queue, symbols
+
+    @staticmethod
+    def execute_rpn(output_queue):
+        result_stack = []
+        i = 0
+        while i < len(output_queue):
+
+            # n.b. operators were recorded as strings, whislt variables are Variable objects
+            if not isinstance(output_queue[i], str):
+                # not an operator
+                result_stack.append(output_queue[i])
+
+            elif output_queue[i] == "-":
+                # negation
+                result_stack[-1] = result_stack[-1].__neg__()
+
+            else:
+                # other operator
+                operator = output_queue[i]
+                rarg = result_stack.pop()
+                larg = result_stack.pop()
+
+                result_stack.append(CnfFromString.apply_operator(larg, rarg, operator))
+
+            i += 1
+
+        return result_stack[0]
+
+    @staticmethod
+    def apply_operator(larg, rarg, operator):    
+        if operator == "&":
+            return larg.__and__(rarg)
+        elif operator == "|":
+            return larg.__or__(rarg)
+        elif operator == "^":
+            return larg.__xor__(rarg)
+        elif operator == ">>":
+            return larg.rshift(rarg)
+
+
+
+
 # Change this to NaiveCnf if you want.
 cnfClass = Cnf

tests/run_tests.py

@@ -222,6 +222,44 @@ def testImplication(self):
             (v1 >> v2).dis
         )
 
+class ParserTest(unittest.TestCase):
+    def compare(self, string):
+        v1 = Variable('v1')
+        v2 = Variable('v2')
+        v3 = Variable('v3')
+
+        # print eval(string), CnfFromString().create(string)
+        parsed_cnf, symbol = CnfFromString.create(string)
+        self.assertEqual(hash(eval(string)), hash(parsed_cnf))
+
+    def testParser(self):
+        self.compare("v1")
+        self.compare("-v1")
+        self.compare('--v1')
+        self.compare('(-(-v1))')
+
+        self.compare("-v1 & -v2 | v3")
+        self.compare("((-v1) & -v2) | v3")
+
+        self.compare("v1 & -v2 | -v3")
+        self.compare(("v1 & v2 | v3"))
+
+        self.compare("(v1 & v2)")
+        self.compare("-(v1 & v2)")
+
+        self.compare("-(v1 & -v2) | v3")
+        self.compare("(-v1 & v2)")
+
+        self.compare("(v1 & -(v2 | v3))")
+
+        self.compare("-(v2 | v3)")
+        self.compare("v1 | -(v2 | v3)")
+
+        self.compare("v1 & (v2 | v3)")
+        self.compare("(v1 & v2) | v3")
+        self.compare("v1 & v2 | v3")
+
+
 class DimacsTest(unittest.TestCase):
     def testDimacs(self):
         v1 = Variable("v1")