pyabc: updated Bob's scripts

1 files changed, 331 insertions, 0 deletions

diff --git a/scripts/main.py b/scripts/main.py
new file mode 100644
index 00000000..70dcf103
--- /dev/null
+++ b/scripts/main.py
@@ -0,0 +1,331 @@
+import os
+##import par
+##from abc_common import *
+import abc_common
+
+#this makes par the dominant module insteat of abc_common
+from par import *
+
+import sys
+import math
+import time
+from  pyabc_split import *
+##import pdb
+##from IPython.Debugger import Tracer; debug_here = Tracer()
+
+
+#x('source ../../abc.rc')
+#abc_common.x('source ../../abc.rc')
+
+
+#IBM directories
+# directories = ['ibmhard']
+ibmhard = (33,34,36,37,28,40,42,44,48,5,49,50,52,53,58,59,6,64,66,67,68,\
+           69,70,71,72,73,74,75,76,78,79,80,81,82,83,84,86,9,87,89,90,0,10,\
+           11,12,14,15,16,2,19,20,29,31,32)
+
+
+#directories = ['IBM_converted']
+#ibm_convert = (3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,\
+#               27,28,29,30,31,32,33,34,35,36,37,38,39,40,41)
+#IBM_converted = range(42)[3:]
+
+#the smaller files in ascending order
+#IBM_converted = (26,38,21,15,22,23,20,27,16,19,24,28,18,9,8,7,6,25,17,3,4)
+
+#the larger file in order (skipping 39)
+#IBM_converted = (39,5,40,41,13,12,10,14,11,31,33,36,29,34,35,37,30)
+IBM_converted = (5,40,41,13,12,10,14,11,31,33,36,29,34,35,37,30)
+
+def scorriter():
+    """ apply scorr with increasing conflicts up to 100"""
+    x('time')
+    run_command('r p_0.aig')
+    n = 20
+    while n < 1000:
+        print_circuit_stats()
+        run_command('scorr -C %d'%n)
+        x('ind -C %d'%1000)
+        if is_unsat():
+            print 'n = %d'%n
+            break
+        n = 2*n
+    x('time')
+     
+def simplifyq():
+    # set_globals()
+    n=n_ands()
+    if n > 30000:
+        if n<45000:
+            abc("&get;&scl;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr;&get;&scorr -F 2;&dc2;&put;w temp.aig")
+        else:
+            abc("&get;&scl;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr;&get;&dc2;&put;w temp.aig")
+    n = n_ands()
+    if n < 30000:
+        if n > 15000:
+            abc("scl;rw;dr;lcorr;rw;dr;scorr;fraig;dc2;dr;dc2rs;w temp.aig")
+        else:
+            abc("scl;rw;dr;lcorr;rw;dr;scorr;fraig;dc2;dr;scorr -F 2;dc2rs;w temp.aig")    
+    if n < 10000:
+        m = min( 30000/n, 8 )
+        if m > 2:
+            abc( "scorr -F %d"%m)
+    run_command("ps")
+
+def constraints():
+    """Determine if a set of files in a set of
+    directories has constraints and print out the results."""
+    for s in directories:
+        print("\ndirectory is "+s)
+        jj=eval(s)
+        print(jj)
+        for j in range(len(jj)):
+            x("\nr ../DIR/%s/p_%smp.aig"%(s,jj[j]))
+            print("structural:")
+            x('constr -s')
+            print("inductive constraints:")
+            x('constr ')
+
+def strip():
+    """Strip out each output of a multi-output example and write it
+    into a separate file"""
+    os.chdir('../DIR')
+    abc('r p_all_smp.aig')
+    po = n_pos()
+    print_circuit_stats()
+    for j in range(po):
+        abc('r p_all_smp.aig')
+        abc('cone -s -O %d'%j)
+        abc('scl;rw;trm')
+        abc('w p_%d.aig'%j)
+        print_circuit_stats()
+
+def lst(list,match):
+    result = []
+    for j in range(len(list)):
+        if list[j][-len(match):] == match:
+            result.append(list[j])
+    return result
+
+def lste(list,match,excp):
+    result = []
+    for j in range(len(list)):
+        if list[j][-len(match):] == match:
+            if excp in list[j]:
+                continue
+            result.append(list[j])
+    return result
+
+def blif2aig():
+    """ converts blif files into aig files"""
+    #os.chdir('../ibm-web')
+    list_all = os.listdir('.')
+    l_blif = lst(list_all,'.blif')
+    for j in range(len(l_blif)):
+        name = l_blif[j][:-5]
+        print '%s '%name,
+        abc('r %s.blif'%name)
+        abc('st')
+        abc('fold')
+        abc('w %s.aig'%name)
+        ps()
+
+def la():
+    return list_aig('')
+
+def list_aig(s):
+    """ prnts out the sizes of aig files"""
+    #os.chdir('../ibm-web')
+    list_all = os.listdir('.')
+    dir = lst(list_all,'.aig')
+    dir.sort()
+    for j in range(len(dir)):
+        name = dir[j][:-4]
+        if not s in name:
+            continue
+        print '%s '%name,
+        abc('r %s.aig'%name)
+        ps()
+    return dir
+
+def convert_ibm():
+    """ converts blif files (with constraints?) into aig files"""
+    os.chdir('../ibm-web')
+    list_ibm = os.listdir('.')
+    l_blif = lst(list_ibm,'.blif')
+    for j in range(len(l_blif)):
+        name = l_blif[j][:-5]
+        run_command('read_blif %s.blif'%name)
+        abc('undc')
+        abc('st -i')
+        abc('zero')
+        run_command('w %s.aig'%name)
+        """if a<100000000:
+            f = min(8,max(1,40000/a))
+            #run_command('scorr -c -F %d'%f)
+            #print 'Result of scorr -F %d: '%f,
+            print_circuit_stats()
+            run_command('w p_%d.aig'%j)"""
+
+def cl():
+    cleanup()
+
+def cleanup():
+    list = os.listdir('.') 
+    for j in range(len(list)):
+        name = list[j]
+        if (('_smp' in name) or ('_save' in name) or ('_backup' in name) or ('_osave' in name)
+            or ('_best' in name) or ('_gsrm' in name) or ('gore' in name) or 
+            ('_bip' in name) or ('sm0' in name) or ('gabs' in name) 
+            or ('temp' in name) or ('__' in name) or ('greg' in name) or ('tf2' in name)
+            or ('gsrm' in name) or ('_rpm' in name ) or ('gsyn' in name) or ('beforerpm' in name)
+            or ('afterrpm' in name) or ('initabs' in name) or ('.status' in name) or ('_init' in name)
+            or ('_osave' in name) or ('tt_' in name) or ('_before' in name) or ('_after' in name)
+            or ('_and' in name) or ('_final' in name) or ('_spec' in name) or ('temp.a' in name) or ('_sync' in name)
+            ):
+            os.remove(name)
+        
+def simp_mbi():
+    os.chdir('../mbi')
+    list_ibm = os.listdir('.')
+    l_aig = lst(list_ibm,'.aig')
+    for j in range(len(l_aig)):
+        name = l_aig[j][:-4]
+        run_command('r %s.aig'%name)
+        run_command('st')
+        print '\n%s: '%name
+        print_circuit_stats()
+        quick_simp()
+        scorr_comp()
+        simplify()
+        run_command('w %s_smp.aig'%name)
+
+def strip_names():
+    os.chdir('../mbi')
+    list_ibm = os.listdir('.')
+    l_aig = lst(list_ibm,'.aig')
+    for j in range(len(l_aig)):
+        name = l_aig[j][:-4]
+        run_command('r %s.aig'%name)
+        run_command('st')
+        print '\n%s: '%name
+        print_circuit_stats()
+        quick_simp()
+        scorr_comp()
+        simplify()
+        run_command('w %s_smp.aig'%name)
+
+def map_ibm():
+    os.chdir('../ibmmike2')
+    list_ibm = os.listdir('.')
+    l_blif = lst(list_ibm,'.blif')
+    result = []
+    print len(l_blif)
+    for j in range(len(l_blif)):
+        name = l_blif[j][:-5]
+        result.append('%s = %d'%(name,j))
+    return result
+
+
+def absn(a,c,s):
+    """ testing Niklas abstraction with various conflict limits
+    a= method (0 - regular cba,
+               1 - pure pba,
+               2 - cba with pba at the end,
+               3 cba and pba interleaved at each step
+    c = conflict limit
+    s = No. of stable steps without cex"""
+    global G_C, G_T, latches_before_abs, x_factor, f_name
+    set_globals()
+    latches_before_abs = n_latches()
+    print 'Start: ',
+    print_circuit_stats()
+    print 'Een abstraction params: Method #%d, %d conflicts, %d stable'%(a,c,s)
+    run_command('&get; &abs_newstart -v -A %d -C %d -S %d'%(a,c,s))
+    bmcdepth = n_bmc_frames()
+    print 'BMC depth = %d'%n_bmc_frames()
+    abc('&w absn_greg.aig; &abs_derive; &put; w absn_gabs.aig')
+    print 'Final abstraction: ',
+    print_circuit_stats()
+    write_file('absn')
+    return "Done"
+
+        
+def xfiles():
+    global f_name
+    #output = sys.stdout
+    #iterate over all ESS files
+    #saveout = sys.stdout
+    #output = open("ibm_log.txt",'w')
+    # sys.stdout = output
+    os.chdir('../ess/f58m')
+    print 'Directories are %s'%directories
+    for s in directories:
+        sss=  '../%s'%s
+        os.chdir(sss)
+        print "\nDirectory is %s\n"%s
+        jj=eval(s)
+        print (jj)
+        run_command('time')
+        for j in range(len(jj)):
+            print ' '
+            set_fname('p_%dsmp23'%jj[j])#file f_name.aig is read in
+            print 'p_%dsmp23'%jj[j]
+            run_command('time')
+            result = dprove3(1)
+            print result
+            run_command('time')
+        run_command('time')
+    os.chdir('../../python')
+    #sys.stdout = saveout
+    #output.close()
+
+def sublist(L,I):
+    z = []
+    for i in range(len(I)):
+        s = L[I[i]],
+        s = list(s)
+        z = z + s
+    return z
+
+def s2l(s):
+    """ takes the string s divided by '\n' and makess a list of items"""
+    result = []
+    while len(s)>2:
+        j = s.find('\n')
+        result.append(s[:j])
+        s = s[j+1:]
+    return result
+
+def select(lst, s):
+    result = []
+    print lst
+    for j in range(len(lst)):
+        if s in lst[j]:
+            s1 = lst[j]
+            k = s1.find(':')
+            s1 = s1[:k]
+            result.append(s1)
+    return result
+
+def process_result(name):
+    f = open(name,'r')
+    s = f.read()
+    f.close()
+    lst = s2l(s)
+    result = select(lst,'Timeout')
+    return result
+
+
+def main():
+    stackno = 0
+    if len(sys.argv) != 2:
+        print "usage: %s <aig filename>"%sys.argv[0]
+        sys.exit(1)
+    aig_filename = sys.argv[1]
+    x("source ../../abc.rc")
+    read(aig_filename)
+    dprove3(1)
+# a test to  whether the script is being called from the command line
+if __name__=="__main__":
+    main()