The result of merging with recent PyABC changes.

Makefile

@@ -43,7 +43,7 @@ CFLAGS   += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES)
 CXXFLAGS += $(CFLAGS) 
 
 #LIBS := -m32 -ldl -rdynamic -lreadline -ltermcap
-LIBS := -ldl /usr/lib64/libreadline.a /usr/lib64/libncurses.a -rdynamic
+LIBS := -lreadline
 
 SRC  := 
 GARBAGE := core core.* *.stackdump ./tags $(PROG)

scripts/abc.rc

@@ -1,14 +1,13 @@
 python new_abc_commands.py
-python reachx_cmd.py
+python -c "import reachx_cmd"
-#python C:\Research\ABC\AIG\Python\reachx_cmd.py
 
 # global parameters
 set check         # checks intermediate networks
 #set checkfio      # prints warnings when fanins/fanouts are duplicated
-set checkread     # checks new networks after reading from file
+#set checkread     # checks new networks after reading from file
-set backup        # saves backup networks retrived by "undo" and "recall"
+#set backup        # saves backup networks retrived by "undo" and "recall"
-set savesteps 1   # sets the maximum number of backup networks to save 
+#set savesteps 1   # sets the maximum number of backup networks to save 
-set progressbar   # display the progress bar
+#set progressbar   # display the progress bar
 
 # program names for internal calls
 set dotwin dot.exe
@@ -25,6 +24,10 @@ set gnuplotwin wgnuplot.exe
 set gnuplotunix gnuplot
 
 # standard aliases
+alias srw "b; rw; b"
+alias fix "ps; st; ps; srw; ps; plat; cycle -x -F 1; plat; logic; undc; st; zero; ps; scorr; ps" 
+alias fixp "st; srw; cycle -x -F 1; logic; undc; st; zero "
+
 alias b balance
 alias cl cleanup
 alias clp collapse
@@ -67,8 +70,8 @@ alias rvl read_verlib
 alias rsup read_super mcnc5_old.super
 alias rlib read_library
 alias rlibc read_library cadence.genlib
-alias rw rewrite
+alias rw drw
-alias rwz rewrite -z
+alias rwz drw -z
 alias rf refactor
 alias rfz refactor -z
 alias re restructure
@@ -98,18 +101,18 @@ alias wv write_verilog
 
 # standard scripts
 alias share       "b; multi; fx; b"
-alias resyn       "b; rw; rwz; b; rwz; b"
+alias resyn       "b; drw; rwz; b; rwz; b"
-alias resyn2      "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
+alias resyn2      "b; drw; rf; b; drw; rwz; b; rfz; rwz; b"
-alias resyn2a     "b; rw; b; rw; rwz; b; rwz; b"
+alias resyn2a     "b; drw; b; drw; rwz; b; rwz; b"
 alias resyn3      "b; rs; rs -K 6; b; rsz; rsz -K 6; b; rsz -K 5; b"
-alias compress    "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
+alias compress    "b -l; drw -l; rwz -l; b -l; rwz -l; b -l"
 
-alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
+alias compress2   "b -l; drw -l; rf -l; b -l; drw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
 alias choice      "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
 alias choice2     "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
-alias rwsat       "st; rw -l; b -l; rw -l; rf -l"
+alias rwsat       "st; drw -l; b -l; drw -l; rf -l"
-alias rwsat2      "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l"
+alias rwsat2      "st; drw -l; b -l; drw -l; rf -l; fraig; drw -l; b -l; drw -l; rf -l"
-alias shake       "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
+alias shake       "st; ps; sat -C 5000; drw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
 
 alias snap fraig_store
 alias unsnap fraig_restore
@@ -126,24 +129,24 @@ alias icb "ic -M 2 -B 10 -s"
 alias cs "care_set "
 
 # resubstitution scripts for the IWLS paper
-alias src_rw      "st; rw -l; rwz -l; rwz -l" 
+alias src_rw      "st; drw -l; rwz -l; rwz -l" 
 alias src_rs      "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l" 
-alias src_rws     "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" 
+alias src_rws     "st; drw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" 
-alias resyn2rs    "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b"
+alias resyn2rs    "b; rs -K 6; drw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; drw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b"
-alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
+alias compress2rs "b -l; rs -K 6 -l; drw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; drw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
 alias c2 "ua; compress2rs; sa"
 alias ic "indcut -v"
 alias lp "lutpack"
 alias c "ua; compress; sa"
-alias c1 "ua; compress;b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; sa" 
+alias c1 "ua; compress;b -l; rs -K 6 -l; drw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; sa" 
 alias dr dretime
 alias ds dsec -v
 alias dp dprove -v
 
 
 # experimental implementation of don't-cares
-alias resyn2rsdc    "b; rs -K 6 -F 2; rw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; rw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b"
+alias resyn2rsdc    "b; rs -K 6 -F 2; drw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; drw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b"
-alias compress2rsdc "b -l; rs -K 6 -F 2 -l; rw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; rw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
+alias compress2rsdc "b -l; rs -K 6 -F 2 -l; drw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; drw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
 
 # minimizing for FF literals
 alias fflitmin    "compress2rs; ren; sop; ps -f"
@@ -222,9 +225,10 @@ alias lcr "&get; &lcorr; &put"
 
 alias trm "logic;trim;st;ps"
 
-alias smp   "ua;ps;scl;ps;rw;dr;lcorr;rw;dr;ps;scorr;ps;fraig;ps;dc2;dr;scorr -F 2;ps;dc2rs;w temp.aig"
+alias smp   "ua;ps;scl;ps;drw;dr;lcorr;drw;dr;ps;scorr;ps;fraig;ps;dc2;dr;scorr -F 2;ps;dc2rs;w temp.aig"
-alias smp1   "ua;ps;scl;ps;rw;dr;lcorr;rw;dr;ps;scorr;ps;fraig;ps;dc2;dr;ps;dc2rs;w temp.aig"
+alias smp1   "scl;drw;dr;lcorr;drw;dr;scorr;fraig;dc2rs"
-alias smpf  "ua;ps;scl;lcr;ps;rw;dr;ps;scr;ps;dc2;&get;&scorr -F 2;&put;dr;ps;dc2;ps;w temp.aig"
+alias smp2   "ua;ps;scl;ps;drw;dr;lcorr;drw;dr;ps;scorr;ps;fraig;ps;dc2;dr;ps;dc2rs;w temp.aig"
+alias smpf  "ua;ps;scl;lcr;ps;drw;dr;ps;scr;ps;dc2;&get;&scorr -F 2;&put;dr;ps;dc2;ps;w temp.aig"
 
 
 alias &smp   "ua;&get;&ps;&scl;&ps;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&ps;&scorr;&ps;&fraig;&ps;&dc2;&put;dr;&get;&scorr -F 2;&ps;&dc2;&put;w temp.aig"
@@ -233,7 +237,7 @@ alias smplite '&get;&scl;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&dc2;
 
 alias &smp1   "ua;&get;&ps;&scl;&ps;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&ps;&scorr;&ps;&fraig;&ps;&dc2;&put;dr;&get;&ps;&dc2;&put;w temp.aig"
 
-alias &smpf  "ua;ps;rw;&get;&ps;&scl;&ps;&put;dr;&get;&ps;&lcorr;&ps;&dc2;&ps;&scorr;&ps;&put;rw;ps;w temp.aig"
+alias &smpf  "ua;ps;drw;&get;&ps;&scl;&ps;&put;dr;&get;&ps;&lcorr;&ps;&dc2;&ps;&scorr;&ps;&put;drw;ps;w temp.aig"
 
 #for each output separately
 alias simpk "dprove -vrcbkmiu -B 10 -D 1000"
@@ -323,7 +327,12 @@ alias %scr "%get;%st;%scorr;%put;st"
 
 alias sc "fold;w tempc.aig;unfold -s"
 alias uc "r tempc.aig;unfold -s"
-alias smpc "scl;rw;ps;scorr -c;ps;fraig;ps;compress2rs;ps"
+alias smpc "scl;drw;ps;scorr -c;ps;fraig;ps;compress2rs;ps"
+
+alias abseen "&get;,abs -vt=60 -timeout=60 -bob=10 -aig=temp.aig;r temp.aig"
+alias pdreen "&get;,pdr -vt=60"
+alias inteen "&get;,imc -vt=60"
+alias bmceen "&get;,bmc -vt=60"
 
 
 

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()

scripts/new_abc_commands.py

@@ -1,36 +1,17 @@
-
+import sys
-# You can use 'from pyabc import *' and then not need the pyabc. prefix everywhere
-
 import os
 import pyabc
-import abc_common
+import par
 import tempfile
 import shutil
 import redirect
-
+import optparse
-# A new command is just a function that accepts a list of string arguments
-#   The first argument is always the name of the command
-#   It MUST return an integer. -1: user quits, -2: error. Return 0 for success.
-
-# a command that calls prove(1) and returns success
-def prove_cmd(args):
-    result = abc_common.prove(1)
-    print result
-    return 0
-
-# registers the command:
-#   The first argument is the function
-#   The second argument is the category (mainly for the ABC help command)
-#   The third argument is the new command name
-#   Keep the fourth argument 0, or consult with Alan
-
-pyabc.add_abc_command(prove_cmd, "ZPython", "/prove", 0)
 
 def read_cmd(args):
     if len(args)==2:
-        abc_common.read_file_quiet(args[1])
+        par.read_file_quiet(args[1])
     else:
-        abc_common.read_file()
+        par.read_file()
     return 0
 
 pyabc.add_abc_command(read_cmd, "ZPython", "/rf", 0)
@@ -109,75 +90,67 @@ def print_aiger_result(args):
     
 pyabc.add_abc_command(print_aiger_result, "ZPython", "/print_aiger_result", 0)
 
-def super_prove_aiger_cmd(args):
+def proof_command_wrapper(prooffunc, category_name, command_name, change):
 
-    noisy = len(args)==2 and args[1]=='-n'
+    def wrapper(argv):
+        
+        usage = "usage: %prog [options] <aig_file>"
+    
+        parser = optparse.OptionParser(usage, prog=command_name)
+    
+        parser.add_option("-n", "--no_redirect", dest="noisy", action="store_true", default=False, help="don't redirect output")
+        parser.add_option("-d", "--current_dir", dest="current_dir", action="store_true", default=False, help="stay in current directory")
 
-    if not noisy:
+        options, args = parser.parse_args(argv)
-        pyabc.run_command('/pushredirect')
+        
-        pyabc.run_command('/pushdtemp')
+        if len(args) != 2:
-    
+            print args
-    try:
+            parser.print_usage()
-        result = abc_common.super_prove()
+            return 0
-    except:
-        result = None
-    
-    if not noisy:
-        pyabc.run_command('/popdtemp')
-        pyabc.run_command('/popredirect')
             
-    if result=="SAT":
+        aig_filename = os.path.abspath(args[1])
-        print 1
-    elif result=="UNSAT":
-        print 0
-    else:
-        print 2
 
-    return 0
+        if not options.noisy:
-    
-pyabc.add_abc_command(super_prove_aiger_cmd, "ZPython", "/super_prove_aiger", 0)
-
-
-def prove_one_by_one_cmd(args):
-    
-    noisy = len(args)==2 and args[1]=='-n'
-
-    # switch to a temporary directory
-    pyabc.run_command('/pushdtemp')
-    
-    # write a copy of the original file in the temporary directory
-    pyabc.run_command('w original_aig_file.aig')
-    
-    # iterate through the ouptus
-    for po in range(0, pyabc.n_pos()):
-        
-        if not noisy:
             pyabc.run_command('/pushredirect')
-
+            
-        # replace the nework with the cone of the current PO
+        if not options.current_dir:
-        pyabc.run_command( 'cone -O %d -s'%po )
+            pyabc.run_command('/pushdtemp')
-
+            
-        # run super_prove
         try:
-            result = abc_common.super_prove()
+            for d in os.environ['PATH'].split(':'):
+                bip = os.path.join(d, 'bip')
+                if os.path.exists(bip):
+                    pyabc.run_command("load_plugin %s Bip"%bip)
+                    break
+
+            basename = os.path.basename( aig_filename )
+            shutil.copyfile(aig_filename, basename)
+            aig_filename = basename
+
+            par.read_file_quiet(aig_filename)
+            result = prooffunc()
+            
+            par.cex_list = []
         except:
-            result = 'UNKNOWN'
+            result = None
 
-        if not noisy:
+        if not options.current_dir:
+            pyabc.run_command('/popdtemp')
+
+        if not options.noisy:
             pyabc.run_command('/popredirect')
+                
+        if result=="SAT":
+            print 1
+        elif result=="UNSAT":
+            print 0
+        else:
+            print 2
 
-        print 'PO %d is %s'%(po, result)
+        return 0
-        
-        # stop if the result is not UNSAT
-        if result != "UNSAT":
-            break
-
-        # read the original file for the next iteration
-        pyabc.run_command('r original_aig_file.aig')
-        
-    # go back to the original directory
-    pyabc.run_command('/popdtemp')
-
-    return 0
     
-pyabc.add_abc_command(prove_one_by_one_cmd, "ZPython", "/prove_one_by_one", 0)
+    pyabc.add_abc_command(wrapper, category_name, command_name, change)
+
+proof_command_wrapper(par.super_prove,  'HWMCC11', '/super_prove_aiger',  0)
+proof_command_wrapper(par.simple_prove, 'HWMCC11', '/simple_prove_aiger', 0)
+proof_command_wrapper(par.simple_bip,   'HWMCC11', '/simple_bip_aiger',   0)

scripts/simple_bip.sh

@@ -0,0 +1,14 @@
+#!/bin/sh
+
+abc_root()
+{
+    cwd="$(pwd)"
+    cd $(dirname "$1")
+    echo $(dirname "$(pwd)")
+    cd "${cwd}"
+}
+
+abc_dir=$(abc_root "$0")
+bin_dir="${abc_dir}"/bin
+
+exec ${bin_dir}/abc -c "/simple_bip_aiger $*"

scripts/simple_prove.sh

@@ -0,0 +1,14 @@
+#!/bin/sh
+
+abc_root()
+{
+    cwd="$(pwd)"
+    cd $(dirname "$1")
+    echo $(dirname "$(pwd)")
+    cd "${cwd}"
+}
+
+abc_dir=$(abc_root "$0")
+bin_dir="${abc_dir}"/bin
+
+exec ${bin_dir}/abc -c "/simple_prove_aiger $*"

scripts/super_prove.sh

@@ -10,6 +10,5 @@ abc_root()
 
 abc_dir=$(abc_root "$0")
 bin_dir="${abc_dir}"/bin
-aig_file="$1"
 
-exec ${bin_dir}/abc -c "/rf ${aig_file} ; /super_prove_aiger"
+exec ${bin_dir}/abc -c "/super_prove_aiger $*"

src/base/cmd/cmdUtils.c

@@ -454,7 +454,7 @@ FILE * CmdFileOpen( Abc_Frame_t * pAbc, char *sFileName, char *sMode, char **pFi
         else
         {
             // print the path/name of the resource file 'abc.rc' that is being loaded
-            if ( strlen(sRealName) >= 6 && strcmp( sRealName + strlen(sRealName) - 6, "abc.rc" ) == 0 )            
+            if ( !silent && strlen(sRealName) >= 6 && strcmp( sRealName + strlen(sRealName) - 6, "abc.rc" ) == 0 )            
                 printf( "Loading resource file \"%s\".\n", sRealName );
         }
     }

src/python/abcpy_test.py

@@ -34,7 +34,7 @@ import optparse
 def pytest3_cmd(args):
     usage = "usage: %prog [options]"
     
-    parser = optparse.OptionParser(usage)
+    parser = optparse.OptionParser(usage, prog="pytest3")
     
     parser.add_option("-c", "--cmd", dest="cmd", help="command to ask help for")
     parser.add_option("-v", "--version", action="store_true", dest="version", help="display Python Version")

src/python/module.make

@@ -57,7 +57,7 @@ pyabc.tgz : $(PROG) $(ABC_PYTHON_SRC:_wrap.c=.py) $(ABC_PYTHON_FILES_PREFIX)/abc
     $(ABC_PYTHON) $(ABC_PYTHON_FILES_PREFIX)/package.py \
         --abc=$(PROG) \
         --abc_sh=$(ABC_PYTHON_FILES_PREFIX)/abc.sh \
-        --pyabc=$(ABC_PYTHON_SRC:_wrap.c=.py) \
+        --pyabc=$(ABC_PYTHON_FILES_PREFIX) \
         --out=$@ \
         $(ABC_PYTHON_OPTIONS)
 
@@ -66,8 +66,6 @@ PYABC_INSTALL_TARGET := $(PYABC_INSTALL_TARGET)
 
 PYABC_INSTALL_DIR ?= /hd/common/pyabc/builds/pyabc_builds/
 
-.PHONY: zzz
-
 pyabc_install_target: pyabc_extension_bdist
     mkdir -p "$(PYABC_INSTALL_DIR)/$(PYABC_INSTALL_TARGET)"
     tar \

src/python/package.py

@@ -70,7 +70,10 @@ def package(abc_exe, abc_sh, pyabc, ofname, scripts_dir, use_sys):
                     add_file( tf, fullname, os.path.join("pyabc/scripts", fn), 0666, mtime)
     
     add_dir(tf, "pyabc/lib", mtime)
-    add_file( tf, pyabc, "pyabc/lib/pyabc.py", 0666, mtime)
+    
+    for entry in os.listdir(pyabc):
+        if entry.endswith('.py'):
+            add_file( tf, os.path.join(pyabc, entry), os.path.join("pyabc/lib", entry), 0666, mtime)
     
     if not use_sys:
         # ZIP standard library    

src/python/pyabc.i

@@ -262,8 +262,6 @@ void pyabc_internal_set_command_callback( PyObject* callback )
     pyabc_internal_python_command_callback = callback;
 }
 
-PyThreadState *_save;
-
 static int pyabc_internal_abc_command_callback(Abc_Frame_t * pAbc, int argc, char ** argv)
 {
     int i;
@@ -271,13 +269,15 @@ static int pyabc_internal_abc_command_callback(Abc_Frame_t * pAbc, int argc, cha
     PyObject* args;
     PyObject* arglist;
     PyObject* res;
-
+    
+    PyGILState_STATE gstate;
+    
     long lres;
     
     if ( !pyabc_internal_python_command_callback )
             return 0;
             
-    Py_BLOCK_THREADS
+    gstate = PyGILState_Ensure();
             
     args = PyList_New(argc);
     
@@ -292,14 +292,14 @@ static int pyabc_internal_abc_command_callback(Abc_Frame_t * pAbc, int argc, cha
 
     if ( !res )
     {
-        Py_UNBLOCK_THREADS
+        PyGILState_Release(gstate);
         return -1;
     }
     
     lres = PyInt_AsLong(res);
     Py_DECREF(res);
 
-    Py_UNBLOCK_THREADS
+    PyGILState_Release(gstate);
     
     return lres;
 }
@@ -309,11 +309,11 @@ int run_command(char* cmd)
     Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
     int rc;
     
-    Py_UNBLOCK_THREADS
+    Py_BEGIN_ALLOW_THREADS
     
     rc = Cmd_CommandExecute(pAbc, cmd);
     
-    Py_BLOCK_THREADS
+    Py_END_ALLOW_THREADS
     
     return rc;
 }
@@ -401,13 +401,15 @@ int Util_SignalSystem(const char* cmd)
 {
     PyObject* arglist;
     PyObject* res;
+    
+    PyGILState_STATE gstate;
 
     long lres;
     
     if ( !pyabc_internal_system_callback )
             return -1;
             
-    Py_BLOCK_THREADS
+    gstate = PyGILState_Ensure();
             
     arglist = Py_BuildValue("(O)", PyString_FromString(cmd));
     Py_INCREF(arglist);
@@ -417,14 +419,14 @@ int Util_SignalSystem(const char* cmd)
 
     if ( !res )
     {
-        Py_UNBLOCK_THREADS
+        PyGILState_Release(gstate);
         return -1;
     }
     
     lres = PyInt_AsLong(res);
     Py_DECREF(res);
 
-    Py_UNBLOCK_THREADS
+    PyGILState_Release(gstate);
     
     return lres;
 }
@@ -437,12 +439,14 @@ int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name)
     PyObject* arglist;
     PyObject* res;
     
+    PyGILState_STATE gstate;
+    
     *out_name = NULL;
 
     if ( !pyabc_internal_tmpfile_callback )
             return 0;
             
-    Py_BLOCK_THREADS
+    gstate = PyGILState_Ensure();
             
     arglist = Py_BuildValue("(ss)", prefix, suffix);
     Py_INCREF(arglist);
@@ -452,7 +456,7 @@ int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name)
 
     if ( !res )
     {
-        Py_UNBLOCK_THREADS
+        PyGILState_Release(gstate);
         return -1;
     }
     
@@ -463,7 +467,7 @@ int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name)
     
     Py_DECREF(res);
 
-    Py_UNBLOCK_THREADS
+    PyGILState_Release(gstate);
     
     return open(*out_name, O_WRONLY);
 }
@@ -472,11 +476,13 @@ void Util_SignalTmpFileRemove(const char* fname, int fLeave)
 {
     PyObject* arglist;
     PyObject* res;
+    
+    PyGILState_STATE gstate;
 
     if ( !pyabc_internal_tmpfile_remove_callback )
             return;
             
-    Py_BLOCK_THREADS
+    gstate = PyGILState_Ensure();
             
     arglist = Py_BuildValue("(si)", fname, fLeave);
     Py_INCREF(arglist);
@@ -485,7 +491,7 @@ void Util_SignalTmpFileRemove(const char* fname, int fLeave)
     Py_DECREF(arglist);
     Py_XDECREF(res);
 
-    Py_UNBLOCK_THREADS
+    PyGILState_Release(gstate);
 }
 
 void pyabc_internal_set_util_callbacks( PyObject* system_callback, PyObject* tmpfile_callback, PyObject* tmpfile_remove_callback )
@@ -607,18 +613,18 @@ class _Cex(object):
         return _cex_get_frame(self.pCex)
        
 def cex_get_vector():
-	
+    
-	res = []
+    res = []
-	
+    
-	for i in xrange(_cex_get_vec_len()):
+    for i in xrange(_cex_get_vec_len()):
-		cex = _cex_get_vec(i)
+        cex = _cex_get_vec(i)
-	
+
-		if cex is None:
+        if cex is None:
-			res.append(None)
+            res.append(None)
-		else:
+        else:
-			res.append(_Cex(cex)) 		
+            res.append(_Cex(cex))
-	
+    
-	return res
+    return res
        
 def cex_get():
 
@@ -1045,7 +1051,7 @@ def cmd_python(cmd_args):
     
     usage = "usage: %prog [options] <Python files>"
     
-    parser = optparse.OptionParser(usage)
+    parser = optparse.OptionParser(usage, prog="python")
     
     parser.add_option("-c", "--cmd", dest="cmd", help="Execute Python command directly")
     parser.add_option("-v", "--version", action="store_true", dest="version", help="Display Python Version")

src/python/reachx_cmd.py

@@ -42,18 +42,6 @@ def popen_and_wait_with_timeout(timeout,cmd, *args, **kwargs):
             
         return -1
 
-@contextmanager
-def replace_sys_argv(argv):
-    if 'argv' in sys.__dict__:
-        old_argv = sys.argv
-        sys.argv = argv
-        yield
-        sys.argv = old_argv
-    else:
-        sys.argv = argv
-        yield
-        del sys.argv
-
 @contextmanager
 def temp_file_name(suffix=""):
     file = tempfile.NamedTemporaryFile(delete=False, suffix=suffix)
@@ -105,13 +93,12 @@ def run_reachx_cmd(effort, timeout):
 def reachx_cmd(argv):
     usage = "usage: %prog [options]"
     
-    parser = optparse.OptionParser(usage)
+    parser = optparse.OptionParser(usage, prog="reachx")
     
     parser.add_option("-e", "--effort", dest="effort", type=int, default=0, help="effort level. [default=0, means unlimited]")
     parser.add_option("-t", "--timeout", dest="timeout", type=int, default=0, help="timeout in seconds [default=0, unlimited]")
 
-    with replace_sys_argv(argv):
+    options, args = parser.parse_args(argv)
-        options, args = parser.parse_args()
 
     rc = run_reachx_cmd(options.effort, options.timeout)
     print "%s command: jabc returned: %d"%(argv[0], rc)

src/python/setup.py

@@ -63,5 +63,5 @@ setup(
     name='pyabc',
     version='1.0',
     ext_modules=[ext],
-    py_modules=['pyabc','getch','pyabc_split','redirect']
+    py_modules=['pyabc','getch','pyabc_split','redirect', 'reachx_cmd']
 )