diff options
Diffstat (limited to 'scripts/new_abc_commands.py')
| -rw-r--r-- | scripts/new_abc_commands.py | 257 |
1 files changed, 0 insertions, 257 deletions
diff --git a/scripts/new_abc_commands.py b/scripts/new_abc_commands.py deleted file mode 100644 index 22718f07..00000000 --- a/scripts/new_abc_commands.py +++ /dev/null @@ -1,257 +0,0 @@ -import sys -import os -import pyabc -import par -import tempfile -import shutil -import redirect -import optparse - -from contextlib import contextmanager - -def read_cmd(args): - if len(args)==2: - par.read_file_quiet(args[1]) - else: - par.read_file() - return 0 - -pyabc.add_abc_command(read_cmd, "ZPython", "/rf", 0) - -def chdir_cmd(args): - os.chdir( args[1] ) - return 0 - -pyabc.add_abc_command(chdir_cmd, "ZPython", "/cd", 0) - -def pwd_cmd(args): - print os.getcwd() - return 0 - -pyabc.add_abc_command(pwd_cmd, "ZPython", "/pwd", 0) - -def ls_cmd(args): - os.system("ls " + " ".join(args[1:])) - return 0 - -pyabc.add_abc_command(ls_cmd, "ZPython", "/ls", 0) - -pushd_temp_stack = [] - -def pushdtemp_cmd(args): - tmpdir = tempfile.mkdtemp() - pushd_temp_stack.append( (os.getcwd(), tmpdir) ) - os.chdir(tmpdir) - return 0 - -pyabc.add_abc_command(pushdtemp_cmd, "ZPython", "/pushdtemp", 0) - -def popdtemp_cmd(args): - prev, temp = pushd_temp_stack.pop() - os.chdir(prev) - shutil.rmtree(temp, ignore_errors=True) - return 0 - -pyabc.add_abc_command(popdtemp_cmd, "ZPython", "/popdtemp", 0) - -pushredirect_stack = [] - -def push_redirect_cmd(args): - fdout = redirect.start_redirect( redirect.null_file, sys.stdout) - pushredirect_stack.append( (sys.stdout, fdout) ) - - fderr = redirect.start_redirect( redirect.null_file, sys.stderr) - pushredirect_stack.append( (sys.stderr, fderr) ) - - return 0 - -pyabc.add_abc_command(push_redirect_cmd, "ZPython", "/pushredirect", 0) - -def pop_redirect_cmd(args): - err, fderr = pushredirect_stack.pop() - redirect.end_redirect(err, fderr) - - out, fdout = pushredirect_stack.pop() - redirect.end_redirect(out, fdout) - - return 0 - -pyabc.add_abc_command(pop_redirect_cmd, "ZPython", "/popredirect", 0) - -def print_aiger_result(args): - status = pyabc.prob_status() - - if status==1: - print 0 - elif status==0: - print 1 - else: - print 2 - - return 0 - -pyabc.add_abc_command(print_aiger_result, "ZPython", "/print_aiger_result", 0) - -@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): - - 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") - - options, args = parser.parse_args(argv) - - if len(args) != 2: - 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') - - 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 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') - - return 0 - - pyabc.add_abc_command(wrapper, category_name, command_name, change) - -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) - -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] ) - - 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': - par.report_liveness_result(id, 0) - return True - elif result=='failed': - par.report_liveness_result(id, 1) - return True - - return False - - try: - niklas.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) |