fixes for simple_livness

Makefile

 
+ABC_PYTHON=/usr/bin/python
+
 CC   := gcc
 CXX  := g++
 LD   := $(CXX)

scripts/new_abc_commands.py

@@ -214,24 +214,27 @@ 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):
     
+    import niklas
+    from pyaig import utils
+
     def simplify(aiger_in, aiger_out):
         
+        with niklas.temp_file_names(2, suffix='.aig') as tmp:
+
             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] )
+            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:
@@ -246,7 +249,7 @@ def simple_liveness_prooffunc(aig_filename):
         return False
 
     try:
-        run_niklas_multi(aig_filename, simplify=simplify, report_result=report_result)
+        niklas.run_niklas_multi(aig_filename, simplify=simplify, report_result=report_result)
     except:
         import traceback
         traceback.print_exc()

scripts/niklas.py

@@ -47,6 +47,9 @@ def parse_bip_status(status):
 
 def run_bip(args, aiger):
 
+    import redirect
+    with redirect.redirect():
+
         with temp_file_names(1) as tmpnames:
 
             args = [
@@ -95,17 +98,23 @@ def run_niklas_single(aiger, simplify, report_result, timeout=None):
             
             for id, res in splitter:
                 
+                print 'NIKLAS: process %d finished with'%id, res
+                
                 if id == sleep_id:
+                    print 'NIKLAS: timeout'
                     return False
                 
-                if id == simplifier_id:
+                elif id == simplifier_id:
+                    print 'NIKLAS: simplify ended'
                     if not res:
                         continue
+                    print 'NIKLAS: killing'
                     splitter.kill(kill_if_simplified)
                     splitter.fork_all( simplified_funcs )
                     continue
                     
-                if report_result(res):
+                elif report_result(res):
+                    print 'NIKLAS: RESULT'
                     return True
 
     return False