script changes for HWMCC13 (finally submitted version)

scripts/main.py

 import os
+import time
+from datetime import *
 ##import par
 ##from abc_common import *
 import abc_common
@@ -17,26 +19,6 @@ from  pyabc_split import *
 #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')
@@ -159,6 +141,48 @@ def list_aig(s=''):
         result = result + [name]
     return result
 
+def list_original():
+    list_dir = os.listdir('.')
+    list_dir.sort()
+    out = []
+    for i in range(len(list_dir)):
+        name = '%s/original.aig'%list_dir[i]
+        if os.access('%s'%name,os.R_OK):
+            abc('r %s;&ps'%name)
+            if n_latches() > 0 and n_pos() > 1:
+                size = str(sizeof())
+                print list_dir[i],
+                ps()
+                out = out + ['%s: %s'%(list_dir[i],size)]
+    return out
+
+def list_size(s=''):
+    """ prnts out the sizes of aig files. Leaves .aig as part of name"""
+    #os.chdir('../ibm-web')
+    list_all = os.listdir('.')
+    dir = lst(list_all,'.aig')
+    dir.sort()
+    result = []
+    for j in range(len(dir)):
+##        name = dir[j][:-4]
+        name = dir[j] #leaves .aig as part of name
+        if not s_in_s(s,name):
+            continue
+        print '%s '%name,
+##        abc('r %s.aig'%name)
+        abc('r %s'%name)
+        ps()
+        result = result + [name[:-4]] #takes .aig off of name
+    return result
+
+def rename(l=[]):
+    for j in range(len(l)):
+        name = l[j]
+        name1 = name +'.aig'
+        name2 = name[:-4]+'simp.aig' #take off _smp and put on simp
+        os.rename(name1,name2)
+    
+
 def list_blif(s=''):
     """ prnts out the sizes of aig files"""
     #os.chdir('../ibm-web')
@@ -222,11 +246,15 @@ def cleanup():
             (s_in_s('_bip', name)) or (s_in_s('sm0', name)) or (s_in_s('gabs', name)) 
             or (s_in_s('temp', name)) or (s_in_s('__', name)) or (s_in_s('greg', name)) or (s_in_s('tf2', name))
             or (s_in_s('gsrm', name)) or (s_in_s('_rpm', name )) or (s_in_s('gsyn', name)) or (s_in_s('beforerpm', name))
-            or (s_in_s('afterrpm', name)) or (s_in_s('initabs', name)) or (s_in_s('.status', name)) or (s_in_s('_init', name))
+            or (s_in_s('afterrpm', name)) or (s_in_s('initabs', name)) or (s_in_s('_init', name))
             or (s_in_s('_osave', name)) or (s_in_s('tt_', name)) or (s_in_s('_before', name)) or (s_in_s('_after', name))
-            or (s_in_s('_and', name)) or (s_in_s('_final', name)) or (s_in_s('_spec', name)) or (s_in_s('temp.a', name))
+            or (s_in_s('_and', name)) or (s_in_s('_spec', name)) or (s_in_s('temp.a', name))
             or (s_in_s('_sync', name)) or (s_in_s('_old', name)) or (s_in_s('_cone_', name)) or (s_in_s('_abs', name))
-            or (s_in_s('_vabs', name))
+            or (s_in_s('_vabs', name)) or (s_in_s('_gla', name)) or (s_in_s('vabs', name)) or (s_in_s('_mp2', name))
+            or (s_in_s('_sc1', name)) or (s_in_s('_sc2', name)) or (s_in_s('_after', name))
+            or (s_in_s('_before', name)) or (s_in_s('_aigs_', name)) or (s_in_s('_cex.', name))
+            or (s_in_s('_bmc1', name)) or (s_in_s('_p0_', name)) or (s_in_s('_p1_', name))
+            or (s_in_s('_unsolv', name)) or (s_in_s('_iso1', name))
             ):
             os.remove(name)
         
@@ -296,6 +324,32 @@ def absn(a,c,s):
     write_file('absn')
     return "Done"
 
+def time_stamp():
+    d=datetime.today()
+    s = d.strftime('%m.%d.%y-%X')
+    return s
+
+def apply_sp(list):
+    global m_trace
+    s = time_stamp()
+    out_name = "%s-traces.txt"%s
+    print out_name
+    if os.access(out_name,os.R_OK):
+        os.remove(out_name)
+    f = open(out_name,'w')
+    print f
+    for j in range(len(list)):
+        name = list[j]
+        print '\n\n**** %s ****\n'%name
+        f.write('\n\n****%s ****'%name)
+        read_file_quiet(name)
+        result = super_prove()
+        trace = result[1]
+        s = str(trace)
+        f.write('\n\n')
+        f.write(s)
+        f.flush()
+    f.close()
          
 def xfiles():
     global f_name

scripts/simple_prove.sh → scripts/multi_prove.sh

@@ -11,4 +11,4 @@ abc_root()
 abc_dir=$(abc_root "$0")
 bin_dir="${abc_dir}"/bin
 
-exec ${bin_dir}/abc -c "/simple_prove_aiger $*"
+exec ${bin_dir}/abc -c "/multi_prove_aiger $*"

scripts/new_abc_commands.py

@@ -7,6 +7,8 @@ import shutil
 import redirect
 import optparse
 
+from contextlib import contextmanager
+
 def read_cmd(args):
     if len(args)==2:
         par.read_file_quiet(args[1])
@@ -90,7 +92,50 @@ def print_aiger_result(args):
     
 pyabc.add_abc_command(print_aiger_result, "ZPython", "/print_aiger_result", 0)
 
-def proof_command_wrapper(prooffunc, category_name, command_name, change):
+@contextmanager
+def replace_report_result(multi):
+    
+    def report_result(po, result):
+        
+        print "REPORT RESULT: ", po, result
+        
+        print >> stdout, "%d"%result
+        print >> stdout, "b%d"%po
+        print >> stdout, "."
+        
+    def report_liveness_result(po, result):
+        
+        print "REPORT RESULT: ", po, result
+        
+        print >> stdout, "%d"%result
+        print >> stdout, "j%d"%po
+        print >> stdout, "."
+
+    def report_bmc_depth(depth):
+        
+        if not multi:
+            print "REPORT BMC DEPTH:", depth
+            print >> stdout, "u%d"%depth
+    
+    with redirect.save_stdout() as stdout:
+        
+        old_report_result = par.report_result
+        par.report_result = report_result
+        
+        #old_report_liveness_result = par.report_liveness_result
+        par.report_liveness_result = report_liveness_result
+
+        old_report_bmc_depth = par.report_bmc_depth
+        par.report_bmc_depth = report_bmc_depth
+        
+        try:
+            yield
+        finally:
+            par.report_result = old_report_result
+            #~ par.report_liveness_result = report_liveness_result
+            par.report_bmc_depth = old_report_bmc_depth
+
+def proof_command_wrapper_internal(prooffunc, category_name, command_name, change, multi=False):
 
     def wrapper(argv):
         
@@ -104,12 +149,13 @@ def proof_command_wrapper(prooffunc, category_name, command_name, change):
         options, args = parser.parse_args(argv)
         
         if len(args) != 2:
-            print args
             parser.print_usage()
             return 0
             
         aig_filename = os.path.abspath(args[1])
 
+        with replace_report_result(multi):
+
             if not options.noisy:
                 pyabc.run_command('/pushredirect')
                 
@@ -127,30 +173,82 @@ def proof_command_wrapper(prooffunc, category_name, command_name, change):
                 shutil.copyfile(aig_filename, basename)
                 aig_filename = basename
 
-            par.read_file_quiet(aig_filename)
-            result = prooffunc()
+                result = prooffunc(aig_filename)
                 
                 par.cex_list = []
             except:
                 result = None
 
+            if not multi:
+                
+                if result=="SAT":
+                    par.report_result(0,1)
+                elif result=="UNSAT":
+                    par.report_result(0,0)
+                elif type(result)==list and len(result)>0 and result[0] == "SAT":
+                    par.report_result(0,1)
+                elif type(result)==list and len(result)>0 and result[0] == "UNSAT":
+                    par.report_result(0,0)
+                else:
+                    par.report_result(0,2)
+
             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
-
         return 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)
+def proof_command_wrapper(prooffunc, category_name, command_name, change, multi=False):
+    def pf(aig_filename):
+        par.read_file_quiet(aig_filename)
+        return prooffunc()
+    return proof_command_wrapper_internal(pf, category_name, command_name, change, multi)
+
+proof_command_wrapper(par.sp,  'HWMCC13', '/super_prove_aiger',  0)
+proof_command_wrapper(par.simple,  'HWMCC13', '/simple_aiger',  0)
+proof_command_wrapper(par.simple_bip,  'HWMCC13', '/simple_bip_aiger',  0)
+proof_command_wrapper(par.simple_sat,  'HWMCC13', '/simple_sat_aiger',  0)
+proof_command_wrapper(par.mp,  'HWMCC13', '/multi_prove_aiger',  0, multi=True)
+
+from niklas import run_niklas_multi
+
+def simple_liveness_prooffunc(aig_filename):
+    
+    def simplify(aiger_in, aiger_out):
+        
+        saved = utils.save_po_info(aiger_in, tmp[0])
+        
+        par.read_file_quiet(tmp[0])
+        par.pre_simp()
+        pyabc.run_command( 'write_aiger %s'%tmp[1] )
+
+        #~ pyabc.run_command( 'read_aiger %s'%tmp[0] )
+        #~ pyabc.run_command( 'dc2 ; dc2 ; dc2 ; dc2' )
+        #~ pyabc.run_command( 'write_aiger %s'%tmp[1] )
+
+        utils.restore_po_info( saved, tmp[1], aiger_out )
+        
+    def report_result(id, res):
+        
+        if res and 'result' in res:
+            result = res['result']
+            if result=='proved':
+                par.report_liveness_result(id, 0)
+                return True
+            elif result=='failed':
+                par.report_liveness_result(id, 1)
+                return True
+            
+        return False
+
+    try:
+        run_niklas_multi(aig_filename, simplify=simplify, report_result=report_result)
+    except:
+        import traceback
+        traceback.print_exc()
+
+proof_command_wrapper_internal( simple_liveness_prooffunc, "HWMCC13", "/simple_liveness_aiger", 0, multi=True)

scripts/niklas.py

+import os
+import sys
+import time
+import tempfile
+import subprocess
+
+from contextlib import contextmanager
+
+import pyabc
+import pyabc_split
+
+@contextmanager
+def temp_file_names(N, suffix=""):
+    
+    files = []
+    
+    try:
+        
+        for i in xrange(N):
+            files.append( tempfile.NamedTemporaryFile(suffix=suffix) )
+            
+        yield [ f.name for f in files ]
+    
+    finally:
+        for f in files:
+            f.close()
+        
+def parse_bip_status(status):
+    
+    res = {}
+    
+    for line in open(status, 'r'):
+        
+        line = line.strip()
+        
+        colon = line.find(':')
+        
+        if colon < 0:
+            continue
+            
+        field = line[:colon]
+        data = line[colon+2:]
+        
+        res[field] = data
+    
+    return res
+
+def run_bip(args, aiger):
+
+    with temp_file_names(1) as tmpnames:
+
+        args = [
+            'bip',
+            '-abc',
+            '-input=%s'%aiger,
+            '-output=%s'%tmpnames[0],
+        ] + args;
+        
+        rc = subprocess.call(args, preexec_fn=pyabc._set_death_signal)
+        
+        if rc!=0:
+            return None
+            
+        return parse_bip_status(tmpnames[0])
+
+from pyaig import AIG, read_aiger, write_aiger, utils
+
+def run_niklas_single(aiger, simplify, report_result, timeout=None):
+    
+    orig_args = [
+        [ ',live', '-k=l2s', '-eng=treb-abs' ],
+        [ ',live', '-k=inc' ],
+        [ ',live', '-k=l2s', '-eng=bmc' ],
+    ]
+    
+    simplified_args = [
+        [ ',live', '-k=inc' ],
+        [ ',live', '-k=l2s', '-eng=bmc' ],
+        [ ',live', '-k=l2s', '-eng=treb' ],
+    ]
+    
+    with temp_file_names(1, suffix='.aig') as simple_aiger:
+
+        orig_funcs = [ pyabc_split.defer(run_bip)(a, aiger) for a in orig_args ]
+        simplified_funcs = [ pyabc_split.defer(run_bip)(a, simple_aiger[0]) for a in simplified_args ]
+
+        with pyabc_split.make_splitter() as splitter:
+
+            sleep_id = splitter.fork_one( lambda : time.sleep(timeout ) ) if timeout else None
+            
+            ids = splitter.fork_all( orig_funcs )
+            kill_if_simplified = ids[1:]
+            
+            simplifier_id = splitter.fork_one( pyabc_split.defer(simplify)(aiger, simple_aiger[0]) )
+            
+            for id, res in splitter:
+                
+                if id == sleep_id:
+                    return False
+                
+                if id == simplifier_id:
+                    if not res:
+                        continue
+                    splitter.kill(kill_if_simplified)
+                    splitter.fork_all( simplified_funcs )
+                    continue
+                    
+                if report_result(res):
+                    return True
+
+    return False
+
+def run_niklas_multi(aiger, simplify, report_result):
+    
+    with open(aiger, 'r') as fin:
+        aig = read_aiger( fin )
+        
+    n_j_pos = aig.n_justice()
+    assert n_j_pos > 0
+    
+    if n_j_pos==1:
+        return run_niklas_single( aiger, simplify, report_result=lambda res: report_result(0, res) )
+    
+    with temp_file_names(n_j_pos, suffix='.aig') as single_aiger:
+        
+        def extract(j_po):
+            with open(single_aiger[j_po], 'w') as fout:
+                write_aiger(utils.extract_justice_po(aig, j_po), fout)
+                
+        for _ in pyabc_split.split_all_full( [pyabc_split.defer(extract)(i) for i in xrange(n_j_pos) ] ):
+            pass
+            
+        unsolved = set( xrange(n_j_pos) )
+        
+        timeout = 1
+        
+        while unsolved:
+            for j_po in sorted(unsolved):
+                if run_niklas_single( single_aiger[j_po], simplify, report_result=lambda res: report_result(j_po, res), timeout=timeout ):
+                    unsolved.remove(j_po)
+            timeout *= 2
+        
+    return not unsolved
+    
+if __name__ == "__main__":    
+
+    def simplify(aiger_in, aiger_out):
+
+        with temp_file_names(2, suffix='.aig') as tmp:
+
+            saved = utils.save_po_info(aiger_in, tmp[0])
+
+            pyabc.run_command( 'read_aiger %s'%tmp[0] )
+            pyabc.run_command( 'dc2 ; dc2 ; dc2 ; dc2' )
+            pyabc.run_command( 'write_aiger %s'%tmp[1] )
+
+            utils.restore_po_info( saved, tmp[1], aiger_out )
+            
+        return True
+
+    def report_result(id, res):
+        
+        if res and 'result' in res:
+            result = res['result']
+            if result=='proved':
+                print "PROVED: ", id
+                return True
+            elif result=='failed':
+                print "FAILED:", id
+                return True
+            
+        return False
+        
+    aiger = "test.aig"
+
+    while True:
+        try:
+            run_niklas_multi(aiger, simplify=simplify, report_result=report_result)
+        except:
+            import traceback
+            traceback.print_exc()
+

scripts/bmc2.sh → scripts/simple.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} ; /pushredirect ; /pushdtemp ; bmc2 ; /popdtemp ; /popredirect ; /print_aiger_result"
+exec ${bin_dir}/abc -c "/simple_aiger $*"

scripts/bmc3.sh → scripts/simple_liveness.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} ; /pushredirect ; /pushdtemp ; bmc3 ; /popdtemp ; /popredirect ; /print_aiger_result"
+exec ${bin_dir}/abc -c "/simple_liveness_aiger $*"

scripts/dprove.sh → scripts/simple_sat.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} ; /pushredirect ; /pushdtemp ; dprove ; /popdtemp ; /popredirect ; /print_aiger_result"
+exec ${bin_dir}/abc -c "/simple_sat_aiger $*"