pyabc: updated Bob's scripts

5 files changed, 5125 insertions, 395 deletions

diff --git a/scripts/abc.rc b/scripts/abc.rc
index b7144f4a..c04151da 100644
--- a/scripts/abc.rc
+++ b/scripts/abc.rc
@@ -1,14 +1,15 @@
 python new_abc_commands.py
 python reachx_cmd.py
-#python C:\Research\ABC\AIG\Python\reachx_cmd.py
+
+load_plugin bip "Bip"
 
 # global parameters
 set check         # checks intermediate networks
 #set checkfio      # prints warnings when fanins/fanouts are duplicated
-set checkread     # checks new networks after reading from file
-set backup        # saves backup networks retrived by "undo" and "recall"
-set savesteps 1   # sets the maximum number of backup networks to save 
-set progressbar   # display the progress bar
+#set checkread     # checks new networks after reading from file
+#set backup        # saves backup networks retrived by "undo" and "recall"
+#set savesteps 1   # sets the maximum number of backup networks to save 
+#set progressbar   # display the progress bar
 
 # program names for internal calls
 set dotwin dot.exe
@@ -25,6 +26,10 @@ set gnuplotwin wgnuplot.exe
 set gnuplotunix gnuplot
 
 # standard aliases
+alias srw "b; rw; b"
+alias fix "ps; st; ps; srw; ps; plat; cycle -x -F 1; plat; logic; undc; st; zero; ps; scorr; ps" 
+alias fixp "st; srw; cycle -x -F 1; logic; undc; st; zero "
+
 alias b balance
 alias cl cleanup
 alias clp collapse
@@ -67,8 +72,8 @@ alias rvl read_verlib
 alias rsup read_super mcnc5_old.super
 alias rlib read_library
 alias rlibc read_library cadence.genlib
-alias rw rewrite
-alias rwz rewrite -z
+alias rw drw
+alias rwz drw -z
 alias rf refactor
 alias rfz refactor -z
 alias re restructure
@@ -98,18 +103,18 @@ alias wv write_verilog
 
 # standard scripts
 alias share       "b; multi; fx; b"
-alias resyn       "b; rw; rwz; b; rwz; b"
-alias resyn2      "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
-alias resyn2a     "b; rw; b; rw; rwz; b; rwz; b"
+alias resyn       "b; drw; rwz; b; rwz; b"
+alias resyn2      "b; drw; rf; b; drw; rwz; b; rfz; rwz; b"
+alias resyn2a     "b; drw; b; drw; rwz; b; rwz; b"
 alias resyn3      "b; rs; rs -K 6; b; rsz; rsz -K 6; b; rsz -K 5; b"
-alias compress    "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
+alias compress    "b -l; drw -l; rwz -l; b -l; rwz -l; b -l"
 
-alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
+alias compress2   "b -l; drw -l; rf -l; b -l; drw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
 alias choice      "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
 alias choice2     "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
-alias rwsat       "st; rw -l; b -l; rw -l; rf -l"
-alias rwsat2      "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l"
-alias shake       "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
+alias rwsat       "st; drw -l; b -l; drw -l; rf -l"
+alias rwsat2      "st; drw -l; b -l; drw -l; rf -l; fraig; drw -l; b -l; drw -l; rf -l"
+alias shake       "st; ps; sat -C 5000; drw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
 
 alias snap fraig_store
 alias unsnap fraig_restore
@@ -126,24 +131,24 @@ alias icb "ic -M 2 -B 10 -s"
 alias cs "care_set "
 
 # resubstitution scripts for the IWLS paper
-alias src_rw      "st; rw -l; rwz -l; rwz -l" 
+alias src_rw      "st; drw -l; rwz -l; rwz -l" 
 alias src_rs      "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l" 
-alias src_rws     "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" 
-alias resyn2rs    "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b"
-alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
+alias src_rws     "st; drw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" 
+alias resyn2rs    "b; rs -K 6; drw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; drw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b"
+alias compress2rs "b -l; rs -K 6 -l; drw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; drw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
 alias c2 "ua; compress2rs; sa"
 alias ic "indcut -v"
 alias lp "lutpack"
 alias c "ua; compress; sa"
-alias c1 "ua; compress;b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; sa" 
+alias c1 "ua; compress;b -l; rs -K 6 -l; drw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; sa" 
 alias dr dretime
 alias ds dsec -v
 alias dp dprove -v
 
 
 # experimental implementation of don't-cares
-alias resyn2rsdc    "b; rs -K 6 -F 2; rw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; rw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b"
-alias compress2rsdc "b -l; rs -K 6 -F 2 -l; rw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; rw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
+alias resyn2rsdc    "b; rs -K 6 -F 2; drw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; drw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b"
+alias compress2rsdc "b -l; rs -K 6 -F 2 -l; drw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; drw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
 
 # minimizing for FF literals
 alias fflitmin    "compress2rs; ren; sop; ps -f"
@@ -222,9 +227,10 @@ alias lcr "&get; &lcorr; &put"
 
 alias trm "logic;trim;st;ps"
 
-alias smp   "ua;ps;scl;ps;rw;dr;lcorr;rw;dr;ps;scorr;ps;fraig;ps;dc2;dr;scorr -F 2;ps;dc2rs;w temp.aig"
-alias smp1   "ua;ps;scl;ps;rw;dr;lcorr;rw;dr;ps;scorr;ps;fraig;ps;dc2;dr;ps;dc2rs;w temp.aig"
-alias smpf  "ua;ps;scl;lcr;ps;rw;dr;ps;scr;ps;dc2;&get;&scorr -F 2;&put;dr;ps;dc2;ps;w temp.aig"
+alias smp   "ua;ps;scl;ps;drw;dr;lcorr;drw;dr;ps;scorr;ps;fraig;ps;dc2;dr;scorr -F 2;ps;dc2rs;w temp.aig"
+alias smp1   "scl;drw;dr;lcorr;drw;dr;scorr;fraig;dc2rs"
+alias smp2   "ua;ps;scl;ps;drw;dr;lcorr;drw;dr;ps;scorr;ps;fraig;ps;dc2;dr;ps;dc2rs;w temp.aig"
+alias smpf  "ua;ps;scl;lcr;ps;drw;dr;ps;scr;ps;dc2;&get;&scorr -F 2;&put;dr;ps;dc2;ps;w temp.aig"
 
 
 alias &smp   "ua;&get;&ps;&scl;&ps;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&ps;&scorr;&ps;&fraig;&ps;&dc2;&put;dr;&get;&scorr -F 2;&ps;&dc2;&put;w temp.aig"
@@ -233,7 +239,7 @@ alias smplite '&get;&scl;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&dc2;
 
 alias &smp1   "ua;&get;&ps;&scl;&ps;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&ps;&scorr;&ps;&fraig;&ps;&dc2;&put;dr;&get;&ps;&dc2;&put;w temp.aig"
 
-alias &smpf  "ua;ps;rw;&get;&ps;&scl;&ps;&put;dr;&get;&ps;&lcorr;&ps;&dc2;&ps;&scorr;&ps;&put;rw;ps;w temp.aig"
+alias &smpf  "ua;ps;drw;&get;&ps;&scl;&ps;&put;dr;&get;&ps;&lcorr;&ps;&dc2;&ps;&scorr;&ps;&put;drw;ps;w temp.aig"
 
 #for each output separately
 alias simpk "dprove -vrcbkmiu -B 10 -D 1000"
@@ -323,7 +329,12 @@ alias %scr "%get;%st;%scorr;%put;st"
 
 alias sc "fold;w tempc.aig;unfold -s"
 alias uc "r tempc.aig;unfold -s"
-alias smpc "scl;rw;ps;scorr -c;ps;fraig;ps;compress2rs;ps"
+alias smpc "scl;drw;ps;scorr -c;ps;fraig;ps;compress2rs;ps"
+
+alias abseen "&get;,abs -vt=60 -timeout=60 -bob=10 -aig=temp.aig;r temp.aig"
+alias pdreen "&get;,pdr -vt=60"
+alias inteen "&get;,imc -vt=60"
+alias bmceen "&get;,bmc -vt=60"
 
 
 
diff --git a/scripts/abc_common.py b/scripts/abc_common.py
index 891a918b..df2b731b 100644
--- a/scripts/abc_common.py
+++ b/scripts/abc_common.py
@@ -1,9 +1,13 @@
 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
 
 """
@@ -40,7 +44,7 @@ stackno_gabs = stackno_gore = stackno_greg= 0
 STATUS_UNKNOWN = -1
 STATUS_SAT = 0
 STATUS_UNSAT = 1
-RESULT = ('SAT' , 'SAT', 'UNSAT', 'UNDECIDED but reduced', 'UNDECIDED, no reduction', 'UNDCIDED but reduced'  )
+RESULT = ('SAT' , 'SAT', 'UNSAT', 'UNDECIDED', 'UNDECIDED,', 'UNDCIDED'  )
 Sat_reg = 0
 Sat_true = 1
 Unsat = 2
@@ -190,29 +194,6 @@ def read_file():
 def rf():
     read_file()
 
-##def read_file():
-##    """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
-##    x_factor = 1
-##    max_bmc = -1
-##    print 'Type in the name of the aig file to be read in'
-##    s = raw_input()
-##    if s[-4:] == '.aig':
-##        f_name = s[:-4]
-##    else:
-##        f_name = s
-##        s = s+'.aig'
-##    run_command(s)
-##    initial_f_name = f_name
-##    print_circuit_stats()
-##    
-##def rf():
-##    """just an alias for read_file"""
-##    read_file()
 
 def write_file(s):
     """this is the main method for writing the current circuit to an AIG file on disk.
@@ -236,7 +217,7 @@ def wf():
 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 abstract ones, for which it is known that there is not cex out to that depth."""
+    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)
@@ -301,43 +282,7 @@ def rc(file):
     """reads <file> so that if constraints are explicit, it will preserve them"""
     abc('&r %s;&put'%file)                         
 
-##def push(file):
-##    """ saves <file>.aig in stack_x"""
-##    global stackno_gabs, stackno_gsrm, stackno_greg
-##    if 'gabs' in file:
-##        snm = 'gabs'
-##    elif 'gsrm' in file:
-##        snm = 'gsrm'
-##    elif 'x' in file:
-##        snm = 'greg'
-##    else:
-##        print 'wrong file name'
-##        return 
-##    print snm
-##    sn = 'stackno_%s'%snm
-##    print sn
-##    exec 'sn += sn'
-##    print sn, eval(sn)
-##    run_command("r %s.aig"%file)
-##    run_command("w %s_%d.aig"%(file,eval(sn)))
-##
-##def pop(file):
-##    """ reads top <file>.aig in stack_1 and saves it in <file>.aig"""
-##    global stackno_gabs, stackno_gsrm, stackno_greg
-##    if 'gabs' in file:
-##        sn = 'gabs'
-##    if 'gsrm' in file:
-##        sn = 'gsrm'
-##    if 'x' in file:
-##        sn = 'greg'
-##    else:
-##        print 'wrong file name'
-##        return 
-##    run_command("r %s_%d.aig"%(file,eval(sn)))
-##    run_command("w %s.aig"%file)
-##    os.remove("%s_%d.aig"%(file,eval(sn))) 
-##    exec 'sn = sn-1'
-##    # need to protect against wrong stack count
+
 
 def fast_int(n):
     """This is used to eliminate easy-to-prove outputs. Arg n is conflict limit to be used
@@ -382,10 +327,10 @@ def simplify():
     # set_globals()
 ##    print 'simplify initial ',
 ##    ps()
-    abc('w t.aig')
+    #abc('w t.aig')
     n=n_ands()
     abc('scl')
-    if n > 30000:
+    if n > 40000:
         abc('&get;&scl;&put')
         n = n_ands()
         if n < 100000:
@@ -393,7 +338,7 @@ def simplify():
             run_command('ps')
             print '.',
             n = n_ands()
-            if n<45000:
+            if n<60000:
                 abc("&get;&scorr -F 2;&put;dc2rs")
                 print '.',
                 #ps()
@@ -403,28 +348,34 @@ def simplify():
                 #ps()
             n = n_ands()
     n = n_ands()
-    if n <= 30000:
+    if n <= 40000:
         print '.',
         #ps()
-        if n > 15000:
+        if n > 30000:
             abc("dc2rs")
             print '.',
-        else:
-            abc("scorr -F 2;dc2rs")
-            print '.',
-            #ps()
+##        else:
+##            abc("scorr -F 2;dc2rs")
+##            print '.',
+##            ps()
     n = max(1,n_ands())
-    ps()
-    if n < 20000:
+    #ps()
+    if n < 30000:
+        abc('scl;rw;dr;lcorr;rw;dr')
         m = int(min( 60000/n, 16))
         #print 'm = %d'%m
-        if m >= 4:
-            j = 4
+        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 check_size() == 1:
+                #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()
@@ -464,6 +415,25 @@ def iterate_simulation(latches_before):
             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"""
@@ -472,8 +442,7 @@ def iterate_abstraction_refinement(latches_before,NBF):
         F = 2000
     else:
         F = 2*NBF
-    print '\nIterating BMC or BDD reachability'
-    reach_sw = 0
+    print '\nIterating BMC/PDR'
     always_reach = 0
     cexf = 0
     reach_failed = 0
@@ -490,36 +459,47 @@ def iterate_abstraction_refinement(latches_before,NBF):
         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  (reach_sw ==1)) and not reach_failed)):
+        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))
-            reach_sw = 1
+            #cmd = 'reachx -t %d'%max(10,int(t))
+            cmd = '&get;,pdr -vt=%f'%t
         else:
-            reach_sw = 0
-            cmd = 'bmc3 -C %d -T %f -F %d'%(G_C,t,F)
-        print 'RUNNING %s'%cmd
+            #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 'Reachability went to %d frames, '%n_bmc_frames()
+            #print 'Depth reached %d frames, '%n_bmc_frames()
             print 'UNSAT'
             return Unsat
         cexf = cex_frame()
-        set_max_bmc(cexf -1)
-        if ((not is_sat()) and (reach_sw == 1)):
+        #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():
-            set_max_bmc(cex_frame()-1)
+            #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()
-            if reach_sw == 0:
+            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
@@ -543,29 +523,18 @@ def abstract():
     print 'Start: ',
     print_circuit_stats()
     c = 1.5*G_C
-    #c = 20000
-    t = max(1,1.25*G_T)
-    method = 3
-    if n_ands() > 100000:
-        method = 0
+    #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
-    if max_bmc == -1:
-        time = max(1,.01*G_T)
-        abc('bmc3 -C %d -T %f -F 165'%(.01*G_C, time))
-        set_max_bmc(bmc_depth())
-    f = min(250,1.5*max_bmc)
-    f = max(20, f)
-    f = 10*f
-    if not method == 0:
-        b = 10
-        b = max(b,max_bmc+2)
-        b = b*2**(x_factor-1)
-        b = 2*b
-        print 'Neen abstraction params: Bob = %d, Method #%d, %d conflicts, %d stable, %d sec., %d frames'%(b,method,c/3,s,t,f)
-        abc('&get; &abs_newstart -v -B %f -A %d -C %d -S %d -V %f -F %d'%(b,method,c/3,s,t,f))
-    else:
-        abc('&get;&abs_start -v -C 500000 -R 1')
-    #abc('w abstemp.aig')
+    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
@@ -573,8 +542,8 @@ def abstract():
     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()
+##    print 'First abstraction: ',
+##    print_circuit_stats()
     latches_after = n_latches()
     #if latches_before_abs == latches_after:
     if latches_after >= .98*latches_before_abs:
@@ -583,7 +552,7 @@ def abstract():
         return Undecided_no_reduction    
     # refinement loop
     if (n_ands() + n_latches() + n_pis()) < 15000:
-        print 'Running simulation iteratively'
+        print '\n***Running simulation iteratively'
         for i in range(5):
             result = iterate_simulation(latches_before_abs)
             if result == Restart:
@@ -610,7 +579,8 @@ def absv(n,v):
     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('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)
@@ -648,7 +618,7 @@ def spec():
     set_globals()
     t = max(1,.5*G_T)
     r = max(1,int(t))
-    print 'Running &equiv2 with C = %d, T = %f sec., F = %d -S 1 -R %d'%(G_C,t,200,r)
+    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()
@@ -723,11 +693,13 @@ def speculate():
     set_globals()
     t = max(1,.5*G_T)
     r = max(1,int(t))
-    print '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('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()
+    #print 'Speculation good to %d frames'%n_bmc_frames()
     #simplify()
     if n_pos_before == n_pos():
         print 'No new outputs. Quitting speculate'
@@ -735,6 +707,12 @@ def speculate():
     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:
@@ -746,7 +724,7 @@ def speculate():
     elif k < 120000:
         n = 8
     if n > 0: # simulation can run out of memory for too large designs, so be careful
-        print 'RUNNING simulation iteratively'          
+        print '\n***RUNNING simulation iteratively'          
         for i in range(5):
             result = run_simulation(n)
             if result == Sat_true:
@@ -757,6 +735,7 @@ def speculate():
     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()
@@ -788,7 +767,8 @@ def speculate():
                 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():            
+            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'
@@ -800,11 +780,13 @@ def speculate():
             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)))
-            if (((reach_allowed  or  (reach_sw == 1)) and not reach_failed)):
+            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))
-                reach_sw = 1
+                #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:
@@ -812,16 +794,19 @@ def speculate():
                 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)
-                reach_sw = 0            
-            print 'Running %s'%cmd
+                #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)
+                #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[:3] == 'bmc')):
-                    print 'BMC found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame())
+                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
@@ -829,14 +814,16 @@ def speculate():
                     return Undecided_no_reduction
                 continue
             else:
-                set_max_bmc(bmc_depth())
+                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 reach_sw == 0:
+                if bmc:
+                    break
+                elif max_bmc > 1.2*last_bmc:
                     break
                 else:
-                    if prob_status() == 1:
-                        print 'Reachability converged in %d frames'%n_bmc_frames()
-                        return Unsat
                     reach_failed = 1
                     init = 1
                     continue
@@ -880,28 +867,39 @@ def quick_verify(n):
         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()
-    if is_sat():
-        return Sat_true   
+    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))
+    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
-    N = bmc_depth()
     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
+        print '    Running %s'%cmd
         abc(cmd)        
         status = get_status()
         if status <= Unsat:
@@ -944,7 +942,8 @@ def try_rpm():
         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('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:
@@ -970,13 +969,22 @@ def final_verify():
     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 'Running %s'%cmd
+        print '\n***Running %s'%cmd
         abc(cmd)        
         status = get_status()
         if status <= Unsat:
@@ -984,16 +992,17 @@ def final_verify():
             print RESULT[status]
             return status
         print 'BDD reachability aborted'          
-    #f = max(100,bmc_depth())
-    c = max(G_C/5, 1000)
-    t = max(1,G_T)
-    print '\nRUNNING interpolation with %d conflicts, %d sec, max 100 frames'%(c,t)
-    abc('int -v -F 100 -C %d -T %f'%(c,t))
+    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()
@@ -1005,7 +1014,7 @@ def check_sat():
     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('dsat -C %d'%G_C)
+    abc('orpos;dsat -C %d'%G_C)
     if is_sat():
         return Sat_true
     elif is_unsat():
@@ -1026,7 +1035,7 @@ 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 '\nTrying induction'
+    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)
@@ -1055,11 +1064,11 @@ def final_verify_recur(K):
         if status >= Unsat:
             return status
         if  i > 0:
-            print 'SAT returned, trying less abstract backup'
+            print 'SAT returned, Running less abstract backup'
             continue
         break
     if ((i == 0) and (status > Unsat) and (n_ands() > 0)):
-        print '\nTrying speculate on initial backup number %d:'%i,
+        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:
@@ -1073,29 +1082,42 @@ def final_verify_recur(K):
         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()
-    #print 'trying forward'
+    if n_latches == 0:
+        return check_sat()
+    #print '\n*** Running forward'
     try_forward()
-    #print 'trying quick simp'
+    #print \n*** Running quick simp'
     quick_simp()
-    #print 'trying_scorr_constr'
+    #print 'Running_scorr_constr'
     status = try_scorr_constr()
     #status = 3
-    #print 'trying trm'
+    #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()
@@ -1132,7 +1154,7 @@ def try_phase():
     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() > 30000)):
+    if ((n == 1) or (n_ands() > 40000)):
         return
     print 'Number of possible phases = %d'%n
     abc('w %s_savetemp.aig'%f_name)
@@ -1140,7 +1162,7 @@ def try_phase():
     nl = n_latches()
     ni = n_pis()
     no = n_pos()
-    cost_init = (1*n_pis())+(2*n_latches())+.05*n_ands()
+    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)
@@ -1158,7 +1180,7 @@ def try_phase():
         #print_circuit_stats()
         abc('rw;lcorr;trm')
         #print_circuit_stats()
-        cost = (1*n_pis())+(2*n_latches())+.05*n_ands()
+        cost = (1*n_pis())+(2*n_latches())+1*n_ands()
         if cost < cost_min:
             cost_min = cost
             abc('w %s_best.aig'%f_name)
@@ -1207,7 +1229,6 @@ def quick_simp():
         abc('&get;&scl;&put;rw')
 
 def scorr_constr():
-    #return Undecided_no_reduction #temporarily disable the for the moment
     """Extracts implicit constraints and uses them in signal correspondence
     Constraints that are found are folded back when done"""
     na = max(1,n_ands())
@@ -1223,18 +1244,13 @@ def scorr_constr():
     else:
         cmd = 'unfold'
     abc(cmd)
-    if ((n_ands() > na) or (n_pos() == 1)):
+    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 %dd'%f)
-    if n_pos_before == 1:
-        #abc('cone -s -O 0') #don't fold constraints back in
-        abc('fold')
-    else:
-        abc('fold')
-##    abc('fold')
+    abc('scorr -c -F %d'%f)
+    abc('fold')
     return Undecided_no_reduction
 
 def process_status(status):
@@ -1253,7 +1269,7 @@ def input_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 = 0 we skip the first quick_verify"""
+        If a == 1 do not run speculate"""
     global x_factor,xfi,f_name
     x = time.clock()
     max_bmc = -1
@@ -1262,14 +1278,18 @@ def prove(a):
     print_circuit_stats()
     x_factor = xfi
     print 'x_factor = %f'%x_factor
-    print '\nRunning pre_simp'
+    print '\n***Running pre_simp'
     set_globals()
-    status = pre_simp()
-    if status <= Unsat:
+    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('bmc3 -T 2')
+        abc('&get;,bmc -vt=2')
         if is_sat():
             return 'SAT'
     abc('trm')
@@ -1277,8 +1297,9 @@ def prove(a):
     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 '\nRunning quick_verify'
+##    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:
@@ -1286,10 +1307,11 @@ def prove(a):
             print 'Time for proof = %f sec.'%(time.clock() - x)
             return RESULT[status]
         if n_ands() == 0:
-            abc('bmc3 -T 2')
+            #abc('bmc3 -T 2')
+            abc('&get;,bmc -vt=2')
             if is_sat():
                 return 'SAT'
-    print'\nRunning abstract'
+    print'\n***Running abstract'
     nl_b = n_latches()
     status = abstract()
     abc('trm')
@@ -1306,27 +1328,14 @@ def prove(a):
         return RESULT[status]
     abc('w %s_backup_%d.aig'%(initial_f_name,K))
     K = K +1
-    if status == Undecided_reduction:
-        print '\nRunning quick_verify'
-        status = quick_verify(1)
-        status = process_status(status)
-        if status <= Unsat:
-            if  status < Unsat:
-                print 'CEX in frame %d'%cex_frame()
-                #print 'Time for proof = %f sec.'%(time.clock() - x)
-                status = final_verify_recur(K-1)
-            abc('trm')
-            write_file('final')
-            print 'Time for proof = %f sec.'%(time.clock() - x)
-            return RESULT[status]
-    if n_ands() > 20000:
-        print 'Speculation skipped because too large'
+    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'
+        print 'Speculation skipped because no AND nodes'
         K = 2
     else:
-        print '\nRunning speculate'
+        print '\n***Running speculate'
         status = speculate()
         abc('trm')
         write_file('spec')
@@ -1359,11 +1368,11 @@ def prove_g_pos(a):
     init_f_name = f_name
     #fast_int(1)
     print 'Beginning prove_g_pos'
-    result = prove_all_ind()
+    prove_all_ind()
     print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos()
-    print '\n************Trying second level prove****************\n'
+    print '\n************Running second level prove****************\n'
     try_rpm()
-    result = prove(0)
+    result = prove(1) # 1 here means do not try speculate.
     #result = prove_0_ind()
     if result == 'UNSAT':
         print 'Second prove returned UNSAT'
@@ -1372,7 +1381,7 @@ def prove_g_pos(a):
         print 'CEX found'
         return result
     print '\n********** Proving each output separately ************'
-    result = prove_all_ind()
+    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)
@@ -1428,20 +1437,16 @@ def prove_g_pos(a):
     return result
 
 def prove_pos():
-    """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
-    a=0
     x = time.clock()
     #input_x_factor()
     init_f_name = f_name
     #fast_int(1)
-    print 'Beginning prove_g_pos'
-    result = prove_all_ind()
+    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
@@ -1450,6 +1455,7 @@ def prove_pos():
     print 'Number of outputs = %d'%n
     #count = 0
     pos_proved = []
+    pos_disproved = []
     J = 0
     jnext = n-1
     while jnext >= 0:
@@ -1458,43 +1464,36 @@ def prove_pos():
         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)
+        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)
+            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
+            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 OUTPUTS %d thru %d  ******** \n\n'%(jnext+1,jnext_old)
+            print '\n********  UNDECIDED on OUTPUT %d  ******** \n\n'%(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)
+    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 = 'UNDECIDED'
+        result = 'UNRESOLVED'
     else:
-        print 'Proved all outputs. The problem is proved UNSAT'
-        result = 'UNSAT'
-    print 'Total time for prove_g_pos = %f sec.'%(time.clock() - x)
+        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
 
 
@@ -1506,7 +1505,7 @@ def prove_g_pos_split():
     init_f_name = f_name
     #fast_int(1)
     print 'Beginning prove_g_pos_split'
-    result = prove_all_ind()
+    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 ************'  
@@ -1575,7 +1574,7 @@ def group(a,n):
     for J in range(1,n+1):
         abc('r %s_osavetemp.aig'%f_name)
         j = n-J
-        #print 'trying %d to %d'%(j,n)
+        #print 'Running %d to %d'%(j,n)
         extract(j,n)
         #print 'n_latches = %d'%n_latches()
         #if n_latches() >= nli + (nlt - nli)/2:
@@ -1613,10 +1612,10 @@ def prove_0_ind():
     return status
 
 def remove(list):
-    """Removes outputs in list as well as easy output proved by fast interpolation"""
+    """Removes outputs in list"""
     zero(list)
-    abc('scl')
-    fast_int(1)
+    abc('&get;&trim;&put')
+    #fast_int(1)
 
 def zero(list):
     """Zeros out POs in list"""
@@ -1640,7 +1639,14 @@ def super_prove():
         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':
@@ -1662,60 +1668,64 @@ def super_prove():
     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
-    if n == 0:
-        print '\nTrying proof on initial simplified and abstracted circuit\n'
-        abc('r %s_smp.abs.aig'%init_initial_f_name)
-        ps()
-    x = time.clock()
+    xt = time.clock()
     result = 5
-    N = 0
     T = 150
-    if (n_pis()+n_latches() < 250):
-        print ' Trying deep Reachability'
-        run_command('reachx -t 150')
-        #run_command('&get;&reach -vcs -T %d'%T)
-        result = get_status()
-        if result == Unsat:
-            return 'UNSAT'
-        if ((result < Unsat) and (n == 0)):
-            N = 1
-    if ((result >= Unsat) and (N == 0)):
-        print 'Trying deep interpolation'
-        run_command('int -v -F 30000 -C 1000000 -T %d'%T)
-        result = get_status()
-        if result == Unsat:
-            return 'UNSAT'
-##    try_split()
-##    if n_pos() > 1:  
-##        result = prove_g_pos_split()
-##        if result[:5] == 'UNSAT':
-##            return result
-    #ps()
-    abc('r %s_smp.aig'%init_initial_f_name)
+    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()
-    if N == 1:
-        print '\nTrying deep interpolation on initial simplified circuit\n'
-        run_command('int -v -F 30000 -C 1000000 -T %d'%T)
-        result = get_status()
-        if result == Unsat:
-            return 'UNSAT'
-        if result < Unsat:
-            return 'SAT'
-    print '\nTrying deep BMC on initial simplified circuit\n'
-    run_command('bmc3 -v -T %d -F 200000 -C 1000000'%T)
+    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/ability = %f sec.'%(time.clock() - x)
+    print 'Additional time taken by BMC/PDR/Reach = %f sec.'%(time.clock() - xt)
     return result
 
 def try_split():
@@ -1733,12 +1743,74 @@ def time_diff():
     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 = []
-    for j in range(n_pos()):
+    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))
@@ -1750,12 +1822,50 @@ def prove_all_ind():
         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 inductively = ',
+    print '\nOutputs proved = ',
     print plist
     abc('r %s_osavetemp.aig'%f_name)
     remove(plist) #remove the outputs proved
-    return status
+##    #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')
@@ -1787,10 +1897,10 @@ def prove_1():
     print_circuit_stats()
     x_factor = xfi
     print 'x_factor = %f'%x_factor
-    print '\nRunning pre_simp'
+    print '\n***Running pre_simp'
     set_globals()
     status = pre_simp()
-    if status <= Unsat:
+    if ((status <= Unsat) or (n_latches == 0)):
         print 'Time for proof = %f sec.'%(time.clock() - x)
         return RESULT[status]
     abc('trm')
@@ -1799,14 +1909,14 @@ def prove_1():
     K = K +1
     set_globals()
     if ((n_ands() < 30000) and (a == 1) and (n_latches() < 300)):
-        print '\nRunning quick_verify'
+        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'\nRunning abstract'
+    print'\n***Running abstract'
     nl_b = n_latches()
     status = abstract()
     abc('trm')
@@ -1851,5 +1961,47 @@ def qprove():
     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
+    
diff --git a/scripts/main.py b/scripts/main.py
new file mode 100644
index 00000000..70dcf103
--- /dev/null
+++ b/scripts/main.py
@@ -0,0 +1,331 @@
+import os
+##import par
+##from abc_common import *
+import abc_common
+
+#this makes par the dominant module insteat of abc_common
+from par import *
+
+import sys
+import math
+import time
+from  pyabc_split import *
+##import pdb
+##from IPython.Debugger import Tracer; debug_here = Tracer()
+
+
+#x('source ../../abc.rc')
+#abc_common.x('source ../../abc.rc')
+
+
+#IBM directories
+# directories = ['ibmhard']
+ibmhard = (33,34,36,37,28,40,42,44,48,5,49,50,52,53,58,59,6,64,66,67,68,\
+           69,70,71,72,73,74,75,76,78,79,80,81,82,83,84,86,9,87,89,90,0,10,\
+           11,12,14,15,16,2,19,20,29,31,32)
+
+
+#directories = ['IBM_converted']
+#ibm_convert = (3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,\
+#               27,28,29,30,31,32,33,34,35,36,37,38,39,40,41)
+#IBM_converted = range(42)[3:]
+
+#the smaller files in ascending order
+#IBM_converted = (26,38,21,15,22,23,20,27,16,19,24,28,18,9,8,7,6,25,17,3,4)
+
+#the larger file in order (skipping 39)
+#IBM_converted = (39,5,40,41,13,12,10,14,11,31,33,36,29,34,35,37,30)
+IBM_converted = (5,40,41,13,12,10,14,11,31,33,36,29,34,35,37,30)
+
+def scorriter():
+    """ apply scorr with increasing conflicts up to 100"""
+    x('time')
+    run_command('r p_0.aig')
+    n = 20
+    while n < 1000:
+        print_circuit_stats()
+        run_command('scorr -C %d'%n)
+        x('ind -C %d'%1000)
+        if is_unsat():
+            print 'n = %d'%n
+            break
+        n = 2*n
+    x('time')
+     
+def simplifyq():
+    # set_globals()
+    n=n_ands()
+    if n > 30000:
+        if n<45000:
+            abc("&get;&scl;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr;&get;&scorr -F 2;&dc2;&put;w temp.aig")
+        else:
+            abc("&get;&scl;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr;&get;&dc2;&put;w temp.aig")
+    n = n_ands()
+    if n < 30000:
+        if n > 15000:
+            abc("scl;rw;dr;lcorr;rw;dr;scorr;fraig;dc2;dr;dc2rs;w temp.aig")
+        else:
+            abc("scl;rw;dr;lcorr;rw;dr;scorr;fraig;dc2;dr;scorr -F 2;dc2rs;w temp.aig")    
+    if n < 10000:
+        m = min( 30000/n, 8 )
+        if m > 2:
+            abc( "scorr -F %d"%m)
+    run_command("ps")
+
+def constraints():
+    """Determine if a set of files in a set of
+    directories has constraints and print out the results."""
+    for s in directories:
+        print("\ndirectory is "+s)
+        jj=eval(s)
+        print(jj)
+        for j in range(len(jj)):
+            x("\nr ../DIR/%s/p_%smp.aig"%(s,jj[j]))
+            print("structural:")
+            x('constr -s')
+            print("inductive constraints:")
+            x('constr ')
+
+def strip():
+    """Strip out each output of a multi-output example and write it
+    into a separate file"""
+    os.chdir('../DIR')
+    abc('r p_all_smp.aig')
+    po = n_pos()
+    print_circuit_stats()
+    for j in range(po):
+        abc('r p_all_smp.aig')
+        abc('cone -s -O %d'%j)
+        abc('scl;rw;trm')
+        abc('w p_%d.aig'%j)
+        print_circuit_stats()
+
+def lst(list,match):
+    result = []
+    for j in range(len(list)):
+        if list[j][-len(match):] == match:
+            result.append(list[j])
+    return result
+
+def lste(list,match,excp):
+    result = []
+    for j in range(len(list)):
+        if list[j][-len(match):] == match:
+            if excp in list[j]:
+                continue
+            result.append(list[j])
+    return result
+
+def blif2aig():
+    """ converts blif files into aig files"""
+    #os.chdir('../ibm-web')
+    list_all = os.listdir('.')
+    l_blif = lst(list_all,'.blif')
+    for j in range(len(l_blif)):
+        name = l_blif[j][:-5]
+        print '%s '%name,
+        abc('r %s.blif'%name)
+        abc('st')
+        abc('fold')
+        abc('w %s.aig'%name)
+        ps()
+
+def la():
+    return list_aig('')
+
+def list_aig(s):
+    """ prnts out the sizes of aig files"""
+    #os.chdir('../ibm-web')
+    list_all = os.listdir('.')
+    dir = lst(list_all,'.aig')
+    dir.sort()
+    for j in range(len(dir)):
+        name = dir[j][:-4]
+        if not s in name:
+            continue
+        print '%s '%name,
+        abc('r %s.aig'%name)
+        ps()
+    return dir
+
+def convert_ibm():
+    """ converts blif files (with constraints?) into aig files"""
+    os.chdir('../ibm-web')
+    list_ibm = os.listdir('.')
+    l_blif = lst(list_ibm,'.blif')
+    for j in range(len(l_blif)):
+        name = l_blif[j][:-5]
+        run_command('read_blif %s.blif'%name)
+        abc('undc')
+        abc('st -i')
+        abc('zero')
+        run_command('w %s.aig'%name)
+        """if a<100000000:
+            f = min(8,max(1,40000/a))
+            #run_command('scorr -c -F %d'%f)
+            #print 'Result of scorr -F %d: '%f,
+            print_circuit_stats()
+            run_command('w p_%d.aig'%j)"""
+
+def cl():
+    cleanup()
+
+def cleanup():
+    list = os.listdir('.') 
+    for j in range(len(list)):
+        name = list[j]
+        if (('_smp' in name) or ('_save' in name) or ('_backup' in name) or ('_osave' in name)
+            or ('_best' in name) or ('_gsrm' in name) or ('gore' in name) or 
+            ('_bip' in name) or ('sm0' in name) or ('gabs' in name) 
+            or ('temp' in name) or ('__' in name) or ('greg' in name) or ('tf2' in name)
+            or ('gsrm' in name) or ('_rpm' in name ) or ('gsyn' in name) or ('beforerpm' in name)
+            or ('afterrpm' in name) or ('initabs' in name) or ('.status' in name) or ('_init' in name)
+            or ('_osave' in name) or ('tt_' in name) or ('_before' in name) or ('_after' in name)
+            or ('_and' in name) or ('_final' in name) or ('_spec' in name) or ('temp.a' in name) or ('_sync' in name)
+            ):
+            os.remove(name)
+        
+def simp_mbi():
+    os.chdir('../mbi')
+    list_ibm = os.listdir('.')
+    l_aig = lst(list_ibm,'.aig')
+    for j in range(len(l_aig)):
+        name = l_aig[j][:-4]
+        run_command('r %s.aig'%name)
+        run_command('st')
+        print '\n%s: '%name
+        print_circuit_stats()
+        quick_simp()
+        scorr_comp()
+        simplify()
+        run_command('w %s_smp.aig'%name)
+
+def strip_names():
+    os.chdir('../mbi')
+    list_ibm = os.listdir('.')
+    l_aig = lst(list_ibm,'.aig')
+    for j in range(len(l_aig)):
+        name = l_aig[j][:-4]
+        run_command('r %s.aig'%name)
+        run_command('st')
+        print '\n%s: '%name
+        print_circuit_stats()
+        quick_simp()
+        scorr_comp()
+        simplify()
+        run_command('w %s_smp.aig'%name)
+
+def map_ibm():
+    os.chdir('../ibmmike2')
+    list_ibm = os.listdir('.')
+    l_blif = lst(list_ibm,'.blif')
+    result = []
+    print len(l_blif)
+    for j in range(len(l_blif)):
+        name = l_blif[j][:-5]
+        result.append('%s = %d'%(name,j))
+    return result
+
+
+def absn(a,c,s):
+    """ testing Niklas abstraction with various conflict limits
+    a= method (0 - regular cba,
+               1 - pure pba,
+               2 - cba with pba at the end,
+               3 cba and pba interleaved at each step
+    c = conflict limit
+    s = No. of stable steps without cex"""
+    global G_C, G_T, latches_before_abs, x_factor, f_name
+    set_globals()
+    latches_before_abs = n_latches()
+    print 'Start: ',
+    print_circuit_stats()
+    print 'Een abstraction params: Method #%d, %d conflicts, %d stable'%(a,c,s)
+    run_command('&get; &abs_newstart -v -A %d -C %d -S %d'%(a,c,s))
+    bmcdepth = n_bmc_frames()
+    print 'BMC depth = %d'%n_bmc_frames()
+    abc('&w absn_greg.aig; &abs_derive; &put; w absn_gabs.aig')
+    print 'Final abstraction: ',
+    print_circuit_stats()
+    write_file('absn')
+    return "Done"
+
+        
+def xfiles():
+    global f_name
+    #output = sys.stdout
+    #iterate over all ESS files
+    #saveout = sys.stdout
+    #output = open("ibm_log.txt",'w')
+    # sys.stdout = output
+    os.chdir('../ess/f58m')
+    print 'Directories are %s'%directories
+    for s in directories:
+        sss=  '../%s'%s
+        os.chdir(sss)
+        print "\nDirectory is %s\n"%s
+        jj=eval(s)
+        print (jj)
+        run_command('time')
+        for j in range(len(jj)):
+            print ' '
+            set_fname('p_%dsmp23'%jj[j])#file f_name.aig is read in
+            print 'p_%dsmp23'%jj[j]
+            run_command('time')
+            result = dprove3(1)
+            print result
+            run_command('time')
+        run_command('time')
+    os.chdir('../../python')
+    #sys.stdout = saveout
+    #output.close()
+
+def sublist(L,I):
+    z = []
+    for i in range(len(I)):
+        s = L[I[i]],
+        s = list(s)
+        z = z + s
+    return z
+
+def s2l(s):
+    """ takes the string s divided by '\n' and makess a list of items"""
+    result = []
+    while len(s)>2:
+        j = s.find('\n')
+        result.append(s[:j])
+        s = s[j+1:]
+    return result
+
+def select(lst, s):
+    result = []
+    print lst
+    for j in range(len(lst)):
+        if s in lst[j]:
+            s1 = lst[j]
+            k = s1.find(':')
+            s1 = s1[:k]
+            result.append(s1)
+    return result
+
+def process_result(name):
+    f = open(name,'r')
+    s = f.read()
+    f.close()
+    lst = s2l(s)
+    result = select(lst,'Timeout')
+    return result
+
+
+def main():
+    stackno = 0
+    if len(sys.argv) != 2:
+        print "usage: %s <aig filename>"%sys.argv[0]
+        sys.exit(1)
+    aig_filename = sys.argv[1]
+    x("source ../../abc.rc")
+    read(aig_filename)
+    dprove3(1)
+# a test to  whether the script is being called from the command line
+if __name__=="__main__":
+    main()
diff --git a/scripts/new_abc_commands.py b/scripts/new_abc_commands.py
index 21d62d33..83c4d8a3 100644
--- a/scripts/new_abc_commands.py
+++ b/scripts/new_abc_commands.py
@@ -1,36 +1,16 @@
-
-# You can use 'from pyabc import *' and then not need the pyabc. prefix everywhere
-
 import os
 import pyabc
-import abc_common
+import par
 import tempfile
 import shutil
 import redirect
-
-# A new command is just a function that accepts a list of string arguments
-#   The first argument is always the name of the command
-#   It MUST return an integer. -1: user quits, -2: error. Return 0 for success.
-
-# a command that calls prove(1) and returns success
-def prove_cmd(args):
-    result = abc_common.prove(1)
-    print result
-    return 0
-
-# registers the command:
-#   The first argument is the function
-#   The second argument is the category (mainly for the ABC help command)
-#   The third argument is the new command name
-#   Keep the fourth argument 0, or consult with Alan
-
-pyabc.add_abc_command(prove_cmd, "ZPython", "/prove", 0)
+import optparse
 
 def read_cmd(args):
     if len(args)==2:
-        abc_common.read_file_quiet(args[1])
+        par.read_file_quiet(args[1])
     else:
-        abc_common.read_file()
+        par.read_file()
     return 0
 
 pyabc.add_abc_command(read_cmd, "ZPython", "/rf", 0)
@@ -109,75 +89,61 @@ def print_aiger_result(args):
     
 pyabc.add_abc_command(print_aiger_result, "ZPython", "/print_aiger_result", 0)
 
-def super_prove_aiger_cmd(args):
-
-    noisy = len(args)==2 and args[1]=='-n'
+def proof_command_wrapper(prooffunc, category_name, command_name, change):
 
-    if not noisy:
-        pyabc.run_command('/pushredirect')
-        pyabc.run_command('/pushdtemp')
+    def wrapper(argv):
+        
+        usage = "usage: %prog [options] <aig_file>"
     
-    try:
-        result = abc_common.super_prove()
-    except:
-        result = None
+        parser = optparse.OptionParser(usage, prog=command_name)
     
-    if not noisy:
-        pyabc.run_command('/popdtemp')
-        pyabc.run_command('/popredirect')
-            
-    if result=="SAT":
-        print 1
-    elif result=="UNSAT":
-        print 0
-    else:
-        print 2
+        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")
 
-    return 0
-    
-pyabc.add_abc_command(super_prove_aiger_cmd, "ZPython", "/super_prove_aiger", 0)
-
-
-def prove_one_by_one_cmd(args):
-    
-    noisy = len(args)==2 and args[1]=='-n'
-
-    # switch to a temporary directory
-    pyabc.run_command('/pushdtemp')
-    
-    # write a copy of the original file in the temporary directory
-    pyabc.run_command('w original_aig_file.aig')
-    
-    # iterate through the ouptus
-    for po in range(0, pyabc.n_pos()):
+        options, args = parser.parse_args(argv)
         
-        if not noisy:
-            pyabc.run_command('/pushredirect')
-
-        # replace the nework with the cone of the current PO
-        pyabc.run_command( 'cone -O %d -s'%po )
+        if len(args) != 2:
+            print args
+            parser.print_usage()
+            return 0
+            
+        aig_filename = os.path.abspath(args[1])
 
-        # run super_prove
+        if not options.noisy:
+            pyabc.run_command('/pushredirect')
+            
+        if not options.current_dir:
+            pyabc.run_command('/pushdtemp')
+            
         try:
-            result = abc_common.super_prove()
-        except:
-            result = 'UNKNOWN'
+            basename = os.path.basename( aig_filename )
+            shutil.copyfile(aig_filename, basename)
+            aig_filename = basename
 
-        if not noisy:
-            pyabc.run_command('/popredirect')
+            par.read_file_quiet(aig_filename)
+            result = prooffunc()
+            
+            par.cex_list = []
+        except:
+            result = None
 
-        print 'PO %d is %s'%(po, result)
-        
-        # stop if the result is not UNSAT
-        if result != "UNSAT":
-            break
+        if not options.current_dir:
+            pyabc.run_command('/popdtemp')
 
-        # read the original file for the next iteration
-        pyabc.run_command('r original_aig_file.aig')
-        
-    # go back to the original directory
-    pyabc.run_command('/popdtemp')
+        if not options.noisy:
+            pyabc.run_command('/popredirect')
+                
+        if result=="SAT":
+            print 1
+        elif result=="UNSAT":
+            print 0
+        else:
+            print 2
 
-    return 0
+        return 0
     
-pyabc.add_abc_command(prove_one_by_one_cmd, "ZPython", "/prove_one_by_one", 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)
diff --git a/scripts/par.py b/scripts/par.py
new file mode 100644
index 00000000..21f209df
--- /dev/null
+++ b/scripts/par.py
@@ -0,0 +1,4270 @@
+from pyabc import *
+import pyabc_split
+import redirect
+import sys
+import os
+import time
+import math
+import main
+
+global G_C,G_T,latches_before_abs,latches_before_pba,n_pos_before,x_factor,methods,last_winner
+global last_cex,JV,JP, cex_list,max_bmc, last_cx, pord_on
+
+"""
+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 cex_get()
+int cex_put()
+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,', 'UNDECIDED'  )
+Sat = Sat_reg = 0
+Sat_true = 1
+Unsat = 2
+Undecided = 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
+j_last = 0
+seed = 113
+init_simp = 1
+K_backup = init_time = 0
+last_verify_time = 20
+last_cex = last_winner = 'None'
+last_cx = 0
+trim_allowed = True
+pord_on = False
+sec_sw = False
+sec_options = ''
+cex_list = []
+TERM = 'USL'
+t_init = 2 #initial time for poor man's concurrency.
+methods = ['PDR', 'INTRP', 'BMC',
+           'SIM', 'REACHX',
+           'PRE_SIMP', 'SUPER_PROVE2', 'PDRM', 'REACHM', 'BMC3','Min_Retime',
+           'For_Retime','REACHP','REACHN','PDRsd','prove_part_2',
+           'prove_part_3','verify','sleep','PDRMm','prove_part_1',
+           'run_parallel','INTRPb', 'INTRPm', 'REACHY', 'REACHYc','RareSim','simplify', 'speculate',
+           'quick_sec', 'BMC_J']
+#'0.PDR', '1.INTERPOLATION', '2.BMC', '3.SIMULATION',
+#'4.REACHX', '5.PRE_SIMP', '6.SUPER_PROVE', '7.PDRM', '8.REACHM', 9.BMC3'
+# 10. Min_ret, 11. For_ret, 12. REACHP, 13. REACHN 14. PDRseed 15.prove_part_2,
+#16.prove_part_3, 17.verify, 18.sleep, 19.PDRMm, 20.prove_part_1,
+#21.run_parallel, 22.INTRP_bwd, 23. Interp_m 24. REACHY 25. REACHYc 26. Rarity Sim 27. simplify
+#28. speculate, 29. quick_sec, 30 bmc3 -S
+win_list = [(0,.1),(1,.1),(2,.1),(3,.1),(4,.1),(5,-1),(6,-1),(7,.1)]
+FUNCS = ["(pyabc_split.defer(abc)('&get;,pdr -vt=%f'%t))",
+         "(pyabc_split.defer(abc)('&get;,imc -vt=%f'%(t)))",
+         "(pyabc_split.defer(abc)('&get;,bmc -vt=%f'%t))",
+         "(pyabc_split.defer(simulate)(t))",
+         "(pyabc_split.defer(abc)('reachx -t %d'%t))",
+         "(pyabc_split.defer(pre_simp)())",
+         "(pyabc_split.defer(super_prove)(2))",
+         "(pyabc_split.defer(pdrm)(t))",
+         "(pyabc_split.defer(abc)('&get;&reachm -vcs -T %d'%t))",
+         "(pyabc_split.defer(abc)('bmc3 -C 1000000 -T %f'%t))",
+         "(pyabc_split.defer(abc)('dr;&get;&lcorr;&dc2;&scorr;&put;dr'))",
+         "(pyabc_split.defer(abc)('dr -m;&get;&lcorr;&dc2;&scorr;&put;dr'))",
+         "(pyabc_split.defer(abc)('&get;&reachp -vr -T %d'%t))",
+         "(pyabc_split.defer(abc)('&get;&reachn -vr -T %d'%t))",
+         "(pyabc_split.defer(abc)('&get;,pdr -vt=%f -seed=521'%t))",
+         "(pyabc_split.defer(prove_part_2)(K))",
+         "(pyabc_split.defer(prove_part_3)(K))",
+         "(pyabc_split.defer(verify)(JV,t))",
+         "(pyabc_split.defer(sleep)(t))",
+         "(pyabc_split.defer(pdrmm)(t))",
+         "(pyabc_split.defer(prove_part_1)'(%d)'%(K))",
+         "(pyabc_split.defer(run_parallel)(JP,t,'TERM'))",
+         "(pyabc_split.defer(abc)('&get;,imc -bwd -vt=%f'%t))",
+         "(pyabc_split.defer(abc)('int -C 1000000 -F 10000 -K 2 -T %f'%t))",
+         "(pyabc_split.defer(abc)('&get;&reachy -v -T %d'%t))",
+         "(pyabc_split.defer(abc)('&get;&reachy -cv -T %d'%t))",
+         "(pyabc_split.defer(simulate2)(t))",
+         "(pyabc_split.defer(simplify)())",
+         "(pyabc_split.defer(speculate)())",
+         "(pyabc_split.defer(quick_sec)(t))",
+         "(pyabc_split.defer(bmc_s)(t))"
+         ]
+##         "(pyabc_split.defer(abc)('bmc3 -C 1000000 -T %f -S %d'%(t,int(1.5*max_bmc))))"
+#note: interp given 1/2 the time.
+allreachs = [4,8,12,13,24,25]
+reachs = [24]
+allpdrs = [0,7,14,19]
+pdrs = [0,7]
+allbmcs = [2,9,30]
+exbmcs = [2,9]
+bmcs = [9,30]
+allintrps = [1,22,23]
+bestintrps = [23]
+intrps = [23]
+allsims = [3,26]
+sims = [3]
+allslps = [18]
+slps = [18]
+
+JVprove = [7,1,4,24]
+JV = pdrs+intrps+bmcs+sims #sets what is run in parallel '17. verify' above
+JP = JV + [27] # sets what is run in  '21. run_parallel' above 27 simplify should be last because it can't time out.
+#_____________________________________________________________
+
+
+# Function definitions:
+# simple functions: ________________________________________________________________________
+# set_globals, abc, q, x, has_any_model, is_sat, is_unsat, push, pop
+
+# ALIASES
+
+def initialize():
+    global xfi, max_bmc, last_time,j_last, seed, init_simp, K_backup, last_verify_time
+    global init_time, last_cex, last_winner, trim_allowed, t_init, sec_options, sec_sw
+    global n_pos_before, n_pos_proved, last_cx, pord_on
+    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
+    j_last = 0
+    seed = 113
+    init_simp = 1
+    K_backup = init_time = 0
+    last_verify_time = 20
+    last_cex = last_winner = 'None'
+    last_cx = 0
+    trim_allowed = True
+    pord_on = False
+    t_init = 2 #this will start sweep time in find_cex_par to 2*t_init here
+    sec_sw = False
+    sec_options = ''
+    cex_list = []
+    n_pos_before = n_pos()
+    n_pos_proved = 0
+
+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 ;addpi'%f_name)
+    abc('w %s_savetempreal.aig'%f_name)
+    with redirect.redirect( redirect.null_file, sys.stdout ):
+##        with redirect.redirect( redirect.null_file, sys.stderr ):
+        reparam()
+    n = n_pis()
+    abc('r %s_savetempreal.aig'%f_name)
+    return n
+
+def timer(t):
+    btime = time.clock()
+    time.sleep(t)
+    print t
+    return time.clock() - btime
+
+def sleep(t):
+    time.sleep(t)
+    return Undecided
+        
+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 convert(t):
+    t = int(t*100)
+    return str(float(t)/100)
+
+def set_engines(N=0):
+    """
+    Sets the MC engines that are used in verification according to
+    if there are 4 or 8 processors.
+    """
+    global reachs,pdrs,sims,intrps,bmcs
+    if N == 0:
+        N = os.sysconf(os.sysconf_names["SC_NPROCESSORS_ONLN"])
+    if N == 1:
+        reachs = [24]
+        pdrs = [7]
+##        bmcs = [30]
+        bmcs = [9]
+        intrps = []
+        sims = []
+        slps = [18]
+    elif N == 2:
+        reachs = [24]
+        pdrs = [7]
+        bmcs = [30]
+        intrps = []
+        sims = []
+        slps = [18]
+    elif N == 4:
+        reachs = [24]
+        pdrs = [7]
+        bmcs = [9,30]
+        intrps = [23]
+        sims = []
+        slps = [18]
+    elif N == 8:
+        reachs = [24]
+        pdrs = [0,7]
+        bmcs = [9,30]
+        intrps = [23]
+        sims = [3]
+        slps = [18]
+
+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 remove_spaces(s):
+    y = ''
+    for t in s:
+        if not t == ' ':
+            y = y + t
+    return y
+
+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, win_list,seed, sec_options
+    global win_list, init_simp, po_map
+    set_engines(4) #temporary
+    ps()
+    init_simp = 1
+    win_list = [(0,.1),(1,.1),(2,.1),(3,.1),(4,.1),(5,-1),(6,-1),(7,.1)] #initialize winning engine list
+    po_map = range(n_pos())
+    initialize()
+##    x_factor = 1
+##    seed = 223
+##    max_bmc = -1
+    if fname is None:
+        print 'Type in the name of the aig file to be read in'
+        s = raw_input()
+        s = remove_spaces(s)
+    else:
+        s = fname
+    if s[-4:] == '.aig':
+        f_name = s[:-4]
+    else:
+        f_name = s
+        s = s+'.aig'
+##    run_command(s)
+    run_command('&r %s;&put'%s)
+    set_globals()
+    initial_f_name = f_name
+    init_initial_f_name = f_name
+    abc('addpi')
+    
+def read_file():
+    global win_list, init_simp, po_map
+    read_file_quiet()
+##    ps()
+##    init_simp = 1
+##    win_list = [(0,.1),(1,.1),(2,.1),(3,.1),(4,.1),(5,-1),(6,-1),(7,.1)] #initialize winning engine list
+##    po_map = range(n_pos())
+
+def rf():
+##    set_engines(4) #temporary
+    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,
+    ps()
+    abc('w '+ss)
+
+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
+    c = cex_frame()
+    if c > 0:
+        b = c-1
+    else:
+        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)
+        elif is_unsat():
+            print 'PIs=%d,POs=%d,FF=%d,ANDs=%d,max depth = infinity'%(i,o,l,a)
+        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 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)                         
+
+#more complex functions: ________________________________________________________
+#, abstract, pba, speculate, final_verify, dprove3
+
+def timer(s):
+    btime = time.clock()
+    abc(s)
+    print 'time = %f'%(time.clock() - btime)
+
+def med_simp():
+    x = time.time()
+    abc("&get;&scl;&dc2;&lcorr;&dc2;&scorr;&fraig;&dc2;&put;dr")
+    #abc("dc2rs")
+    ps()
+    print 'time = %f'%(time.time() - x)
+
+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()
+    abc('&get;&scl;&lcorr;&put')
+    n =n_ands()
+    p_40 = False
+    if (40000 < n and n < 100000):
+        p_40 = True
+        abc("&get;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr")
+        n = n_ands()
+        if n<60000:
+            abc("&get;&scorr -F 2;&put;dc2rs")
+        else: # n between 60K and 100K
+            abc("dc2rs")
+    n = n_ands()
+    if (30000 < n  and n <= 40000):
+        if not p_40:
+            abc("&get;&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr")
+            abc("&get;&scorr -F 2;&put;dc2rs")
+        else:
+            abc("dc2rs")            
+    n = n_ands()
+    if n <= 30000:
+        abc('scl -m;drw;dr;lcorr;drw;dr')
+        nn = max(1,n)
+        m = int(min( 60000/nn, 16))
+        if m >= 1:
+            j = 1
+            while j <= m:
+                set_size()
+                if j<8:
+                    abc('dc2')
+                else:
+                    abc('dc2rs')
+                abc('scorr -C 5000 -F %d'%j)
+                if check_size():
+                    break
+                j = 2*j
+                continue
+    return get_status()
+            
+def simulate2(t):
+    """Does rarity simulation. Simulation is restricted by the amount
+    of memory it might use. At first wide but shallow simulation is done, followed by
+    successively more narrow but deeper simulation. 
+    seed is globally initiallized to 113 when a new design is read in"""
+    global x_factor, f_name, tme, seed
+    btime = time.clock()
+    diff = 0
+    while True:
+        f = 5
+        w = 255
+        for k in range(9): #this controls how deep we go
+            f = min(f *2, 3500)
+            w = max(((w+1)/2)-1,1)
+            abc('sim3 -m -F %d -W %d -R %d'%(f,w,seed))
+            seed = seed+23
+            if is_sat():
+                return 'SAT'
+            if ((time.clock()-btime) > t):
+                return 'UNDECIDED'
+
+
+def simulate(t):
+    abc('&get')
+    result = eq_simulate(t)
+    return result
+
+def eq_simulate(t):
+    """Simulation is restricted by the amount
+    of memory it might use. At first wide but shallow simulation is done, followed by
+    successively more narrow but deeper simulation. The aig to be simulated must be in the & space
+    If there are equivalences, it will refine them. Otherwise it is a normal similation
+    seed is globally initiallized to 113 when a new design is read in"""
+    global x_factor, f_name, tme, seed
+    btime = time.clock()
+    diff = 0
+    while True:
+        f = 5
+        w = 255
+        for k in range(9):
+            f = min(f *2, 3500)
+            r = f/20
+            w = max(((w+1)/2)-1,1)
+##            abc('&sim3 -R %d -W %d -N %d'%(r,w,seed))
+            abc('&sim -F %d -W %d -R %d'%(f,w,seed))
+            seed = seed+23
+            if is_sat():
+                return 'SAT'
+            if ((time.clock()-btime) > t):
+                return 'UNDECIDED'
+
+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: ',
+        ps()
+    return   
+
+def refine_with_cex():
+    """Refines the greg (which contains the original problem with the set of FF's that have been abstracted).
+    This uses the current cex to modify the greg file to reflect which regs are in the
+    new current abstraction"""
+    global f_name
+    #print 'CEX in frame %d for output %d'%(cex_frame(),cex_po())
+    #abc('&r %s_greg.aig; &abs_refine -t; &w %s_greg.aig'%(f_name,f_name))
+    abc('&r %s_greg.aig;&w %s_greg_before.aig'%(f_name,f_name))
+##    run_command('&abs_refine -s -M 25; &w %s_greg.aig'%f_name)
+    run_command('&abs_refine -s; &w %s_greg.aig'%f_name)
+    #print ' %d FF'%n_latches()
+    return
+
+def 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, last_verify_time, x, win_list, last_winner, last_cex, t_init, j_last, sweep_time
+    global cex_list, last_cx
+    sweep_time = 2
+    if NBF == -1:
+        F = 2000
+    else:
+        F = 2*NBF
+    print '\nIterating abstraction refinement'
+    J = slps+intrps+pdrs+bmcs+sims
+    print sublist(methods,J)
+    last_verify_time = t = x_factor*max(50,max(1,2.5*G_T))
+    initial_verify_time = last_verify_time = t
+    reg_verify = True
+    print 'Verify time set to %d'%last_verify_time
+    while True: #cex based refinement
+        generate_abs(1) #generate new gabs file from refined greg file
+        set_globals()
+        latches_after = n_latches()
+        if rel_cost_t([pis_before_abs,latches_before_abs, ands_before_abs])> -.1:
+            break
+        if latches_after >= .90*latches_before:
+            break
+        t = last_verify_time
+        yy = time.time()
+        abc('w %s_beforerpm.aig'%f_name)
+        rep_change = reparam() #new - must do reconcile after to make cex compatible
+        abc('w %s_afterrpm.aig'%f_name)
+        if reg_verify:
+            status = verify(J,t)
+        else:
+            status = pord_1_2(t)
+###############
+        if status == Sat_true:
+            print 'Found true cex'
+            reconcile(rep_change)
+            return Sat_true
+        if status == Unsat:
+            return status
+        if status == Sat:
+            reconcile(rep_change) # makes the cex compatible with original before reparam and puts original in work space
+            abc('write_status %s_before.status'%f_name)
+            refine_with_cex()
+            if is_sat(): # if cex can't refine, status is set to Sat_true
+                print 'Found true cex in output %d'%cex_po()
+                return Sat_true
+            else:
+                continue
+        else:
+            break
+    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, last_verify_time, x, win_list, j_last, sims
+    global latches_before_abs, ands_before_abs, pis_before_abs
+    j_last = 0
+    set_globals()
+    #win_list = []
+    latches_before_abs = n_latches()
+    ands_before_abs = n_ands()
+    pis_before_abs = n_real_inputs()
+    abc('w %s_before_abs.aig'%f_name)
+    print 'Start: ',
+    ps()
+    funcs = [eval('(pyabc_split.defer(initial_abstract)())')]
+    # fork off BMC3 and PDRm along with initial abstraction
+    t = 10000 #want to run as long as initial abstract takes.
+##    J = sims+pdrs+bmcs+intrps
+    J = pdrs+bmcs+bestintrps
+    if n_latches() < 80:
+        J = J + [4]
+    funcs = create_funcs(J,t) + funcs
+    mtds = sublist(methods,J) + ['initial_abstract'] #important that initial_abstract goes last
+    m,NBF = fork_last(funcs,mtds)
+    if is_sat():
+        print 'Found true counterexample in frame %d'%cex_frame()
+        return Sat_true
+    if is_unsat():
+        return Unsat
+    set_max_bmc(NBF)
+    NBF = bmc_depth()
+    print 'Abstraction good to %d frames'%max_bmc
+    #note when things are done in parallel, the &aig is not restored!!!
+    abc('&r %s_greg.aig; &w initial_greg.aig; &abs_derive; &put; w initial_gabs.aig; w %s_gabs.aig'%(f_name,f_name))
+    set_max_bmc(NBF)
+    print 'Initial abstraction: ',
+    ps()
+    abc('w %s_init_abs.aig'%f_name)
+    latches_after = n_latches()
+##    if latches_after >= .90*latches_before_abs:
+    if ((rel_cost_t([pis_before_abs, latches_before_abs, ands_before_abs])> -.1) or (latches_after >= .90*latches_before_abs)):
+        abc('r %s_before_abs.aig'%f_name)
+        print "Little reduction!"
+        return Undecided_no_reduction
+    sims_old = sims
+    sims=sims[:1] #make it so that rarity sim is not used since it can't find a cex
+    result = abstraction_refinement(latches_before_abs, NBF)
+    sims = sims_old
+    if result <= Unsat:
+        return result
+##    if n_latches() >= .90*latches_before_abs:
+    if ((rel_cost_t([pis_before_abs, latches_before_abs, ands_before_abs])> -.1) or (latches_after >= .90*latches_before_abs)):
+##    if rel_cost_t([pis_before_abs,latches_before_abs, ands_before_abs])> -.1:
+        abc('r %s_before_abs.aig'%f_name) #restore original file before abstract.
+        print "Little reduction!"
+        result = Undecided_no_reduction    
+    return result
+
+def initial_abstract_old():
+    global G_C, G_T, latches_before_abs, x_factor, last_verify_time, x, win_list
+    set_globals()
+    time = max(1,.1*G_T)
+    abc('&get;,bmc -vt=%f'%time)
+    set_max_bmc(bmc_depth())
+    c = 2*G_C
+    f = max(2*max_bmc,20)
+    b = min(max(10,max_bmc),200)
+    t = x_factor*max(1,2*G_T)
+    s = min(max(3,c/30000),10) # stability between 3 and 10 
+    cmd = '&get;,abs -bob=%d -stable=%d -timeout=%d -vt=%d -depth=%d'%(b,s,t,t,f)
+##    print cmd
+    print 'Running initial_abstract with bob=%d,stable=%d,time=%d,depth=%d'%(b,s,t,f)
+    abc(cmd)
+    abc('&w %s_greg.aig'%f_name)
+##    ps()
+
+def initial_abstract():
+    global G_C, G_T, latches_before_abs, x_factor, last_verify_time, x, win_list, max_bmc
+    set_globals()
+    time = max(1,.1*G_T)
+    abc('&get;,bmc -vt=%f'%time)
+    set_max_bmc(bmc_depth())
+    c = 2*G_C
+    f = max(2*max_bmc,20)
+    b = min(max(10,max_bmc),200)
+    t = x_factor*max(1,2*G_T)
+    s = min(max(3,c/30000),10) # stability between 3 and 10 
+    cmd = '&get;,abs -bob=%d -stable=%d -timeout=%d -vt=%d -depth=%d'%(b,s,t,t,f)
+##    print cmd
+    print 'Running initial_abstract with bob=%d,stable=%d,time=%d,depth=%d'%(b,s,t,f)
+    abc(cmd)
+    bmc_depth()
+##    pba_loop(max_bmc+1)
+    abc('&w %s_greg.aig'%f_name)
+    return max_bmc
+
+def abs_m():
+    set_globals()
+    y = time.time()
+    nl = n_abs_latches() #initial set of latches
+    c = 2*G_C
+    t = x_factor*max(1,2*G_T) #total time
+    bmd = bmc_depth()
+    if bmd < 0:
+        abc('bmc3 -T 2') #get initial depth estimate
+        bmd = bmc_depth()
+    f = bmd
+    abc('&get')
+    y = time.time()
+    cmd = '&abs_cba -v -C %d -T %0.2f -F %d'%(c,.8*t,bmd) #initial absraction
+##    print '\n%s'%cmd
+    abc(cmd)
+    b_old = b = n_bmc_frames()
+    f = min(2*bmd,max(bmd,1.6*b))
+    print 'cba: latches = %d, depth = %d'%(n_abs_latches(),b)
+##    print n_bmc_frames()
+    while True:
+        if (time.time() - y) > .9*t:
+            break
+        nal = n_abs_latches()
+        cmd = '&abs_cba -v -C %d -T %0.2f -F %d'%(c,.8*t,f) #f is 2*bmd and is the maximum number of frames allowed
+##        print '\n%s'%cmd
+        abc(cmd)
+##        print n_bmc_frames()
+        b_old = b
+        b = n_bmc_frames() 
+        nal_old = nal 
+        nal = n_abs_latches() #nal - nal_old is the number of latches added by cba
+        #b - b_old is the additional time frames added by cba
+        f = min(2*bmd,max(bmd,1.6*b))   #may be this should just be bmd
+        f = max(f,1.5*bmd)
+        print 'cba: latches = %d, depth = %d'%(nal,b)
+        if ((nal == nal_old) and (b >= 1.5*b_old) and b >= 1.5*bmd):
+            """
+            Went at least bmd depth and saw too many frames without a cex
+            (ideally should know how many frames without a cex)
+            """
+            print 'Too many frames without cex'
+            break
+        if b > b_old: #if increased depth
+            continue
+        if nal > .9*nl: # try to minimize latches
+##            cmd = '&abs_pba -v -S %d -F %d -T %0.2f'%(b,b+2,.2*t)
+            cmd = '&abs_pba -v -F %d -T %0.2f'%(b+2,.2*t)
+##            print '\n%s'%cmd
+            abc(cmd)
+            b = n_bmc_frames()
+            nal_old = nal
+            nal = n_abs_latches()
+            print 'pba: latches = %d, depth = %d'%(nal,b)
+##            print n_bmc_frames()
+            if nal_old < nal: #if latches increased there was a cex
+                continue
+            if nal > .9*nl: # if still too big 
+                return
+        continue 
+##    b = n_bmc_frames()
+    cmd = '&abs_pba -v -F %d -T %0.2f'%(b+2,.2*t)
+##    print '\n%s'%cmd
+    abc(cmd)
+    b = n_bmc_frames()
+    print 'pba: latches = %d, depth = %d'%(n_abs_latches(),b)
+##    print n_bmc_frames()
+    print 'Total time = %0.2f'%(time.time()-y)
+
+def n_abs_latches():
+    abc('&w pba_temp.aig') #save the &space
+    abc('&abs_derive;&put')
+    abc('&r pba_temp.aig')
+    return n_latches()
+        
+def pba_loop(F):
+    n = n_abs_latches()
+    while True:
+        run_command('&abs_pba -v -C 100000 -F %d'%F)
+        abc('&w pba_temp.aig')
+        abc('&abs_derive;&put')
+        abc('&r pba_temp.aig')
+        N = n_latches()
+##        if n == N or n == N+1:
+##            break
+##        elif N > n:
+        if N > n:
+            print 'cex found'
+        break
+##        else:
+##            break
+    
+##def sec_m(options):
+##    """
+##    This assumes that a miter has been loaded into the workspace. The miter has been
+##    constructed using &miter. Then we demiter it using command 'demiter'
+##    This produces parts 0 and 1, renamed  A_name, and B_name.
+##    We then do speculate immediately. Options are passed to &srm2 using the
+##    options given by sec_options
+##    """
+##    global f_name,sec_sw, A_name, B_name, sec_options
+##    A_name = f_name+'_part0'
+##    B_name = f_name+'_part1'
+##    run_command('demiter')
+##    #simplify parts A and B here?
+##    abc('r %s_part1.aig;scl;dc2;&get;&lcorr;&scorr;&put;dc2;dc2;w %s_part1.aig'%(f_name,f_name))
+##    ps()
+##    abc('r %s_part0.aig;scl;dc2;&get;&lcorr;&scorr;&put;dc2;dc2;w %s_part0.aig'%(f_name,f_name))
+##    ps()
+##    #simplify done
+##    f_name = A_name
+##    return sec(B_name,options)
+
+def ss(options):
+    """Alias for super_sec"""
+    global max_bmc, init_initial_f_name, initial_f_name,win_list, last_verify_time, sec_options
+    sec_options = options
+    print 'Executing speculate'
+    result = speculate()
+    return result
+
+
+def quick_sec(t):
+##    fb_name = f_name[:-3]+'New'
+##    abc('&get;&miter -s %s.aig;&put'%fb_name)
+##    abc('w %s.%s_miter.aig'%(f_name,fb_name))
+    quick_simp()
+    verify(slps+ pdrs+bmcs+intrps,t)
+    if is_unsat():
+        return 'UNSAT'
+    if is_sat():
+        return 'SAT'
+    else:
+        return'UNDECIDED'
+
+def pp_sec():
+    print 'First file: ',
+    read_file_quiet()
+    ps()
+    abc('&w original_secOld.aig')
+    print 'Second file: ',
+    read_file_quiet()
+    ps()
+    abc('&w original_secNew.aig')
+
+
+def sup_sec():
+    global TERM
+    """
+    form miter of original_sec(Old,New), and then run in parallel quick_sec(28), speculate(29), and
+    run_parallel(21) with JP set to 
+    """
+    global f_name,sec_sw, A_name, B_name, sec_options
+    #preprocess files to get rid of dangling FF
+    abc('&r original_secOld.aig;&scl -ce;&w Old.aig')
+    abc('&r original_secNew.aig;&scl -ce;&w New.aig')
+    #done preprocessing
+    read_file_quiet('Old')
+    abc('&get;&miter -s New.aig;&put')
+    set_globals()
+    yy = time.time()
+    A_name = f_name # Just makes it so that we can refer to A_name later in &srm2
+    B_name = 'New'
+    f_name = 'miter'
+    abc('w %s.aig'%f_name)
+    sec_options = 'l'
+    sec_sw = True
+    JP = [18,27] # sleep and simplify. JP  sets the things run in parallel in method 21.
+                    #TERM sets the stopping condition
+    TERM = 'USL' #Sat, Unsat or Last
+    print sublist(methods,[27,21,28,29]+JV)
+    t = 100 #this is the amount of time to run
+            #18 is controlled by t, 28(speculate) is not, 29(quick_sec) does quick_simp and then controlled by t
+    run_parallel([21,28,29],t,'US') #21 is run_parallel with JP and TERM.
+                                    #run simplify for t sec, speculate,
+                                    #and quick_sec (quick_simp and then verify(JV) for t)
+    if is_unsat():
+        return 'UNSAT'
+    if is_sat():
+        return 'SAT'
+    else:
+        return 'UNDECIDED' # should do sp or something
+        
+
+def sec(B_part,options):
+    """
+    This assumes that the original aig (renamed A_name below) is already read into the working space.
+    Then we form a miter using &miter between two circuits, A_name, and B_name.
+    We then do speculate immediately. Optionally we could simplify A and B
+    and then form the miter and start from there. The only difference in speculate
+    is that &srm2 is used, which only looks at equivalences where one comes from A and
+    one from B. Options are -a and -b which says use only flops in A or in B or both. The
+    switch sec_sw controls what speculate does when it generates the SRM.
+    """
+    global f_name,sec_sw, A_name, B_name, sec_options
+    yy = time.time()
+    A_name = f_name # Just makes it so that we can refer to A_name later in &srm2
+    B_name = B_part
+    run_command('&get; &miter -s %s.aig; &put'%B_name)
+##    abc('orpos')
+    f_name = A_name+'.'+B_name+'_miter' # reflect that we are working on a miter.
+    abc('w %s.aig'%f_name)
+    print 'Miter = ',
+    ps()
+##    result = pre_simp()
+##    write_file('smp')
+##    if result <= Unsat:
+##        return RESULT[result]
+    sec_options = options
+    if sec_options == 'ab':
+        sec_options = 'l' #it will be changed to 'ab' after &equiv
+    sec_sw = True 
+    result = speculate() #should do super_sec here.
+    sec_options = ''
+    sec_sw = False
+    if result <= Unsat:
+        result = RESULT[result]
+    else:
+        result = sp()
+    print 'Total time = %d'%(time.time() - yy)
+    return result
+
+def filter(opts):
+    global A_name,B_name
+    """ This is for filter which effectively only recognizes options -f -g"""
+    if (opts == '' or opts == 'l'): #if 'l' this is used only for initial &equiv2 to get initial equiv creation
+        return
+    if opts == 'ab':
+        run_command('&filter -f %s.aig %s.aig'%(A_name,B_name))
+        return
+    if not opts == 'f':
+        opts = 'g'
+    run_command('&filter -%s'%opts)
+
+def check_if_spec_first():
+    global sec_sw, A_name, B_name, sec_options, po_map
+    set_globals()
+    t = max(1,.5*G_T)
+    r = max(1,int(t))
+    abc('w check_save.aig')
+    abc('&w check_and.aig')
+    abc("&get; &equiv3 -v -F 20 -T %f -R %d"%(t,5*r))
+    filter('g')
+    abc("&srm; r gsrm.aig")
+    print 'Estimated # POs = %d for initial speculation'%n_pos()
+    result = n_pos() > max(50,.25*n_latches())
+    abc('r check_save.aig')
+    abc('&r check_and.aig')
+    return result
+
+def initial_speculate():
+    global sec_sw, A_name, B_name, sec_options, po_map
+    set_globals()
+    t = max(1,.5*G_T)
+    r = max(1,int(t))
+##    print 'Running &equiv3'
+##    abc('&w before3.aig')
+    if sec_options == 'l':
+        cmd = "&get; &equiv3 -lv -F 20 -T %f -R %d"%(3*t,15*r)
+    else:
+        cmd = "&get; &equiv3 -v -F 20 -T %f -R %d"%(3*t,15*r)
+##    print cmd
+    abc(cmd)
+##    print 'AND space after &equiv3: ',
+##    run_command('&ps')
+    if (sec_options == 'l'):
+        if sec_sw:
+            sec_options = 'ab'
+        else:
+            sec_options = 'f'
+            print sec_options
+    filter(sec_options)
+    abc('&w initial_gore.aig')
+##    print 'Running &srm'
+    if sec_sw:
+        cmd = "&srm2 -%s %s.aig %s.aig; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%(sec_options,A_name,B_name,f_name,f_name)
+        abc(cmd)
+        po_map = range(n_pos())
+        return
+    else:
+        cmd = "&srm; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%(f_name,f_name)
+        abc(cmd)
+        if (n_pos() > 100):
+            sec_options = 'g'
+            print 'sec_option changed to "g"'
+            filter(sec_options)
+            abc(cmd)
+        po_map = range(n_pos())
+
+def test_against_original():
+    '''tests whether we have a cex hitting an original PO'''
+    abc('&w %s_save.aig'%f_name) #we oreserve whatever was in the & space
+    abc('&r %s_gore.aig'%f_name)
+    abc('testcex')
+    PO = cex_po()
+    abc('&r %s_save.aig'%f_name)
+    if PO > -1:
+##        print 'cex fails an original PO'
+        return True
+    else:
+        return False
+
+def set_cex_po(n=0):
+    """
+    if cex falsifies a non-real PO return that PO first,
+    else see if cex_po is one of the original, then take it next
+    else return -1 which means that the cex is not valid and hence an error.
+    parameter n = 1 means test the &-space
+    """
+    global n_pos_before, n_pos_proved #these refer to real POs
+    if n == 0:
+        abc('testcex -a -O %d'%(n_pos_before-n_pos_proved))
+    else:
+        abc('testcex -O %d'%(n_pos_before-n_pos_proved))
+    PO = cex_po()
+    if PO >= (n_pos_before - n_pos_proved): #cex_po is not an original
+##        print 'cex PO = %d'%PO
+        return PO # after original so take it.
+    if n == 0:
+        abc('testcex -a')
+    else:
+        abc('testcex')
+    PO = cex_po()
+    cx = cex_get()
+    if PO > -1:
+        if test_against_original(): #this double checks that it is really an original PO
+            cex_put(cx)
+            return PO
+        else:
+            return -1 #error
+##    if PO < 0 or PO >= (n_pos_before - n_pos_proved): # not a valid cex because already tested outside original.
+##        PO = -1 #error
+    return PO
+##    print 'cex PO = %d'%PO
+
+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, last_verify_time, trim_allowed, n_pos_before
+    global t_init, j_last, sec_sw, A_name, B_name, sec_options, po_map, sweep_time, sims, cex_list, n_pos_proved,ifpord1
+    global last_cx
+    last_cx = 0
+    ifpord1 = 1
+    if sec_sw:
+        print 'A_name = %s, B_name = %s, f_name = %s, sec_options = %s'%(A_name, B_name, f_name, sec_options)
+    elif n_ands()> 6000 and sec_options == '':
+        sec_options = 'g'
+        print 'sec_options set to "g"'
+        
+    def refine_with_cex():
+        """Refines the gore file to reflect equivalences that go away because of cex"""
+        global f_name
+##        print 'Refining',
+##        abc('&r %s_gore.aig;&w %s_gore_before.aig'%(f_name,f_name))
+        abc('write_status %s_before.status'%f_name)
+        abc('&r %s_gore.aig; &resim -m'%f_name)
+        filter(sec_options)
+        run_command('&w %s_gore.aig'%f_name)
+        return
+    
+##    def refine_with_cexs():
+##        """Refines the gore file to reflect equivalences that go away because of cexs in cex_list"""
+##        global f_name, cex_list
+##        print 'Multiple refining'
+##        abc('&r %s_gore.aig'%f_name)
+####        run_command('&ps')
+##        for j in range(len(cex_list)):
+##            cx = cex_list[j]
+##            if cx == None:
+##                continue
+##            cex_put(cx)
+##            run_command('&resim -m') #put the jth cex into the cex space and use it to refine the equivs
+##        filter(sec_options)
+##        abc('&w %s_gore.aig'%f_name)
+####        run_command('&ps')
+##        cex_list = [] #done with this list.
+##        return
+
+    def set_cex(lst):
+        """ assumes only one in lst """
+        for j in range(len(lst)):
+            cx = lst[j]
+            if cx == None:
+                continue
+            else:
+                cex_put(cx)
+                break
+
+##    def test_all_cexs(lst):
+##        """tests all cex"s to see if any violate original POs
+##        if it does, return the original PO number
+##        if not return -1
+##        """
+##        global n_pos_before, cex_list
+##        run_command('&r %s_gore.aig'%f_name)
+##        for j in range(len(cex_list)):
+##            cx = lst[j]
+##            if cx == None:
+##                continue
+##            cex_put(cx)
+##            PO = set_cex_po()   #if cex falsifies non-real PO it will set this first
+##            if PO == -1:        # there is a problem with cex since it does not falsify any PO
+##                continue        #we continue because there may be another valid cex in list
+##            return PO           #we will only process one cex for now.
+##        return -1               #a real PO is not falsified by any of the cexs
+
+    def generate_srm():
+        """generates a speculated reduced model (srm) from the gore file"""
+        global f_name, po_map, sec_sw, A_name, B_name, sec_options, n_pos_proved
+##        print 'Generating'
+        pos = n_pos()
+        ab = n_ands()
+        if sec_sw:
+            run_command('&r %s_gore.aig; &srm2 -%s %s.aig %s.aig; r gsrm.aig; w %s_gsrm.aig'%(f_name,sec_options,A_name,B_name,f_name))
+        else:
+            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
+##        ps()
+        po_map = range(n_pos())
+##        cmd = '&get;&lcorr;&scorr;&trim -i;&put;w %s_gsrm.aig'%f_name
+##        cmd = 'lcorr;&get;&trim -i;&put;w %s_gsrm.aig'%f_name
+##        print 'Executing %s'%cmd
+##        abc(cmd)
+        ps()
+        n_pos_proved = 0
+        return 'OK'
+    
+    n_pos_before = n_pos()
+    n_pos_proved = 0
+    n_latches_before = n_latches()    
+    set_globals()
+    t = max(1,.5*G_T)#irrelevant
+    r = max(1,int(t))
+    j_last = 0
+    J = sims+pdrs+bmcs+intrps
+    funcs = [eval('(pyabc_split.defer(initial_speculate)())')]
+    funcs = create_funcs(J,10000)+funcs #want other functins to run until initial speculate stops
+    mtds = sublist(methods,J) + ['initial_speculate'] #important that initial_speculate goes last
+    fork_last(funcs,mtds)
+##    ps()
+    if is_unsat():
+        return Unsat
+    if is_sat():
+        return Sat_true
+    if n_pos_before == n_pos():
+        print 'No new outputs. Quitting speculate'
+        return Undecided_no_reduction # return result is unknown
+##    cmd = 'lcorr;&get;&trim -i;&put;w %s_gsrm.aig'%f_name
+    #print 'Executing %s'%cmd
+    abc('w initial_gsrm.aig')
+##    ps()
+##    abc(cmd)
+    print 'Initial speculation: ',
+    ps()
+    if n_latches() == 0:
+        return check_sat()
+    if sec_options == 'l' and sec_sw:
+        sec_options = 'ab' #finished with initial speculate with the 'l' option
+        print "sec_options set to 'ab'"
+    elif sec_options == 'l':
+        sec_options = 'f'
+        print "sec_options set to 'f'"
+    po_map = range(n_pos()) #we need this because the initial_speculate is done in parallel and po_map is not passed back.
+    npi = n_pis()
+    set_globals()
+    if is_sat():
+        return Sat_true
+    simp_sw = init = True
+    print '\nIterating speculation refinement'
+    sims_old = sims
+    sims = sims[:1] #make it so rarity simulation is not used since it can't find a cex.
+    J = slps+sims+pdrs+intrps+bmcs
+    print sublist(methods,J)
+    t = max(50,max(1,2*G_T))
+    last_verify_time = t
+    print 'Verify time set to %d'%last_verify_time
+    reg_verify = True
+    ref_time = time.time()
+    sweep_time = 2
+    ifpord1=1
+    while True: # refinement loop
+        set_globals()
+        yy = time.time()
+        if not init:
+            abc('r %s_gsrm.aig'%f_name) #this is done only to set the size of the previous gsrm.
+            abc('w %s_gsrm_before.aig'%f_name)
+            set_size()
+            result = generate_srm()
+            yy = time.time()
+            # if the size of the gsrm did not change after generating a new gsrm
+            # and if the cex is valid for the gsrm, then the only way this can happen is if
+            # the cex_po is an original one.
+            if check_size(): #same size before and after
+                if check_cex(): #valid cex failed to refine possibly
+                    if 0 <= cex_po() and cex_po() < (n_pos_before - n_pos_proved): #original PO
+                        print 'Found cex in original output = %d'%cex_po()
+                        print 'Refinement time = %s'%convert(time.time() - ref_time)
+                        return Sat_true
+                    elif check_same_gsrm(f_name): #if two gsrms are same, then failed to refine
+                        print 'CEX failed to refine'
+                        return Error
+                else:
+                    print 'not a valid cex'
+                    return Error
+            if n_latches() == 0:
+                print 'Refinement time = %s'%convert(time.time() - ref_time)
+                return check_sat()
+        init = False # make it so that next time it is not the first time through
+        if not t == last_verify_time: # heuristic that if increased last verify time,
+                                      # then try pord_all 
+            t = last_verify_time
+            if reg_verify:
+                t_init = (time.time() - yy)/2 #start poor man's concurrency at last cex fime found
+                t_init = min(10,t_init)
+                reg_verify = False #will cause pord_all to be used next
+                print 'pord_all turned on'
+                t = last_verify_time
+                print 'Verify time set to %d'%t
+        abc('w %s_beforerpm.aig'%f_name)
+        rep_change = reparam() #must be paired with reconcile below if cex
+        abc('w %s_afterrpm.aig'%f_name)
+        if reg_verify:
+            result = verify(J,t)
+        else:
+            result = pord_1_2(t)
+        if result == Unsat:
+            print 'UNSAT'
+            print 'Refinement time = %s'%convert(time.time() - ref_time)
+            return Unsat
+        if result < Unsat:
+            if not reg_verify:
+                set_cex(cex_list)
+##        if reg_verify: 
+            reconcile(rep_change) #end of pairing with reparam()
+            assert (npi == n_cex_pis()),'ERROR: #pi = %d, #cex_pi = %d'%(npi,n_cex_pis())
+            abc('&r %s_gore.aig;&w %s_gore_before.aig'%(f_name,f_name)) #we are making sure that none of the original POs fail
+            PO = set_cex_po() #testing the &space
+            if (-1 < PO and PO < (n_pos_before-n_pos_proved)):
+                print 'Found cex in original output = %d'%cex_po()
+                print 'Refinement time = %s'%convert(time.time() - ref_time)
+                return Sat_true
+            if PO == -1:
+                return Error
+            refine_with_cex()    #change the number of equivalences
+            continue
+##            else: # we used pord_all()
+##                cex_list = reconcile_all(cex_list, rep_change)  #end of pairing with reparam()
+##                PO = test_all_cexs(cex_list) #we have to make sure that none of the cex's fail the original POs.
+##                if 0 <= PO and PO < (n_pos_before - n_pos_proved):
+##                    print 'PO = %d, n_pos_before = %d, n_pos_proved = %d'%(PO,n_pos_before, n_pos_proved)
+##                    print 'Found one of cexs in original output = %d'%cex_po()
+##                    print 'Refinement time = %0.2f'%(time.time() - ref_time)
+##                    return Sat_true
+##                if PO == -1:
+##                    return Error
+##                refine_with_cexs()
+##                continue
+        elif (is_unsat() or n_pos() == 0):
+            print 'UNSAT'
+            print 'Refinement time = %s'%convert(time.time() - ref_time)
+            return Unsat
+        else: #if undecided, record last verification time
+            print 'Refinement returned undecided in %d sec.'%t
+            last_verify_time = t
+            #########################added
+            if reg_verify: #try one last time with parallel POs cex detection (find_cex_par) if not already tried
+                abc('r %s_beforerpm.aig'%f_name) # to continue refinement, need to restore original
+                t_init = min(last_verify_time,(time.time() - yy)/2) #start poor man's concurrency at last cex fime found
+                t_init = min(10,t_init)
+                reg_verify = False
+                t = last_verify_time # = 2*last_verify_time
+                abc('w %s_beforerpm.aig'%f_name)
+                rep_change = reparam() #must be paired with reconcile()below
+                abc('w %s_afterrpm.aig'%f_name)
+                result = pord_1_2(t) #main call to verification
+                if result == Unsat:
+                    print 'UNSAT'
+                    print 'Refinement time = %s'%convert(time.time() - ref_time)
+                    return Unsat
+                if is_sat():
+                    assert result == get_status(),'result: %d, status: %d'%(result,get_status())
+                    set_cex(cex_list)
+                    reconcile(rep_change)
+                    PO = set_cex_po() #testing the &space
+                    if (-1 < PO and PO < (n_pos_before-n_pos_proved)):
+                        print 'Found cex in original output = %d'%cex_po()
+                        print 'Refinement time = %s'%convert(time.time() - ref_time)
+                        return Sat_true
+                    if PO == -1:
+                        return Error
+                    refine_with_cex()    #change the number of equivalences
+                    continue
+##                    cex_list = reconcile_all(cex_list, rep_change)  #end of pairing with reparam()
+##                    PO = test_all_cexs(cex_list) #we have to make sure that none of the cex's fail the original POs.
+##                    if 0 <= PO and PO < (n_pos_before - n_pos_proved):
+##                        print 'found SAT in true output = %d'%cex_po()
+##                        print 'Refinement time = %s'%convert(time.time() - ref_time)
+##                        return Sat_true
+##                    if PO == -1:
+##                        return Error
+##                    refine_with_cexs()#change the number of equivalences
+##                    continue
+                elif is_unsat():
+                    print 'UNSAT'
+                    print 'Refinement time = %s'%convert(time.time() - ref_time)
+                    return Unsat
+                else: #if undecided, record last verification time
+                    last_verify_time = t
+                    print 'UNDECIDED'
+                    break
+            ################### added
+            else:
+                break
+    sims = sims_old
+    print 'UNDECIDED'
+    print 'Refinement time = %s'%convert(time.time() - ref_time)
+    write_file('spec')
+    if n_pos_before == n_pos():
+        return Undecided_no_reduction 
+    else:
+        return Undecided_reduction
+
+def simple_bip(t=1000):
+    y = time.time()
+    J = [0,1,2,30,5] #5 is pre_simp
+    funcs = create_funcs(J,t)
+    mtds =sublist(methods,J)
+    fork_last(funcs,mtds)
+    result = get_status()
+    if result > Unsat:
+        write_file('smp')
+        result = verify(slps+[0,1,2,30],t)
+    print 'Time for simple_bip = %0.2f'%(time.time()-y)
+    return RESULT[result] 
+
+def simple_prove(t=1000):
+    y = time.time()
+    J = [7,9,23,30,5]
+    funcs = create_funcs(J,t)
+    mtds =sublist(methods,J)
+    fork_last(funcs,mtds)
+    result = get_status()
+    if result > Unsat:
+        write_file('smp')
+        result = verify(slps+[7,9,23,30],t)
+    print 'Time for simple_prove = %0.2f'%(time.time()-y)
+    return RESULT[result] 
+
+def check_same_gsrm(f):
+##    return False #disable the temporarily until can figure out why this is there
+    """checks gsrm miters before and after refinement and if equal there is an error"""
+    global f_name
+    abc('r %s_gsrm.aig'%f)
+##    ps()
+    run_command('miter -c %s_gsrm_before.aig'%f)
+##    ps()
+    abc('&get; ,bmc -timeout=5')
+    result = True #if the same
+    if is_sat(): #if different
+        result = False
+    abc('r %s_gsrm.aig'%f)
+##    ps()
+    return result
+
+def check_cex():
+    """ check if the last cex still asserts one of the outputs.
+    If it does then we have an error"""
+    global f_name
+    abc('read_status %s_before.status'%f_name)
+    abc('&r %s_gsrm_before.aig'%f_name)
+##    abc('&r %s_gsrm.aig'%f_name)
+    run_command('testcex')
+    print 'cex po = %d'%cex_po()
+    return cex_po() >=0
+##    if cex_po() == -1: # means gsrm changes after refinement - no output is asserted.
+##        return False
+##    else:
+##        return True
+
+def set_size():
+    """Stores  the problem size of the current design.
+    Size is defined as (PIs, POs, ANDS, FF)""" 
+    global npi, npo, nands, nff, nmd
+    npi = n_pis()
+    npo = n_pos()
+    nands = n_ands()
+    nff = n_latches()
+    nmd = max_bmc
+    #print npi,npo,nands,nff
+
+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
+    #print n_pis(),n_pos(),n_ands(),n_latches()
+    result = ((npi == n_pis()) and (npo == n_pos()) and (nands == n_ands()) and (nff == n_latches()) )
+    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. Also more time is allocated if n =1"""
+    global last_verify_time
+    trim()
+    if n == 1:
+        simplify()
+        if n_latches == 0:
+            return check_sat()
+        trim()
+        if is_sat():
+            return Sat_true
+    #print 'After trimming: ',
+    #ps()
+    set_globals()
+    last_verify_time = t = max(1,.4*G_T)
+    if n == 1:
+        last_verify_time = t = max(1,2*G_T)
+    print 'Verify time set to %d '%last_verify_time
+    J = [18] + intrps+bmcs+pdrs+sims
+    status = verify(J,t)
+    return status
+
+##def process_status():
+##    if n_latches() == 0:
+##        status = check_sat()
+##    else:
+##        status = get_status()
+##    return status
+
+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 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. -1,0,1 => 3,0,2
+    """
+    if n_latches() == 0:
+        return check_sat()
+    status = prob_status() #interrogates ABC for the current status of the problem.
+    # 0 = SAT i.e. Sat_reg = 0 so does not have to be changed.
+    if status == 1:
+        status = Unsat
+    if status == -1: #undecided
+        status = Undecided
+    return status
+
+def reparam():
+    """eliminates PIs which if used in abstraction or speculation must be restored by
+    reconcile and the cex made compatible with file beforerpm"""
+##    return
+    rep_change = False
+    n = n_pis()
+##    abc('w t1.aig')
+    abc('&get;,reparam -aig=%s_rpm.aig; r %s_rpm.aig'%(f_name,f_name))
+##    abc('w t2.aig')
+##    abc('testcex')
+    if n_pis() == 0:
+        print 'Number of PIs reduced to 0. Added a dummy PI'
+        abc('addpi')
+    nn = n_pis()
+    if nn < n:
+        print 'Reparam: PIs %d => %d'%(n,nn)
+        rep_change = True
+    return rep_change
+
+def reconcile(rep_change):
+    """used to make current cex compatible with file before reparam() was done.
+    However, the cex may have come
+    from extracting a single output and verifying this.
+    Then the cex_po is 0 but the PO it fails could be anything.
+    So testcex rectifies this."""
+    global n_pos_before, n_pos_proved
+##    print 'rep_change = %s'%rep_change
+    if rep_change == False:
+        return
+    abc('&r %s_beforerpm.aig; &w tt_before.aig'%f_name)
+    abc('write_status %s_after.status;write_status tt_after.status'%f_name)
+    abc('&r %s_afterrpm.aig;&w tt_after.aig'%f_name)
+    POa = set_cex_po(1)   #this should set cex_po() to correct PO. A 1 here means it uses &space to check
+    abc('reconcile %s_beforerpm.aig %s_afterrpm.aig'%(f_name,f_name))
+    # reconcile modifies cex and restores work AIG to beforerpm
+    abc('write_status %s_before.status;write_status tt_before.status'%f_name)
+    POb = set_cex_po()
+##    assert POa == POb, 'cex PO afterrpm = %d, cex PO beforerpm = %d'%(POa,POb)
+    if POa != POb:
+        abc('&r %s_beforerpm.aig; &w tt_before.aig'%f_name)
+        abc('&r %s_afterrpm.aig; &w tt_after.aig'%f_name)
+        print 'cex PO afterrpm = %d, cex PO beforerpm = %d'%(POa,POb)
+##        assert POa == POb, 'cex PO afterrpm = %d, cex PO beforerpm = %d'%(POa,POb)
+
+def reconcile_all(lst, rep_change):
+    """reconciles the list of cex's"""
+    global f_name, n_pos_before, n_pos_proved
+    if rep_change == False:
+        return lst
+    list = []
+    for j in range(len(lst)):
+        cx = lst[j]
+        if cx == None:
+            continue
+        cex_put(cx)
+        reconcile(rep_change)
+        list = list + [cex_get()]
+    return list
+    
+
+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:
+            trim()
+            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 verify(J,t):
+    """This method is used for finding a cex during refinement, but can also
+    be used for proving the property. t is the maximum time to be used by
+    each engine J is the list of methods to run in parallel. See FUNCS for list"""
+    global x_factor, final_verify_time, last_verify_time, methods
+    set_globals()
+    t = int(max(1,t))
+    N = bmc_depth()
+    L = n_latches()
+    I = n_real_inputs()
+##    mtds = sublist(methods,J)
+    #heuristic that if bmc went deep, then reachability might also
+    if ( ((I+L<350)&(N>100))  or  (I+L<260) or (L<80) ):
+        J = J+reachs
+        J = remove_intrps(J)
+        if L < 80:
+            J=J+[4]
+    mtds = sublist(methods,J)
+    print mtds
+    #print J,t
+    F = create_funcs(J,t)
+    (m,result) = fork(F,mtds) #FORK here
+    assert result == get_status(),'result: %d, status: %d'%(result,get_status())
+    return result
+
+    
+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 not n_latches() == 0:
+        print 'circuit is not combinational'
+        return Undecided
+##    print 'Circuit is combinational - checking with dsat'
+    abc('&get') #save the current circuit
+    abc('orpos;dsat -C %d'%G_C)
+    if is_sat():
+        return Sat_true
+    elif is_unsat():
+        return Unsat
+    else:
+        abc('&put') #restore
+        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."""
+    global last_verify_time
+    #print 'Proving final_verify_recur(%d)'%K
+    last_verify_time = 2*last_verify_time
+    print 'Verify time increased to %d'%last_verify_time
+    for j in range(K):
+        i = K-(j+1)
+        abc('r %s_backup_%d.aig'%(initial_f_name,i))
+        if ((i == 0) or (i ==2)): #don't try final verify on original last one
+            status = prob_status()
+            break
+        print '\nVerifying backup number %d:'%i,
+        #abc('r %s_backup_%d.aig'%(initial_f_name,i))
+        ps()
+        #J = [18,0,1,2,3,7,14]
+        J = slps+sims+intrps+bmcs+pdrs
+        t = last_verify_time
+        status = verify(J,t)
+        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:
+##            pre_simp()
+            status = speculate()
+            if ((status <= Unsat) or (status == Error)):
+                return status
+        #J = [18,0,1,2,3,7,14]
+        J = slps+sims+intrps+bmcs+pdrs
+        t = 2*last_verify_time
+        print 'Verify time increased to %d'%last_verify_time
+        status = verify(J,t)
+    if status == Unsat:
+        return status
+    else:
+        return Undecided_reduction
+        
+def smp():
+    abc('smp')
+    write_file('smp')
+
+def dprove():
+    abc('dprove -cbjupr')
+
+def trim():
+    global trim_allowed
+    if not trim_allowed:
+        return
+##    abc('trm;addpi')
+    reparam()
+##    print 'exiting trim'
+
+def prs():
+    y = time.clock()
+    pre_simp()
+    print 'Time = %s'%convert(time.clock() - y)
+    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"""
+    global trim_allowed
+    set_globals()
+    abc('&get; &scl; &put')
+    if (n_ands() > 200000 or n_latches() > 50000 or n_pis() > 40000):
+        print 'Problem too large, simplification skipped'
+        return 'Undecided'
+    if ((n_ands() > 0) or (n_latches()>0)):
+        trim()
+##        ps()
+    if n_latches() == 0:
+        return check_sat()
+    best_fwrd_min([10,11])
+    ps()
+    status = try_scorr_constr()
+    if ((n_ands() > 0) or (n_latches()>0)):
+        trim()
+    if n_latches() == 0:
+        return check_sat()
+    status = process_status(status)
+    if status <= Unsat:
+        return status
+    simplify()
+    print 'Simplify: ',
+    ps()
+    if n_latches() == 0:
+        return check_sat()
+    if trim_allowed:
+        t = min(15,.3*G_T)
+##        try_tempor(t)
+        try_temps(15)
+        if n_latches() == 0:
+            return check_sat()
+        try_phase()
+        if n_latches() == 0:
+            return check_sat()
+        if ((n_ands() > 0) or (n_latches()>0)):
+            trim()
+    status = process_status(status)
+    if status <= Unsat:
+        return status
+    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 factors(n):
+    l = [1,]
+    nn = n
+    while n > 1:
+        for i in (2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53):
+            if not i <nn:
+                break
+            if n%i == 0:
+                l = l + [i,]
+                n = n/i
+        if not n == 1:
+            l = l + [n,]
+        break
+    return sorted(l)
+
+def select(x,y):
+    z = []
+    for i in range(len(x)):
+        if x[i]:
+            z = z + [y[i],]
+    return z
+    
+def ok_phases(n):
+    """ only try those where the resulting n_ands does not exceed 60000"""
+    f = factors(n)
+    sp = subproducts(f)
+    s = map(lambda m:m*n_ands()< 90000,sp)
+    z = select(s,sp)
+    return z
+
+def subproducts(ll):
+    ss = (product(ll),)
+    #print ll
+    n = len(ll)
+    if n == 1:
+        return ss
+    for i in range(n):
+        kk = drop(i,ll)
+        #print kk
+        ss = ss+(product(kk),)
+        #print ss
+        ss = ss+subproducts(kk)
+        #print ss
+    result =tuple(set(ss))
+    #result.sort()
+    return tuple(sorted(result))
+
+def product(ll):
+    n = len(ll)
+    p = 1
+    if n == 1:
+        return ll[0]
+    for i in range(n):
+        p = p*ll[i]
+    return p
+
+def drop(i,ll):
+    return ll[:i]+ll[i+1:]
+
+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"""
+    global init_simp
+    trim()
+    n = n_phases()
+##    if ((n == 1) or (n_ands() > 45000) or init_simp == 0):
+    if ((n == 1) or (n_ands() > 45000)):
+        return
+##    init_simp = 0
+    print 'Trying phase abstraction - Max phase = %d'%n,
+    #ps()
+##    trim()
+    #ps()
+    abc('w %s_phase_temp.aig'%f_name)
+    na = n_ands()
+    nl = n_latches()
+    ni = n_pis()
+    no = n_pos()
+    z = ok_phases(n)
+    print z,
+    if len(z) == 1:
+        return
+    #p = choose_phase()
+    p = z[1]
+    abc('phase -F %d'%p)
+##    ps()
+    #print z
+    if no == n_pos(): #nothing happened because p is not mod period
+        print 'Phase %d is incompatible'%p
+        abc('r %s_phase_temp.aig'%f_name)
+        if len(z)< 3:
+            return
+        else:
+            p = z[2]
+            #print 'Trying phase = %d:  '%p,
+            abc('phase -F %d'%p)
+            if no == n_pos(): #nothing happened because p is not mod period
+                print 'Phase %d is incompatible'%p
+                abc('r %s_phase_temp.aig'%f_name)
+                return
+    #print 'Trying phase = %d:  '%p,
+    print 'Simplifying with %d phases: => '%p,
+    simplify()
+    trim()
+    ps()
+    cost = rel_cost([ni,nl,na])
+    print 'New relative cost = %f'%(cost)
+    if cost <  -.01:
+        abc('w %s_phase_temp.aig'%f_name)
+        if ((n_latches() == 0) or (n_ands() == 0)):
+            return
+        if n_phases() == 1: #this bombs out if no latches
+            return
+        else:
+            try_phase()
+            return
+    elif len(z)>2: #Try the next eligible phase.
+        abc('r %s_phase_temp.aig'%f_name)
+        if p == z[2]: #already tried this
+            return
+        p = z[2]
+        print 'Trying phase = %d: => '%p,
+        abc('phase -F %d'%p)
+        if no == n_pos(): #nothing happened because p is not mod period
+            print 'Phase = %d is not compatible'%p
+            return
+        ps()
+        print 'Simplify with %d phases: '%p,
+        simplify()
+        trim()
+        ps()
+        cost = rel_cost([ni,nl,na])
+        print 'New relative cost = %f'%(cost)
+        if cost < -.01:
+            print 'Phase abstraction with %d phases obtained:'%p,
+            print_circuit_stats()
+            abc('w %s_phase_temp.aig'%f_name)
+            if ((n_latches() == 0) or (n_ands() == 0)):
+                return
+            if n_phases() == 1: # this bombs out if no latches
+                return
+            else:
+                try_phase()
+                return
+    abc('r %s_phase_temp.aig'%f_name)
+    #ps()
+    return
+
+def try_temp(t=15):
+    btime = time.clock()
+    trim()
+    print'Trying temporal decomposition - for max %s sec. '%convert(t),
+    abc('w %s_best.aig'%f_name)
+    ni = n_pis()
+    nl = n_latches()
+    na = n_ands()
+    best = [ni,nl,na]
+    F = create_funcs([18],t) #create a timer function
+    F = F + [eval('(pyabc_split.defer(abc)("tempor -s; trm; scr; trm; tempor; trm; scr; trm"))')]
+    for i,res in pyabc_split.abc_split_all(F):
+        break
+    cost = rel_cost(best)
+    print 'Cost = %0.2f'%cost
+    if cost < .01:
+        ps()
+        return
+    else:
+        abc('r %s_best.aig'%f_name)
+
+def try_temps(t=15):
+    best = (n_pis(),n_latches(),n_ands())
+    while True:
+        try_temp(t)
+        if ((best == (n_pis(),n_latches(),n_ands())) or n_ands() > .9 * best[2] ):
+            break
+        elif n_latches() == 0:
+            break
+        else:
+            best = (n_pis(),n_latches(),n_ands())
+        
+def try_tempor(t):
+    btime = time.clock()
+    trim()
+    print'Trying temporal decomposition - for max %s sec. '%convert(t),
+    abc('w %s_best.aig'%f_name)
+    ni = n_pis()
+    nl = n_latches()
+    na = n_ands()
+    best = [ni,nl,na]
+    F = create_funcs([18],t) #create a timer function
+    #Caution: trm done in the following removes POs and PIs
+##    F = F + [eval('(pyabc_split.defer(abc)("tempor -s -C %d; trm; lcr; scr; trm"))'%(2*na))]
+##    F = F + [eval('(pyabc_split.defer(abc)("tempor -C %d; trm; lcr; scr; trm"))'%(2*na))]
+    F = F + [eval('(pyabc_split.defer(abc)("tempor -s; trm; lcr; scr; trm"))')]
+    F = F + [eval('(pyabc_split.defer(abc)("tempor -C; trm; lcr; scr; trm"))')]
+    n_done = 0
+    new_best = 0
+##    debug_here()
+    for i,res in pyabc_split.abc_split_all(F):
+        if i == 0:
+            break
+        else:
+            cost = rel_cost(best)
+            print 'Cost = %0.2f'%cost
+            if cost < .01:
+                abc('w %s_best.aig'%f_name)
+                best = [n_pis(),n_latches(),n_ands()]
+                new_best = 1
+            n_done = n_done+1
+            if n_done == 2:
+                break
+            else:
+                continue
+    abc('r %s_best.aig'%f_name)
+    ps()
+    if new_best == 0: #nothing new
+        print 'No reduction or timeout occurred'
+        return
+    if n_latches() == 0:
+        return
+    abc('scr;smp')
+    trim()
+    cost = rel_cost_t([ni,nl,na]) #see how much it improved
+##    print 'rel_cost_t = %0.2f'%cost
+    if (cost < -.01):
+        print 'time = %f: '%(time.clock() - btime),
+        if cost < -1:
+            print 'Trying second tempor'
+            try_tempor(t)
+        print 'Reduction: time=%f'%(time.clock() - btime)
+        return
+    else:
+        print 'No reduction'
+        return    
+
+def rel_cost_t(J):
+    """ weighted relative costs versus previous stats."""
+    if n_latches() == 0:
+        return -10
+    nli = J[0]+J[1]
+    na = J[2]
+    if ((nli == 0) or (na == 0)):
+        return 100
+    nri = n_real_inputs()
+    #ri = (float(nri)-float(ni))/float(ni)
+    rli = (float(n_latches()+nri)-float(nli))/float(nli)
+    ra = (float(n_ands())-float(na))/float(na)
+##    cost = 10*rli + .1*ra
+    cost = 10*rli + .5*ra
+##    print 'cost = %0.2f'%c
+##    print 'cost = %0.2f'%cost
+    return cost    
+
+def rel_cost(J):
+    """ weighted relative costs versus previous stats."""
+    global f_name
+    if n_latches() == 0:
+        return -10
+    nri = n_real_inputs()
+    ni = J[0]
+    nl = J[1]
+    na = J[2]
+    if (ni == 0 or na == 0 or nl == 0):
+        return 100
+    ri = (float(nri)-float(ni))/float(ni)
+    rl = (float(n_latches())-float(nl))/float(nl)
+    ra = (float(n_ands())-float(na))/float(na)
+    cost = 1*ri + 10*rl + .1*ra
+##    print 'Relative cost = %0.2f'%cost
+    return cost
+
+def best_fwrd_min(J):
+    global f_name, methods
+    mtds = sublist(methods,J)
+    F = create_funcs(J,0)
+    #print 'Trying forward retiming: running %s in parallel'%(mtds)
+    (m,result) = fork_best(F,mtds) #FORK here
+    print '%s: '%mtds[m],
+    
+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 -m;lcorr;drw')
+    else:
+        abc('&get;&scl;&lcorr;&put;drw')
+
+def scorr_constr():
+    """Extracts implicit constraints and uses them in signal correspondence
+    Constraints that are found are folded back when done"""
+##################### Temporary
+#    return Undecided_no_reduction
+#####################
+    na = max(1,n_ands())
+    n_pos_before = n_pos()
+    if ((na > 40000) or n_pos()>1):
+        return Undecided_no_reduction
+    abc('w %s_savetemp.aig'%f_name)
+    if n_ands() < 3000:
+        cmd = 'unfold -a -F 2'
+    else:
+        cmd = 'unfold'
+    abc(cmd)
+    if n_pos() == n_pos_before:
+        print 'No constraints found'
+        return Undecided_no_reduction
+    if (n_ands() > na): #no constraints found
+        abc('r %s_savetemp.aig'%f_name)
+        return Undecided_no_reduction
+    #print_circuit_stats()
+    na = max(1,n_ands())
+##    f = 1
+    f = 18000/na
+    f = min(f,4)
+    f = max(1,f)
+    print 'Number of constraints = %d, frames = %d'%((n_pos() - n_pos_before),f)
+    abc('scorr -c -F %d'%f)
+    abc('fold')
+    trim()
+    ps()
+    return Undecided_no_reduction
+
+def try_scorr_c(f):
+    """ Trying multiple frames because current version has a bug."""
+    set_globals()
+    abc('unfold -F %d'%f)
+    abc('scorr -c -F %d'%f)
+    abc('fold')
+    t = max(1,.1*G_T)
+    abc('&get;,bmc3 -vt=%f'%t)
+    if is_sat(): 
+        return 0
+    else:
+        trim()
+        return 1
+    
+
+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_sec():
+##    """
+##    Like 'prove' proves all the outputs together. Speculation is done first
+##    If undecided, the do super_prove.
+##    """
+##    global x_factor,xfi,f_name, last_verify_time,K_backup, sec_options
+##    max_bmc = -1
+##    K_backup = K = 0
+##    result = prove_part_1(K) #initial simplification here
+##    if n_latches() == 0:
+##        return 1,result
+##    K = K_backup
+##    if ((result == 'SAT') or (result == 'UNSAT')):
+##        return 1,result
+##    assert K==1, 'K = %d'%K
+##    result = prove_part_3(K) #speculation done here
+##    if ((result == 'SAT') or (result == 'UNSAT')):
+##        return 1,result
+##    else:
+##        return 1,super_prove(0)
+##
+##    #################### End of ss
+##    K = K_backup
+##    #print 'after speculate'
+##    status = get_status()
+##    assert 0<K and K<4, 'K = %d'%K
+##    if K > 1: # for K = 1, we will leave final verification for later
+##        print 'Entering final_verify_recur(%d) from prove()'%K
+##        status = final_verify_recur(K) # will start verifying with final verify
+##                    #starting at backup number K-1 (either K = 2 or 3 here
+##                    #1 if spec found true sat on abs, 2 can happen if abstraction
+##                    #did not work but speculation worked,
+##                    #3 if still undecided after spec)
+##    else: #K=1 means that abstraction did not work and was proved wrong by speculation
+##        if a == 0:
+##            result = prove_spec_first()
+##            if ((result == 'SAT') or (result == 'UNSAT')):
+##                return 1,result
+##    write_file('final')
+##    return (not K == 1),RESULT[status]
+
+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 skip speculate. K is the number of the next backup
+        if a == 2 skip initial simplify and speculate"""
+    global x_factor,xfi,f_name, last_verify_time,K_backup, t_init, sec_options
+    spec_first = False
+    max_bmc = -1
+    K_backup = K = 0
+    if a == 2: #skip initial simplification
+        print 'Using quick simplification',
+        abc('lcorr;drw')
+        status = process_status(get_status())
+        if status <= Unsat:
+            result = RESULT[status]
+        else:
+            ps()
+            write_file('smp')
+            abc('w %s_backup_%d.aig'%(initial_f_name,K)) #writing backup 0
+            K_backup = K = K+1
+            result = 'UNDECIDED'
+    else:
+        result = prove_part_1(K) #initial simplification here
+        if ((result == 'SAT') or (result == 'UNSAT')):
+            return 1,result
+        if n_latches() == 0:
+            return 1,result
+        if a == 0:
+            spec_first = False
+##            spec_first = check_if_spec_first()
+            if spec_first:
+                sec_options = 'g'
+                print 'sec_options set to "g"'
+    if n_latches() == 0:
+        return 1,result
+    K = K_backup
+    if ((result == 'SAT') or (result == 'UNSAT')):
+        return 1,result
+    assert K==1, 'K = %d'%K
+    t_init = 2
+    if spec_first and a == 0:
+        result = prove_part_3(K)
+    else:
+        result = prove_part_2(K) #abstraction done here
+    K = K_backup
+    if ((result == 'SAT') or (result == 'UNSAT')):
+        return 1,result
+    assert 0<K and K<3, 'K = %d'%K 
+    if a == 0:
+        t_init = 2
+        if spec_first:
+            result = prove_part_2(K) #speculation 2one here
+        else:
+            result = prove_part_3(K)
+        if ((result == 'SAT') or (result == 'UNSAT')):
+            return 1,result
+    K = K_backup
+    #print 'after speculate'
+    status = get_status()
+    assert 0<K and K<4, 'K = %d'%K
+    if (((K > 2) and (n_pos()>1)) or ((K == 2) and  spec_first)): # for K = 1, we will leave final verification for later
+        print 'Entering final_verify_recur(%d) from prove()'%K
+        status = final_verify_recur(K) # will start verifying with final verify
+                    #starting at backup number K-1 (either K = 2 or 3 here
+                    #1 if spec found true sat on abs, 2 can happen if abstraction
+                    #did not work but speculation worked,
+                    #3 if still undecided after spec)
+    #K=1 or 2 and not spec_first means that abstraction did not work and was proved wrong by speculation
+    elif ((a == 0) and K == 1):
+            t_init = 2
+            result = prove_spec_first()
+            if ((result == 'SAT') or (result == 'UNSAT')):
+                return 1,result
+    write_file('final')
+    return (not K == 1),RESULT[status]
+
+def psf():
+    x = time.time()
+    result = prove_spec_first()
+    print 'Total clock time for %s = %f sec.'%(init_initial_f_name,(time.time() - x))
+    return result
+
+def prove_spec_first():
+    """Proves all the outputs together. If ever an abstraction
+        was done then if SAT is returned,
+        we make RESULT return "undecided".
+        """
+    global x_factor,xfi,f_name, last_verify_time,K_backup
+    max_bmc = -1
+    K_backup = K = 1
+##    result = prove_part_1(K) #initial simplification here
+##    if n_latches() == 0:
+##        return result
+##    K = K_backup
+##    if ((result == 'SAT') or (result == 'UNSAT')):
+##        return result
+##    assumes that initial simplification has been done already.
+    assert K==1, 'K = %d'%K
+    result = prove_part_3(K) #speculation done here
+    K = K_backup
+    if ((result == 'SAT') or (result == 'UNSAT')):
+        return result
+    assert 0<K and K<3, 'K = %d'%K
+    K = K_backup #K = 1 => speculation did not do anything
+    if K == 1: # so don't try abstraction because it did not work the first time
+        return 'UNDECIDED'
+    result = prove_part_2(K) #abstraction done here
+    if result == 'UNSAT':
+        return result
+    if result == 'SAT': # abstraction proved speculation wrong.
+        K = 2
+    assert 0<K and K<4, 'K = %d'%K
+    if K > 1: # for K = 1, we will leave final verification for later
+        print 'Entering final_verify_recur(%d) from prove()'%K
+        status = final_verify_recur(K) # will start verifying with final verify
+                    #starting at backup number K-1 (either K = 2 or 3 here
+                    #1 if spec found true sat on abs, 2 can happen if
+                    #speculation worked but abstraction proved it wrong,
+                    #3 if still undecided after spec and abstraction)
+    write_file('final')
+    return RESULT[status]
+
+
+def prove_part_1(K):
+    global x_factor,xfi,f_name, last_verify_time,K_backup
+    #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()
+        set_globals()
+        t = 1000
+        funcs = [eval('(pyabc_split.defer(pre_simp)())')]
+##        J = sims+pdrs+bmcs+intrps
+        J = pdrs+bmcs+bestintrps
+        funcs = create_funcs(J,t)+ funcs #important that pre_simp goes last
+        mtds =sublist(methods,J) + ['pre_simplify']
+        fork_last(funcs,mtds)
+##        funcs = [eval(FUNCS[3])] + [eval(FUNCS[0])] + [eval(FUNCS[1])] + [eval(FUNCS[2])] + [eval(FUNCS[9])] + [eval(FUNCS[7])] + funcs
+##        fork_last(funcs,['SIM', 'PDR','INTRP','BMC', 'BMC3', 'PDRm','pre_simp'])
+        status = get_status()
+    else:
+        status = check_sat()
+    if ((status <= Unsat) or (n_latches() == 0)):
+        return RESULT[status]
+    if n_ands() == 0:
+        abc('&get;,bmc -vt=2')
+        if is_sat():
+            return 'SAT'
+    trim()
+    write_file('smp')
+    abc('w %s_backup_%d.aig'%(initial_f_name,K)) #writing backup 0
+    K_backup = K = K+1
+    #K=1 
+    set_globals()
+    return 'UNDECIDED'
+
+def prove_part_2(K):
+    """does the abstraction part of prove"""
+    global x_factor,xfi,f_name, last_verify_time,K_backup, trim_allowed
+    print'\n***Running abstract'
+    nl_b = n_latches()
+    status = abstract() #ABSTRACTION done here
+##    write_file('abs')
+##    print 'Abstract finished'
+    if status == Undecided_no_reduction:
+        K_backup = K = K-1 #K = 0
+    if status == Unsat:
+        write_file('abs')
+        return RESULT[status]
+##    trim()
+    #just added in
+    if status < Unsat:
+        write_file('abs')
+        print 'CEX in frame %d'%cex_frame()
+        return RESULT[status]
+    if  K > 0:
+        t_old = trim_allowed
+        if pord_on:
+            trim_allowed = False
+        pre_simp()
+        trime_allowed = t_old
+    #end of added in
+    write_file('abs')
+    status = process_status(status)
+    if ((status <= Unsat)  or  status == Error):
+        if  status < Unsat:
+            print 'CEX in frame %d'%cex_frame()
+            return RESULT[status]
+        return RESULT[status]
+    abc('w %s_backup_%d.aig'%(initial_f_name,K)) # writing backup 1 (or 0) after abstraction
+    K_backup = K = K+1
+    #K = 1 or 2 here
+    return 'UNDECIDED'
+    
+def prove_part_3(K):
+    """does the speculation part of prove"""
+    global x_factor,xfi,f_name, last_verify_time,K_backup, init_initial_f_name
+    global max_bmc, sec_options
+    #K_backup = K = K +1 #K = 1 or 2 K =1 means that abstraction did not reduce
+    assert 0 < K and K < 3, 'K = %d'%K
+    if ((n_ands() > 10000) and sec_options == ''):
+        sec_options = 'g'
+        print 'sec_options set to "g"'
+    if n_ands() == 0:
+        print 'Speculation skipped because no AND nodes'
+    else:
+        print '\n***Running speculate'
+##        pre_simp()
+        status = speculate() #SPECULATION done here
+        if status == Unsat:
+            return RESULT[status]
+        old_f_name = f_name
+##        if not status < Unsat:
+##            pre_simp()
+##        write_file('spec1')
+##        #we do not do the continuation of speculation right now so the following is not needed.
+##        #abc('&r %s_gore.aig;&w %s_gore.aig'%(old_f_name,f_name)) #very subtle -needed for continuing spec refinement
+        status = process_status(status)
+        if status == Unsat:
+            return RESULT[status]
+        elif ((status < Unsat) or (status == Error)):
+            print 'CEX in frame %d'%cex_frame()
+            if K == 1: #if K = 1 then abstraction was not done.
+                print 'speculate found cex on original'
+                return RESULT[status] # speculate found cex on original
+            K_backup = K = K-1 #since spec found a true cex, then result of abstract was wrong
+            print 'cex means that abstraction was invalid'
+            print 'Initial simplified AIG restored => ',
+            abc('r %s_smp.aig'%init_initial_f_name)
+            max_bmc = -1
+            ps()
+            assert K == 1, 'K = %d'%K
+        else: 
+            trim()
+            print 'Problem still undecided'
+            abc('w %s_backup_%d.aig'%(initial_f_name,K)) # writing backup 2 or 1
+                                                        # 2 after speculation and abstraction
+                                                        # 1 if abstraction did not reduce
+            K_backup = K = K+1
+            assert 1<K and K<4, 'K = %d'%K
+##            write_file('spec2')
+    trim()
+    return 'UNDECIDED'
+
+def prove_all(dir,t):
+    """Prove all aig files in this directory using super_prove and record the results in results.txt"""
+##    t = 1000 #This is the timeoout value
+    xtime = time.time()
+##    dir = main.list_aig('')
+    results = []
+    f =open('results_%d.txt'%len(dir), 'w')
+    for name in dir:
+        read_file_quiet(name)
+        print '\n         **** %s:'%name,
+        ps()
+        F = create_funcs([18,6],t) #create timer function as i = 0 Here is the timer
+        for i,res in pyabc_split.abc_split_all(F):
+            break
+        tt = time.time()
+        if i == 0:
+            res = 'Timeout'
+        str = '%s: %s, time = %s'%(name,res,convert(tt-xtime))
+        if res == 'SAT':
+            str = str + ', cex_frame = %d'%cex_frame()
+        str = str +'\n'
+        f.write(str)
+        f.flush()
+        results = results + ['%s: %s, time = %s'%(name,res,convert(tt-xtime))]
+        xtime = tt
+##    print results
+    f.close()
+    return results
+
+    
+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
+    x = time.time()
+    #input_x_factor()
+    init_f_name = f_name
+    print 'Beginning prove_g_pos'
+    prove_all_ind()
+    print 'Number of outputs reduced to %d by fast induction with constraints'%n_pos()
+    print '\n****Running second level prove****************\n'
+    reparam()
+##    try_rpm()
+##    k,result = prove(1) # 1 here means do not try speculate.
+##    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 fast induction with constraints'%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
+    #Now prove each remaining output separately.
+    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()
+        f_name = f_name + '_%d'%jnext_old
+        result = prove_1()
+        if result == 'UNSAT':
+            if jnext_old > jnext+1:
+                print '********  PROVED OUTPUTS [%d-%d]  ******** '%(jnext+1,jnext_old)
+            else:
+                print '********  PROVED OUTPUT %d  ******** '%(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 '********  UNDECIDED on OUTPUTS %d thru %d  ******** '%(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)
+        trim()
+        write_file('group')
+        result = 'UNDECIDED'
+    else:
+        print 'Proved all outputs. The problem is proved UNSAT'
+        result = 'UNSAT'
+    print 'Total clock time for prove_g_pos = %f sec.'%(time.time() - x)
+    return result
+
+def prove_pos(i):
+    """
+    i=1 means to execute prove_all_ind first
+    Proved outputs are removed if all the outputs have not been proved.
+    If ever one of the proofs returns SAT, we continue and try to resolve other outputs."""
+    global f_name, max_bmc,x_factor,x
+    x = time.time()
+    #input_x_factor()
+    init_f_name = f_name
+    print 'Beginning prove_pos'
+    remove_0_pos()
+    if i:
+        prove_all_ind()
+    print 'Number of outputs reduced to %d by quick induction with constraints'%n_pos()
+    print '********** 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 = []
+    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()    
+        result = super_prove(2) #do not do initial simplification
+        if result == 'UNSAT':
+            print '********  PROVED OUTPUT %d  ******** '%(jnext_old)
+            pos_proved = pos_proved + range(jnext +1,jnext_old+1)
+            continue
+        if result == 'SAT':
+            print '********  DISPROVED OUTPUT %d  ******** '%(jnext_old)
+            pos_disproved = pos_disproved + range(jnext +1,jnext_old+1)
+            continue
+        else:
+            print '********  UNDECIDED on OUTPUT %d  ******** '%(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)
+        trim()
+        write_file('group')
+        result = 'UNRESOLVED'
+    else:
+        print 'Proved or disproved all outputs. The problem is proved RESOLVED'
+        result = 'RESOLVED'
+    print 'Total clock time for prove_pos = %f sec.'%(time.time() - x)
+    return result
+
+def remove_pos(lst):
+    """Takes a list of pairs where the first part of a pair is the PO number and
+    the second is the result 1 = disproved, 2 = proved, 3 = unresolved. Then removes
+    the proved and disproved outputs and returns the aig with the unresolved
+    outputs"""
+    proved = disproved = unresolved = []
+    for j in range(len(lst)):
+        jj = lst[j]
+        if jj[1] == 2:
+            proved = proved + [jj[0]]
+        if (jj[1] == 1 or (jj[1] == 0)):
+            disproved = disproved +[jj[0]]
+        if jj[1] > 2:
+            unresolved = unresolved +[jj[0]]
+    print '%d outputs proved'%len(proved)
+##    print disproved
+##    abc('w xxx__yyy.aig')
+    if not proved == []:
+        if ((max(proved)>n_pos()-1) or min(proved)< 0):
+            print proved
+        remove(proved)
+            
+
+#functions for proving multiple outputs in parallel
+#__________________________________________________
+
+def prove_only(j):
+    """ extract the jth output and try to prove it"""
+    global max_bmc, init_initial_f_name, initial_f_name, f_name,x
+    #abc('w %s__xsavetemp.aig'%f_name)
+    extract(j,j)
+    set_globals()
+    ps()
+    print '\nProving output %d'%(j)
+    f_name = f_name + '_%d'%j
+    result = prove_1()
+    #abc('r %s__xsavetemp.aig'%f_name)
+    if result == 'UNSAT':
+        print '********  PROVED OUTPUT %d  ******** '%(j)
+        return Unsat
+    if result == 'SAT':
+        print '********  DISPROVED OUTPUT %d  ******** '%(j)
+        return Sat
+    else:
+        print '********  UNDECIDED on OUTPUT %d  ******** '%(j)
+        return Undecided
+
+def verify_only(j,t):
+    """ extract the jth output and try to prove it"""
+    global max_bmc, init_initial_f_name, initial_f_name, f_name,x, reachs, last_cex, last_winner, methods
+##    ps()
+##    print 'Output = %d'%j
+    extract(j,j)
+##    ps()
+    set_globals()
+    if n_latches() == 0:
+        result = check_sat()
+    else:
+        f_name = f_name + '_%d'%j
+        # make it so that jabc is not used here
+        reachs_old = reachs
+        reachs = reachs[1:] #just remove jabc from this.
+        res = verify(slps+sims+pdrs+bmcs+intrps,t) #keep the number running at the same time as small as possible.
+##        res = verify(sims+pdrs+bmcs+intrps,t) #keep the number running at the same time as small as possible.
+        reachs = reachs_old
+        result = get_status()
+        assert res == result,'result: %d, status: %d'%(res,get_status())
+    if result > Unsat:
+##        print result
+##        print '******* %d is undecided ***********'%j
+        return result
+    elif result == Unsat:
+##        print '******** PROVED OUTPUT %d  ******** '%(j)
+        return result
+    elif ((result < Unsat) and (not result == None)):
+        print '******** %s DISPROVED OUTPUT %d  ******** '%(last_cex,j)
+##        print ('writing %d.status'%j), result, get_status()
+        abc('write_status %d.status'%j)
+        last_winner = last_cex
+        return result
+    else:
+        print '****** %d result is %d'%(j,result) 
+        return result
+
+def verify_range(j,k,t):
+    """ extract the jth thru kth output and try to prove their OR"""
+    global max_bmc, init_initial_f_name, initial_f_name, f_name,x, reachs, last_cex, last_winner, methods
+    extract(j,k)
+    abc('orpos')
+    set_globals()
+    if n_latches() == 0:
+        result = check_sat()
+    else:
+        f_name = f_name + '_%d'%j
+        # make it so that jabc is not used here
+        reachs_old = reachs
+        reachs = reachs[1:] #just remove jabc from this.
+        res = verify(sims+pdrs+bmcs+intrps,t) #keep the number running at the sme time as small as possible.
+        reachs = reachs_old
+        result = get_status()
+        assert res == result,'result: %d, status: %d'%(res,get_status())
+    if result > Unsat:
+##        print result
+##        print '******* %d is undecided ***********'%j
+        return result
+    elif result == Unsat:
+##        print '******** PROVED OUTPUT %d  ******** '%(j)
+        return result
+    elif ((result < Unsat) and (not result == None)):
+        print '******** %s DISPROVED OUTPUT %d  ******** '%(last_cex,j)
+##        print ('writing %d.status'%j), result, get_status()
+        abc('write_status %d.status'%j)
+        last_winner = last_cex
+        return result
+    else:
+        print '****** %d result is %d'%(j,result) 
+        return result
+
+def prove_n_par(n,j):
+    """prove n outputs in parallel starting at j"""
+    F = []
+    for i in range(n):
+        F = F + [eval('(pyabc_split.defer(prove_only)(%s))'%(j+i))]
+    #print S
+    #F = eval(S)
+    result = []
+    print 'Proving outputs %d thru %d in parallel'%(j,j+n-1)
+    for i,res in pyabc_split.abc_split_all(F):
+        result = result +[(j+i,res)]
+    #print result
+    return result
+
+def prove_pos_par(t,BREAK):
+    """Prove all outputs in parallel and break on BREAK"""
+    return run_parallel([],t,BREAK)
+
+def prove_pos_par0(n):
+    """ Group n POs grouped and prove in parallel until all outputs have been proved"""
+    f_name = initial_f_name
+    abc('w %s__xsavetemp.aig'%f_name)
+    result = []
+    j = 0
+    N = n_pos()
+    while j < N-n:
+        abc('r %s__xsavetemp.aig'%f_name)
+        result = result + prove_n_par(n,j)
+        j = j+n
+    if N > j:
+        result = result + prove_n_par(N-j,j)
+    abc('r %s__xsavetemp.aig'%initial_f_name)
+    ps()
+    print result
+    remove_pos(result)
+    write_file('group')
+    return
+
+def prop_decomp():
+    """decompose a single property into multiple ones (only for initial single output),
+    by finding single and double literal primes of the outputs."""
+    if n_pos()>1:
+        return
+    run_command('outdec -v -L 2')
+    if n_pos()>1:
+        ps()
+
+
+def distribute(N,div):
+    """
+    we are going to verify outputs in groups
+    """
+    n = N/div
+    rem = N - (div * (N/div))
+    result = []
+    for j in range(div):
+        if rem >0:
+            result = result +[n+1]
+            rem = rem -1
+        else:
+            result = result + [n]
+    return result    
+
+def find_cex_par(tt):
+    """prove n outputs at once and quit at first cex. Otherwise if no cex found return aig
+    with the unproved outputs"""
+    global trim_allowed,last_winner, last_cex, n_pos_before, t_init, j_last, sweep_time
+    b_time = time.time() #Wall clock time
+    n = n_pos()
+    remove_0_pos()
+    N = n_pos()
+    full_time = all_proc = False
+    print 'Number of POs: %d => %d'%(n,N)
+    if N == 0:
+        return Unsat
+##    inc = 5  #******* increment for grouping for sweep set here *************
+##    inc = min(12,max(inc, int(.1*N)))
+    inc = 1+N/100
+##    if N <1.5*inc: # if near the increment for grouping try to get it below.
+##        prove_all_ind()
+##        N = n_pos()
+    if inc == 1:
+        prove_all_ind()
+        N = n_pos()
+    T = int(tt) #this is the total time to be taken in final verification run before quitting speculation
+##    if inc == 10:
+##        t_init = 10
+##    t = max(t_init/2,T/20)
+##    if N <= inc:
+##        t = T
+##    print "inc = %d, Sweep time = %s, j_group = %d"%(inc,convert(t),j_last)
+    t = sweep_time/2 #start sweeping at last time where cex was found.
+##    it used to be t = 1 here but it did not make sense although seemed to work.
+##    inc = 2
+    while True: #poor man's concurrency
+        N = n_pos()
+        if N == 0:
+            return Unsat
+        #sweep_time controls so that when sweep starts after a cex, it starts at the last sweep time
+        t = max(2,2*t) #double sweep time
+        if t > .75*T:
+            t = T
+            full_time = True
+        if ((N <= inc) or (N < 13)):
+            t = sweep_time = T
+            full_time = True
+            inc = 1
+##            sweep_time = 2*sweep_time
+        if not t == T:
+            t= sweep_time = max(t,sweep_time)
+##            t = sweep_time
+##new heuristic
+        if (all_proc and sweep_time > 8): #stop poor man's concurrency and jump to full time.
+            t = sweep_time = T
+            full_time - True #this might be used to stop speculation when t = T and the last sweep
+##                           found no cex and we do not prove Unsat on an output
+        abc('w %s__ysavetemp.aig'%f_name)
+        ps()
+        if N < 50:
+            inc = 1
+        print "inc = %d, Sweep time = %s, j_last = %d"%(inc,convert(t),j_last)
+        F = []
+##        G = []
+        #make new lambda functions since after the last pass some of the functions may have been proved and eliminated.
+        for i in range(N):
+            F = F + [eval('(pyabc_split.defer(verify_only)(%d,%s))'%(i,convert(T)))] #make time large and let sleep timer control timeouts
+##            G = G + [range(i,i+1)]
+        ######
+        result = []
+        outcome = ''
+        N = len(F)
+        rng = range(1+(N-1)/inc)
+        rng = rng[j_last:]+rng[:j_last] #pick up in range where last found cex.
+##        print 'rng = ',
+##        print rng
+        k = -1
+        bb_time = time.time()
+        for j in rng:
+            k = k+1 #keeps track of how many groups we have processed.
+            j_last = j
+            J = j*inc
+            JJ = J+inc
+            JJ = min(N,JJ)
+            if J == JJ-1:
+                print 'Function = %d '%J,
+            else:
+                print 'Functions = [%d,%d]'%(J,JJ-1)
+            Fj = create_funcs([18],t+1) #create timer function as i = 0 Here is the timer
+            Fj = Fj + F[J:JJ]
+            count = 0
+            fj_time = time.time()
+            abc('r %s__ysavetemp.aig'%f_name) #important need to restore aig here so the F refers to right thing when doing verify_only.
+##                                             # because verify_only changes the aig.
+##            ps()
+            for i,res in pyabc_split.abc_split_all(Fj):
+                count = count+1
+                Ji = J+i-1 #gives output number
+                if ((res == 0) or (res == 1)):
+                    abc('read_status %d.status'%Ji)
+                    res = get_status()
+                    outcome = 'CEX: Frame = %d, PO = %d, Time = %s'%(cex_frame(),Ji,convert((time.time() - fj_time)))
+                    break
+                if i == 0: #sleep timer expired
+                    outcome = '*** Time expired in %s sec. Next group = %d to %d ***'%(convert(time.time() - fj_time),JJ,min(N,JJ+inc))
+                    break
+                elif res == None: #this should not happen
+                    print res
+                    print Ji,RESULT[res],
+                else: # output Ji was proved
+                    result = result + [[Ji,res]]
+                    if count >= inc:
+                        outcome = '--- all group processed without cex ---'
+                        all_proc = True
+                        break
+                    continue #this can only happen if inc > 1
+            # end of for i loop
+            if ((res < Unsat) and (not res == None)): 
+                break
+            else:
+                continue # continue j loop
+        #end of for j loop
+        if k < len(rng):      
+            t_init = t/2 #next time start with this time.
+        else:
+            j_last = j_last+1 #this was last j and we did not find cex, so start at next group
+        print outcome + ' => ' ,
+        if ((res < Unsat) and (not res == None)):
+            t_init = t/2
+            abc('read_status %d.status'%Ji) #make sure we got the right status file.
+            #actually if doing abstraction we could remove proved outputs now, but we do not. -**inefficiency**
+            return res
+        else: #This implies that no outputs were disproved. Thus can remove proved outputs.
+            abc('r %s__ysavetemp.aig'%f_name) #restore original aig
+            if not result == []:
+                res = []
+                for j in range(len(result)):
+                    k = result[j]
+                    if k[1] == 2:
+                        res = res + [k[0]]
+##                print res
+##                result = mapp(res,G)
+                result = res
+##                print result
+                remove(result) #remove the outputs that were proved UNSAT.
+                #This is OK for both abstract and speculate
+                print 'Number of POs reduced to %d'%n_pos()
+                if n_pos() == 0:
+                    return Unsat
+            if t>=T:
+                return Undecided
+            else:
+                continue
+    return Undecided
+
+def remap_pos():
+    """ maintains a map of current outputs to original outputs"""
+    global po_map
+    k = j = 0
+    new = []
+    assert n_pos() == len(po_map), 'length of po_map, %d, and current # POs, %d, don"t agree'%(len(po_map),n_pos())
+    for j in range(len(po_map)):
+        N = n_pos()
+        abc('removepo -N %d'%k) # this removes the output if it is 0 driven
+        if n_pos() == N:
+            new = new + [po_map[j]]
+            k = k+1
+    if len(new) < len(po_map):
+##        print 'New map = ',
+##        print new
+        po_map = new
+
+def prove_mapped():
+    """
+    assumes that srm is in workspace and takes the unsolved outputs and proves
+    them by using proved outputs as constraints.
+    """
+    global po_map
+##    print po_map
+    po_map.sort() #make sure mapped outputs are in order
+    for j in po_map: #put unsolved outputs first
+        run_command('swappos -N %d'%j)
+        print j
+    N = n_pos()
+    assert N > len(po_map), 'n_pos = %d, len(po_map) = %d'%(N, len(po_map))
+    run_command('constr -N %d'%(N-len(po_map))) #make the other outputs constraints
+    run_command('fold') #fold constraints into remaining outputs.
+    ps()
+    prove_all_mtds(100)
+    
+def mapp(R,G):
+    result = []
+    for j in range(len(R)):
+        result = result + G[R[j]]
+    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
+    x = time.clock()
+    #input_x_factor()
+    init_f_name = f_name
+    print 'Beginning prove_g_pos_split'
+    prove_all_ind()
+    print 'Number of outputs reduced to %d by fast induction with constraints'%n_pos()
+    reparam()
+##    try_rpm()
+    print '********** 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 '********  PROVED OUTPUTS [%d-%d]  ******** '%(jnext+1,jnext_old)
+            else:
+                print '********  PROVED OUTPUT %d  ******** '%(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 '********  UNDECIDED on OUTPUTS %d thru %d  ******** '%(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)
+            trim()
+            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)
+        trim()
+        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')   # eliminated because need to keep same number of inputs.
+
+def remove_intrps(J):
+    JJ = []
+    for i in J:
+        if i in allintrps:
+            continue
+        else:
+            JJ = JJ +[i]
+    return JJ
+        
+    
+
+def remove(lst):
+    """Removes outputs in list"""
+    global po_map
+    n_before = n_pos()
+    zero(lst)
+##    remap_pos()
+    remove_0_pos()
+    print 'list',
+    lst
+    print 'n_before = %d, n_list = %d, n_after = %d'%(n_before, len(lst), n_pos())
+    
+
+def zero(list):
+    """Zeros out POs in list"""
+    for j in list:
+        run_command('zeropo -N %d'%j)
+
+def remove_0_pos():
+    global po_map
+    """removes the 0 pos, but no pis because we might get cexs and need the correct number of pis
+    Should keep tract of if original POs are 0 and are removed.
+    Can this happen outside of prove_all_ind or
+    pord_all which can set proved outputs to 0???
+    """
+    run_command('&get; &trim -i; &put; addpi') #adds a pi only if there are none
+    po_map = range(n_pos())
+##    # gone back to original method of removing pos. Thus po_map is irrelevant
+##    remap_pos()
+##    abc('addpi')
+
+def psp():
+    quick_simp()
+    result = run_parallel([6,21],500,'US') #runs 'run_parallel' and sp() in parallel. run_parallel uses
+                #JP and TERM to terminate.
+    return result
+
+def sp():
+    """Alias for super_prove"""
+    print 'Executing super_prove'
+    result = super_prove(0)
+    return result
+
+
+##def super_sec(options):
+##    """Main proof technique now for seq eq checking. 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,win_list, last_verify_time, sec_options
+##    sec_options = options
+##    init_initial_f_name = initial_f_name
+##    if x_factor > 1:
+##        print 'x_factor = %f'%x_factor
+##        input_x_factor()
+##    max_bmc = -1
+##    x = time.time()
+##    k = 2
+##    K,result = prove_sec()
+##    if ((result == 'SAT') or (result == 'UNSAT')):
+##        print '%s: total clock time taken by super_prove = %f sec.'%(result,(time.time() - x))
+##        return
+##    elif ((result[:3] == 'UND') and (n_latches() == 0)):
+##        return result
+##    print '%s: total clock time taken by super_prove = %f sec.'%(result,(time.time() - x))
+##    if n_pos() > 1:
+##        print 'Entering prove_g_pos'
+##        result = prove_g_pos(0)
+##        print result
+##        if result == 'UNSAT':
+##            print 'Total clock time taken by super_prove = %f sec.'%(time.time() - x)
+##            return result
+##        if result == 'SAT':
+##            k = 1 #Don't try to prove UNSAT on an abstraction that had SAT
+##                    # should go back to backup 1 since probably spec was bad.
+##            if check_abs(): #if same as abstract version, check original simplified version
+##                k = 0
+##    y = time.time()
+##    if K == 0: #K = 0 means that speculate found cex in abstraction.
+##        k=0
+##    print 'Entering BMC_VER_result(%d)'%k
+##    result = BMC_VER_result(k)
+##    #print 'win_list = ',win_list
+##    print 'Total clock time taken by last gasp verification = %f sec.'%(time.time() - y)
+##    print 'Total clock time for %s = %f sec.'%(init_initial_f_name,(time.time() - x))
+##    return result
+
+def super_prove(n=0):
+    """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
+    n controls call to prove(n)
+    n = 2 means skip initial simplify and speculate,
+    n=1 skip initial simp.
+    """
+    global max_bmc, init_initial_f_name, initial_f_name,win_list, last_verify_time
+    init_initial_f_name = initial_f_name
+    if x_factor > 1:
+        print 'x_factor = %f'%x_factor
+        input_x_factor()
+    max_bmc = -1
+    x = time.time()
+    k = 2
+    if n == 2:
+        K,result = prove(2)
+    else:
+        K,result = prove(0)
+    if ((result == 'SAT') or (result == 'UNSAT')):
+        print '%s: total clock time taken by super_prove = %f sec.'%(result,(time.time() - x))
+        return result
+    elif ((result[:3] == 'UND') and (n_latches() == 0)):
+        return result
+    print '%s: total clock time taken by super_prove = %f sec.'%(result,(time.time() - x))
+    y = time.time()
+    if K == 0: #K = 0 means that speculate found cex in abstraction.
+        k=0
+    if n == 2:
+        print 'Entering BMC_VER()'
+        result = BMC_VER() #typically called from a super_prove run in parallel.
+        if result == 'SAT': #this is because we have done an abstraction and cex is invalid.
+            result = 'UNDECIDED'
+    else:
+        print 'Entering BMC_VER_result(%d)'%k
+        result = BMC_VER_result(k)
+    #print 'win_list = ',win_list
+    print result
+    print 'Total clock time taken by last gasp verification = %f sec.'%(time.time() - y)
+    print 'Total clock time for %s = %f sec.'%(init_initial_f_name,(time.time() - x))
+    return result
+
+def reachm(t):
+    x = time.clock()
+    #print 'trying reachm'
+    abc('&get;&reachm -vcs -T %d'%t)
+    print 'reachm done in time = %f'%(time.clock() - x)
+    return get_status()
+
+def reachp(t):
+    x = time.clock()
+    #print 'trying reachm2'
+    abc('&get;&reachp -rv -T %d'%t)
+    print 'reachm2 done in time = %f'%(time.clock() - x)
+    return get_status()
+
+def reachn(t):
+    x = time.clock()
+    #print 'trying reachm3'
+    abc('&get;&reachn -rv -T %d'%t)
+    print 'reachm3 done in time = %f'%(time.clock() - x)
+    return get_status()
+    
+def reachx(t):
+    x = time.time()
+    #print 'trying reachx'
+    abc('reachx -t %d'%t)
+    print 'reachx  done in time = %f'%(time.time() - x)
+    return get_status()
+
+def reachy(t):
+    x = time.clock()
+    #print 'trying reachy'
+    abc('&get;&reachy -v -T %d'%t)
+    print 'reachy done in time = %f'%(time.clock() - x)
+    return get_status()
+    
+
+def create_funcs(J,t):
+    """evaluates strings indexed by J in methods given by FUNCS
+    Returns a list of lambda functions for the strings in FUNCs
+    If J = [], then create provers for all POs"""
+    funcs = []
+    for j in range(len(J)):
+        k=J[j]
+        funcs = funcs + [eval(FUNCS[k])]
+    return funcs
+
+def check_abs():
+    global init_initial_f_name
+    abc('w %s_save.aig'%init_initial_f_name)
+    ni = n_pis()
+    nl = n_latches()
+    na = n_ands()
+    abc('r %s_smp_abs.aig'%init_initial_f_name)
+    if ((ni == n_pis()) and (nl == n_latches()) and (na == n_ands())):
+        return True
+    else:
+        abc('r %s_save.aig'%init_initial_f_name)
+        return False
+
+"""make a special version of BMC_VER_result that just works on the current network"""
+def BMC_VER():
+    global init_initial_f_name, methods, last_verify_time
+    #print init_initial_f_name
+    xt = time.time()
+    result = 5
+    t = max(2*last_verify_time,100)
+    print 'Verify time set to %d'%t
+    N = bmc_depth()
+    L = n_latches()
+    I = n_real_inputs()
+    X = pyabc_split.defer(abc)
+    J = slps + pdrs + [23] + bmcs
+    if ( ((I+L<350)&(N>100))  or  (I+L<260) or (L<80) ):
+        J = J+reachs # add all reach methods
+        if L < 80:
+            J = J + [4]
+    F = create_funcs(J,t)
+    mtds = sublist(methods,J)
+    print '%s'%mtds
+    (m,result) = fork_break(F,mtds,'US')
+    print '(m,result) = %d,%s'%(m,result)
+    result = RESULT[result]
+    print 'BMC_VER() result = %s'%result
+    return result
+
+        
+def BMC_VER_result(n):
+    global init_initial_f_name, methods, last_verify_time
+    #print init_initial_f_name
+    xt = time.time()
+    result = 5
+    if n == 0:
+        abc('r %s_smp.aig'%init_initial_f_name)
+        print '\n***Running proof on initial simplified circuit\n',
+        ps()
+    elif n == 1:
+        abc('r %s_smp_abs.aig'%init_initial_f_name)        
+        print '\n***Running proof on abstracted circuit',
+        ps()
+    else: # n was 2
+        print '\n***Running proof on final unproved circuit',
+        ps()
+    t = max(2*last_verify_time,1000)
+    print 'Verify time set to %d'%t
+    #status = verify(J,t)
+    N = bmc_depth()
+    L = n_latches()
+    I = n_real_inputs()
+    X = pyabc_split.defer(abc)
+    J = slps + pdrs + [23] +bmcs
+##    [0,1,7,14] # try pdr, interpolation, and pdrm
+##    if n == 0:
+##        J = J+ bmcs #add BMC #eveen if n =1 or 2 we want to find a cex
+    #heuristic that if bmc went deep, then reachability might also
+    if ( ((I+L<350)&(N>100))  or  (I+L<260) or (L<80) ):
+        #J = J+[4,13] #add reachx and reachn
+        J = J+reachs # add all reach methods
+        if L < 80:
+            J = J + [4]
+    #F = eval(S)
+    F = create_funcs(J,t)
+    mtds = sublist(methods,J)
+    print '%s'%mtds
+    (m,result) = fork(F,mtds)
+    result = get_status()
+    if result == Unsat:
+        return 'UNSAT'
+    if n == 0:
+        if result < Unsat:
+            return 'SAT'
+        if result > Unsat: #still undefined
+            return 'UNDECIDED'
+    elif n == 1: #just tried abstract version - try initial simplified version
+        if result < Unsat:
+            return BMC_VER_result(0)
+        else: #if undecided on good abstracted version, does not make sense to try initial one
+            return 'UNDECIDED'
+    else: # n was 2, just tried final unresolved version - now try abstract version
+        if result < Unsat: 
+            return BMC_VER_result(1) #try abstract version
+        else: #undecided on final unproved circuit. Probably can't do better.
+            return 'UNDECIDED'
+            
+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.
+    Prints out unproved outputs Finally removes 0 outputs
+    """
+    global n_pos_proved, n_pos_before
+    n_proved = 0
+    N = n_pos()
+##    remove_0_pos()
+##    print '0 valued output removal changed POs from %d to %d'%(N,n_pos())
+    if n_pos() == 1:
+        return
+    abc('w %s_osavetemp.aig'%f_name)
+    lst = range(n_pos())
+##    list.reverse()
+##    for j in list[1:]:
+    for j in lst:
+##        abc('zeropo -N 0')
+        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 -ux -C 10000 -F %d'%f)
+##        run_command('print_status')
+        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
+            if j < n_pos_before - n_pos_proved:
+                n_proved = n_proved + 1 # keeps track of real POs proved.
+        elif status < Unsat:
+            print '-%d'%j,
+        else:
+            print '*%d'%j,
+    remove_0_pos()
+    n_pos_proved = n_pos_proved + n_proved 
+    print '\nThe number of POs reduced from %d to %d'%(N,n_pos())
+    #return status
+
+def prove_all_mtds(t):
+    """
+    Tries to prove output k  with multiple methods in parallel,
+    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:
+        run_command('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')
+##        cmd = '&get;,pdr -vt=%d'%t #put in parallel.
+##        abc(cmd)
+        verify(pdrs+bmcs+intrps+sims,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,
+    assert not is_sat(), 'one of the POs is SAT' #we can do better than this
+    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, 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('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')
+        cmd = '&get;,pdr -vt=%d'%t #put in parallel.
+        abc(cmd)
+        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_each_ind():
+    """Tries to prove output k by induction,  """
+    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('cone -s -O %d'%j)
+        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_each_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('cone -O %d -s'%j)
+        abc('scl -m')
+        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 disprove_each_bmc(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('cone -O %d -s'%j)
+        abc('scl -m')
+        abc('bmc3 -T %d'%t)
+        status = get_status()
+        abc('r %s_osavetemp.aig'%f_name)
+        if status == Sat:
+            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 pord_1_2(t):
+    """ two phase pord. First one tries with 10% of the time. If not solved then try with full time"""
+    global n_pos_proved, ifpord1, pord_on
+    pord_on = True # make sure that we do not reparameterize after abstract in prove_2
+    n_pos_proved = 0
+    if ifpord1:
+        print 'Trying each output for %0.2f sec'%(.1*t)
+        result = pord_all(.1*t) #we want to make sure that there is no easy cex.
+        if (result <= Unsat):
+            return result
+    ifpord1 = 0
+    print 'Trying each output for %0.2f sec'%t
+    result = pord_all(t+2*G_T) #make sure there is enough time to abstract
+    pord_on = False #done with pord
+    return result
+
+def pord_all(t):
+    """Tries to prove or disprove each output j by PDRM BMC3 or SIM. in time t"""
+    global cex_list, n_pos_proved, last_cx, pord_on, ifpord1
+    print 'last_cx = %d'%last_cx
+    btime = time.time()
+    N = n_pos()
+##    remove_0_pos()
+    print '0 valued output removal changed POs from %d to %d'%(N,n_pos())
+##    bmc_ss(t)
+##    if is_sat():
+##        cex_list = cex_get_vector()
+##        return Sat
+    prove_all_ind() ############ change this to keep track of n_pos_proved
+    nn = n_pos()
+    abc('w %s_osavetemp.aig'%f_name)
+    if nn < 4: #Just cut to the chase immediately.
+        return Undecided
+    lst = range(n_pos())
+    proved = disproved = []
+##    abc('&get') #using this space to save original file
+##    with redirect.redirect( redirect.null_file, sys.stdout ):
+##        with redirect.redirect( redirect.null_file, sys.stderr ):
+    cx_list = []
+    n_proved = 0
+    lcx = last_cx + 1
+    lst = lst[lcx:]+lst[:lcx]
+    lst.reverse()
+    n_und = 0
+    for j in lst:
+        print ''
+        print j,
+        abc('&put; cone -O %d -s'%j)
+        abc('scl -m')
+##                ps()
+##        run_parallel(slps+sims+bmcs+pdrs+[6],t,'US')
+        result = run_sp2_par(t)
+        print 'run_sp2_par result is %s'%result
+        if result == 'UNDECIDED':
+            n_und = n_und + 1
+            status = Undecided
+            if ((n_und > 1) and not ifpord1):
+                break
+        elif result == 'SAT':
+            status = Sat
+            disproved = disproved + [j]
+            last_cx = j
+            cx = cex_get()
+            cx_list = cx_list + [cx]
+            assert len(cx_list) == len(disproved), cx_list
+            if len(cx_list) > 0:
+                break
+        else: #is unsat here
+            status = Unsat
+            proved = proved + [j]
+            if j < n_pos_before - n_pos_proved:
+                n_proved = n_proved +1
+    n_pos_proved = n_pos_proved + n_proved
+    print '\nProved %d outputs'%len(proved)
+    print 'Disproved %d outputs'%len(disproved)
+    print 'Time for pord_all was %0.2f'%(time.time() - btime)
+    NN = len(proved+disproved)
+    cex_list = cx_list
+    if len(disproved)>0:
+        assert status == Sat, 'status = %d'%status
+        return Sat
+    else:
+        abc('r %s_osavetemp.aig'%f_name)
+##        abc('&put') # returning original to work spece
+        remove(proved)
+        print '\nThe number of unproved POs reduced from %d to %d'%(N,n_pos())
+        if n_pos() > 0:
+            return Undecided
+        else:
+            return Unsat
+
+def bmc_ss(t):
+    """
+    finds a set cexs in t seconds starting at 2*N where N is depth of bmc -T 1
+    The cexs are put in the global cex_list
+    """
+    global cex_list
+    x = time.time()
+    tt = min(10,max(1,.05*t))
+    abc('bmc3 -T %0.2f'%tt)
+    N = n_bmc_frames()
+    if N <= max_bmc:
+        return Undecided
+##    print bmc_depth()
+##    abc('bmc3 -C 1000000 -T %f -S %d'%(t,int(1.5*max(3,max_bmc))))
+    run_command('bmc3 -vs -C 1000000 -T %f -S %d'%(t,2*N))
+    if is_sat():
+        cex_list = cex_get_vector() #does this get returned from a concurrent process?
+        n = count_non_None(cex_list)
+        print '%d cexs found in %0.2f sec at frame %d'%(n,(time.time()-x),cex_frame())
+    return get_status()
+
+def list_non_None(lst):
+    """ return [i for i,s in enumerate(cex_list) if not s == None]"""
+    L = []
+    for i in range(len(lst)):
+        if not lst[i] == None:
+            L = L + [i]
+    return L
+
+def count_non_None(lst):
+    #return len([i for i,s in enumerate(cex_list) if not s == None]
+    count = 0
+    for i in range(len(lst)):
+        if not lst[i] == None:
+            count = count + 1
+    return count
+
+def remove_disproved_pos(lst):
+    for i in range(len(lst)):
+        if not lst[i] == None:
+            abc('zeropo -N %d'%i)
+    remove_0_pos()
+        
+def bmc_s(t):
+    """ finds a cex in t seconds starting at 2*N where N is depth of bmc -T 1"""
+    x = time.time()
+    tt = min(5,max(1,.05*t))
+    abc('bmc3 -T %0.2f'%tt)
+    if is_sat():
+        print 'cex found in %0.2f sec at frame %d'%((time.time()-x),cex_frame())
+        return get_status()
+##    abc('bmc3 -T 1')
+    N = n_bmc_frames()
+##    print bmc_depth()
+##    abc('bmc3 -C 1000000 -T %f -S %d'%(t,int(1.5*max(3,max_bmc))))
+    cmd = 'bmc3 -J 2 -D 4000 -C 1000000 -T %f -S %d'%(t,2*N)
+##    print cmd
+    abc(cmd)
+    if is_sat():
+        print 'cex found in %0.2f sec at frame %d'%((time.time()-x),cex_frame())
+    return get_status()
+
+
+def pdr(t):
+    abc('&get; ,pdr -vt=%f'%t)
+    return RESULT[get_status()]
+
+def pdrm(t):
+    abc('pdr -v -C 0 -T %f'%t)
+    return RESULT[get_status()]
+
+def pdrmm(t):
+    abc('pdr -mv -C 0 -T %f'%t)
+    return RESULT[get_status()]
+
+def split(n):
+    abc('orpos;&get')
+    abc('&posplit -v -N %d;&put;dc2'%n)
+    trim()
+
+def keep_splitting():
+    for j in range(5):
+        split(5+j)
+        no = n_pos()
+        status = prove_g_pos_split()
+        if status <= Unsat:
+            return status
+        if no == n_pos():
+            return Undecided
+
+def drill(n):
+    run_command('&get; &reachm -vcs -H 5 -S %d -T 50 -C 40'%n)
+
+def prove_1():
+    """
+    A version of prove(). Called only during prove_pos or prove_g_pos or prove_only when we
+    have speculated and produced multiple outputs. Does speculation only in final_verify_recur.
+    Proves all the outputs together. If ever an abstraction was done then
+    if SAT is returned,we make RESULT return "undecided".
+    """
+    global x_factor,xfi,f_name,x, initial_f_name
+    x = time.time()
+    max_bmc = -1
+    K = 0
+    print 'Initial: ',
+    ps()
+    x_factor = xfi
+    print 'x_factor = %f'%x_factor
+    write_file('smp')
+    initial_f_name_save = initial_f_name #needed because we are making local backups here.
+    initial_f_name = '%s_temp'%initial_f_name
+    abc('w %s_backup_%d.aig'%(initial_f_name,K)) #backup 0
+    K = K +1 #K = 1 is next backup
+    set_globals()
+    print'\n***Running abstract'
+    nl_b = n_latches()
+    status = abstract()
+    trim()
+    write_file('abs')
+    status = process_status(status)
+    if ((status <= Unsat)  or  status == Error):
+        if  status < Unsat:
+            print 'CEX in frame %d'%cex_frame(),
+            print 'abstract found a cex in unabstacted circuit'
+            print 'Time for proof = %f sec.'%(time.time() - x)
+            initial_f_name = initial_f_name_save
+            return RESULT[status]
+        print 'Time for proof = %f sec.'%(time.time() - x)
+        initial_f_name = initial_f_name_save
+        return RESULT[status]
+    abc('w %s_backup_%d.aig'%(initial_f_name,K)) #backup 1
+    print 'Entering final_verify_recur(2) from prove_1()'
+    status = final_verify_recur(2) 
+    trim()
+    write_file('final')
+    print 'Time for proof = %f sec.'%(time.time() - x)
+    initial_f_name = initial_f_name_save
+    return RESULT[status]
+    
+def pre_reduce():
+    x = time.clock()
+    pre_simp()
+    write_file('smp')
+    abstract()
+    write_file('abs')
+    print 'Time = %f'%(time.clock() - x)
+
+def sublist(L,I):
+    # return [s for i,s in enumerate(L) if i in I]
+    z = []
+    for i in range(len(I)):
+        s = L[I[i]],
+        s = list(s)
+        z = z + s
+    return z
+
+#PARALLEL FUNCTIONS
+"""  funcs should look like
+funcs = [pyabc_split.defer(abc)('&get;,bmc -vt=50;&put'),pyabc_split.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 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 tf():
+    result = top_fork()
+    return result
+
+def top_fork(J,t):
+    global x_factor, final_verify_time, last_verify_time, methods
+    set_globals()
+    mtds = sublist(methods,J)
+    F = create_funcs(J,t)
+    print 'Running %s in parallel for max %d sec.'%(mtds,t)
+    (m,result) = fork_last(F,mtds) #FORK here
+    return get_status()
+
+def run_sp2_par(t):
+    """ Runs the single method super_prove(2), timed for t seconds."""
+    global cex_list,methods
+    J = slps+[6]
+    funcs = create_funcs(J,t) 
+    y = time.time()
+    for i,res in pyabc_split.abc_split_all(funcs):
+        #print 'i,res = %d,%s'%(i,res)
+        t = time.time()-y
+        if i == 0:
+            print 'sleep timer expired in %0.2f'%t
+            return 'UNDECIDED'
+        else:
+            if res == 'UNSAT':
+                print 'SUPER_PROVE2 proved UNSAT in %0.2f sec.'%t
+                return 'UNSAT'
+            elif res == 'UNDECIDED':
+                print 'SUPER_PROVE2 proved UNDECIDED in %0.2f sec.'%t
+                return 'UNDECIDED'
+            else:
+                print 'SUPER_PROVE2 found cex in %0.2f sec.'%t
+                return 'SAT'
+            
+
+def run_parallel(J,t,BREAK):
+    """ Runs the listed methods J, each for time = t, in parallel and
+    breaks according to BREAK = subset of '?USLB'"""
+    global cex_list,  methods
+    mtds = sublist(methods,J)
+    F = create_funcs(J,t) #if J = [] we are going to create functions that process each output separately.
+                            #if 18, then these are run in parallel with sleep
+    if ((J == []) ):
+        result = fork_break(F,mtds,BREAK)
+##        #redirect here to suppress printouts.
+##        with redirect.redirect( redirect.null_file, sys.stdout ):
+##            with redirect.redirect( redirect.null_file, sys.stderr ):
+##                result = fork_break(F,mtds,BREAK)
+    elif 'L' in BREAK:
+        result = fork_last(F,mtds)
+    elif 'B' in BREAK:
+        result = fork_best(F,mtds)
+    else:
+        result = fork_break(F,mtds,BREAK)
+    return result
+
+def fork_all(funcs,mtds):
+    """Runs funcs in parallel and continue running until all are done"""
+    global methods
+    y = time.time()
+    for i,res in pyabc_split.abc_split_all(funcs):
+        status = prob_status()
+        t = time.time()-y
+        if not status == -1: #solved here
+            if status == 1: #unsat
+                print '%s proved UNSAT in %f sec.'%(mtds[i],t)
+            else:
+                print '%s found cex in %f sec. - '%(mtds[i],t),
+                if not mtds[i] == 'REACHM':
+                    print 'cex depth at %d'%cex_frame()
+                else:
+                    print ' '
+            continue
+        else:
+            print '%s was undecided in %f sec. '%(mtds[i],t)
+    return i,res
+
+def fork_break(funcs,mtds,BREAK):
+    """
+    Runs funcs in parallel and breaks according to BREAK <= '?US'
+    If mtds = 'sleep' or [], we are proving outputs in parallel
+    Saves cex's found in cex_list in case we are proving POs.
+    """
+    global methods,last_verify_time,seed,cex_list,last_winner,last_cex
+    seed = seed + 3 # since parallel processes do not chenge the seed in the prime process, we need to change it here
+    cex_list = lst = []
+    y = time.time() #use wall clock time because parent fork process does not use up compute time.
+    for i,res in pyabc_split.abc_split_all(funcs):
+        status = get_status()
+        t = time.time()-y
+        lm = len(mtds)
+        if ((lm < 2) and not i == 0): # the only single mtds case is where it is 'sleep'
+            M = 'Output %d'%(i-lm)
+        else:
+            M = mtds[i]
+            last_winner = M
+        if M == 'sleep':
+            print 'sleep: time expired in %s sec.'%convert(t)
+            assert status >= Unsat,'status = %d'%status
+            break
+        if ((status > Unsat) and '?' in BREAK): #undecided
+                break
+        elif status == Unsat: #unsat
+            print '%s: UNSAT in %s sec.'%(M,convert(t))
+            if 'U' in BREAK:
+                break
+        elif status < Unsat: #status == 0 - cex found
+            if M in methods:                
+                if methods.index(M) in exbmcs+allreachs+allpdrs+[1]: #set the known best depth so far. [1] is interp
+                    set_max_bmc(n_bmc_frames())
+            last_cex = M
+            print '%s: -- cex in %0.2f sec. at depth %d => '%(M,t,cex_frame()),
+            cex_list = cex_list+[cex_get()] #accumulates multiple cex's and puts them on list.
+            if len(cex_list)>1:
+                print 'len(cex_list): %d'%len(cex_list)
+            if 'S' in BREAK:
+                break
+        else:
+            continue
+    return i,status
+
+def fork_best(funcs,mts):
+    """ fork the functions, If not solved, take the best result in terms of AIG size"""
+    global f_name
+    n = len(mts)-1
+    y = time.time()
+    m_best = -1
+    best_size = [n_pis(),n_latches(),n_ands()]
+##    print best_size
+    abc('w %s_best_aig.aig'%f_name)
+    for i,res in pyabc_split.abc_split_all(funcs):
+        status = prob_status()
+##        print i,
+##        ps()
+##        print i,res,
+        #ps()
+        if not status == -1: #solved here
+            m = i
+            t = time.time()-y
+            if status == 1: #unsat
+                print '%s proved UNSAT in %f sec.'%(mtds[i],t)
+            else:
+                print '%s found cex in %f sec. - '%(mtds[i],t),
+            break
+        else:
+            cost = rel_cost(best_size)
+##            print i,cost
+            if cost < 0:
+                best_size = [n_pis(),n_latches(),n_ands()]
+##                print best_size
+                m_best = i
+##                print m_best
+                abc('w %s_best_aig.aig'%f_name)
+    abc('r %s_best_aig.aig'%f_name)
+    return m_best,res
+
+def fork_last(funcs,mtds):
+    """ fork the functions, and take first definitive answer, but
+    if last method ends first, then kill others"""
+    n = len(mtds)-1
+    m = -1
+    y = time.time()
+    lst = ''
+    print mtds
+    for i,res in pyabc_split.abc_split_all(funcs):
+        status = prob_status()
+        if not status == -1: #solved here
+            m = i
+            t = int(time.time()-y)
+            if status == 1: #unsat
+                print '%s proved UNSAT in %d sec.'%(mtds[i],t)
+            else:
+                print '%s found cex in %s sec. - '%(mtds[i],convert(t)),
+            break
+        elif i == n:
+            t = int(time.time()-y)
+            m = i
+            print '%s: %d sec.'%(mtds[i],t)
+            ps()
+            break
+        elif mtds[i] == 'sleep':
+            t = time.time()-y
+            print 'sleep timer expired in %0.2f'%t
+            break
+        lst = lst + ', '+mtds[i]
+    return m,res
+
+def fork(funcs,mtds):
+    """ runs funcs in parallel This keeps track of the verify time
+    when a cex was found, and if the time to find
+    the cex was > 1/2 allowed time, then last_verify_time is increased by 2"""
+    global win_list, methods, last_verify_time,seed
+    beg_time = time.time()
+    i,res = fork_break(funcs,mtds,'US') #break on Unsat of Sat.
+    t = time.time()-beg_time        #wall clock time because fork does not take any compute time.
+    if t > .4*last_verify_time:
+##    if t > .15*last_verify_time: ##### temp
+        t = last_verify_time = last_verify_time + .1*t
+        #print 'verify time increased to %s'%convert(t)
+    assert res == get_status(),'res: %d, status: %d'%(res,get_status())
+    return i,res
+
+
+def save_time(M,t):
+    global win_list,methods
+    j = methods.index(M)
+    win_list = win_list + [(j,t)]
+    #print win_list
+
+def summarize(lst):
+    result = [0]*10
+    for j in range(len(lst)):
+        k = lst[j]
+        result[k[0]]=result[k[0]]+k[1]
+    return result
+
+def top_n(lst,n):
+    result = []
+    ll = list(lst) #makes a copy
+    m = min(n,len(ll))
+    for i in range(m):
+        mx_index = ll.index(max(ll))
+        result = result + [mx_index]
+        ll[mx_index] = -1
+    return result
+
+def super_pre_simp():
+    while True:
+        nff = n_latches()
+        print 'Calling pre_simp'
+        pre_simp()
+        if n_latches() == nff:
+            break
+
+#______________________________
+#new synthesis command
+
+def synculate(t):
+    """
+    Finds candidate sequential equivalences and refines them by simulation, BMC, or reachability
+    using any cex found. If any are proved, then they are used to reduce the circuit. The final aig
+    is a new synthesized circuit where all the proved equivalences are merged.
+    If we put this in a loop with increasing verify times, then each time we work with a simpler model
+    and new equivalences. Should approach srm. If in a loop, we can remember the cex_list so that we don't
+    have to deal with disproved equivalences. Then use refine_with_cexs to trim the initial equivalences.
+    If used in synthesis, need to distinguish between
+    original outputs and new ones. Things to take care of: 1. a PO should not go away until it has been processes by merged_proved_equivalences
+    2. Note that &resim does not use the -m option where as in speculation - m is used. It means that if
+    an original PO isfound to be SAT, the computation quits becasue one of the output
+    miters has been disproved.
+    """    
+    global G_C,G_T,n_pos_before, x_factor, n_latches_before, last_verify_time, f_name,cex_list, max_verify_time
+    
+    
+    def refine_with_cexs():
+        """Refines the gores file to reflect equivalences that go away because of cexs in cex_list"""
+        global f_name
+        abc('&r %s_gores.aig'%f_name)
+        for j in range(len(cex_list)):
+            cex_put(cex_list[j])
+            run_command('&resim') #put the jth cex into the cex space and use it to refine the equivs
+        abc('&w %s_gores.aig'%f_name)
+        return
+    
+    def generate_srms():
+        """generates a synthesized reduced model (srms) from the gores file"""
+        global f_name, po_map
+        abc('&r %s_gores.aig; &srm -sf; r gsrms.aig; w %s_gsrms.aig'%(f_name,f_name))
+        print 'New srms = ',ps()
+        po_map = range(n_pos())
+        return 'OK'
+
+    def merge_proved_equivalences():
+        #this only changes the gores file.
+        run_command('&r %s_gores.aig; &equiv_mark -vf %s_gsrms.aig; &reduce -v; &w %s_gores.aig'%(f_name,f_name,f_name))
+        return
+
+    def generate_equivalences():
+        set_globals()
+        t = max(1,.5*G_T)
+        r = max(1,int(t))
+        cmd = "&get; &equiv2 -C %d -F 200 -T %f -S 1 -R %d"%((G_C),t,r)
+        abc(cmd)
+        #run_command('&ps')
+        eq_simulate(.5*t)
+        #run_command('&ps')
+        cmd = '&semi -W 63 -S 5 -C 500 -F 20 -T %d'%(.5*t)
+        abc(cmd)
+        #run_command('&ps')
+        run_command('&w %s_gores.aig'%f_name)
+
+    remove_0_pos() #makes sure no 0 pos to start
+    cex_list = []
+    n_pos_before = n_pos()
+    n_latches_before = n_latches()
+##    print 'Generating equivalences'
+    generate_equivalences()
+##    print 'Generating srms file'
+    generate_srms() #this should not create new 0 pos
+##    if n_pos()>100:
+##        removed
+    remove_0_pos()
+    n_pos_last = n_pos()
+    if n_pos_before == n_pos():
+        print 'No equivalences found. Quitting synculate'
+        return Undecided_no_reduction
+    print 'Initial synculation: ',ps()
+##    ps()
+    set_globals()
+    simp_sw = init = True
+    simp_sw = False #temporary
+    print '\nIterating synculation refinement'
+    abc('w initial_sync.aig')
+    max_verify_time = t
+    print 'max_verify_time = %d'%max_verify_time
+    """
+        in the following loop we increase max_verify_time by twice time spent to find last cexs or Unsat's
+        We iterate only when we have proved cex + unsat > 1/2 n_pos. Then we update srms and repeat.        
+    """
+    while True:                 # refinement loop
+        t = max_verify_time     #this may have been increased since the last loop
+##        print 'max_verify_time = %d'%max_verify_time
+        set_globals()
+        if not init:
+            generate_srms()     #generates a new gsrms file and leaves it in workspace
+##            print 'generate_srms done'
+            if n_pos() == n_pos_before:
+                break
+            if n_pos() == n_pos_last:   #if nothing new, then quit if max_verification time is reached.
+                if t > max_verify_time:
+                    break
+            if simp_sw:                     #Warning: If this holds then simplify could create some 0 pos
+                na = n_ands()
+                simplify()
+                while True:
+                    npo = n_pos()
+##                    print 'npos = %d'%npo
+                    merge_proved_equivalences() #So we need to merge them here. Can merging create more???
+                    generate_srms()
+                    if npo == n_pos():
+                        break
+                if n_ands() > .7*na:            #if not significant reduction, stop simplification
+                    simp_sw = False             #simplify only once.
+            if n_latches() == 0:
+                return check_sat()
+        n_pos_last = n_pos()
+        init = False                        # make it so that next time it is not the first time through
+        syn_par(t)
+        if (len(cex_list)+len(result)) == 0: #nothing happened aand ran out of time.
+            break
+        abc('w %s_gsrms.aig'%f_name)
+        #print 'No. of cexs after syn_parallel = %d'%len(cex_list)
+        merge_proved_equivalences()         #changes the underlying gores file by merging fanouts of proved eqs
+        #print 'merge done'
+        refine_with_cexs()                  #changes the gores file by refining the equivalences in it using cex_list.
+        #print 'refine_with_cexs done'
+        continue
+    extract(0,n_pos_before) #get rid of unproved outputs
+    return
+
+def syn_par(t):
+    """prove n outputs at once and quit at first cex. Otherwise if no cex found return aig
+    with the unproved outputs"""
+    global trim_allowed,max_verify_time, n_pos_before
+    global cex_list, result
+    b_time = time.time()
+    n = n_pos()
+    if n == n_pos_before:
+        return
+    mx = n_pos()
+    if n_pos() - n_pos_before > 50:
+        mx = n_pos_before + 50
+    r = range(n_pos_before, mx)     
+    N = max(1,(mx-n_pos_before)/2)
+    abc('w %s__ysavetemp.aig'%f_name) 
+    F = [eval(FUNCS[18])] #create a timer function
+    #print r
+    for i in r:
+        F = F + [eval('(pyabc_split.defer(verify_only)(%d,%d))'%(i,t))]
+    cex_list = result = []
+    outcome = ''
+    #redirect printout here
+##    with redirect.redirect( redirect.null_file, sys.stdout ):
+##        with redirect.redirect( redirect.null_file, sys.stderr ):
+    for i,res in pyabc_split.abc_split_all(F):
+        status = get_status()
+##        print i
+        if i == 0:          #timed out
+            outcome = 'time expired after = %d'%(time.time() - b_time)
+            break
+        if status < Unsat:
+            cex_list = cex_list + [cex_get()]                    
+        if status == Unsat:
+            result = result + [r[i-1]]
+        if (len(result)+len(cex_list))>= N:
+            T = time.time() - b_time
+            if T > max_verify_time/2:
+                max_verify_time = 2*T
+            break
+        continue
+    if not outcome == '':
+        print outcome
+##    print 'cex_list,prove_list = ',cex_list,result
+    abc('r %s__ysavetemp.aig'%f_name) #restore initial aig so that pos can be 0'ed out
+    if not result == []: # found some unsat's
+##        min_r = min(result)
+##        max_r = max(result)
+##        no = n_pos()
+##        assert (0 <= min_r and max_r < no), 'min_r, max_r, length = %d, %d, %d'%(min_r,max_r,len(result))
+        zero(result)
+    return
+    #print "Number PO's proved = %d"%len(result)
+
+def absec(n):
+    #abc('w t.aig')
+    for j in range(n):
+        print '\nFrame %d'%(j+1)
+        run_command('absec -F %d'%(j+1))
+        if is_unsat():
+            print 'UNSAT'
+            break
+    
+
+"""
+    we might be proving some original pos as we go, and on the other hand we might have some equivalences that we
+    can't prove. There are two uses, in verification
+    verification - we want to remove the proved pos whether they are original or not. But if a cex for an original, then need to
+                    remember this.
+    synthesis - the original outputs need to be kept and ignored in terms of cex's - supposedly they can't be proved.
+"""
+
+""" Experimental"""
+
+def csec():
+    global f_name
+    if os.path.exists('%s_part0.aig'%f_name):
+        os.remove('%s_part0.aig'%f_name)
+    run_command('demiter')
+    if not os.path.exists('%s_part0.aig'%f_name):
+        return
+    run_command('r %s_part0.aig'%f_name)
+    ps()
+    run_command('comb')
+    ps()
+    abc('w %s_part0comb.aig'%f_name)
+    run_command('r %s_part1.aig'%f_name)
+    ps()
+    run_command('comb')
+    ps()
+    abc('w %s_part1comb.aig'%f_name)
+    run_command('&get; &cec %s_part0comb.aig'%(f_name))
+    if is_sat():
+        return 'SAT'
+    if is_unsat():
+        return 'UNSAT'
+    else:
+        return 'UNDECIDED'
+
+    ###########################
+####        we will verify outputs ORed in groups of g[i]
+####        here we take div = N so no ORing
+##        div = max(1,N/1)
+##        g = distribute(N,div)
+##        if len(g) <= 1:
+##            t = tt
+##        g.reverse()
+####        print g
+##        x = 0
+##        G = []
+##        for i in range(div):
+##            y = x+g[i]
+##            F = F + [eval('(pyabc_split.defer(verify_range)(%d,%d,%s))'%(x,y,convert(t)))]
+##            G = G + [range(x,y)]
+##            x = y
+####        print G
+###########################
+
+def sop_balance(k):
+    abc('st; if -K %d;ps'%k)
+    for i in range(2):
+        run_command('st; if -K %d;ps'%k)
+    run_command('st; if  g -C %d -K %d;ps'%(k+4,k+4))
+    for i in range(3):
+        run_command('st;&get; &dch; &put; if -K %d;ps'%k)
+
+def map_lut_dch(k):
+    for i in range(5):
+        run_command('st;if -a -K %d; ps; st; dch; ps; if -a -K %d; ps; mfs ;ps; lutpack; ps'%(k,k))
+    
+def map_lut(k):
+    for i in range(5):
+        run_command('st; if -e -K %d; ps;  mfs ;ps; lutpack -L 50; ps'%(k))
+    
+