pyabc: remove python integration from abc, it is moved to a separate extension

1 files changed, 0 insertions, 2007 deletions

diff --git a/scripts/abc_common.py b/scripts/abc_common.py
deleted file mode 100644
index df2b731b..00000000
--- a/scripts/abc_common.py
+++ /dev/null
@@ -1,2007 +0,0 @@
-from pyabc import *
-import pyabc_split
-import par
-import redirect
-import sys
-import os
-import time
-import math
-
-
-global G_C,G_T,latches_before_abs,latches_before_pba,n_pos_before,x_factor
-
-"""
-The functions that are currently available from module _abc are:
-
-int n_ands();
-int n_pis();
-int n_pos();
-int n_latches();
-int n_bmc_frames();
-int prob_status(); 1 = unsat, 0 = sat, -1 = unsolved
-
-int run_command(char* cmd);
-
-bool has_comb_model();
-bool has_seq_model();
-bool is_true_cex();
-bool is_valid_cex();
-  return 1 if the number of PIs in the current network and in the current counter-example are equal
-int  n_cex_pis();
-  return the number of PIs in the current counter-example
-int  n_cex_regs();
-  return the number of flops in the current counter-example
-int  cex_po();
-  returns the zero-based output PO number that is SAT by cex
-int  cex_frame();
-  return the zero-based frame number where the outputs is SAT
-The last four APIs return -1, if the counter-example is not defined. 
-"""
-
-#global variables
-
-stackno_gabs = stackno_gore = stackno_greg= 0
-STATUS_UNKNOWN = -1
-STATUS_SAT = 0
-STATUS_UNSAT = 1
-RESULT = ('SAT' , 'SAT', 'UNSAT', 'UNDECIDED', 'UNDECIDED,', 'UNDCIDED'  )
-Sat_reg = 0
-Sat_true = 1
-Unsat = 2
-Undecided_reduction = 3
-Undecided_no_reduction = 4
-Error = 5
-Restart = 6
-xfi = x_factor = 1  #set this to higher for larger problems or if you want to try harder during abstraction
-max_bmc = -1
-last_time = 0
-
-# Function definitions:
-# simple functions: ________________________________________________________________________
-# set_globals, abc, q, x, has_any_model, is_sat, is_unsat, push, pop
-
-# ALIASES
-def p():
-    return prove()
-
-def ps():
-    print_circuit_stats()
-
-def n_real_inputs():
-    """This gives the number of 'real' inputs. This is determined by trimming away inputs that
-    have no connection to the logic. This is done by the ABC alias 'trm', which changes the current
-    circuit. In some applications we do not want to change the circuit, but just to know how may inputs
-    would go away if we did this. So the current circuit is saved and then restored afterwards."""
-    abc('w %s_savetempreal.aig; logic; trim; st'%f_name)
-    n = n_pis()
-    abc('r %s_savetempreal.aig'%f_name)
-    return n
-
-def long(t):
-    if t<20:
-        t = t
-    else:
-        t = 20+(t-20)/3
-    return max(10,t)
-
-def rif():
-    """Not used"""
-    global f_name
-    print 'Type in the name of the aig file to be read in'
-    s = raw_input()
-    if s[-5:] == '.blif':
-        f_name = s[:-5]
-    else:
-        f_name = s
-        s = s+'.blif'
-    run_command(s)
-    x('st;constr -i')
-    print_circuit_stats()
-    a = n_ands()
-    f = max(1,30000/a)
-    f = min (f,16)
-    x('scorr -c -F %d'%f)
-    x('fold')
-    print_circuit_stats()
-    x('w %s_c.aig'%f_name)
-
-def abc(cmd):
-    abc_redirect_all(cmd)
-    
-
-def abc_redirect( cmd, dst = redirect.null_file, src = sys.stdout ):
-    """This is our main way of calling an ABC function. Redirect, means that we suppress any output from ABC"""
-    with redirect.redirect( dst, src ):
-        return run_command( cmd )
-
-
-def abc_redirect_all( cmd ):
-    """This is our main way of calling an ABC function. Redirect, means that we suppress any output from ABC, including error printouts"""
-    with redirect.redirect( redirect.null_file, sys.stdout ):
-        with redirect.redirect( redirect.null_file, sys.stderr ):
-            return run_command( cmd )
-
-def set_globals():
-    """This sets global parameters that are used to limit the resources used by all the operations
-    bmc, interpolation BDDs, abstract etc. There is a global factor 'x_factor' that can
-    control all of the various resource limiting parameters"""
-    global G_C,G_T,x_factor
-    nl=n_latches()
-    na=n_ands()
-    np = n_pis()
-    #G_C = min(500000,(3*na+500*(nl+np)))
-    G_C = x_factor * min(100000,(3*na+500*(nl+np)))
-    #G_T = min(250,G_C/2000)
-    G_T = x_factor * min(75,G_C/2000)
-    G_T = max(1,G_T)
-    #print('Global values: BMC conflicts = %d, Max time = %d sec.'%(G_C,G_T))
-    
-def a():
-    """this puts the system into direct abc input mode"""
-    print "Entering ABC direct-input mode. Type q to quit ABC-mode"
-    n = 0
-    while True:
-        print '     abc %d> '%n,
-        n = n+1
-        s = raw_input()
-        if s == "q":
-            break
-        run_command(s) 
-
-def set_fname(name):
-    """ Another way to set an f_name, but currently this is not used"""
-    global f_name
-    s = name
-    if s[-4:] == '.aig':
-        f_name = s[:-4]
-    else:
-        f_name = s
-        s = s+'.aig'
-    #read in file
-    run_command(s)
-    #print_circuit_stats()
-
-def read_file_quiet(fname=None):
-    """This is the main program used for reading in a new circuit. The global file name is stored (f_name)
-    Sometimes we want to know the initial starting name. The file name can have the .aig extension left off
-    and it will assume that the .aig extension is implied. This should not be used for .blif files.
-    Any time we want to process a new circuit, we should use this since otherwise we would not have the
-    correct f_name."""
-    global max_bmc,  f_name, d_name, initial_f_name, x_factor, init_initial_f_name
-    x_factor = 1
-    max_bmc = -1
-    
-    if fname is None:
-        print 'Type in the name of the aig file to be read in'
-        s = raw_input()
-    else:
-        s = fname
-        
-    if s[-4:] == '.aig':
-        f_name = s[:-4]
-    else:
-        f_name = s
-        s = s+'.aig'
-        
-    run_command(s)
-    initial_f_name = f_name
-    init_initial_f_name = f_name
-    
-def read_file():
-    read_file_quiet()
-    print_circuit_stats()
-
-def rf():
-    read_file()
-
-
-def write_file(s):
-    """this is the main method for writing the current circuit to an AIG file on disk.
-    It manages the name of the file, by giving an extension (s). The file name 'f_name'
-    keeps increasing as more extensions are written. A typical sequence is
-    name, name_smp, name_smp_abs, name_smp_abs_spec, name_smp_abs_spec_final"""
-    global f_name
-    """Writes out the current file as an aig file using f_name appended with argument"""
-    f_name = '%s_%s'%(f_name,s)
-    ss = '%s.aig'%(f_name)
-    print 'WRITING %s: '%ss,
-    print_circuit_stats()
-    abc('w '+ss)
-    
-def wf():
-    """Not used"""
-    print 'input type of file to be written'
-    s = raw_input()
-    write_file(s)
-
-def bmc_depth():
-    """ Finds the number of BMC frames that the latest operation has used. The operation could be BMC, reachability
-    interpolation, abstract, speculate. max_bmc is continually increased. It reflects the maximum depth of any version of the circuit
-    including g ones, for which it is known that there is not cex out to that depth."""
-    global max_bmc
-    b = n_bmc_frames()
-    max_bmc = max(b,max_bmc)
-    return max_bmc
-
-def set_max_bmc(b):
-    """ Keeps increasing max_bmc which is the maximum number of time frames for
-    which the current circuit is known to be UNSAT for"""
-    global max_bmc
-    max_bmc = max(b,max_bmc)
-
-def print_circuit_stats():
-    """Stardard way of outputting statistice about the current circuit"""
-    global max_bmc
-    i = n_pis()
-    o = n_pos()
-    l = n_latches()
-    a = n_ands()
-    b = max(max_bmc,bmc_depth())
-    c = cex_frame()
-    if b>= 0:
-        if c>=0:
-            print 'PIs = %d, POs = %d, FF = %d, ANDs = %d, max depth = %d, CEX depth = %d'%(i,o,l,a,b,c)
-        else:
-            print 'PIs = %d, POs = %d, FF = %d, ANDs = %d, max depth = %d'%(i,o,l,a,b)
-    else:
-        if c>=0:
-            print 'PIs = %d, POs = %d, FF = %d, ANDs = %d, CEX depth = %d'%(i,o,l,a,c)
-        else:
-            print 'PIs = %d, POs = %d, FF = %d, ANDs = %d'%(i,o,l,a)
-
-def q():
-    exit()
-
-def x(s):
-    """execute an ABC command"""
-    print "RUNNING: ", s
-    run_command(s)
-
-def has_any_model():
-    """ check if a satisfying assignment has been found"""
-    res = has_comb_model() or has_seq_model()
-    return res
-
-def is_unsat():
-    if prob_status() == 1:
-        return True
-    else:
-        return False
-
-def is_sat():
-    if prob_status() == 0:
-        return True
-    else:
-        return False
-
-def wc(file):
-    """writes <file> so that costraints are preserved explicitly"""
-    abc('&get;&w %s'%file)
-
-def rc(file):
-    """reads <file> so that if constraints are explicit, it will preserve them"""
-    abc('&r %s;&put'%file)                         
-
-
-
-def fast_int(n):
-    """This is used to eliminate easy-to-prove outputs. Arg n is conflict limit to be used
-    in the interpolation routine. Typically n = 1 or 10"""
-    n_po = n_pos()
-    abc('int -k -C %d'%n)
-    print 'Reduced POs from %d to %d'%(n_po,n_pos())
-
-def refine_with_cex():
-    """Refines the greg (which contains the original problem with the set of FF's that have been abstracted).
-    This generates a new abstraction (gabs) and modifies the greg file to reflect which regs are in the
-    current abstraction"""
-    global f_name
-    print 'CEX in frame %d for output %d'%(cex_frame(),cex_po())
-    abc('&r %s_greg.aig; &abs_refine; &w %s_greg.aig'%(f_name,f_name))
-    return
-
-def generate_abs(n):
-    """generates an abstracted  model (gabs) from the greg file. The gabs file is automatically
-    generated in the & space by &abs_derive. We store it away using the f_name of the problem
-    being solved at the moment. The f_name keeps changing with an extension given by the latest
-    operation done - e.g. smp, abs, spec, final, group. """
-    global f_name
-    #we have a cex and we use this generate a new gabs file
-    abc('&r %s_greg.aig; &abs_derive; &put; w %s_gabs.aig'%(f_name,f_name)) # do we still need the gabs file
-    if n == 1:
-        print 'New abstraction: ',
-        print_circuit_stats()
-    return   
-
-    
-#more complex functions: ________________________________________________________
-#, abstract, pba, speculate, final_verify, dprove3
-
-
-def simplify():
-    """Our standard simplification of logic routine. What it does depende on the problem size.
-    For large problems, we use the &methods which use a simple circuit based SAT solver. Also problem
-    size dictates the level of k-step induction done in 'scorr' The stongest simplification is done if
-    n_ands < 20000. Then it used the clause based solver and k-step induction where |k| depends
-    on the problem size """
-    # set_globals()
-##    print 'simplify initial ',
-##    ps()
-    #abc('w t.aig')
-    n=n_ands()
-    abc('scl')
-    if n > 40000:
-        abc('&get;&scl;&put')
-        n = n_ands()
-        if n < 100000:
-            abc("&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr")
-            run_command('ps')
-            print '.',
-            n = n_ands()
-            if n<60000:
-                abc("&get;&scorr -F 2;&put;dc2rs")
-                print '.',
-                #ps()
-            else:
-                abc("dc2rs")
-                print '.',
-                #ps()
-            n = n_ands()
-    n = n_ands()
-    if n <= 40000:
-        print '.',
-        #ps()
-        if n > 30000:
-            abc("dc2rs")
-            print '.',
-##        else:
-##            abc("scorr -F 2;dc2rs")
-##            print '.',
-##            ps()
-    n = max(1,n_ands())
-    #ps()
-    if n < 30000:
-        abc('scl;rw;dr;lcorr;rw;dr')
-        m = int(min( 60000/n, 16))
-        #print 'm = %d'%m
-        if m >= 1:
-            j = 1
-            while j <= m:
-                set_size()
-                #print 'j - %d'%j
-                #abc('scl;dr;dc2;scorr -C 5000 -F %d'%j)
-                if j<8:
-                    abc('dc2')
-                else:
-                    abc('dc2rs')
-                abc('scorr -C 5000 -F %d'%j)
-                if check_size():
-                    break
-                j = 2*j
-                #ps()
-                continue
-            print '.',
-
-
-def iterate_simulation(latches_before):
-    """Subroutine of 'abstract' which does the refinement of the abstracted model,
-    using counterexamples found by simulation. Simulation is controlled by the amount
-    of memory it might use. At first wide but shallow simulation is done, bollowed by
-    successively more narrow but deeper simulation"""
-    global x_factor, f_name
-##    print 'RUNNING simulation iteratively'
-    f = 5
-    w = 255
-    for k in range(9):
-        f = min(f *2, 3500)
-        w = max(((w+1)/2)-1,1)
-        print '.',
-        abc('sim -m -F %d -W %d'%(f,w))
-        if not is_sat():
-            continue
-        while True:
-            refine_with_cex()
-            if is_sat():
-                print 'cex failed to refine abstraction '
-                return Sat_true
-            generate_abs(0)
-            latches_after = n_latches()
-            print 'Latches increased to %d'%latches_after
-            if latches_after >= .99*latches_before:
-                abc('r %s_savetempabs.aig'%f_name)
-                print "No reduction!."
-                return Undecided_no_reduction
-            abc('sim -m -F %d -W %d'%(f,w))
-            if not is_sat():
-                break
-
-def simulate():
-    """Simulation is controlled by the amount
-    of memory it might use. At first wide but shallow simulation is done, bollowed by
-    successively more narrow but deeper simulation"""
-    global x_factor, f_name
-##    print 'RUNNING simulation iteratively'
-    f = 5
-    w = 255
-    for k in range(9):
-        f = min(f *2, 3500)
-        w = max(((w+1)/2)-1,1)
-        print '.',
-        abc('sim -m -F %d -W %d'%(f,w))
-        if is_sat():
-            print 'cex found in frame %d'%cex_frame()
-            return 'SAT'
-    return 'UNDECIDED'
-        
-
-def iterate_abstraction_refinement(latches_before,NBF):
-    """Subroutine of 'abstract' which does the refinement of the abstracted model,
-    using counterexamples found by BMC or BDD reachability"""
-    global x_factor, f_name
-    if NBF == -1:
-        F = 2000
-    else:
-        F = 2*NBF
-    print '\nIterating BMC/PDR'
-    always_reach = 0
-    cexf = 0
-    reach_failed = 0
-    while True:
-        #print 'Generating problem abstraction'
-        generate_abs(1)
-        set_globals()
-        latches_after = n_latches()
-        if latches_after >= .98*latches_before:
-##            print 'No reduction'
-##            abc('r &s_savetemp.aig'%f_name)
-            break
-        ri = n_real_inputs() # No. of inputs after trm
-        nlri = n_latches()+ri
-        #reach_allowed = ((nlri<150) or (((cexf>250))&(nlri<300)))
-        reach_allowed = ((nlri<75) or (((cexf>250))&(nlri<300)))
-        pdr_allowed  = True
-        bmc = False
-        t = max(1,G_T)
-        if not F == -1:
-            F = int(1.5*max_bmc)
-        if (((reach_allowed  or pdr_allowed ) and not reach_failed)):
-            #cmd = 'reach -B 200000 -F 3500 -T %f'%t
-            #cmd = 'reachx -e %d -t %d'%(int(long(t)),max(10,int(t)))
-            #cmd = 'reachx -t %d'%max(10,int(t))
-            cmd = '&get;,pdr -vt=%f'%t
-        else:
-            #cmd = 'bmc3 -C %d -T %f -F %d'%(G_C,t,F)
-            bmc = True
-            cmd = '&get;,bmc -vt=%f'%(t)
-            #cmd = '&get;,pdr -vt=%f'%(t)
-        print '\n***RUNNING %s'%cmd
-        #run_command(cmd)
-        last_bmc = max_bmc
-        abc(cmd)
-        if prob_status() == 1:
-            #print 'Depth reached %d frames, '%n_bmc_frames()
-            print 'UNSAT'
-            return Unsat
-        cexf = cex_frame()
-        #print 'cex depth = %d'%cexf
-        #set_max_bmc(cexf -1)
-        if ((not is_sat()) ):
-            reach_failed = 1 # if ever reach failed, then we should not try it again on more refined models
-        if is_sat():
-            #print 'CEX in frame %d for output %d'%(cex_frame(),cex_po())
-            #set_max_bmc(cexf-1)
-            refine_with_cex() # if cex can't refine, status is set to Sat_true
-            if is_sat():
-                print 'cex did not refine. Implies true_sat'
-                return Sat_true
-        else:
-            print "No CEX found in %d frames"%n_bmc_frames()
-            set_max_bmc(n_bmc_frames())
-            if bmc:
-                break
-            elif max_bmc> 1.2*last_bmc: # if pdr increased significantly over abs, the assume OK
-                break
-            else:
-                continue
-    latches_after = n_latches()
-    if latches_after >= .98*latches_before:
-        abc('r %s_savetempabs.aig'%f_name)
-        print "No reduction!"
-        return Undecided_no_reduction
-    else:
-        print 'Latches reduced from %d to %d'%(latches_before, n_latches())
-        return Undecided_reduction
-
-
-def abstract():
-    """ abstracts using N Een's method 3 - cex/proof based abstraction. The result is further refined using
-    simulation, BMC or BDD reachability"""
-    global G_C, G_T, latches_before_abs, x_factor
-    set_globals()
-    latches_before_abs = n_latches()
-    abc('w %s_savetempabs.aig'%f_name)
-    print 'Start: ',
-    print_circuit_stats()
-    c = 1.5*G_C
-    #t = max(1,1.25*G_T)
-    t = 2*max(1,1.25*G_T)
-    s = min(max(3,c/30000),10) # stability between 3 and 10
-    time = max(1,.01*G_T)
-    abc('&get;,bmc -vt=%f'%time)
-    print 'BMC went %d frames'%n_bmc_frames()
-    set_max_bmc(bmc_depth())
-    f = max(2*max_bmc,20)
-    b = min(max(10,max_bmc),200)
-    cmd = '&get;,abs -bob=%d -stable=%d -timeout=%f -vt=%f -depth=%d'%(b,s,t,t,f)
-    print '     Running %s'%cmd
-    run_command(cmd)
-    if is_sat():
-        print 'Found true counterexample in frame %d'%cex_frame()
-        return Sat_true
-    NBF = bmc_depth()
-    print 'Abstraction good to %d frames'%n_bmc_frames()
-    set_max_bmc(NBF)
-    abc('&w %s_greg.aig; &abs_derive; &put; w %s_gabs.aig'%(f_name,f_name))
-##    print 'First abstraction: ',
-##    print_circuit_stats()
-    latches_after = n_latches()
-    #if latches_before_abs == latches_after:
-    if latches_after >= .98*latches_before_abs:
-        abc('r %s_savetempabs.aig'%f_name)
-        print "No reduction!"
-        return Undecided_no_reduction    
-    # refinement loop
-    if (n_ands() + n_latches() + n_pis()) < 15000:
-        print '\n***Running simulation iteratively'
-        for i in range(5):
-            result = iterate_simulation(latches_before_abs)
-            if result == Restart:
-                return result
-            if result == Sat_true:
-                return result
-    result = iterate_abstraction_refinement(latches_before_abs, NBF)
-    #if the result is 'Restart' we return and the calling routine increase
-    #x_factor to try one more time.
-    return result
-
-def absv(n,v):
-    """This is a version of 'abstract' which can control the methods used in Een's abstraction code (method = n)
-    as well as whether we want to view the output of this (v = 1)"""
-    global G_C, G_T, latches_before_abs, x_factor
-    #input_x_factor()
-    #x_factor = 3
-    set_globals()
-    latches_before_abs = n_latches()
-    print 'Start: ',
-    print_circuit_stats()
-    c = 1.5*G_C
-    t = max(1,1.25*G_T)
-    s = min(max(3,c/30000),10) # stability between 3 and 10
-    if max_bmc == -1:
-        time = max(1,.01*G_T)
-        #abc('bmc3 -C %d -T %f -F 165'%(.01*G_C, time))
-        abc('&get;,bmc -vt=%f'%time)
-        set_max_bmc(bmc_depth())
-    f = min(250,1.5*max_bmc)
-    f = max(20, f)
-    f = 10*f
-    b = x_factor*20
-    if not n == 0:
-        b = 10
-        b = max(b,max_bmc+2)
-        b = b*2**(x_factor-1)
-        b = 2*b
-    print 'Neen abstraction params: Method #%d, %d conflicts, %d stable, %f sec.'%(n,c/3,s,t)
-    if v == 1:
-        run_command('&get; &abs_newstart -v -B %f -A %d -C %d -S %d -V %f'%(b,n,c/3,s,t))
-    else:
-        abc('&get; &abs_newstart -v -B %f -A %d -C %d -S %d -T %f'%(b,n,c/3,s,t))
-    set_max_bmc(n_bmc_frames())
-    print 'Abstraction good to %d'%n_bmc_frames()
-    abc('&w %s_greg.aig; &abs_derive; &put; w %s_gabs.aig'%(f_name,f_name))
-    print 'Final abstraction: ',
-    print_circuit_stats()
-    latches_after = n_latches()    
-    if latches_after >= .98*latches_before_abs:
-        print "No reduction!"
-        return Undecided_no_reduction
-    return Undecided_reduction
-
-def spec():
-    """Main speculative reduction routine. Finds candidate sequential equivalences and refines them by simulation, BMC, or reachability
-    using any cex found. """
-    input_x_factor()
-    global G_C,G_T,n_pos_before, x_factor, n_latches_before
-    set_globals()
-    n_pos_before = n_pos()
-    n_latches_before = n_latches()    
-    set_globals()
-    t = max(1,.5*G_T)
-    r = max(1,int(t))
-    print '\n***Running &equiv2 with C = %d, T = %f sec., F = %d -S 1 -R %d'%(G_C,t,200,r)
-    abc("&get; &equiv2 -C %d -F 200 -T %f -S 1 -R %d; &semi -F 50; &speci -F 20 -C 1000;&srm; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%((G_C),t,r,f_name,f_name))
-    print 'Initial speculation: ',
-    print_circuit_stats()
-    print 'Speculation good to %d frames'%n_bmc_frames()
-    return
-
-def speculate():
-    """Main speculative reduction routine. Finds candidate sequential equivalences and refines them by simulation, BMC, or reachability
-    using any cex found. """
-    
-    global G_C,G_T,n_pos_before, x_factor, n_latches_before
-    set_globals()
-    n_pos_before = n_pos()
-    
-    def refine_with_cex():
-        """Refines the gore file to reflect equivalences that go away because of cex"""
-        global f_name
-        print 'CEX in frame %d for output %d'%(cex_frame(),cex_po())
-        abc('&r %s_gore.aig; &resim -m; &w %s_gore.aig'%(f_name,f_name))
-        #abc('&r %s_gore.aig; &equiv2 -vx ; &w %s_gore.aig'%(f_name,f_name))
-        return
-    
-    def generate_srm(n):
-        """generates a speculated reduced model (srm) from the gore file"""
-        global f_name
-        pos = n_pos()
-        ab = n_ands()
-        abc('&r %s_gore.aig; &srm ; r gsrm.aig; w %s_gsrm.aig'%(f_name,f_name)) #do we still need to write the gsrm file
-        if n == 0:
-            if ((pos == n_pos()) and (ab == n_ands())):
-                print 'Failed to refine'
-                return 'failed'
-        if n == 1:
-            print 'Spec. Red. Miter: ',
-            print_circuit_stats()
-        return 'OK'
-
-    def run_simulation(n):
-        f = 5
-        w = (256/n)-1
-        for k in range(9):
-            f = min(f * 2, 3500)
-            w = max(((w+1)/2)-1,1)
-            print '.',
-            #generate_srm(0)
-            abc('sim -m -F %d -W %d'%(f,w))
-            if not is_sat():
-                continue                
-            if cex_po() < n_pos_before:
-                print 'Sim found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame())
-                return Sat_true                    
-            refine_with_cex()
-            if n_pos_before == n_pos():            
-                return Undecided_no_reduction
-            while True:
-                result = generate_srm(0)
-                if result == 'failed':
-                    return Sat_true
-                abc('sim -m -F %d -W %d'%(f,w))
-                if not is_sat():
-                    break                
-                if cex_po() < n_pos_before:
-                    print 'Sim found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame())
-                    return Sat_true                    
-                refine_with_cex()
-                if n_pos_before == n_pos():            
-                    return Undecided_no_reduction
-        return Undecided_no_reduction
-    
-    n_pos_before = n_pos()
-    n_latches_before = n_latches()    
-    set_globals()
-    t = max(1,.5*G_T)
-    r = max(1,int(t))
-    abc('write spec_temp.aig')
-    print '\n***Running &equiv2 with C = %d, T = %f sec., F = %d -S 1 -R %d'%(G_C,t,200,r)
-##    abc("&get; &equiv2 -C %d -F 200 -T %f -S 1 -R %d; &semi -F 50; &speci -F 20 -C 1000;&srm; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%((G_C),t,r,f_name,f_name))
-    abc("&get; &equiv2 -C %d -F 200 -T %f -S 1 -R %d; &semi -W 63 -S 5 -C 500 -F 500; &speci -F 200 -C 5000;&srm; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%((G_C),t,r,f_name,f_name))
-    print 'Initial speculation: ',
-    print_circuit_stats()
-    #print 'Speculation good to %d frames'%n_bmc_frames()
-    #simplify()
-    if n_pos_before == n_pos():
-        print 'No new outputs. Quitting speculate'
-        return Undecided_no_reduction # return result is unknown
-    if is_sat():
-        #print '\nWARNING: if an abstraction was done, need to refine it further\n'
-        return Sat_true
-    if n_latches() > .98*n_latches_before:
-        pre_simp()
-        if n_latches() > .98*n_latches_before:
-            print 'Quitting speculation - not enough gain'
-            abc('r spec_temp.aig')
-            return Undecided_no_reduction # not worth it
-    k = n_ands() + n_latches() + n_pis()
-    n = 0
-    if k < 15000:
-        n = 1
-    elif k < 30000:
-        n = 2
-    elif k < 60000:
-        n = 4
-    elif k < 120000:
-        n = 8
-    if n > 0: # simulation can run out of memory for too large designs, so be careful
-        print '\n***RUNNING simulation iteratively'          
-        for i in range(5):
-            result = run_simulation(n)
-            if result == Sat_true:
-                return result
-    simp_sw = 1
-    int_sw = 1
-    reach_sw = 0
-    cexf = 0
-    reach_failed = 0
-    init = 1
-    run_command('write temptemp.aig')
-    print '\nIterating BMC or BDD reachability'
-    while True: # now try real hard to get the last cex.
-        set_globals()
-        if not init:
-            set_size()
-            result = generate_srm(1)
-            if check_size() == True:
-                print 'Failed to refine'
-                return Error
-            if result == 'failed':
-                return Sat_true
-            if simp_sw == 1:
-                na = n_ands()
-                simplify()
-                if n_ands() > .7*na: #if not significant reduction, stop simplification
-                    simp_sw = 0
-            if n_latches() == 0:
-                return check_sat()
-        init = 0 # make it so that next time it is not the first time through
-        time = max(1,G_T/(5*n_pos()))
-        if int_sw ==1:
-            npo = n_pos()
-            if n_pos() > .5*npo:  # if not sufficient reduction, turn this off
-                int_sw = 0
-        if is_sat():        #if fast interpolation found a cex
-            cexf = cex_frame()
-            set_max_bmc(cexf - 1)
-            if cex_po() < n_pos_before:
-                print 'Int found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame())
-                return Sat_true
-            refine_with_cex()
-            if ((n_pos_before == n_pos()) or (n_latches_before == n_latches())):            
-                abc('r temp_spec.aig')
-                return Undecided_no_reduction
-            if is_sat():
-                print '1. cex failed to refine abstraction'
-                return Sat_true
-            continue
-        else:
-            if n_latches() == 0:
-                return check_sat()
-            ri = n_real_inputs()  #seeing how many inputs would trm get rid of
-            nlri = n_latches() + ri
-            reach_allowed = ((nlri<75) or (((cexf>250)) and (nlri<300)))
-            pdr_allowed = True
-            bmc = False
-            if (((reach_allowed  or pdr_allowed ) and not reach_failed)):
-                t = max(1,1.2*G_T)
-                f = max(3500, 2*max_bmc)
-                #cmd = 'reachx -t %d'%max(10,int(t))
-                cmd ='&get;,pdr -vt=%f'%t
-            else:
-                t = max(1,1.5*G_T)
-                if max_bmc == -1:
-                    f = 200
-                else:
-                    f = max_bmc
-                f = int(1.5*f)
-                #cmd = 'bmc3 -C %d -T %f -F %f'%(1.5*G_C,1.2*t,f)
-                bmc = True
-                cmd = '&get;,bmc -vt=%f'%(1.2*t)
-            print '\n***Running %s'%cmd
-            last_bmc = max_bmc
-            abc(cmd)
-            #run_command(cmd)
-            if is_sat():
-                cexf = cex_frame()
-                #set_max_bmc(cexf  - 1)
-                #This is a temporary fix since reachx always reports cex_ps = 0
-                if ((cex_po() < n_pos_before) and (cmd[:4] == '&get')):
-                    print 'BMC/PDR found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame())
-                    return Sat_true
-                #End of temporary fix
-                refine_with_cex()#change the number of equivalences
-                if n_pos_before == n_pos():            
-                    return Undecided_no_reduction
-                continue
-            else:
-                set_max_bmc(n_bmc_frames())
-                if prob_status() == 1:
-                        #print 'Convergence reached in %d frames'%n_bmc_frames()
-                        return Unsat
-                print 'No cex found in %d frames'%n_bmc_frames()
-                if bmc:
-                    break
-                elif max_bmc > 1.2*last_bmc:
-                    break
-                else:
-                    reach_failed = 1
-                    init = 1
-                    continue
-    if n_pos_before == n_pos():
-        return Undecided_no_reduction 
-    else:
-        return Undecided_reduction
-
-def set_size():
-    """Stores  the problem size of the current design. Size is defined as (PIs, POs, ANDS, FF, max_bmc)""" 
-    global npi, npo, nands, nff, nmd
-    npi = n_pis()
-    npo = n_pos()
-    nands = n_ands()
-    nff = n_latches()
-    nmd = max_bmc
-
-def check_size():
-    """Assumes the problem size has been set by set_size before some operation. This checks if the size was changed
-    Size is defined as (PIs, POs, ANDS, FF, max_bmc)
-    Returns TRUE is size is the same""" 
-    global npi, npo, nands, nff, nmd
-    result = ((npi == n_pis()) and (npo == n_pos()) and (nands == n_ands()) and (nff == n_latches()) and (nmd == max_bmc))
-##    if result == 1:
-##        print 'Size unchanged'
-    return result
-
-def inferior_size():
-    """Assumes the problem size has been set by set_size beore some operation.
-    This checks if the new size is inferior (larger) to the old one 
-    Size is defined as (PIs, POs, ANDS, FF)""" 
-    global npi, npo, nands, nff
-    result = ((npi < n_pis()) or (npo < n_pos()) or (nands < n_ands()) )
-    return result
-
-def quick_verify(n):
-    """Low resource version of final_verify n = 1 means to do an initial simplification first"""
-    abc('trm')
-    if n == 1:
-        simplify()
-        if n_latches == 0:
-            return check_sat()
-        abc('trm')
-        if is_sat():
-            return Sat_true
-    print 'After trimming: ',
-    print_circuit_stats()
-    #try_rpm()
-    set_globals()
-    t = max(1,.4*G_T)
-    print '    Running PDR for %d sec '%(t)
-    abc('&get;,pdr -vt=%f'%(t*.8))
-    status = get_status()
-    if not status == Unsat:
-        print 'PDR went to %d frames, '%n_bmc_frames(),
-    print RESULT[status]
-    return status #temporary
-    if status <= Unsat:
-        return status
-    N = bmc_depth()
-    c = max(G_C/10, 1000)
-    t = max(1,.4*G_T)
-    print '    RUNNING interpolation with %d conflicts, max %d sec and 100 frames'%(c,t)
-    #abc('int -v -F 100 -C %d -T %f'%(c,t))
-    abc(',imc -vt=%f '%t)
-    status = get_status()
-    if status <= Unsat:
-        print 'Interpolation went to %d frames, '%n_bmc_frames(),
-        print RESULT[status]
-        return status
-    L = n_latches()
-    I = n_real_inputs()
-    if ( ((I+L<200)&(N>100))  or  (I+L<125)  or  L < 51 ): #heuristic that if bmc went deep, then reachability might also
-        t = max(1,.4*G_T)
-        cmd = 'reachx -t %d'%max(10,int(t))
-        print '    Running %s'%cmd
-        abc(cmd)        
-        status = get_status()
-        if status <= Unsat:
-            print 'Reachability went to %d frames, '%n_bmc_frames()
-            print RESULT[status]
-            return status
-        print 'BDD reachability aborted'
-    simplify() #why is this here
-    if n_latches() == 0:
-        print 'Simplified to 0 FF'
-        return check_sat()
-    set_max_bmc(bmc_depth()) # doesn't do anything
-    print 'No success, max_depth = %d'%max_bmc
-    return Undecided_reduction
-
-def get_status():
-    """this simply translates the problem status encoding done by ABC (-1,0,1)=(undecided,SAT,UNSAT) into the status code used by our python code."""
-    status = prob_status() #interrogates ABC for the current status of the problem.
-    # 0 = SAT
-    if status == 1:
-        status = Unsat
-    if status == -1: #undecided
-        status = Undecided_no_reduction
-    return status
-
-def try_rpm():
-    """rpm is a cheap way of doing reparameterization and is an abstraction method, so may introduce false cex's.
-    It finds a minimum cut between the PIs and the main sequential logic and replaces this cut by free inputs.
-    A quick BMC is then done, and if no cex is found, we assume the abstraction is valid. Otherwise we revert back
-    to the original problem before rpm was tried."""
-    global x_factor
-    if n_ands() > 30000:
-        return
-    set_globals()
-    pis_before = n_pis()
-    abc('w %s_savetemp.aig'%f_name)
-    abc('rpm')
-    result = 0
-    if n_pis() < .5*pis_before:
-        bmc_before = bmc_depth()
-        #print 'running quick bmc to see if rpm is OK'
-        t = max(1,.1*G_T)
-        #abc('bmc3 -C %d, -T %f'%(.1*G_C, t))
-        abc('&get;,bmc -vt=%f'%t)
-        if is_sat(): #rpm made it sat by bmc test, so undo rpm
-            abc('r %s_savetemp.aig'%f_name)
-        else:
-            abc('trm')
-            print 'WARNING: rpm reduced PIs to %d. May make SAT.'%n_pis()
-            result = 1
-    else:
-        abc('r %s_savetemp.aig'%f_name)
-    return result
-            
-def final_verify():
-    """This is the final method for verifying anything is nothing else has worked. It first tries BDD reachability
-    if the problem is small enough. If this aborts or if the problem is too large, then interpolation is called."""
-    global x_factor
-    set_globals()
-##    simplify()
-##    if n_latches() == 0:
-##        return check_sat()
-##    abc('trm')
-    #rpm_result = try_rpm()
-    set_globals()
-    N = bmc_depth()
-    L = n_latches()
-    I = n_real_inputs()
-    #try_induction(G_C)
-    c = max(G_C/5, 1000)
-    t = max(1,G_T)
-    print '\n***Running PDR for %d sec'%(t)
-    abc('&get;,pdr -vt=%f'%(t*.8))
-    status = get_status()
-    if status <= Unsat:
-        print 'PDR went to %d frames, '%n_bmc_frames(),
-        print RESULT[status]
-        return status
-    if ( ((I+L<250)&(N>100))  or  (I+L<200) or (L<51) ): #heuristic that if bmc went deep, then reachability might also
-        t = max(1,1.5*G_T)
-        #cmd = 'reach -v -B 1000000 -F 10000 -T %f'%t
-        #cmd = 'reachx -e %d'%int(long(t))
-        #cmd = 'reachx -e %d -t %d'%(int(long(t)),max(10,int(t)))
-        cmd = 'reachx -t %d'%max(10,int(t))
-        print '\n***Running %s'%cmd
-        abc(cmd)        
-        status = get_status()
-        if status <= Unsat:
-            print 'Reachability went to %d frames, '%n_bmc_frames(),
-            print RESULT[status]
-            return status
-        print 'BDD reachability aborted'          
-    return status #temporary
-    #f = max(100, bmc_depth())
-    print '\n***RUNNING interpolation with %d conflicts, %d sec, max 100 frames'%(c,t)
-    #abc('int -v -F 100 -C %d -T %f'%(c,t))
-    abc(',imc -vt=%f '%t)
-    status = get_status()
-    if status <= Unsat:
-        print 'Interpolation went to %d frames, '%n_bmc_frames(),
-        print RESULT[status]
-        return status
-    t = max(1,G_T)
-    simplify()
-    if n_latches() == 0:
-        return check_sat()
-    print 'Undecided'
-    return Undecided_reduction
-
-def check_sat():
-    """This is called if all the FF have disappeared, but there is still some logic left. In this case,
-    the remaining logic may be UNSAT, which is usually the case, but this has to be proved. The ABC command 'dsat' is used fro combinational problems"""
-##    if n_ands() == 0:
-##        return Unsat
-    abc('orpos;dsat -C %d'%G_C)
-    if is_sat():
-        return Sat_true
-    elif is_unsat():
-        return Unsat
-    else:
-        return Undecided_no_reduction
-
-def try_era(s):
-    """era is explicit state enumeration that ABC has. It only works if the number of PIs is small,
-    but there are cases where it works and nothing else does"""
-    if n_pis() > 12:
-        return
-    cmd = '&get;&era -mv -S %d;&put'%s
-    print 'Running %s'%cmd
-    run_command(cmd)
-
-def try_induction(C):
-    """Sometimes proving the property directly using induction works but not very often.
-    For 'ind' to work, it must have only 1 output, so all outputs are or'ed together temporarily"""
-    return Undecided_reduction
-    print '\n***Running induction'
-    abc('w %s_temp.aig'%f_name)
-    abc('orpos; ind -uv -C %d -F 10'%C)
-    abc('r %s_savetemp.aig'%f_name)
-    status = prob_status()
-    if not status == 1:
-        return Undecided_reduction
-    print 'Induction succeeded'
-    return Unsat
-
-def final_verify_recur(K):
-    """During prove we make backups as we go. These backups have increasing abstractions done, which can cause
-    non-verification by allowing false counterexamples. If an abstraction fails with a cex, we can back up to
-    the previous design before the last abstraction and try to proceed from there. K is the backup number we
-    start with and this decreases as the backups fails. For each backup, we just try final_verify.
-    If ever we back up to 0, which is the backup just after simplify, we then try speculate on this. This often works
-    well if the problem is a SEC problem where there are a lot of equivalences across the two designs."""
-    for j in range(K):
-        i = K-(j+1)
-        if i == 0: #don't try final verify on original
-            status = 3
-            break
-        print '\nVerifying backup number %d:'%i,
-        abc('r %s_backup_%d.aig'%(initial_f_name,i))
-        print_circuit_stats()
-        status = final_verify()
-        if status >= Unsat:
-            return status
-        if  i > 0:
-            print 'SAT returned, Running less abstract backup'
-            continue
-        break
-    if ((i == 0) and (status > Unsat) and (n_ands() > 0)):
-        print '\n***Running speculate on initial backup number %d:'%i,
-        abc('r %s_backup_%d.aig'%(initial_f_name,i))
-        ps()
-        if n_ands() < 20000:
-            status = speculate()
-            if ((status <= Unsat) or (status == Error)):
-                return status
-        status = final_verify()
-    if status == Unsat:
-        return status
-    else:
-        return Undecided_reduction
-        
-
-def smp():
-    pre_simp()
-    write_file('smp')
-
-def pre_simp():
-    """This uses a set of simplification algorithms which preprocesses a design.
-    Includes forward retiming, quick simp, signal correspondence with constraints, trimming away
-    PIs, and strong simplify"""
-##    print "Trying BMC for 2 sec."
-##    abc("&get; ,bmc -vt=2")
-##    if is_sat():
-##        return Sat_true
-    set_globals()
-    if n_latches == 0:
-        return check_sat()
-    #print '\n*** Running forward'
-    try_forward()
-    #print \n*** Running quick simp'
-    quick_simp()
-    #print 'Running_scorr_constr'
-    status = try_scorr_constr()
-    #status = 3
-    #print 'Running trm'
-    if ((n_ands() > 0) or (n_latches()>0)):
-        abc('trm')
-    print 'Forward, quick_simp, scorr_constr,: ',
-    print_circuit_stats()
-    if n_latches() == 0:
-        return check_sat()
-    status = process_status(status)
-    if status <= Unsat:
-        return status
-    simplify()
-    print 'Simplify: ',
-    print_circuit_stats()
-    #abc('w temp_simp.aig')
-    if n_latches() == 0:
-        return check_sat()
-    try_phase()
-    if n_latches() == 0:
-        return check_sat()
-    #abc('trm')
-    if ((n_ands() > 0) or (n_latches()>0)):
-        abc('trm')
-    status = process_status(status)
-    if status <= Unsat:
-        return status
-    status = try_scorr_constr()
-    abc('trm')
-    return process_status(status)
-
-def try_scorr_constr():
-    set_size()
-    abc('w %s_savetemp.aig'%f_name)
-    status = scorr_constr()
-    if inferior_size():
-        abc('r %s_savetemp.aig'%f_name)
-    return status
-
-def process(status):
-    """Checks if there are no FF and if so checks if the remaining combinational
-    problem is UNSAT"""
-    if n_latches() == 0:
-        return check_sat()
-    return status
-
-def try_phase():
-    """Tries phase abstraction. ABC returns the maximum clock phase it found using n_phases.
-    Then unnrolling is tried up to that phase and the unrolled model is quickly
-    simplified (with retiming to see if there is a significant reduction.
-    If not, then revert back to original""" 
-    n = n_phases()
-    if ((n == 1) or (n_ands() > 40000)):
-        return
-    print 'Number of possible phases = %d'%n
-    abc('w %s_savetemp.aig'%f_name)
-    na = n_ands()
-    nl = n_latches()
-    ni = n_pis()
-    no = n_pos()
-    cost_init = (1*n_pis())+(2*n_latches())+1*n_ands()
-    cost_min = cost_init
-    cost = cost_init
-    abc('w %s_best.aig'%f_name)
-    for j in range(4):
-        abc('r %s_savetemp.aig'%f_name)
-        p = 2**(j+1)
-        if p > n:
-            break
-        abc('phase -F %d'%p)
-        if na == n_ands():
-            break
-        abc('scl;rw')
-        if n_latches() > nl: #why would this ever happen
-            break
-        #print_circuit_stats()
-        abc('rw;lcorr;trm')
-        #print_circuit_stats()
-        cost = (1*n_pis())+(2*n_latches())+1*n_ands()
-        if cost < cost_min:
-            cost_min = cost
-            abc('w %s_best.aig'%f_name)
-        else:
-            break
-    if cost < cost_init:
-        abc('r %s_best.aig'%f_name)
-        simplify()
-        abc('trm')
-        print 'Phase abstraction obtained :',
-        print_circuit_stats()
-        return
-    abc('r %s_savetemp.aig'%f_name)
-    return       
-
-def try_forward():
-    """Attempts most forward retiming, and latch correspondence there. If attempt fails to help simplify, then we revert back to the original design
-    This can be effective for equivalence checking problems where synthesis used retiming"""
-    abc('w %s_savetemp.aig'%f_name)
-    if n_ands() < 30000:
-        abc('dr')
-        abc('lcorr')
-        nl = n_latches()
-        na = n_ands()
-        abc('w %s_savetemp0.aig'%f_name)
-        abc('r %s_savetemp.aig'%f_name) 
-        abc('dr -m')
-        abc('lcorr')
-        abc('dr')
-        if ((n_latches() <= nl) and (n_ands() < na)):
-            print 'Forward retiming reduced size to: ',
-            print_circuit_stats()
-            return
-        else:
-            abc('r %s_savetemp0.aig'%f_name)
-            return
-    return       
-
-def quick_simp():
-    """A few quick ways to simplify a problem before more expensive methods are applied.
-    Uses & commands if problem is large. These commands use the new circuit based SAT solver"""
-    na = n_ands()
-    if na < 30000:
-        abc('scl;rw')
-    elif na < 80000:
-        abc('&get;&scl;&put;rw')
-
-def scorr_constr():
-    """Extracts implicit constraints and uses them in signal correspondence
-    Constraints that are found are folded back when done"""
-    na = max(1,n_ands())
-    if ((na > 40000) or n_pos()>1):
-        return Undecided_no_reduction
-    f = 40000/na
-    f = min(f,16)
-    n_pos_before = n_pos()
-    f = 1 #temporary until bug fixed.
-    abc('w %s_savetemp.aig'%f_name)
-    if n_ands() < 3000:
-        cmd = 'unfold -a -F 2'
-    else:
-        cmd = 'unfold'
-    abc(cmd)
-    if ((n_ands() > na) or (n_pos() == n_pos_before)):
-        abc('r %s_savetemp.aig'%f_name)
-        return Undecided_no_reduction
-    print_circuit_stats()
-    print 'Number of constraints = %d'%(n_pos() - n_pos_before)
-    abc('scorr -c -F %d'%f)
-    abc('fold')
-    return Undecided_no_reduction
-
-def process_status(status):
-    """ if there are no FF, the problem is combinational and we still have to check if UNSAT"""
-    if n_latches() == 0:
-        return check_sat()
-    return status
-
-def input_x_factor():
-    """Sets the global x_factor according to user input"""
-    global x_factor, xfi
-    print 'Type in x_factor:',
-    xfi = x_factor = input()
-    print 'x_factor set to %f'%x_factor
-
-def prove(a):
-    """Proves all the outputs together. If ever an abstraction was done then if SAT is returned,
-        we make RESULT return "undecided".
-        If a == 1 do not run speculate"""
-    global x_factor,xfi,f_name
-    x = time.clock()
-    max_bmc = -1
-    K = 0
-    print 'Initial: ',
-    print_circuit_stats()
-    x_factor = xfi
-    print 'x_factor = %f'%x_factor
-    print '\n***Running pre_simp'
-    set_globals()
-    if n_latches() > 0:
-        status = pre_simp()
-    else:
-        status = check_sat()
-    if ((status <= Unsat) or (n_latches() == 0)):
-        print 'Time for proof = %f sec.'%(time.clock() - x)
-        return RESULT[status]
-    if n_ands() == 0:
-        #abc('bmc3 -T 2')
-        abc('&get;,bmc -vt=2')
-        if is_sat():
-            return 'SAT'
-    abc('trm')
-    write_file('smp')
-    abc('w %s_backup_%d.aig'%(initial_f_name,K))
-    K = K +1
-    set_globals()
-##    if ((n_ands() < 30000) and (a == 1) and (n_latches() < 300)):
-    if ((n_ands() < 30000) and (n_latches() < 300)):
-        print '\n***Running quick_verify'
-        status = quick_verify(0)
-        if status <= Unsat:
-            if not status == Unsat:
-                print 'CEX in frame %d'%cex_frame()
-            print 'Time for proof = %f sec.'%(time.clock() - x)
-            return RESULT[status]
-        if n_ands() == 0:
-            #abc('bmc3 -T 2')
-            abc('&get;,bmc -vt=2')
-            if is_sat():
-                return 'SAT'
-    print'\n***Running abstract'
-    nl_b = n_latches()
-    status = abstract()
-    abc('trm')
-    write_file('abs')
-    status = process_status(status)
-    if ((status <= Unsat)  or  status == Error):
-        if  status < Unsat:
-            print 'CEX in frame %d'%cex_frame()
-##            status = final_verify_recur(K)
-##            write_file('final')
-            print 'Time for proof = %f sec.'%(time.clock() - x)
-            return RESULT[status]
-        print 'Time for proof = %f sec.'%(time.clock() - x)
-        return RESULT[status]
-    abc('w %s_backup_%d.aig'%(initial_f_name,K))
-    K = K +1
-    if ((n_ands() > 20000) or (a == 1)):
-        print 'Speculation skipped because either too large or already done'
-        K = 2
-    elif n_ands() == 0:
-        print 'Speculation skipped because no AND nodes'
-        K = 2
-    else:
-        print '\n***Running speculate'
-        status = speculate()
-        abc('trm')
-        write_file('spec')
-        status = process_status(status)
-        if status == Unsat:
-            print 'Time for proof = %f sec.'%(time.clock() - x)
-            return RESULT[status]
-        if ((status < Unsat) or (status == Error)):
-            print 'CEX in frame %d'%cex_frame()
-            K = K-1 #if spec found a true cex, then result of abstract was wrong
-        else:
-            abc('w %s_backup_%d.aig'%(initial_f_name,K))
-            K = K +1
-    status = final_verify_recur(K)
-    abc('trm')
-    write_file('final')
-    print 'Time for proof = %f sec.'%(time.clock() - x)
-    return RESULT[status]
-
-def prove_g_pos(a):
-    """Proves the outputs clustered by a parameter a. 
-    a is the disallowed increase in latch support Clusters must be contiguous
-    If a = 0 then outputs are proved individually. Clustering is done from last to first
-    Output 0 is attempted to be proved inductively using other outputs as constraints.
-    Proved outputs are removed if all the outputs have not been proved.
-    If ever one of the proofs returns SAT, we stop and do not try any other outputs."""
-    global f_name, max_bmc,x_factor
-    x = time.clock()
-    #input_x_factor()
-    init_f_name = f_name
-    #fast_int(1)
-    print 'Beginning prove_g_pos'
-    prove_all_ind()
-    print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos()
-    print '\n************Running second level prove****************\n'
-    try_rpm()
-    result = prove(1) # 1 here means do not try speculate.
-    #result = prove_0_ind()
-    if result == 'UNSAT':
-        print 'Second prove returned UNSAT'
-        return result
-    if result == 'SAT':
-        print 'CEX found'
-        return result
-    print '\n********** Proving each output separately ************'
-    prove_all_ind()
-    print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos()
-    f_name = init_f_name
-    abc('w %s_osavetemp.aig'%f_name)
-    n = n_pos()
-    print 'Number of outputs = %d'%n
-    #count = 0
-    pos_proved = []
-    J = 0
-    jnext = n-1
-    while jnext >= 0:
-        max_bmc = -1
-        f_name = init_f_name
-        abc('r %s_osavetemp.aig'%f_name)
-        #Do in reverse order
-        jnext_old = jnext
-        if a == 0: # do not group
-            extract(jnext,jnext)
-            jnext = jnext -1 
-        else:
-            jnext = group(a,jnext)
-        if jnext_old > jnext+1:
-            print '\nProving outputs [%d-%d]'%(jnext + 1,jnext_old)
-        else:
-            print '\nProving output %d'%(jnext_old)
-        #ps()
-        #fast_int(1)
-        f_name = f_name + '_%d'%jnext_old
-        result = prove_1()
-        if result == 'UNSAT':
-            if jnext_old > jnext+1:
-                print '\n********  PROVED OUTPUTS [%d-%d]  ******** \n\n'%(jnext+1,jnext_old)
-            else:
-                print '\n********  PROVED OUTPUT %d  ******** \n\n'%(jnext_old)
-            pos_proved = pos_proved + range(jnext +1,jnext_old+1)
-            continue
-        if result == 'SAT':
-            print 'One of output in (%d to %d) is SAT'%(jnext + 1,jnext_old)
-            return result
-        else:
-            print '\n********  UNDECIDED on OUTPUTS %d thru %d  ******** \n\n'%(jnext+1,jnext_old)
-    f_name = init_f_name
-    abc('r %s_osavetemp.aig'%f_name)
-    if not len(pos_proved) == n:
-        print 'Eliminating %d proved outputs'%(len(pos_proved))
-        remove(pos_proved)
-        abc('trm')
-        write_file('group')
-        result = 'UNDECIDED'
-    else:
-        print 'Proved all outputs. The problem is proved UNSAT'
-        result = 'UNSAT'
-    print 'Total time for prove_g_pos = %f sec.'%(time.clock() - x)
-    return result
-
-def prove_pos():
-    """
-    Proved outputs are removed if all the outputs have not been proved.
-    If ever one of the proofs returns SAT, we stop and do not try any other outputs."""
-    global f_name, max_bmc,x_factor
-    x = time.clock()
-    #input_x_factor()
-    init_f_name = f_name
-    #fast_int(1)
-    print 'Beginning prove_pos'
-    prove_all_ind()
-    print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos()
-    print '\n********** Proving each output separately ************'
-    f_name = init_f_name
-    abc('w %s_osavetemp.aig'%f_name)
-    n = n_pos()
-    print 'Number of outputs = %d'%n
-    #count = 0
-    pos_proved = []
-    pos_disproved = []
-    J = 0
-    jnext = n-1
-    while jnext >= 0:
-        max_bmc = -1
-        f_name = init_f_name
-        abc('r %s_osavetemp.aig'%f_name)
-        #Do in reverse order
-        jnext_old = jnext
-        extract(jnext,jnext)
-        jnext = jnext -1 
-        print '\nProving output %d'%(jnext_old)
-        f_name = f_name + '_%d'%jnext_old
-        result = prove_1()
-        if result == 'UNSAT':
-            print '\n********  PROVED OUTPUT %d  ******** \n\n'%(jnext_old)
-            pos_proved = pos_proved + range(jnext +1,jnext_old+1)
-            continue
-        if result == 'SAT':
-            print '\n********  DISPROVED OUTPUT %d  ******** \n\n'%(jnext_old)
-            pos_disproved = pos_disproved + range(jnext +1,jnext_old+1)
-            continue
-        else:
-            print '\n********  UNDECIDED on OUTPUT %d  ******** \n\n'%(jnext_old)
-    f_name = init_f_name
-    abc('r %s_osavetemp.aig'%f_name)
-    list = pos_proved + pos_disproved
-    print 'Proved the following outputs: %s'%pos_proved
-    print 'Disproved the following outputs: %s'%pos_disproved
-    if not len(list) == n:
-        print 'Eliminating %d resolved outputs'%(len(list))
-        remove(list)
-        abc('trm')
-        write_file('group')
-        result = 'UNRESOLVED'
-    else:
-        print 'Proved or disproved all outputs. The problem is proved RESOLVED'
-        result = 'RESOLVED'
-    print 'Total time for prove_pos = %f sec.'%(time.clock() - x)
-    return result
-
-
-def prove_g_pos_split():
-    """like prove_g_pos but quits when any output is undecided"""
-    global f_name, max_bmc,x_factor
-    x = time.clock()
-    #input_x_factor()
-    init_f_name = f_name
-    #fast_int(1)
-    print 'Beginning prove_g_pos_split'
-    prove_all_ind()
-    print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos()
-    try_rpm()
-    print '\n********** Proving each output separately ************'  
-    f_name = init_f_name
-    abc('w %s_osavetemp.aig'%f_name)
-    n = n_pos()
-    print 'Number of outputs = %d'%n
-    pos_proved = []
-    J = 0
-    jnext = n-1
-    while jnext >= 0:
-        max_bmc = -1
-        f_name = init_f_name
-        abc('r %s_osavetemp.aig'%f_name)
-        jnext_old = jnext
-        extract(jnext,jnext)
-        jnext = jnext -1
-        print '\nProving output %d'%(jnext_old)
-        f_name = f_name + '_%d'%jnext_old
-        result = prove_1()
-        if result == 'UNSAT':
-            if jnext_old > jnext+1:
-                print '\n********  PROVED OUTPUTS [%d-%d]  ******** \n\n'%(jnext+1,jnext_old)
-            else:
-                print '\n********  PROVED OUTPUT %d  ******** \n\n'%(jnext_old)
-            pos_proved = pos_proved + range(jnext +1,jnext_old+1)
-            continue
-        if result == 'SAT':
-            print 'One of output in (%d to %d) is SAT'%(jnext + 1,jnext_old)
-            return result
-        else:
-            print '\n********  UNDECIDED on OUTPUTS %d thru %d  ******** \n\n'%(jnext+1,jnext_old)
-            print 'Eliminating %d proved outputs'%(len(pos_proved))
-            # remove outputs proved and return
-            f_name = init_f_name
-            abc('r %s_osavetemp.aig'%f_name)
-            remove(pos_proved)
-            abc('trm')
-            write_file('group')            
-            return 'UNDECIDED'
-    f_name = init_f_name
-    abc('r %s_osavetemp.aig'%f_name)
-    if not len(pos_proved) == n:
-        print 'Eliminating %d proved outputs'%(len(pos_proved))
-        remove(pos_proved)
-        abc('trm')
-        write_file('group')
-        result = 'UNDECIDED'
-    else:
-        print 'Proved all outputs. The problem is proved UNSAT'
-        result = 'UNSAT'
-    print 'Total time = %f sec.'%(time.clock() - x)
-    return result
-
-
-
-def group(a,n):
-    """Groups together outputs beginning at output n and any contiguous preceeding output
-    that does not increase the latch support by a or more"""
-    global f_name, max_bmc
-    nlt = n_latches()
-    extract(n,n)
-    nli = n_latches()
-    if n == 0:
-        return n-1
-    for J in range(1,n+1):
-        abc('r %s_osavetemp.aig'%f_name)
-        j = n-J
-        #print 'Running %d to %d'%(j,n)
-        extract(j,n)
-        #print 'n_latches = %d'%n_latches()
-        #if n_latches() >= nli + (nlt - nli)/2:
-        if n_latches() == nli:
-            continue
-        if n_latches() > nli+a:
-            break
-    abc('r %s_osavetemp.aig'%f_name)
-##    if j == 1:
-##        j = j-1
-    print 'extracting [%d-%d]'%(j,n)
-    extract(j,n)
-    ps()
-    return j-1
-        
-def extract(n1,n2):
-    """Extracts outputs n1 through n2"""
-    no = n_pos()
-    if n2 > no:
-        return 'range exceeds number of POs'
-    abc('cone -s -O %d -R %d'%(n1, 1+n2-n1))
-    abc('scl')
-
-def prove_0_ind():
-    """Uses all other outputs as constraints to try to prove output 0 by induction"""
-    abc('w %s_osavetemp.aig'%f_name)
-    #ps()
-    abc('constr -N %d'%(n_pos()-1))
-    #ps()
-    abc('fold')
-    #ps()
-    abc('ind -u -C 1000000 -F 20')
-    status = get_status()
-    abc('r %s_osavetemp.aig'%f_name)
-    return status
-
-def remove(list):
-    """Removes outputs in list"""
-    zero(list)
-    abc('&get;&trim;&put')
-    #fast_int(1)
-
-def zero(list):
-    """Zeros out POs in list"""
-    for j in list:
-        run_command('zeropo -N %d'%j)
-
-def sp():
-    """Alias for super_prove"""
-    print 'Executing super_prove'
-    result = super_prove()
-    return result
-
-def super_prove():
-    """Main proof technique now. Does original prove and if after speculation there are multiple output left
-    if will try to prove each output separately, in reverse order. It will quit at the first output that fails
-    to be proved, or any output that is proved SAT"""
-    global max_bmc, init_initial_f_name, initial_f_name
-    init_initial_f_name = initial_f_name
-    if x_factor > 1:
-        print 'x_factor = %d'%x_factor
-        input_x_factor()
-    max_bmc = -1
-    x = time.clock()
-    print "Trying BMC for 2 sec."
-    abc("&get; ,bmc -vt=2")
-    if is_sat():
-        print 'Total time taken by super_prove = %f sec.'%(time.clock() - x)
-        return 'SAT'
-    result = prove(0)
-    if ((result[:3] == 'UND') and (n_latches() == 0)):
-        return result
-    k = 1
-    print result
-    if not result[:3] == 'UND':
-        print 'Total time taken by super_prove = %f sec.'%(time.clock() - x)
-        return result
-    if n_pos() > 1:
-        result = prove_g_pos(0)
-        print result
-        if result == 'UNSAT':
-            print 'Total time taken by super_prove = %f sec.'%(time.clock() - x)
-            return result
-        if result == 'SAT':
-            k = 0 #Don't try to prove UNSAT on an abstraction that had SAT
-                    # should go back to backup 1 since probably spec was bad.
-    y = time.clock()
-    result = BMC_VER_result(k)
-    print 'Total time taken by last gasp verification = %f sec.'%(time.clock() - y)
-    print 'Total time for %s = %f sec.'%(init_initial_f_name,(time.clock() - x))
-    return result
-
-def reachm(t):
-    x = time.clock()
-    run_command('&get;&reach -vcs -T %d;&put'%t)
-    print 'Time = %f'%(time.clock() - x)
-    
-def reachx(t):
-    x = time.clock()
-    run_command('reachx -t %d'%t)
-    print 'Time = %f'%(time.clock() - x)
-
-def BMC_VER_result(n):
-    global init_initial_f_name
-    #print init_initial_f_name
-    xt = time.clock()
-    result = 5
-    T = 150
-    if n == 0:
-        abc('r %s_smp.aig'%init_initial_f_name)
-        print '\n***Running proof on initial simplified circuit\n',
-        ps()
-    else:
-        print '\n***Running proof on final unproved circuit'
-        ps()
-    print '    Running PDR for %d sec'%T
-    abc('&get;,pdr -vt=%d'%(T*.8))
-    result = get_status()
-    if result == Unsat:
-        return 'UNSAT'
-    if result > Unsat: #still undefined
-        if (n_pis()+n_latches() < 250):
-            print '    Running Reachability for 150 sec.'
-            abc('reachx -t 150')
-            #run_command('&get;&reach -vcs -T %d'%T)
-            result = get_status()
-            if result == Unsat:
-                return 'UNSAT'
-        if ((result > Unsat) and n ==1):
-            print '    Running interpolation for %f sec.'%T
-            abc(',imc -vt=%f'%T)
-            result = get_status()
-            if result == Unsat:
-                return 'UNSAT'
-    # if n=1 we are trying to prove result on abstracted circuit. If still undefined, then probably does
-    # not make sense to try pdr, reach, int on original simplified circuit, only BMC here.
-    if n == 1:
-        abc('r %s_smp.aig'%init_initial_f_name) #check if the initial circuit was SAT
-        #print 'Reading %s_smp'%init_initial_f_name,
-    #run_command('bmc3 -v -T %d -F 200000 -C 1000000'%T)
-    print '***Running BMC on initial simplified circuit'
-    ps()
-    print '\n'
-    abc('&get;,bmc -vt=%f'%T)
-    result = get_status()
-    if result < Unsat:
-        result = 'SAT'
-        print ' CEX found in frame %d'%cex_frame()
-    else:
-        result = 'UNDECIDED'
-    print 'Additional time taken by BMC/PDR/Reach = %f sec.'%(time.clock() - xt)
-    return result
-
-def try_split():
-    abc('w %s_savetemp.aig'%f_name)
-    na = n_ands()
-    split(3)
-    if n_ands()> 2*na:
-        abc('r %s_savetemp.aig'%f_name)
-    
-
-def time_diff():
-    global last_time
-    new_time = time.clock()
-    diff = new_time - last_time
-    last_time = new_time
-    result = 'Lapsed time = %.2f sec.'%diff
-    return result
-
-def prove_all_ind():
-    """Tries to prove output k by induction, using other outputs as constraints. If ever an output is proved
-    it is set to 0 so it can't be used in proving another output to break circularity.
-    Finally all zero'ed ooutputs are removed. """
-    N = n_pos()
-    remove_0_pos()
-    print '0 valued output removal changed POs from %d to %d'%(N,n_pos())
-    abc('w %s_osavetemp.aig'%f_name)
-    list = range(n_pos())
-    for j in list:
-        #abc('r %s_osavetemp.aig'%f_name)
-        abc('swappos -N %d'%j)
-        remove_0_pos() #may not have to do this if constr works well with 0'ed outputs
-        abc('constr -N %d'%(n_pos()-1))
-        abc('fold')
-        n = max(1,n_ands())
-        f = max(1,min(40000/n,16))
-        f = int(f)
-        abc('ind -u -C 10000 -F %d'%f)
-        status = get_status()
-        abc('r %s_osavetemp.aig'%f_name)
-        if status == Unsat:
-            print '+',
-            abc('zeropo -N %d'%j)
-            abc('w %s_osavetemp.aig'%f_name) #if changed, store it permanently
-        print '%d'%j,
-    remove_0_pos()
-    print '\nThe number of POs reduced from %d to %d'%(N,n_pos())
-    #return status
-
-def prove_all_pdr(t):
-    """Tries to prove output k by PDR. If ever an output is proved
-    it is set to 0. Finally all zero'ed ooutputs are removed. """
-    N = n_pos()
-    remove_0_pos()
-    print '0 valued output removal changed POs from %d to %d'%(N,n_pos())
-    abc('w %s_osavetemp.aig'%f_name)
-    list = range(n_pos())
-    for j in list:
-        #abc('r %s_osavetemp.aig'%f_name)
-        abc('cone -O %d -s'%j)
-        abc('scl')
-        abc('&get;,pdr -vt=%d'%t)
-        status = get_status()
-        abc('r %s_osavetemp.aig'%f_name)
-        if status == Unsat:
-            print '+',
-            abc('zeropo -N %d'%j)
-            abc('w %s_osavetemp.aig'%f_name) #if changed, store it permanently
-        print '%d'%j,
-    remove_0_pos()
-    print '\nThe number of POs reduced from %d to %d'%(N,n_pos())
-    #return status
-
-
-def remove_0_pos():
-    abc('&get; &trim; &put')
-
-    
-def prove_all_ind2():
-    """Tries to prove output k by induction, using outputs > k as constraints. Removes proved outputs from POs."""
-    abc('w %s_osavetemp.aig'%f_name)
-    plist = []
-    list = range(n_pos())
-##    if r == 1:
-##        list.reverse()
-    for j in list:
-        abc('r %s_osavetemp.aig'%f_name)
-        extract(j,n_pos())
-        abc('constr -N %d'%(n_pos()-1))
-        abc('fold')
-        n = max(1,n_ands())
-        f = max(1,min(40000/n,16))
-        f = int(f)
-        abc('ind -u -C 10000 -F %d'%f)
-        status = get_status()
-        if status == Unsat:
-            plist = plist + [j]
-            print '-',
-##        else:
-##            status = pdr(1)
-##            if status == Unsat:
-##                print '+',
-##                plist = plist + [j]
-        print '%d'%j,
-    print '\nOutputs proved = ',
-    print plist
-    abc('r %s_osavetemp.aig'%f_name)
-    remove(plist) #remove the outputs proved
-##    #the following did not work because abc command constr, allows only  last set of outputs to be constraints
-##    abc('w %s_osavetemp.aig'%f_name)
-##    plist = []
-##    list = range(n_pos())
-##    list.reverse()
-##    for j in list:
-##        abc('r %s_osavetemp.aig'%f_name)
-##        extract(j,n_pos())
-##        abc('constr -N %d'%(n_pos()-1))
-##        abc('fold')
-##        n = max(1,n_ands())
-##        f = max(1,min(40000/n,16))
-##        f = int(f)
-##        abc('ind -u -C 10000 -F %d'%f)
-##        status = get_status()
-##        if status == Unsat:
-##            plist = plist + [j]
-##            print '-',
-####        else:
-####            status = pdr(1)
-####            if status == Unsat:
-####                print '+',
-####                plist = plist + [j]
-##        print '%d'%j,
-##    print '\nOutputs proved = ',
-##    print plist.reverse
-##    abc('r %s_osavetemp.aig'%f_name)
-##    remove(plist) #remove the outputs proved
-##    return status
-
-def pdr(t):
-    abc('&get; ,pdr -vt=%f'%t)
-    result = get_status()
-
-def split(n):
-    abc('orpos;&get')
-    abc('&posplit -v -N %d;&put;dc2;trm'%n)
-
-def keep_splitting():
-    for j in range(5):
-        split(5+j)
-        no = n_pos()
-        status = prove_g_pos_split(0)
-        if status <= Unsat:
-            return status
-        if no == n_pos():
-            return Undecided
-
-def drill(n):
-    run_command('&get; &reach -vcs -H 5 -S %d -T 50 -C 40'%n)
-
-def prove_1():
-    """Proves all the outputs together. If ever an abstraction was done then if SAT is returned,
-        we make RESULT return "undecided".
-        """
-    a = 1
-    global x_factor,xfi,f_name
-    x = time.clock()
-    max_bmc = -1
-    K = 0
-    print 'Initial: ',
-    print_circuit_stats()
-    x_factor = xfi
-    print 'x_factor = %f'%x_factor
-    print '\n***Running pre_simp'
-    set_globals()
-    status = pre_simp()
-    if ((status <= Unsat) or (n_latches == 0)):
-        print 'Time for proof = %f sec.'%(time.clock() - x)
-        return RESULT[status]
-    abc('trm')
-    write_file('smp')
-    abc('w %s_backup_%d.aig'%(initial_f_name,K))
-    K = K +1
-    set_globals()
-    if ((n_ands() < 30000) and (a == 1) and (n_latches() < 300)):
-        print '\n***Running quick_verify'
-        status = quick_verify(0)
-        if status <= Unsat:
-            if not status == Unsat:
-                print 'CEX in frame %d'%cex_frame()
-            print 'Time for proof = %f sec.'%(time.clock() - x)
-            return RESULT[status]
-    print'\n***Running abstract'
-    nl_b = n_latches()
-    status = abstract()
-    abc('trm')
-    write_file('abs')
-    status = process_status(status)
-    if ((status <= Unsat)  or  status == Error):
-        if  status < Unsat:
-            print 'CEX in frame %d'%cex_frame()
-            print 'Time for proof = %f sec.'%(time.clock() - x)
-            return RESULT[status]
-        print 'Time for proof = %f sec.'%(time.clock() - x)
-        return RESULT[status]
-    abc('w %s_backup_%d.aig'%(initial_f_name,K))
-    status = final_verify_recur(2)
-    abc('trm')
-    write_file('final')
-    print 'Time for proof = %f sec.'%(time.clock() - x)
-    return RESULT[status]
-
-def qprove():
-    global x_factor
-    x = time.clock()
-    x_factor = 3
-    print '\n*********pre_simp**********\n'
-    pre_simp()
-    print '\n*********absv**********\n'
-    result = absv(3,1)
-    x_factor = 2
-    print '\n*********absv**********\n'
-    result = absv(3,1)
-    print '\n*********speculate**********\n'
-    result = speculate()
-    if result <= Unsat:
-        return RESULT[result]
-    print '\n*********absv**********\n'
-    result = absv(3,1)
-    print '\n*********prove_pos**********\n'
-    result = prove_pos()
-    if result == 'UNDECIDED':
-        print '\n*********BMC_VER_result**********\n'
-        result = BMC_VER_result(1)
-    print 'Time for proof = %f sec.'%(time.clock() - x)
-    return result
-    
-def pre_reduce():
-    x = time.clock()
-    pre_simp()
-    write_file('smp')
-    abstract()
-    write_file('abs')
-    print 'Time = %f'%(time.clock() - x)
-
-
-#PARALLEL FUNCTIONS
-"""  funcs should look like
-funcs = [defer(abc)('&get;,bmc -vt=50;&put'),defer(super_prove)()]
-After this is executed funcs becomes a special list of lambda functions
-which are given to abc_split_all to be executed as in fork below.
-It has been set up so that each of the functions works on the current aig and
-possibly transforms it. The new aig and status is always read into the master when done
-
-"""
-
-def fork(funcs):
-    """ runs funcs in parallel"""
-    for i,res in pyabc_split.abc_split_all(funcs):
-        status = prob_status()
-        if not status == -1:
-            print i,status
-            ps()
-            break
-        else:
-            print i,status
-            ps()
-            continue
-    return status
-
-def handler_s(res):
-    """ This serial handler returns True if the problem is solved by the first returning function,
-    in which case, the problem is replaced by the new aig and status.
-    """
-    if not res == -1:
-        #replace_prob()
-        print ('UNSAT','SAT')[res]
-        return True
-    else:
-        return False
-