diff --git a/demo.py b/demo.py
index ad07c4c..d4c03af 100644
--- a/demo.py
+++ b/demo.py
@@ -1,4 +1,4 @@
-import plyproto.parser as plyproto
+import plyxproto.parser as plyproto
 
 test1 = """package tutorial;"""
 
@@ -16,7 +16,9 @@
 option java_outer_classname = "PushNotifications";
 option optimize_for = SPEED;
 
-  message Person(types.Actor) {
+  policy slice_user <foobar>
+
+  message Person(core.Actor) {
       required string name = 1;
       required int32 id = 2;
       optional string email = 3;
@@ -45,5 +47,6 @@
   extensions 500 to max;
 }"""
 
+p5 = '''policy foo <exists foo: foo.x=foo.y>'''
 parser = plyproto.ProtobufAnalyzer()
-print(parser.parse_string(test3))
+print(parser.parse_string(p5))
diff --git a/foldemo.py b/foldemo.py
new file mode 100644
index 0000000..e924e54
--- /dev/null
+++ b/foldemo.py
@@ -0,0 +1,18 @@
+from plyxproto.logicparser import *
+import ply.lex as lex
+import ply.yacc as yacc
+
+test_1 = "true"
+test_2 = "a | b"
+test_3 = "exists a: x=y"
+test_4 = "forall a: exists b: x.b=y.b"
+test_5 = "forall a: {{ a.endswith('good') }} "
+
+DEBUG = 0
+
+lexer = lex.lex(module=FOLLexer(), debug=DEBUG)#, optimize=1)
+parser = yacc.yacc(module=FOLParser(), start='goal', debug=DEBUG)
+
+for x,v in globals().items():
+    if x.startswith('test_'):
+        print parser.parse(v, lexer = lexer, debug=DEBUG)
diff --git a/plyxproto/helpers.py b/plyxproto/helpers.py
new file mode 100644
index 0000000..b059c17
--- /dev/null
+++ b/plyxproto/helpers.py
@@ -0,0 +1,178 @@
+class LexHelper:
+    offset = 0
+    def get_max_linespan(self, p):
+        defSpan=[1e60, -1]
+        mSpan=[1e60, -1]
+        for sp in range(0, len(p)):
+            csp = p.linespan(sp)
+            if csp[0] == 0 and csp[1] == 0:
+                if hasattr(p[sp], "linespan"):
+                    csp = p[sp].linespan
+                else:
+                    continue
+            if csp == None or len(csp) != 2: continue
+            if csp[0] == 0 and csp[1] == 0: continue
+            if csp[0] < mSpan[0]: mSpan[0] = csp[0]
+            if csp[1] > mSpan[1]: mSpan[1] = csp[1]
+        if defSpan == mSpan: return (0,0)
+        return tuple([mSpan[0]-self.offset, mSpan[1]-self.offset])
+
+    def get_max_lexspan(self, p):
+        defSpan=[1e60, -1]
+        mSpan=[1e60, -1]
+        for sp in range(0, len(p)):
+            csp = p.lexspan(sp)
+            if csp[0] == 0 and csp[1] == 0:
+                if hasattr(p[sp], "lexspan"):
+                    csp = p[sp].lexspan
+                else:
+                    continue
+            if csp == None or len(csp) != 2: continue
+            if csp[0] == 0 and csp[1] == 0: continue
+            if csp[0] < mSpan[0]: mSpan[0] = csp[0]
+            if csp[1] > mSpan[1]: mSpan[1] = csp[1]
+        if defSpan == mSpan: return (0,0)
+        return tuple([mSpan[0]-self.offset, mSpan[1]-self.offset])
+
+    def set_parse_object(self, dst, p):
+        dst.setLexData(linespan=self.get_max_linespan(p), lexspan=self.get_max_lexspan(p))
+        dst.setLexObj(p)
+
+class Base(object):
+    parent = None
+    lexspan = None
+    linespan = None
+
+    def v(self, obj, visitor):
+        if obj == None:
+            return
+        elif hasattr(obj, "accept"):
+            obj.accept(visitor)
+        elif isinstance(obj, list):
+            for s in obj:
+                self.v(s, visitor)
+            pass
+        pass
+
+    @staticmethod
+    def p(obj, parent):
+        if isinstance(obj, list):
+            for s in obj:
+                Base.p(s, parent)
+
+        if hasattr(obj, "parent"):
+            obj.parent = parent
+
+# Lexical unit - contains lexspan and linespan for later analysis.
+class LU(Base):
+    def __init__(self, p, idx):
+        self.p = p
+        self.idx = idx
+        self.pval = p[idx]
+        self.lexspan = p.lexspan(idx)
+        self.linespan = p.linespan(idx)
+
+        # If string is in the value (raw value) and start and stop lexspan is the same, add real span
+        # obtained by string length.
+        if isinstance(self.pval, str) \
+                and self.lexspan != None \
+                and self.lexspan[0] == self.lexspan[1] \
+                and self.lexspan[0] != 0:
+            self.lexspan = tuple([self.lexspan[0], self.lexspan[0] + len(self.pval)])
+        super(LU, self).__init__()
+
+    @staticmethod
+    def i(p, idx):
+        if isinstance(p[idx], LU): return p[idx]
+        if isinstance(p[idx], str): return LU(p, idx)
+        return p[idx]
+
+    def describe(self):
+        return "LU(%s,%s)" % (self.pval,  self.lexspan)
+
+    def __str__(self):
+        return self.pval
+
+    def __repr__(self):
+        return self.describe()
+
+    def accept(self, visitor):
+        self.v(self.pval, visitor)
+
+    def __iter__(self):
+        for x in self.pval:
+            yield x
+
+# Base node
+class SourceElement(Base):
+    '''
+    A SourceElement is the base class for all elements that occur in a Protocol Buffers
+    file parsed by plyproto.
+    '''
+    def __init__(self, linespan=[], lexspan=[], p=None):
+        super(SourceElement, self).__init__()
+        self._fields = [] # ['linespan', 'lexspan']
+        self.linespan = linespan
+        self.lexspan = lexspan
+        self.p = p
+
+    def __repr__(self):
+        equals = ("{0}={1!r}".format(k, getattr(self, k))
+                  for k in self._fields)
+        args = ", ".join(equals)
+        return "{0}({1})".format(self.__class__.__name__, args)
+
+    def __eq__(self, other):
+        try:
+            return self.__dict__ == other.__dict__
+        except AttributeError:
+            return False
+
+    def __ne__(self, other):
+        return not self == other
+
+    def setLexData(self, linespan, lexspan):
+        self.linespan = linespan
+        self.lexspan = lexspan
+
+    def setLexObj(self, p):
+        self.p = p
+
+    def accept(self, visitor):
+        pass
+
+class Visitor(object):
+
+    def __init__(self, verbose=False):
+        self.verbose = verbose
+
+    def __getattr__(self, name):
+        if not name.startswith('visit_'):
+            raise AttributeError('name must start with visit_ but was {}'.format(name))
+
+        def f(element):
+            if self.verbose:
+                msg = 'unimplemented call to {}; ignoring ({})'
+                print(msg.format(name, element))
+            return True
+        return f
+
+    # visitor.visit_PackageStatement(self)
+    # visitor.visit_ImportStatement(self)
+    # visitor.visit_OptionStatement(self)
+    # visitor.visit_FieldDirective(self)
+    # visitor.visit_FieldType(self)
+    # visitor.visit_FieldDefinition(self)
+    # visitor.visit_EnumFieldDefinition(self)
+    # visitor.visit_EnumDefinition(self)
+    # visitor.visit_MessageDefinition(self)
+    # visitor.visit_MessageExtension(self)
+    # visitor.visit_MethodDefinition(self)
+    # visitor.visit_ServiceDefinition(self)
+    # visitor.visit_ExtensionsDirective(self)
+    # visitor.visit_Literal(self)
+    # visitor.visit_Name(self)
+    # visitor.visit_Proto(self)
+    # visitor.visit_LU(self)
+
+
diff --git a/plyxproto/logicparser.py b/plyxproto/logicparser.py
new file mode 100644
index 0000000..8bdfb1c
--- /dev/null
+++ b/plyxproto/logicparser.py
@@ -0,0 +1,119 @@
+__author__ = "Sapan Bhatia"
+
+__copyright__ = "Copyright (C) 2017 Open Networking Lab"
+__version__ = "1.0"
+
+import ply.lex as lex
+import ply.yacc as yacc
+
+from helpers import LexHelper, LU
+
+class FOLLexer(object):
+    keywords = ('forall', 'exists', 'true', 'false', 'not')
+
+    tokens = ['ESCAPE', 'COLON', 'IMPLIES', 'OR', 'AND', 'LPAREN', 'RPAREN', 'EQUALS', 'SYMBOL', 'LT', 'RT'] + [k.upper() for k in keywords]
+    # literals = '()+-*/=?:,.^|&~!=[]{};<>@%'
+
+    t_ignore_LINE_COMMENT = '//.*'
+    t_COLON = '\\:'
+    t_IMPLIES = '\\-\\>'
+    t_OR = '\\|'
+    t_LT = '\\<'
+    t_RT = '\\>'
+    t_AND = '\\&'
+    t_LPAREN = '\\('
+    t_RPAREN = '\\)'
+
+    t_EQUALS = '\\='
+
+    literals = '()+-*/=?:,.^|&~!=[]{};<>@%'
+
+    t_ignore = ' \t\f'
+
+    def t_newline(self, t):
+        r'\n+'
+        t.lexer.lineno += len(t.value)
+
+    def t_newline2(self, t):
+        r'(\r\n)+'
+        t.lexer.lineno += len(t.value) / 2
+
+    t_ESCAPE = r'{{ (.|\n)*? }}'
+
+    def t_BLOCK_COMMENT(self, t):
+        r'/\*(.|\n)*?\*/'
+        t.lexer.lineno += t.value.count('\n')
+
+    def t_SYMBOL(self, t):
+        '[A-Za-z_$][\.A-Za-z0-9_+$]*'
+        if t.value in FOLLexer.keywords:
+            t.type = t.value.upper()
+        return t
+
+    def t_error(self, t):
+        print("Illegal character '{}' ({}) in line {}".format(t.value[0], hex(ord(t.value[0])), t.lexer.lineno))
+        t.lexer.skip(1)
+ 
+    
+    
+class FOLParser(object):
+    tokens = FOLLexer.tokens
+    offset = 0
+    lh = LexHelper()
+
+    def setOffset(self, of):
+        self.offset = of
+        self.lh.offset = of
+
+    def p_empty(self, p):
+        '''empty :'''
+        pass
+
+    def p_term_constant(self, p):
+        '''term :   FALSE
+                    | TRUE'''
+        p[0] = p[1]
+
+    def p_fole_not(self, p):
+        '''fole : NOT fole'''
+        p[0] = {p[1]: p[2]}
+
+    def p_fole_term(self, p):
+        '''fole : term'''
+        p[0] = p[1]
+
+    def p_term_symbol(self, p):
+        '''term : SYMBOL'''
+        p[0] = p[1]
+
+    def p_term_python(self, p):
+        '''fole : ESCAPE '''
+        p[0] = {'python': p[1]}
+
+    def p_fole_group(self, p):
+        "fole : LPAREN fole RPAREN"
+        p[0] = p[2]
+
+    def p_fole_equals(self, p):
+        "fole : term EQUALS term"
+        p[0] = {'=': (p[1], p[3])}
+
+    def p_fole_binary(self, p):
+        '''fole : fole AND fole
+                  | fole OR fole
+                  | fole IMPLIES fole'''
+        p[0] = {p[2]: [p[1], p[3]]}
+
+    def p_fole_quant(self, p):
+        '''fole :     FORALL SYMBOL COLON fole
+                      | EXISTS SYMBOL COLON fole'''
+        p[0] = {p[1]: [p[2], p[4]]}
+
+    
+    def p_goal(self, p):
+        '''goal : LT fole RT'''
+        p[0] = p[2]
+
+    def p_error(self, p):
+        print('error: {}'.format(p))
+
diff --git a/plyxproto/model.py b/plyxproto/model.py
index 7acf7a3..3f33704 100644
--- a/plyxproto/model.py
+++ b/plyxproto/model.py
@@ -1,144 +1,4 @@
-__author__ = "Dusan (Ph4r05) Klinec"
-__copyright__ = "Copyright (C) 2014 Dusan (ph4r05) Klinec"
-__license__ = "Apache License, Version 2.0"
-__version__ = "1.0"
-
-class Visitor(object):
-
-    def __init__(self, verbose=False):
-        self.verbose = verbose
-
-    def __getattr__(self, name):
-        if not name.startswith('visit_'):
-            raise AttributeError('name must start with visit_ but was {}'.format(name))
-
-        def f(element):
-            if self.verbose:
-                msg = 'unimplemented call to {}; ignoring ({})'
-                print(msg.format(name, element))
-            return True
-        return f
-
-    # visitor.visit_PackageStatement(self)
-    # visitor.visit_ImportStatement(self)
-    # visitor.visit_OptionStatement(self)
-    # visitor.visit_FieldDirective(self)
-    # visitor.visit_FieldType(self)
-    # visitor.visit_FieldDefinition(self)
-    # visitor.visit_EnumFieldDefinition(self)
-    # visitor.visit_EnumDefinition(self)
-    # visitor.visit_MessageDefinition(self)
-    # visitor.visit_MessageExtension(self)
-    # visitor.visit_MethodDefinition(self)
-    # visitor.visit_ServiceDefinition(self)
-    # visitor.visit_ExtensionsDirective(self)
-    # visitor.visit_Literal(self)
-    # visitor.visit_Name(self)
-    # visitor.visit_Proto(self)
-    # visitor.visit_LU(self)
-
-class Base(object):
-    parent = None
-    lexspan = None
-    linespan = None
-
-    def v(self, obj, visitor):
-        if obj == None:
-            return
-        elif hasattr(obj, "accept"):
-            obj.accept(visitor)
-        elif isinstance(obj, list):
-            for s in obj:
-                self.v(s, visitor)
-            pass
-        pass
-
-    @staticmethod
-    def p(obj, parent):
-        if isinstance(obj, list):
-            for s in obj:
-                Base.p(s, parent)
-
-        if hasattr(obj, "parent"):
-            obj.parent = parent
-
-# Lexical unit - contains lexspan and linespan for later analysis.
-class LU(Base):
-    def __init__(self, p, idx):
-        self.p = p
-        self.idx = idx
-        self.pval = p[idx]
-        self.lexspan = p.lexspan(idx)
-        self.linespan = p.linespan(idx)
-
-        # If string is in the value (raw value) and start and stop lexspan is the same, add real span
-        # obtained by string length.
-        if isinstance(self.pval, str) \
-                and self.lexspan != None \
-                and self.lexspan[0] == self.lexspan[1] \
-                and self.lexspan[0] != 0:
-            self.lexspan = tuple([self.lexspan[0], self.lexspan[0] + len(self.pval)])
-        super(LU, self).__init__()
-
-    @staticmethod
-    def i(p, idx):
-        if isinstance(p[idx], LU): return p[idx]
-        if isinstance(p[idx], str): return LU(p, idx)
-        return p[idx]
-
-    def describe(self):
-        return "LU(%s,%s)" % (self.pval,  self.lexspan)
-
-    def __str__(self):
-        return self.pval
-
-    def __repr__(self):
-        return self.describe()
-
-    def accept(self, visitor):
-        self.v(self.pval, visitor)
-
-    def __iter__(self):
-        for x in self.pval:
-            yield x
-
-# Base node
-class SourceElement(Base):
-    '''
-    A SourceElement is the base class for all elements that occur in a Protocol Buffers
-    file parsed by plyproto.
-    '''
-    def __init__(self, linespan=[], lexspan=[], p=None):
-        super(SourceElement, self).__init__()
-        self._fields = [] # ['linespan', 'lexspan']
-        self.linespan = linespan
-        self.lexspan = lexspan
-        self.p = p
-
-    def __repr__(self):
-        equals = ("{0}={1!r}".format(k, getattr(self, k))
-                  for k in self._fields)
-        args = ", ".join(equals)
-        return "{0}({1})".format(self.__class__.__name__, args)
-
-    def __eq__(self, other):
-        try:
-            return self.__dict__ == other.__dict__
-        except AttributeError:
-            return False
-
-    def __ne__(self, other):
-        return not self == other
-
-    def setLexData(self, linespan, lexspan):
-        self.linespan = linespan
-        self.lexspan = lexspan
-
-    def setLexObj(self, p):
-        self.p = p
-
-    def accept(self, visitor):
-        pass
+from helpers import Base, SourceElement
 
 class PackageStatement(SourceElement):
     def __init__(self, name, linespan=None, lexspan=None, p=None):
@@ -258,6 +118,20 @@
             self.v(self.name, visitor)
             self.v(self.fieldId, visitor)
 
+class PolicyDefinition(SourceElement):
+    def __init__(self, name, body, linespan=None, lexspan=None, p=None):
+        super(PolicyDefinition, self).__init__(linespan=linespan, lexspan=lexspan, p=p)
+        self._fields += ['name', 'body']
+        self.name = name
+        Base.p(self.name, self)
+        self.body = body
+        Base.p(self.body, self)
+
+    def accept(self, visitor):
+        if visitor.visit_EnumDefinition(self):
+            self.v(self.name, visitor)
+            self.v(self.body, visitor)
+
 class EnumDefinition(SourceElement):
     def __init__(self, name, body, linespan=None, lexspan=None, p=None):
         super(EnumDefinition, self).__init__(linespan=linespan, lexspan=lexspan, p=p)
diff --git a/plyxproto/parser.py b/plyxproto/parser.py
index 72899e1..443ebb1 100755
--- a/plyxproto/parser.py
+++ b/plyxproto/parser.py
@@ -9,25 +9,31 @@
 from .model import *
 
 import pdb
+from helpers import LexHelper, LU
+from logicparser import FOLParser, FOLLexer
 
 class ProtobufLexer(object):
     keywords = ('double', 'float', 'int32', 'int64', 'uint32', 'uint64', 'sint32', 'sint64',
                 'fixed32', 'fixed64', 'sfixed32', 'sfixed64', 'bool', 'string', 'bytes',
                 'message', 'required', 'optional', 'repeated', 'enum', 'extensions', 'max',  'extend',
-                'to', 'package', '_service', 'rpc', 'returns', 'true', 'false', 'option', 'import', 'manytoone', 'manytomany', 'onetoone')
+                'to', 'package', '_service', 'rpc', 'returns', 'true', 'false', 'option', 'import', 'manytoone', 'manytomany', 'onetoone', 'policy')
 
     tokens = [
+        'POLICYBODY',
         'NAME',
         'NUM',
         'STRING_LITERAL',
         #'LINE_COMMENT', 'BLOCK_COMMENT',
-
         'LBRACE', 'RBRACE', 'LBRACK', 'RBRACK',
         'LPAR', 'RPAR', 'EQ', 'SEMI', 'DOT',
         'ARROW', 'COLON', 'COMMA', 'SLASH',
+        'DOUBLECOLON',
         'STARTTOKEN'
-
     ] + [k.upper() for k in keywords]
+
+
+    t_POLICYBODY = r'< (.|\n)*? >'
+
     literals = '()+-*/=?:,.^|&~!=[]{};<>@%'
 
     t_NUM = r'[+-]?\d+(\.\d+)?'
@@ -42,6 +48,8 @@
     t_RBRACE = '}'
     t_LBRACK = '\\['
     t_RBRACK = '\\]'
+
+
     t_LPAR = '\\('
     t_RPAR = '\\)'
     t_EQ = '='
@@ -53,6 +61,7 @@
     t_DOT = '\\.'
     t_ignore = ' \t\f'
     t_STARTTOKEN = '\\+'
+    t_DOUBLECOLON = '\\:\\:'
 
     def t_NAME(self, t):
         '[A-Za-z_$][A-Za-z0-9_+$]*'
@@ -73,45 +82,6 @@
         print("Illegal character '{}' ({}) in line {}".format(t.value[0], hex(ord(t.value[0])), t.lexer.lineno))
         t.lexer.skip(1)
 
-class LexHelper:
-    offset = 0
-    def get_max_linespan(self, p):
-        defSpan=[1e60, -1]
-        mSpan=[1e60, -1]
-        for sp in range(0, len(p)):
-            csp = p.linespan(sp)
-            if csp[0] == 0 and csp[1] == 0:
-                if hasattr(p[sp], "linespan"):
-                    csp = p[sp].linespan
-                else:
-                    continue
-            if csp == None or len(csp) != 2: continue
-            if csp[0] == 0 and csp[1] == 0: continue
-            if csp[0] < mSpan[0]: mSpan[0] = csp[0]
-            if csp[1] > mSpan[1]: mSpan[1] = csp[1]
-        if defSpan == mSpan: return (0,0)
-        return tuple([mSpan[0]-self.offset, mSpan[1]-self.offset])
-
-    def get_max_lexspan(self, p):
-        defSpan=[1e60, -1]
-        mSpan=[1e60, -1]
-        for sp in range(0, len(p)):
-            csp = p.lexspan(sp)
-            if csp[0] == 0 and csp[1] == 0:
-                if hasattr(p[sp], "lexspan"):
-                    csp = p[sp].lexspan
-                else:
-                    continue
-            if csp == None or len(csp) != 2: continue
-            if csp[0] == 0 and csp[1] == 0: continue
-            if csp[0] < mSpan[0]: mSpan[0] = csp[0]
-            if csp[1] > mSpan[1]: mSpan[1] = csp[1]
-        if defSpan == mSpan: return (0,0)
-        return tuple([mSpan[0]-self.offset, mSpan[1]-self.offset])
-
-    def set_parse_object(self, dst, p):
-        dst.setLexData(linespan=self.get_max_linespan(p), lexspan=self.get_max_lexspan(p))
-        dst.setLexObj(p)
 
 def srcPort(x):
     if (x):
@@ -124,6 +94,8 @@
     tokens = ProtobufLexer.tokens
     offset = 0
     lh = LexHelper()
+    fol_lexer = lex.lex(module=FOLLexer())#, optimize=1)
+    fol_parser = yacc.yacc(module=FOLParser(), start='goal')
 
     def setOffset(self, of):
         self.offset = of
@@ -325,6 +297,12 @@
         '''enum_body_opt : enum_body'''
         p[0] = p[1]
 
+    def p_policy_definition(self, p):
+        '''policy_definition : POLICY NAME POLICYBODY'''
+        fol = self.fol_parser.parse(p[3], lexer = self.fol_lexer)
+        p[0] = PolicyDefinition(Name(LU.i(p, 2)), fol)
+        self.lh.set_parse_object(p[0], p)
+
     # Root of the enum declaration.
     # enum_definition ::= 'enum' ident '{' { ident '=' integer ';' }* '}'
     def p_enum_definition(self, p):
@@ -446,6 +424,7 @@
         '''topLevel : message_definition
                     | message_extension
                     | enum_definition
+                    | policy_definition
                     | service_definition
                     | import_directive
                     | package_directive