diff options
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | scripts/new_abc_commands.py | 27 | ||||
-rw-r--r-- | scripts/niklas.py | 41 |
3 files changed, 42 insertions, 28 deletions
@@ -1,4 +1,6 @@ +ABC_PYTHON=/usr/bin/python + CC := gcc CXX := g++ LD := $(CXX) diff --git a/scripts/new_abc_commands.py b/scripts/new_abc_commands.py index bf6730bf..22718f07 100644 --- a/scripts/new_abc_commands.py +++ b/scripts/new_abc_commands.py @@ -214,23 +214,26 @@ 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): - 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] ) + with niklas.temp_file_names(2, suffix='.aig') as tmp: - #~ pyabc.run_command( 'read_aiger %s'%tmp[0] ) - #~ pyabc.run_command( 'dc2 ; dc2 ; dc2 ; dc2' ) - #~ pyabc.run_command( 'write_aiger %s'%tmp[1] ) + 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] ) - utils.restore_po_info( saved, tmp[1], aiger_out ) + utils.restore_po_info( saved, tmp[1], aiger_out ) + + return True def report_result(id, 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() diff --git a/scripts/niklas.py b/scripts/niklas.py index cfab8acc..882bd0a7 100644 --- a/scripts/niklas.py +++ b/scripts/niklas.py @@ -47,21 +47,24 @@ def parse_bip_status(status): 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 + import redirect + with redirect.redirect(): + + with temp_file_names(1) as tmpnames: + + args = [ + 'bip', + '-abc', + '-input=%s'%aiger, + '-output=%s'%tmpnames[0], + ] + args; - return parse_bip_status(tmpnames[0]) + 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 @@ -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 |