diff options
Diffstat (limited to 'scripts/new_abc_commands.py')
| -rw-r--r-- | scripts/new_abc_commands.py | 174 |
1 files changed, 136 insertions, 38 deletions
diff --git a/scripts/new_abc_commands.py b/scripts/new_abc_commands.py index 93956f9c..bf6730bf 100644 --- a/scripts/new_abc_commands.py +++ b/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,53 +149,106 @@ 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]) - if not options.noisy: - pyabc.run_command('/pushredirect') - - if not options.current_dir: - pyabc.run_command('/pushdtemp') - - try: - 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 = None + with replace_report_result(multi): - if not options.current_dir: - pyabc.run_command('/popdtemp') + if not options.noisy: + pyabc.run_command('/pushredirect') + + if not options.current_dir: + pyabc.run_command('/pushdtemp') + + try: + 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 + + result = prooffunc(aig_filename) + + par.cex_list = [] + except: + result = None - if not options.noisy: - pyabc.run_command('/popredirect') + if not multi: - if result=="SAT": - print 1 - elif result=="UNSAT": - print 0 - else: - print 2 + 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') 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) |