diff --git a/pebblegame.py b/pebblegame.py
new file mode 100644
index 0000000..9c6c4b4
--- /dev/null
+++ b/pebblegame.py
@@ -0,0 +1,55 @@
+#!/usr/bin/python3
+
+import os 
+import argparse
+import datetime
+from igraph import *
+
+
+parser = argparse.ArgumentParser()
+#parser.add_argument("square", type=int,
+#                    help="display a square of a given number")
+parser.add_argument("mapping", help="select type of mapping[0,1]\n \
+                    0=pebble game 1=reversible pebble game", type=int, choices=[0,1])
+parser.add_argument("file", help="edge list file name", type=str)
+parser.add_argument("-d", "--devices", help="number of devices used for mapping", type=int)
+parser.add_argument("-c", "--cycles", help="number of cycles available for mapping", type=int)
+parser.add_argument("-s", "--sliding", help="allow sliding for pebble game mapping",action="store_true")
+parser.add_argument("--mindev", help="determines the minimum number of devices",action="store_true")
+parser.add_argument("--outdir", help="specify output file directory", type=str)
+parser.add_argument("--compare", help="specify second file to check pebble equivalence", type=str)
+parser.add_argument("-v", "--verbosity", type=int, choices=[0, 1, 2],
+                    help="increase output verbosity")
+
+
+
+args = parser.parse_args()
+
+# read graph file 
+graph = Graph(directed=True)
+graph.Read_Edgelist(args.file,directed=True)
+
+
+
+if args.mindev:
+    # iterative call if mindev issued
+    print('iterative variant')
+
+
+else:
+    # call once 
+
+    # check type of mapping 
+    if args.mapping == 0: # pebble game 
+        pass 
+    elif args.mapping == 1: # reversible pebble game 
+        pass 
+
+
+answer = args.square**2
+if args.verbosity == 2:
+    print("the square of {} equals {}".format(args.square, answer))
+elif args.verbosity == 1:
+    print("{}^2 == {}".format(args.square, answer))
+else:
+    print(answer)
\ No newline at end of file
diff --git a/reg_alloc.py b/reg_alloc.py
index 047facd..710a5e3 100644
--- a/reg_alloc.py
+++ b/reg_alloc.py
@@ -3,6 +3,167 @@
 from z3 import *
 import sys
 import itertools
+import time
+import datetime
+
+
+def boolP(s):
+    if(s):
+        return 1
+    else:
+        return 0
+
+def pebbleGame(g,out,dev,cycles,outf=None,oneshot=True,sliding=True,timeout=None):
+    ''' Implments one-shot pebble game with sliding
+
+        Writes the result of pebble game to `outf`
+        Returns 
+        True, exectime if mapping terminates successfully.
+        False, errormsg if mapping unsuccessful.
+    '''
+
+    succList = dict()
+    for v in g.keys():
+        
+        for p in g[v]:
+            if p not in succList.keys():
+                succList[p] = [v]
+            else:
+                succList[p].append(v)
+
+
+    # assignment variables assigned_v_t
+    assigned = [[ Bool("assigned_%s_%s" % (v, t)) for t in range(T+1) ] for v in range(V) ]
+
+    # previously assigned prev_v_t
+    prevAssigned = [[Bool("prev_%s_%s" % (v,t)) for t in range(T+1)] for v in range(V)]
+
+    s = Solver()
+    # all vertices are not assigned at the start
+    for v in range(V):
+        s.add(assigned[v][0] == False) 
+
+    for v in range(V):
+        for t in range(1,T+1):
+            orTerm = []
+            for oldT in range(t):
+                orTerm.append(assigned[v][oldT])
+            print(len(prevAssigned), len(prevAssigned[v]), v, t)
+            s.add(prevAssigned[v][t] == Or(orTerm))
+
+    #final configuration 
+    for v in out:
+        s.add(assigned[v][T] == True)
+
+    sliding = True 
+    if not sliding:
+        # register allocation 
+        for t in range(1,T+1):
+            for v in range(V):
+                andTerm = []
+                
+                for p in g[v]:
+                    print('T',t,'|',v,'<-',p)
+                    andTerm.append(assigned[p][t])
+                    andTerm.append(assigned[p][t-1])
+                s.add(Or(Not(assigned[v][t]), Or(assigned[v][t-1],And(andTerm))))
+    else:
+        # allocation with sliding 
+        for t in range(1,T+1):
+            
+            for v in range(V):
+
+                orTerm = []
+
+                # all predecessors must be pebbled
+                andTerm = []
+                
+                for p in g[v]:
+                    print('T',t,'|',v,'<-',p)
+                    andTerm.append(assigned[p][t])
+                    andTerm.append(assigned[p][t-1])
+                orTerm.append(And(andTerm))
+                
+                # or any one pebble from a predecessor has been slided
+                for p in g[v]:
+                    
+                    andTerm = []
+                    andTerm.append(assigned[p][t-1]) # was assigned in last cycle
+                    andTerm.append(Not(assigned[p][t])) # this cycle unpebbled 
+
+                    for pr in g[v]: # all the other predecessors are pebbled 
+                        if pr != p:
+                            andTerm.append(assigned[pr][t])
+                            andTerm.append(assigned[pr][t-1])
+                    
+                    # successor must have been pebbled previously
+                    
+                    for succ in succList[p]:
+
+                        if succ != v: 
+                            andTerm.append(prevAssigned[succ][t])
+                            
+                    
+                    orTerm.append(And(andTerm))
+                
+                s.add(Or(Not(assigned[v][t]), Or(assigned[v][t-1],Or(orTerm))))
+
+                        
+
+    # constraint on single time computation
+    for v in range(V):
+
+        for t in range(2,T+1):
+            OrTerm = []
+            for oldt in range(t):
+                OrTerm.append(And(assigned[v][oldt], Not(assigned[v][oldt+1])))
+            s.add(Or(Not(Or(OrTerm)), Not(assigned[v][t])))
+
+    # constraint on number of allocations
+    for t in range(1,T+1):
+        alloc = []
+        for v in range(V):
+            alloc.append(assigned[v][t])
+        #print(N,alloc)
+        alloc.append(N)
+        f = AtMost(*alloc)
+        s.add(f)
+
+    print('Solving model started %s'.format(datetime.datetime.now()))
+    print(s.check())
+    print('Completed solving model %s'.format(datetime.datetime.now()))
+    
+
+
+    if(s.check() == sat):
+        m = s.model()
+        print("Assignment d->v")
+        print('t   |',end='')
+        for v in range(V):
+            print(" %3d" % v, end="")
+        print("")
+        for t in range(T+1):
+            print("t%3d|"%(t),end="")
+            for v in range(V):
+                print(' %3d'% ( boolP(m[assigned[v][t]])), end="")
+            print("",end="\n")
+        
+
+        print("\n Prev Assignment d->v")
+        print('t   |',end='')
+        for v in range(V):
+            print(" %3d" % v, end="")
+        print("")
+        for t in range(T+1):
+            print("t%3d|"%(t),end="")
+            for v in range(V):
+                print(' %3d'% ( boolP(m[prevAssigned[v][t]])), end="")
+            print("",end="\n")
+    else:
+        print('Model could not be solved')
+
+
+
 
 '''
 def PbLe(args, k):
@@ -52,18 +213,18 @@ def PbLe(args, k):
   0>5
   2>5
 '''
-
+'''
 T = 10 # number of cycles 
 
 N = 3  # number of registers
 V = 7  #number of vertices in the graph
 out = [6]
-'''
+
 
 N = 3
 V = 4
 out = [3]
-'''
+
 for v in range(V):
     g[v] = []
 
@@ -72,11 +233,11 @@ def PbLe(args, k):
 g[5] = [2,3,0]
 g[3] = [0]
 g[4] = [0,1]
-'''
+
 
 g[3] = [0,1,2]
 g[1] = [0] 
-'''
+
 succList = dict()
 for v in g.keys():
     
@@ -187,11 +348,7 @@ def PbLe(args, k):
 
 print(s.check())
 
-def boolP(s):
-    if(s):
-        return 1
-    else:
-        return 0
+
 
 if(s.check() == sat):
     m = s.model()
@@ -220,7 +377,7 @@ def boolP(s):
 else:
     print('Model could not be solved')
 
-'''
+
 #for c in s.assertions():
 #    print(c)
 def toSMT2Benchmark(f, status="unknown", name="benchmark", logic=""):
@@ -269,3 +426,30 @@ def toSMT2Benchmark(f, status="unknown", name="benchmark", logic=""):
                 print(" %3d^" % v, end = '')
         print('')
 '''
+
+
+if __name__ == "__main__":
+
+    T = 10 # number of cycles 
+
+    N = 3  # number of registers
+    V = 7  #number of vertices in the graph
+    out = [6]
+    '''
+
+    N = 3
+    V = 4
+    out = [3]
+    '''
+    for v in range(V):
+        g[v] = []
+
+
+    g[6] = [4,5]
+    g[5] = [2,3,0]
+    g[3] = [0]
+    g[4] = [0,1]
+
+
+    pebbleGame(g,out,N,T)
+