abc_common.py 61.9 KB
Newer Older
1 2 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 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494 1495 1496 1497 1498 1499 1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515 1516 1517 1518 1519 1520 1521 1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 1542 1543 1544 1545 1546 1547 1548 1549 1550 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581 1582 1583 1584 1585 1586 1587 1588 1589 1590 1591 1592 1593 1594 1595 1596 1597 1598 1599 1600 1601 1602 1603 1604 1605 1606 1607 1608 1609 1610 1611 1612 1613 1614 1615 1616 1617 1618 1619 1620 1621 1622 1623 1624 1625 1626 1627 1628 1629 1630 1631 1632 1633 1634 1635 1636 1637 1638 1639 1640 1641 1642 1643 1644 1645 1646 1647 1648 1649 1650 1651 1652 1653 1654 1655 1656 1657 1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 1673 1674 1675 1676 1677 1678 1679 1680 1681 1682 1683 1684 1685 1686 1687 1688 1689 1690 1691 1692 1693 1694 1695 1696 1697 1698 1699 1700 1701 1702 1703 1704 1705 1706 1707 1708 1709 1710 1711 1712 1713 1714 1715 1716 1717 1718 1719 1720 1721 1722 1723 1724 1725 1726 1727 1728 1729 1730 1731 1732 1733 1734 1735 1736 1737 1738 1739 1740 1741 1742 1743 1744 1745 1746 1747 1748 1749 1750 1751 1752 1753 1754 1755 1756 1757 1758 1759 1760 1761 1762 1763 1764 1765 1766 1767 1768 1769 1770 1771 1772 1773 1774 1775 1776 1777 1778 1779 1780 1781 1782 1783 1784 1785 1786 1787 1788 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820 1821 1822 1823 1824 1825 1826 1827 1828 1829 1830 1831 1832 1833 1834 1835 1836 1837 1838 1839 1840 1841 1842 1843 1844 1845 1846 1847 1848 1849 1850 1851 1852 1853 1854 1855
from pyabc import *
import redirect
import sys
import os
import time
import math
global G_C,G_T,latches_before_abs,latches_before_pba,n_pos_before,x_factor

"""
The functions that are currently available from module _abc are:

int n_ands();
int n_pis();
int n_pos();
int n_latches();
int n_bmc_frames();
int prob_status(); 1 = unsat, 0 = sat, -1 = unsolved

int run_command(char* cmd);

bool has_comb_model();
bool has_seq_model();
bool is_true_cex();
bool is_valid_cex();
  return 1 if the number of PIs in the current network and in the current counter-example are equal
int  n_cex_pis();
  return the number of PIs in the current counter-example
int  n_cex_regs();
  return the number of flops in the current counter-example
int  cex_po();
  returns the zero-based output PO number that is SAT by cex
int  cex_frame();
  return the zero-based frame number where the outputs is SAT
The last four APIs return -1, if the counter-example is not defined. 
"""

#global variables

stackno_gabs = stackno_gore = stackno_greg= 0
STATUS_UNKNOWN = -1
STATUS_SAT = 0
STATUS_UNSAT = 1
RESULT = ('SAT' , 'SAT', 'UNSAT', 'UNDECIDED but reduced', 'UNDECIDED, no reduction', 'UNDCIDED but reduced'  )
Sat_reg = 0
Sat_true = 1
Unsat = 2
Undecided_reduction = 3
Undecided_no_reduction = 4
Error = 5
Restart = 6
xfi = x_factor = 1  #set this to higher for larger problems or if you want to try harder during abstraction
max_bmc = -1
last_time = 0

# Function definitions:
# simple functions: ________________________________________________________________________
# set_globals, abc, q, x, has_any_model, is_sat, is_unsat, push, pop

# ALIASES
def p():
    return prove()

def ps():
    print_circuit_stats()

def n_real_inputs():
    """This gives the number of 'real' inputs. This is determined by trimming away inputs that
    have no connection to the logic. This is done by the ABC alias 'trm', which changes the current
    circuit. In some applications we do not want to change the circuit, but just to know how may inputs
    would go away if we did this. So the current circuit is saved and then restored afterwards."""
    abc('w %s_savetempreal.aig; logic; trim; st'%f_name)
    n = n_pis()
    abc('r %s_savetempreal.aig'%f_name)
    return n

def long(t):
    if t<20:
        t = t
    else:
        t = 20+(t-20)/3
    return max(10,t)

def rif():
    """Not used"""
    global f_name
    print 'Type in the name of the aig file to be read in'
    s = raw_input()
    if s[-5:] == '.blif':
        f_name = s[:-5]
    else:
        f_name = s
        s = s+'.blif'
    run_command(s)
    x('st;constr -i')
    print_circuit_stats()
    a = n_ands()
    f = max(1,30000/a)
    f = min (f,16)
    x('scorr -c -F %d'%f)
    x('fold')
    print_circuit_stats()
    x('w %s_c.aig'%f_name)

def abc(cmd):
    abc_redirect_all(cmd)
    

def abc_redirect( cmd, dst = redirect.null_file, src = sys.stdout ):
    """This is our main way of calling an ABC function. Redirect, means that we suppress any output from ABC"""
    with redirect.redirect( dst, src ):
        return run_command( cmd )


def abc_redirect_all( cmd ):
    """This is our main way of calling an ABC function. Redirect, means that we suppress any output from ABC, including error printouts"""
    with redirect.redirect( redirect.null_file, sys.stdout ):
        with redirect.redirect( redirect.null_file, sys.stderr ):
            return run_command( cmd )

def set_globals():
    """This sets global parameters that are used to limit the resources used by all the operations
    bmc, interpolation BDDs, abstract etc. There is a global factor 'x_factor' that can
    control all of the various resource limiting parameters"""
    global G_C,G_T,x_factor
    nl=n_latches()
    na=n_ands()
    np = n_pis()
    #G_C = min(500000,(3*na+500*(nl+np)))
    G_C = x_factor * min(100000,(3*na+500*(nl+np)))
    #G_T = min(250,G_C/2000)
    G_T = x_factor * min(75,G_C/2000)
    G_T = max(1,G_T)
    #print('Global values: BMC conflicts = %d, Max time = %d sec.'%(G_C,G_T))
    
def a():
    """this puts the system into direct abc input mode"""
    print "Entering ABC direct-input mode. Type q to quit ABC-mode"
    n = 0
    while True:
        print '     abc %d> '%n,
        n = n+1
        s = raw_input()
        if s == "q":
            break
        run_command(s) 

def set_fname(name):
    """ Another way to set an f_name, but currently this is not used"""
    global f_name
    s = name
    if s[-4:] == '.aig':
        f_name = s[:-4]
    else:
        f_name = s
        s = s+'.aig'
    #read in file
    run_command(s)
    #print_circuit_stats()

def read_file_quiet(fname=None):
    """This is the main program used for reading in a new circuit. The global file name is stored (f_name)
    Sometimes we want to know the initial starting name. The file name can have the .aig extension left off
    and it will assume that the .aig extension is implied. This should not be used for .blif files.
    Any time we want to process a new circuit, we should use this since otherwise we would not have the
    correct f_name."""
    global max_bmc,  f_name, d_name, initial_f_name, x_factor, init_initial_f_name
    x_factor = 1
    max_bmc = -1
    
    if fname is None:
        print 'Type in the name of the aig file to be read in'
        s = raw_input()
    else:
        s = fname
        
    if s[-4:] == '.aig':
        f_name = s[:-4]
    else:
        f_name = s
        s = s+'.aig'
        
    run_command(s)
    initial_f_name = f_name
    init_initial_f_name = f_name
    
def read_file():
    read_file_quiet()
    print_circuit_stats()

def rf():
    read_file()

##def 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.
    It manages the name of the file, by giving an extension (s). The file name 'f_name'
    keeps increasing as more extensions are written. A typical sequence is
    name, name_smp, name_smp_abs, name_smp_abs_spec, name_smp_abs_spec_final"""
    global f_name
    """Writes out the current file as an aig file using f_name appended with argument"""
    f_name = '%s_%s'%(f_name,s)
    ss = '%s.aig'%(f_name)
    print 'WRITING %s: '%ss,
    print_circuit_stats()
    abc('w '+ss)
    
def wf():
    """Not used"""
    print 'input type of file to be written'
    s = raw_input()
    write_file(s)

def bmc_depth():
    """ Finds the number of BMC frames that the latest operation has used. The operation could be BMC, reachability
    interpolation, abstract, speculate. max_bmc is continually increased. It reflects the maximum depth of any version of the circuit
    including abstract ones, for which it is known that there is not cex out to that depth."""
    global max_bmc
    b = n_bmc_frames()
    max_bmc = max(b,max_bmc)
    return max_bmc

def set_max_bmc(b):
    """ Keeps increasing max_bmc which is the maximum number of time frames for
    which the current circuit is known to be UNSAT for"""
    global max_bmc
    max_bmc = max(b,max_bmc)

def print_circuit_stats():
    """Stardard way of outputting statistice about the current circuit"""
    global max_bmc
    i = n_pis()
    o = n_pos()
    l = n_latches()
    a = n_ands()
    b = max(max_bmc,bmc_depth())
    c = cex_frame()
    if b>= 0:
        if c>=0:
            print 'PIs = %d, POs = %d, FF = %d, ANDs = %d, max depth = %d, CEX depth = %d'%(i,o,l,a,b,c)
        else:
            print 'PIs = %d, POs = %d, FF = %d, ANDs = %d, max depth = %d'%(i,o,l,a,b)
    else:
        if c>=0:
            print 'PIs = %d, POs = %d, FF = %d, ANDs = %d, CEX depth = %d'%(i,o,l,a,c)
        else:
            print 'PIs = %d, POs = %d, FF = %d, ANDs = %d'%(i,o,l,a)

def q():
    exit()

def x(s):
    """execute an ABC command"""
    print "RUNNING: ", s
    run_command(s)

def has_any_model():
    """ check if a satisfying assignment has been found"""
    res = has_comb_model() or has_seq_model()
    return res

def is_unsat():
    if prob_status() == 1:
        return True
    else:
        return False

def is_sat():
    if prob_status() == 0:
        return True
    else:
        return False

def wc(file):
    """writes <file> so that costraints are preserved explicitly"""
    abc('&get;&w %s'%file)

def rc(file):
    """reads <file> so that if constraints are explicit, it will preserve them"""
    abc('&r %s;&put'%file)                         

##def 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
    in the interpolation routine. Typically n = 1 or 10"""
    n_po = n_pos()
    abc('int -k -C %d'%n)
    print 'Reduced POs from %d to %d'%(n_po,n_pos())

def refine_with_cex():
    """Refines the greg (which contains the original problem with the set of FF's that have been abstracted).
    This generates a new abstraction (gabs) and modifies the greg file to reflect which regs are in the
    current abstraction"""
    global f_name
    print 'CEX in frame %d for output %d'%(cex_frame(),cex_po())
    abc('&r %s_greg.aig; &abs_refine; &w %s_greg.aig'%(f_name,f_name))
    return

def generate_abs(n):
    """generates an abstracted  model (gabs) from the greg file. The gabs file is automatically
    generated in the & space by &abs_derive. We store it away using the f_name of the problem
    being solved at the moment. The f_name keeps changing with an extension given by the latest
    operation done - e.g. smp, abs, spec, final, group. """
    global f_name
    #we have a cex and we use this generate a new gabs file
    abc('&r %s_greg.aig; &abs_derive; &put; w %s_gabs.aig'%(f_name,f_name)) # do we still need the gabs file
    if n == 1:
        print 'New abstraction: ',
        print_circuit_stats()
    return   

    
#more complex functions: ________________________________________________________
#, abstract, pba, speculate, final_verify, dprove3


def simplify():
    """Our standard simplification of logic routine. What it does depende on the problem size.
    For large problems, we use the &methods which use a simple circuit based SAT solver. Also problem
    size dictates the level of k-step induction done in 'scorr' The stongest simplification is done if
    n_ands < 20000. Then it used the clause based solver and k-step induction where |k| depends
    on the problem size """
    # set_globals()
##    print 'simplify initial ',
##    ps()
    abc('w t.aig')
    n=n_ands()
    abc('scl')
    if n > 30000:
        abc('&get;&scl;&put')
        n = n_ands()
        if n < 100000:
            abc("&dc2;&put;dr;&get;&lcorr;&dc2;&put;dr;&get;&scorr;&fraig;&dc2;&put;dr")
            run_command('ps')
            print '.',
            n = n_ands()
            if n<45000:
                abc("&get;&scorr -F 2;&put;dc2rs")
                print '.',
                #ps()
            else:
                abc("dc2rs")
                print '.',
                #ps()
            n = n_ands()
    n = n_ands()
    if n <= 30000:
        print '.',
        #ps()
        if n > 15000:
            abc("dc2rs")
            print '.',
        else:
            abc("scorr -F 2;dc2rs")
            print '.',
            #ps()
    n = max(1,n_ands())
    ps()
    if n < 20000:
        m = int(min( 60000/n, 16))
        #print 'm = %d'%m
        if m >= 4:
            j = 4
            while j <= m:
                set_size()
                #print 'j - %d'%j
                abc('scl;dr;dc2;scorr -C 5000 -F %d'%j)
                if check_size() == 1:
                    break
                j = 2*j
                #ps()
                continue
            print '.',


def iterate_simulation(latches_before):
    """Subroutine of 'abstract' which does the refinement of the abstracted model,
    using counterexamples found by simulation. Simulation is controlled by the amount
    of memory it might use. At first wide but shallow simulation is done, bollowed by
    successively more narrow but deeper simulation"""
    global x_factor, f_name
##    print 'RUNNING simulation iteratively'
    f = 5
    w = 255
    for k in range(9):
        f = min(f *2, 3500)
        w = max(((w+1)/2)-1,1)
        print '.',
        abc('sim -m -F %d -W %d'%(f,w))
        if not is_sat():
            continue
        while True:
            refine_with_cex()
            if is_sat():
                print 'cex failed to refine abstraction '
                return Sat_true
            generate_abs(0)
            latches_after = n_latches()
            print 'Latches increased to %d'%latches_after
            if latches_after >= .99*latches_before:
                abc('r %s_savetempabs.aig'%f_name)
                print "No reduction!."
                return Undecided_no_reduction
            abc('sim -m -F %d -W %d'%(f,w))
            if not is_sat():
                break

def iterate_abstraction_refinement(latches_before,NBF):
    """Subroutine of 'abstract' which does the refinement of the abstracted model,
    using counterexamples found by BMC or BDD reachability"""
    global x_factor, f_name
    if NBF == -1:
        F = 2000
    else:
        F = 2*NBF
    print '\nIterating BMC or BDD reachability'
    reach_sw = 0
    always_reach = 0
    cexf = 0
    reach_failed = 0
    while True:
        #print 'Generating problem abstraction'
        generate_abs(1)
        set_globals()
        latches_after = n_latches()
        if latches_after >= .98*latches_before:
##            print 'No reduction'
##            abc('r &s_savetemp.aig'%f_name)
            break
        ri = n_real_inputs() # No. of inputs after trm
        nlri = n_latches()+ri
        #reach_allowed = ((nlri<150) or (((cexf>250))&(nlri<300)))
        reach_allowed = ((nlri<75) or (((cexf>250))&(nlri<300)))
        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)):
            #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
        else:
            reach_sw = 0
            cmd = 'bmc3 -C %d -T %f -F %d'%(G_C,t,F)
        print 'RUNNING %s'%cmd
        abc(cmd)
        if prob_status() == 1:
            print 'Reachability went to %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)):
            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)
            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:
                break
            else:
                continue
    latches_after = n_latches()
    if latches_after >= .98*latches_before:
        abc('r %s_savetempabs.aig'%f_name)
        print "No reduction!"
        return Undecided_no_reduction
    else:
        print 'Latches reduced from %d to %d'%(latches_before, n_latches())
        return Undecided_reduction


def abstract():
    """ abstracts using N Een's method 3 - cex/proof based abstraction. The result is further refined using
    simulation, BMC or BDD reachability"""
    global G_C, G_T, latches_before_abs, x_factor
    set_globals()
    latches_before_abs = n_latches()
    abc('w %s_savetempabs.aig'%f_name)
    print 'Start: ',
    print_circuit_stats()
    c = 1.5*G_C
    #c = 20000
    t = max(1,1.25*G_T)
    method = 3
    if n_ands() > 100000:
        method = 0
    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')
    if is_sat():
        print 'Found true counterexample in frame %d'%cex_frame()
        return Sat_true
    NBF = bmc_depth()
    print 'Abstraction good to %d frames'%n_bmc_frames()
    set_max_bmc(NBF)
    abc('&w %s_greg.aig; &abs_derive; &put; w %s_gabs.aig'%(f_name,f_name))
    print 'First abstraction: ',
    print_circuit_stats()
    latches_after = n_latches()
    #if latches_before_abs == latches_after:
    if latches_after >= .98*latches_before_abs:
        abc('r %s_savetempabs.aig'%f_name)
        print "No reduction!"
        return Undecided_no_reduction    
    # refinement loop
    if (n_ands() + n_latches() + n_pis()) < 15000:
        print 'Running simulation iteratively'
        for i in range(5):
            result = iterate_simulation(latches_before_abs)
            if result == Restart:
                return result
            if result == Sat_true:
                return result
    result = iterate_abstraction_refinement(latches_before_abs, NBF)
    #if the result is 'Restart' we return and the calling routine increase
    #x_factor to try one more time.
    return result

def absv(n,v):
    """This is a version of 'abstract' which can control the methods used in Een's abstraction code (method = n)
    as well as whether we want to view the output of this (v = 1)"""
    global G_C, G_T, latches_before_abs, x_factor
    #input_x_factor()
    #x_factor = 3
    set_globals()
    latches_before_abs = n_latches()
    print 'Start: ',
    print_circuit_stats()
    c = 1.5*G_C
    t = max(1,1.25*G_T)
    s = min(max(3,c/30000),10) # stability between 3 and 10
    if max_bmc == -1:
        time = max(1,.01*G_T)
        abc('bmc3 -C %d -T %f -F 165'%(.01*G_C, time))
        set_max_bmc(bmc_depth())
    f = min(250,1.5*max_bmc)
    f = max(20, f)
    f = 10*f
    b = x_factor*20
    if not n == 0:
        b = 10
        b = max(b,max_bmc+2)
        b = b*2**(x_factor-1)
        b = 2*b
    print 'Neen abstraction params: Method #%d, %d conflicts, %d stable, %f sec.'%(n,c/3,s,t)
    if v == 1:
        run_command('&get; &abs_newstart -v -B %f -A %d -C %d -S %d -V %f'%(b,n,c/3,s,t))
    else:
        abc('&get; &abs_newstart -v -B %f -A %d -C %d -S %d -T %f'%(b,n,c/3,s,t))
    set_max_bmc(n_bmc_frames())
    print 'Abstraction good to %d'%n_bmc_frames()
    abc('&w %s_greg.aig; &abs_derive; &put; w %s_gabs.aig'%(f_name,f_name))
    print 'Final abstraction: ',
    print_circuit_stats()
    latches_after = n_latches()    
    if latches_after >= .98*latches_before_abs:
        print "No reduction!"
        return Undecided_no_reduction
    return Undecided_reduction

def spec():
    """Main speculative reduction routine. Finds candidate sequential equivalences and refines them by simulation, BMC, or reachability
    using any cex found. """
    input_x_factor()
    global G_C,G_T,n_pos_before, x_factor, n_latches_before
    set_globals()
    n_pos_before = n_pos()
    n_latches_before = n_latches()    
    set_globals()
    t = max(1,.5*G_T)
    r = max(1,int(t))
    print 'Running &equiv2 with C = %d, T = %f sec., F = %d -S 1 -R %d'%(G_C,t,200,r)
    abc("&get; &equiv2 -C %d -F 200 -T %f -S 1 -R %d; &semi -F 50; &speci -F 20 -C 1000;&srm; r gsrm.aig; w %s_gsrm.aig; &w %s_gore.aig"%((G_C),t,r,f_name,f_name))
    print 'Initial speculation: ',
    print_circuit_stats()
    print 'Speculation good to %d frames'%n_bmc_frames()
    return

def speculate():
    """Main speculative reduction routine. Finds candidate sequential equivalences and refines them by simulation, BMC, or reachability
    using any cex found. """
    
    global G_C,G_T,n_pos_before, x_factor, n_latches_before
    set_globals()
    n_pos_before = n_pos()
    
    def refine_with_cex():
        """Refines the gore file to reflect equivalences that go away because of cex"""
        global f_name
        print 'CEX in frame %d for output %d'%(cex_frame(),cex_po())
        abc('&r %s_gore.aig; &resim -m; &w %s_gore.aig'%(f_name,f_name))
        #abc('&r %s_gore.aig; &equiv2 -vx ; &w %s_gore.aig'%(f_name,f_name))
        return
    
    def generate_srm(n):
        """generates a speculated reduced model (srm) from the gore file"""
        global f_name
        pos = n_pos()
        ab = n_ands()
        abc('&r %s_gore.aig; &srm ; r gsrm.aig; w %s_gsrm.aig'%(f_name,f_name)) #do we still need to write the gsrm file
        if n == 0:
            if ((pos == n_pos()) and (ab == n_ands())):
                print 'Failed to refine'
                return 'failed'
        if n == 1:
            print 'Spec. Red. Miter: ',
            print_circuit_stats()
        return 'OK'

    def run_simulation(n):
        f = 5
        w = (256/n)-1
        for k in range(9):
            f = min(f * 2, 3500)
            w = max(((w+1)/2)-1,1)
            print '.',
            #generate_srm(0)
            abc('sim -m -F %d -W %d'%(f,w))
            if not is_sat():
                continue                
            if cex_po() < n_pos_before:
                print 'Sim found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame())
                return Sat_true                    
            refine_with_cex()
            if n_pos_before == n_pos():            
                return Undecided_no_reduction
            while True:
                result = generate_srm(0)
                if result == 'failed':
                    return Sat_true
                abc('sim -m -F %d -W %d'%(f,w))
                if not is_sat():
                    break                
                if cex_po() < n_pos_before:
                    print 'Sim found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame())
                    return Sat_true                    
                refine_with_cex()
                if n_pos_before == n_pos():            
                    return Undecided_no_reduction
        return Undecided_no_reduction
    
    n_pos_before = n_pos()
    n_latches_before = n_latches()    
    set_globals()
    t = max(1,.5*G_T)
    r = max(1,int(t))
    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))
    print 'Initial speculation: ',
    print_circuit_stats()
    print 'Speculation good to %d frames'%n_bmc_frames()
    #simplify()
    if n_pos_before == n_pos():
        print 'No new outputs. Quitting speculate'
        return Undecided_no_reduction # return result is unknown
    if is_sat():
        #print '\nWARNING: if an abstraction was done, need to refine it further\n'
        return Sat_true
    k = n_ands() + n_latches() + n_pis()
    n = 0
    if k < 15000:
        n = 1
    elif k < 30000:
        n = 2
    elif k < 60000:
        n = 4
    elif k < 120000:
        n = 8
    if n > 0: # simulation can run out of memory for too large designs, so be careful
        print 'RUNNING simulation iteratively'          
        for i in range(5):
            result = run_simulation(n)
            if result == Sat_true:
                return result
    simp_sw = 1
    int_sw = 1
    reach_sw = 0
    cexf = 0
    reach_failed = 0
    init = 1
    print '\nIterating BMC or BDD reachability'
    while True: # now try real hard to get the last cex.
        set_globals()
        if not init:
            set_size()
            result = generate_srm(1)
            if check_size() == True:
                print 'Failed to refine'
                return Error
            if result == 'failed':
                return Sat_true
            if simp_sw == 1:
                na = n_ands()
                simplify()
                if n_ands() > .7*na: #if not significant reduction, stop simplification
                    simp_sw = 0
            if n_latches() == 0:
                return check_sat()
        init = 0 # make it so that next time it is not the first time through
        time = max(1,G_T/(5*n_pos()))
        if int_sw ==1:
            npo = n_pos()
            if n_pos() > .5*npo:  # if not sufficient reduction, turn this off
                int_sw = 0
        if is_sat():        #if fast interpolation found a cex
            cexf = cex_frame()
            set_max_bmc(cexf - 1)
            if cex_po() < n_pos_before:
                print 'Int found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame())
                return Sat_true
            refine_with_cex()
            if n_pos_before == n_pos():            
                return Undecided_no_reduction
            if is_sat():
                print '1. cex failed to refine abstraction'
                return Sat_true
            continue
        else:
            if n_latches() == 0:
                return check_sat()
            ri = n_real_inputs()  #seeing how many inputs would trm get rid of
            nlri = n_latches() + ri
            reach_allowed = ((nlri<75) or (((cexf>250)) and (nlri<300)))
            if (((reach_allowed  or  (reach_sw == 1)) 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
            else:
                t = max(1,1.5*G_T)
                if max_bmc == -1:
                    f = 200
                else:
                    f = max_bmc
                f = int(1.5*f)
                cmd = 'bmc3 -C %d -T %f -F %f'%(1.5*G_C,1.2*t,f)
                reach_sw = 0            
            print 'Running %s'%cmd
            abc(cmd)
            if is_sat():
                cexf = cex_frame()
                set_max_bmc(cexf  - 1)
                #This is a temporary fix since reachx always reports cex_ps = 0
                if ((cex_po() < n_pos_before) and (cmd[:3] == 'bmc')):
                    print 'BMC found true cex: Output = %d, Frame = %d'%(cex_po(),cex_frame())
                    return Sat_true
                #End of temporary fix
                refine_with_cex()#change the number of equivalences
                if n_pos_before == n_pos():            
                    return Undecided_no_reduction
                continue
            else:
                set_max_bmc(bmc_depth())
                print 'No cex found in %d frames'%n_bmc_frames()
                if reach_sw == 0:
                    break
                else:
                    if prob_status() == 1:
                        print 'Reachability converged in %d frames'%n_bmc_frames()
                        return Unsat
                    reach_failed = 1
                    init = 1
                    continue
    if n_pos_before == n_pos():
        return Undecided_no_reduction 
    else:
        return Undecided_reduction

def set_size():
    """Stores  the problem size of the current design. Size is defined as (PIs, POs, ANDS, FF, max_bmc)""" 
    global npi, npo, nands, nff, nmd
    npi = n_pis()
    npo = n_pos()
    nands = n_ands()
    nff = n_latches()
    nmd = max_bmc

def check_size():
    """Assumes the problem size has been set by set_size before some operation. This checks if the size was changed
    Size is defined as (PIs, POs, ANDS, FF, max_bmc)
    Returns TRUE is size is the same""" 
    global npi, npo, nands, nff, nmd
    result = ((npi == n_pis()) and (npo == n_pos()) and (nands == n_ands()) and (nff == n_latches()) and (nmd == max_bmc))
##    if result == 1:
##        print 'Size unchanged'
    return result

def inferior_size():
    """Assumes the problem size has been set by set_size beore some operation.
    This checks if the new size is inferior (larger) to the old one 
    Size is defined as (PIs, POs, ANDS, FF)""" 
    global npi, npo, nands, nff
    result = ((npi < n_pis()) or (npo < n_pos()) or (nands < n_ands()) )
    return result

def quick_verify(n):
    """Low resource version of final_verify n = 1 means to do an initial simplification first"""
    abc('trm')
    if n == 1:
        simplify()
        if n_latches == 0:
            return check_sat()
        abc('trm')
    print 'After trimming: ',
    print_circuit_stats()
    #try_rpm()
    set_globals()
    if is_sat():
        return Sat_true   
    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))
    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
        abc(cmd)        
        status = get_status()
        if status <= Unsat:
            print 'Reachability went to %d frames, '%n_bmc_frames()
            print RESULT[status]
            return status
        print 'BDD reachability aborted'
    simplify() #why is this here
    if n_latches() == 0:
        print 'Simplified to 0 FF'
        return check_sat()
    set_max_bmc(bmc_depth()) # doesn't do anything
    print 'No success, max_depth = %d'%max_bmc
    return Undecided_reduction

def get_status():
    """this simply translates the problem status encoding done by ABC (-1,0,1)=(undecided,SAT,UNSAT) into the status code used by our python code."""
    status = prob_status() #interrogates ABC for the current status of the problem.
    # 0 = SAT
    if status == 1:
        status = Unsat
    if status == -1: #undecided
        status = Undecided_no_reduction
    return status

def try_rpm():
    """rpm is a cheap way of doing reparameterization and is an abstraction method, so may introduce false cex's.
    It finds a minimum cut between the PIs and the main sequential logic and replaces this cut by free inputs.
    A quick BMC is then done, and if no cex is found, we assume the abstraction is valid. Otherwise we revert back
    to the original problem before rpm was tried."""
    global x_factor
    if n_ands() > 30000:
        return
    set_globals()
    pis_before = n_pis()
    abc('w %s_savetemp.aig'%f_name)
    abc('rpm')
    result = 0
    if n_pis() < .5*pis_before:
        bmc_before = bmc_depth()
        #print 'running quick bmc to see if rpm is OK'
        t = max(1,.1*G_T)
        abc('bmc3 -C %d, -T %f'%(.1*G_C, t))
        if is_sat(): #rpm made it sat by bmc test, so undo rpm
            abc('r %s_savetemp.aig'%f_name)
        else:
            abc('trm')
            print 'WARNING: rpm reduced PIs to %d. May make SAT.'%n_pis()
            result = 1
    else:
        abc('r %s_savetemp.aig'%f_name)
    return result
            
def final_verify():
    """This is the final method for verifying anything is nothing else has worked. It first tries BDD reachability
    if the problem is small enough. If this aborts or if the problem is too large, then interpolation is called."""
    global x_factor
    set_globals()
##    simplify()
##    if n_latches() == 0:
##        return check_sat()
##    abc('trm')
    #rpm_result = try_rpm()
    set_globals()
    N = bmc_depth()
    L = n_latches()
    I = n_real_inputs()
    #try_induction(G_C)
    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
        abc(cmd)        
        status = get_status()
        if status <= Unsat:
            print 'Reachability went to %d frames, '%n_bmc_frames(),
            print RESULT[status]
            return status
        print 'BDD reachability aborted'          
    #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))
    status = get_status()
    if status <= Unsat:
        print 'Interpolation went to %d frames, '%n_bmc_frames(),
        print RESULT[status]
        return status
    simplify()
    if n_latches() == 0:
        return check_sat()
    print 'Undecided'
    return Undecided_reduction

def check_sat():
    """This is called if all the FF have disappeared, but there is still some logic left. In this case,
    the remaining logic may be UNSAT, which is usually the case, but this has to be proved. The ABC command 'dsat' is used fro combinational problems"""
##    if n_ands() == 0:
##        return Unsat
    abc('dsat -C %d'%G_C)
    if is_sat():
        return Sat_true
    elif is_unsat():
        return Unsat
    else:
        return Undecided_no_reduction

def try_era(s):
    """era is explicit state enumeration that ABC has. It only works if the number of PIs is small,
    but there are cases where it works and nothing else does"""
    if n_pis() > 12:
        return
    cmd = '&get;&era -mv -S %d;&put'%s
    print 'Running %s'%cmd
    run_command(cmd)

def try_induction(C):
    """Sometimes proving the property directly using induction works but not very often.
    For 'ind' to work, it must have only 1 output, so all outputs are or'ed together temporarily"""
    return Undecided_reduction
    print '\nTrying induction'
    abc('w %s_temp.aig'%f_name)
    abc('orpos; ind -uv -C %d -F 10'%C)
    abc('r %s_savetemp.aig'%f_name)
    status = prob_status()
    if not status == 1:
        return Undecided_reduction
    print 'Induction succeeded'
    return Unsat

def final_verify_recur(K):
    """During prove we make backups as we go. These backups have increasing abstractions done, which can cause
    non-verification by allowing false counterexamples. If an abstraction fails with a cex, we can back up to
    the previous design before the last abstraction and try to proceed from there. K is the backup number we
    start with and this decreases as the backups fails. For each backup, we just try final_verify.
    If ever we back up to 0, which is the backup just after simplify, we then try speculate on this. This often works
    well if the problem is a SEC problem where there are a lot of equivalences across the two designs."""
    for j in range(K):
        i = K-(j+1)
        if i == 0: #don't try final verify on original
            status = 3
            break
        print '\nVerifying backup number %d:'%i,
        abc('r %s_backup_%d.aig'%(initial_f_name,i))
        print_circuit_stats()
        status = final_verify()
        if status >= Unsat:
            return status
        if  i > 0:
            print 'SAT returned, trying less abstract backup'
            continue
        break
    if ((i == 0) and (status > Unsat) and (n_ands() > 0)):
        print '\nTrying speculate on initial backup number %d:'%i,
        abc('r %s_backup_%d.aig'%(initial_f_name,i))
        ps()
        if n_ands() < 20000:
            status = speculate()
            if ((status <= Unsat) or (status == Error)):
                return status
        status = final_verify()
    if status == Unsat:
        return status
    else:
        return Undecided_reduction
        

def 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"""
    set_globals()
    #print 'trying forward'
    try_forward()
    #print 'trying quick simp'
    quick_simp()
    #print 'trying_scorr_constr'
    status = try_scorr_constr()
    #status = 3
    #print 'trying trm'
    if ((n_ands() > 0) or (n_latches()>0)):
        abc('trm')
    print 'Forward, quick_simp, scorr_constr,: ',
    print_circuit_stats()
    status = process_status(status)
    if status <= Unsat:
        return status
    simplify()
    print 'Simplify: ',
    print_circuit_stats()
    if n_latches() == 0:
        return check_sat()
    try_phase()
    if n_latches() == 0:
        return check_sat()
    #abc('trm')
    if ((n_ands() > 0) or (n_latches()>0)):
        abc('trm')
    status = process_status(status)
    if status <= Unsat:
        return status
    status = try_scorr_constr()
    abc('trm')
    return process_status(status)

def try_scorr_constr():
    set_size()
    abc('w %s_savetemp.aig'%f_name)
    status = scorr_constr()
    if inferior_size():
        abc('r %s_savetemp.aig'%f_name)
    return status

def process(status):
    """Checks if there are no FF and if so checks if the remaining combinational
    problem is UNSAT"""
    if n_latches() == 0:
        return check_sat()
    return status

def try_phase():
    """Tries phase abstraction. ABC returns the maximum clock phase it found using n_phases.
    Then unnrolling is tried up to that phase and the unrolled model is quickly
    simplified (with retiming to see if there is a significant reduction.
    If not, then revert back to original""" 
    n = n_phases()
    if ((n == 1) or (n_ands() > 30000)):
        return
    print 'Number of possible phases = %d'%n
    abc('w %s_savetemp.aig'%f_name)
    na = n_ands()
    nl = n_latches()
    ni = n_pis()
    no = n_pos()
    cost_init = (1*n_pis())+(2*n_latches())+.05*n_ands()
    cost_min = cost_init
    cost = cost_init
    abc('w %s_best.aig'%f_name)
    for j in range(4):
        abc('r %s_savetemp.aig'%f_name)
        p = 2**(j+1)
        if p > n:
            break
        abc('phase -F %d'%p)
        if na == n_ands():
            break
        abc('scl;rw')
        if n_latches() > nl: #why would this ever happen
            break
        #print_circuit_stats()
        abc('rw;lcorr;trm')
        #print_circuit_stats()
        cost = (1*n_pis())+(2*n_latches())+.05*n_ands()
        if cost < cost_min:
            cost_min = cost
            abc('w %s_best.aig'%f_name)
        else:
            break
    if cost < cost_init:
        abc('r %s_best.aig'%f_name)
        simplify()
        abc('trm')
        print 'Phase abstraction obtained :',
        print_circuit_stats()
        return
    abc('r %s_savetemp.aig'%f_name)
    return       

def try_forward():
    """Attempts most forward retiming, and latch correspondence there. If attempt fails to help simplify, then we revert back to the original design
    This can be effective for equivalence checking problems where synthesis used retiming"""
    abc('w %s_savetemp.aig'%f_name)
    if n_ands() < 30000:
        abc('dr')
        abc('lcorr')
        nl = n_latches()
        na = n_ands()
        abc('w %s_savetemp0.aig'%f_name)
        abc('r %s_savetemp.aig'%f_name) 
        abc('dr -m')
        abc('lcorr')
        abc('dr')
        if ((n_latches() <= nl) and (n_ands() < na)):
            print 'Forward retiming reduced size to: ',
            print_circuit_stats()
            return
        else:
            abc('r %s_savetemp0.aig'%f_name)
            return
    return       

def quick_simp():
    """A few quick ways to simplify a problem before more expensive methods are applied.
    Uses & commands if problem is large. These commands use the new circuit based SAT solver"""
    na = n_ands()
    if na < 30000:
        abc('scl;rw')
    elif na < 80000:
        abc('&get;&scl;&put;rw')

def scorr_constr():
    #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())
    if ((na > 40000) or n_pos()>1):
        return Undecided_no_reduction
    f = 40000/na
    f = min(f,16)
    n_pos_before = n_pos()
    f = 1 #temporary until bug fixed.
    abc('w %s_savetemp.aig'%f_name)
    if n_ands() < 3000:
        cmd = 'unfold -a -F 2'
    else:
        cmd = 'unfold'
    abc(cmd)
    if ((n_ands() > na) or (n_pos() == 1)):
        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')
    return Undecided_no_reduction

def process_status(status):
    """ if there are no FF, the problem is combinational and we still have to check if UNSAT"""
    if n_latches() == 0:
        return check_sat()
    return status

def input_x_factor():
    """Sets the global x_factor according to user input"""
    global x_factor, xfi
    print 'Type in x_factor:',
    xfi = x_factor = input()
    print 'x_factor set to %f'%x_factor

def prove(a):
    """Proves all the outputs together. If ever an abstraction was done then if SAT is returned,
        we make RESULT return "undecided".
        if a = 0 we skip the first quick_verify"""
    global x_factor,xfi,f_name
    x = time.clock()
    max_bmc = -1
    K = 0
    print 'Initial: ',
    print_circuit_stats()
    x_factor = xfi
    print 'x_factor = %f'%x_factor
    print '\nRunning pre_simp'
    set_globals()
    status = pre_simp()
    if status <= Unsat:
        print 'Time for proof = %f sec.'%(time.clock() - x)
        return RESULT[status]
    if n_ands() == 0:
        abc('bmc3 -T 2')
        if is_sat():
            return 'SAT'
    abc('trm')
    write_file('smp')
    abc('w %s_backup_%d.aig'%(initial_f_name,K))
    K = K +1
    set_globals()
    if ((n_ands() < 30000) and (a == 1) and (n_latches() < 300)):
        print '\nRunning quick_verify'
        status = quick_verify(0)
        if status <= Unsat:
            if not status == Unsat:
                print 'CEX in frame %d'%cex_frame()
            print 'Time for proof = %f sec.'%(time.clock() - x)
            return RESULT[status]
        if n_ands() == 0:
            abc('bmc3 -T 2')
            if is_sat():
                return 'SAT'
    print'\nRunning abstract'
    nl_b = n_latches()
    status = abstract()
    abc('trm')
    write_file('abs')
    status = process_status(status)
    if ((status <= Unsat)  or  status == Error):
        if  status < Unsat:
            print 'CEX in frame %d'%cex_frame()
##            status = final_verify_recur(K)
##            write_file('final')
            print 'Time for proof = %f sec.'%(time.clock() - x)
            return RESULT[status]
        print 'Time for proof = %f sec.'%(time.clock() - x)
        return RESULT[status]
    abc('w %s_backup_%d.aig'%(initial_f_name,K))
    K = K +1
    if 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'
        K = 2
    elif n_ands() == 0:
        print 'Speculation skipped because no and nodes'
        K = 2
    else:
        print '\nRunning speculate'
        status = speculate()
        abc('trm')
        write_file('spec')
        status = process_status(status)
        if status == Unsat:
            print 'Time for proof = %f sec.'%(time.clock() - x)
            return RESULT[status]
        if ((status < Unsat) or (status == Error)):
            print 'CEX in frame %d'%cex_frame()
            K = K-1 #if spec found a true cex, then result of abstract was wrong
        else:
            abc('w %s_backup_%d.aig'%(initial_f_name,K))
            K = K +1
    status = final_verify_recur(K)
    abc('trm')
    write_file('final')
    print 'Time for proof = %f sec.'%(time.clock() - x)
    return RESULT[status]

def prove_g_pos(a):
    """Proves the outputs clustered by a parameter a. 
    a is the disallowed increase in latch support Clusters must be contiguous
    If a = 0 then outputs are proved individually. Clustering is done from last to first
    Output 0 is attempted to be proved inductively using other outputs as constraints.
    Proved outputs are removed if all the outputs have not been proved.
    If ever one of the proofs returns SAT, we stop and do not try any other outputs."""
    global f_name, max_bmc,x_factor
    x = time.clock()
    #input_x_factor()
    init_f_name = f_name
    #fast_int(1)
    print 'Beginning prove_g_pos'
    result = prove_all_ind()
    print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos()
    print '\n************Trying second level prove****************\n'
    try_rpm()
    result = prove(0)
    #result = prove_0_ind()
    if result == 'UNSAT':
        print 'Second prove returned UNSAT'
        return result
    if result == 'SAT':
        print 'CEX found'
        return result
    print '\n********** Proving each output separately ************'
    result = prove_all_ind()
    print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos()
    f_name = init_f_name
    abc('w %s_osavetemp.aig'%f_name)
    n = n_pos()
    print 'Number of outputs = %d'%n
    #count = 0
    pos_proved = []
    J = 0
    jnext = n-1
    while jnext >= 0:
        max_bmc = -1
        f_name = init_f_name
        abc('r %s_osavetemp.aig'%f_name)
        #Do in reverse order
        jnext_old = jnext
        if a == 0: # do not group
            extract(jnext,jnext)
            jnext = jnext -1 
        else:
            jnext = group(a,jnext)
        if jnext_old > jnext+1:
            print '\nProving outputs [%d-%d]'%(jnext + 1,jnext_old)
        else:
            print '\nProving output %d'%(jnext_old)
        #ps()
        #fast_int(1)
        f_name = f_name + '_%d'%jnext_old
        result = prove_1()
        if result == 'UNSAT':
            if jnext_old > jnext+1:
                print '\n********  PROVED OUTPUTS [%d-%d]  ******** \n\n'%(jnext+1,jnext_old)
            else:
                print '\n********  PROVED OUTPUT %d  ******** \n\n'%(jnext_old)
            pos_proved = pos_proved + range(jnext +1,jnext_old+1)
            continue
        if result == 'SAT':
            print 'One of output in (%d to %d) is SAT'%(jnext + 1,jnext_old)
            return result
        else:
            print '\n********  UNDECIDED on OUTPUTS %d thru %d  ******** \n\n'%(jnext+1,jnext_old)
    f_name = init_f_name
    abc('r %s_osavetemp.aig'%f_name)
    if not len(pos_proved) == n:
        print 'Eliminating %d proved outputs'%(len(pos_proved))
        remove(pos_proved)
        abc('trm')
        write_file('group')
        result = 'UNDECIDED'
    else:
        print 'Proved all outputs. The problem is proved UNSAT'
        result = 'UNSAT'
    print 'Total time for prove_g_pos = %f sec.'%(time.clock() - x)
    return result

def prove_pos():
    """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 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos()
    print '\n********** Proving each output separately ************'
    f_name = init_f_name
    abc('w %s_osavetemp.aig'%f_name)
    n = n_pos()
    print 'Number of outputs = %d'%n
    #count = 0
    pos_proved = []
    J = 0
    jnext = n-1
    while jnext >= 0:
        max_bmc = -1
        f_name = init_f_name
        abc('r %s_osavetemp.aig'%f_name)
        #Do in reverse order
        jnext_old = jnext
        if a == 0: # do not group
            extract(jnext,jnext)
            jnext = jnext -1 
        else:
            jnext = group(a,jnext)
        if jnext_old > jnext+1:
            print '\nProving outputs [%d-%d]'%(jnext + 1,jnext_old)
        else:
            print '\nProving output %d'%(jnext_old)
        #ps()
        #fast_int(1)
        f_name = f_name + '_%d'%jnext_old
        result = prove_1()
        if result == 'UNSAT':
            if jnext_old > jnext+1:
                print '\n********  PROVED OUTPUTS [%d-%d]  ******** \n\n'%(jnext+1,jnext_old)
            else:
                print '\n********  PROVED OUTPUT %d  ******** \n\n'%(jnext_old)
            pos_proved = pos_proved + range(jnext +1,jnext_old+1)
            continue
        if result == 'SAT':
            print 'One of output in (%d to %d) is SAT'%(jnext + 1,jnext_old)
            return result
        else:
            print '\n********  UNDECIDED on OUTPUTS %d thru %d  ******** \n\n'%(jnext+1,jnext_old)
    f_name = init_f_name
    abc('r %s_osavetemp.aig'%f_name)
    if not len(pos_proved) == n:
        print 'Eliminating %d proved outputs'%(len(pos_proved))
        remove(pos_proved)
        abc('trm')
        write_file('group')
        result = 'UNDECIDED'
    else:
        print 'Proved all outputs. The problem is proved UNSAT'
        result = 'UNSAT'
    print 'Total time for prove_g_pos = %f sec.'%(time.clock() - x)
    return result


def prove_g_pos_split():
    """like prove_g_pos but quits when any output is undecided"""
    global f_name, max_bmc,x_factor
    x = time.clock()
    #input_x_factor()
    init_f_name = f_name
    #fast_int(1)
    print 'Beginning prove_g_pos_split'
    result = prove_all_ind()
    print 'Number of outputs reduced to %d by induction and fast interpolation'%n_pos()
    try_rpm()
    print '\n********** Proving each output separately ************'  
    f_name = init_f_name
    abc('w %s_osavetemp.aig'%f_name)
    n = n_pos()
    print 'Number of outputs = %d'%n
    pos_proved = []
    J = 0
    jnext = n-1
    while jnext >= 0:
        max_bmc = -1
        f_name = init_f_name
        abc('r %s_osavetemp.aig'%f_name)
        jnext_old = jnext
        extract(jnext,jnext)
        jnext = jnext -1
        print '\nProving output %d'%(jnext_old)
        f_name = f_name + '_%d'%jnext_old
        result = prove_1()
        if result == 'UNSAT':
            if jnext_old > jnext+1:
                print '\n********  PROVED OUTPUTS [%d-%d]  ******** \n\n'%(jnext+1,jnext_old)
            else:
                print '\n********  PROVED OUTPUT %d  ******** \n\n'%(jnext_old)
            pos_proved = pos_proved + range(jnext +1,jnext_old+1)
            continue
        if result == 'SAT':
            print 'One of output in (%d to %d) is SAT'%(jnext + 1,jnext_old)
            return result
        else:
            print '\n********  UNDECIDED on OUTPUTS %d thru %d  ******** \n\n'%(jnext+1,jnext_old)
            print 'Eliminating %d proved outputs'%(len(pos_proved))
            # remove outputs proved and return
            f_name = init_f_name
            abc('r %s_osavetemp.aig'%f_name)
            remove(pos_proved)
            abc('trm')
            write_file('group')            
            return 'UNDECIDED'
    f_name = init_f_name
    abc('r %s_osavetemp.aig'%f_name)
    if not len(pos_proved) == n:
        print 'Eliminating %d proved outputs'%(len(pos_proved))
        remove(pos_proved)
        abc('trm')
        write_file('group')
        result = 'UNDECIDED'
    else:
        print 'Proved all outputs. The problem is proved UNSAT'
        result = 'UNSAT'
    print 'Total time = %f sec.'%(time.clock() - x)
    return result



def group(a,n):
    """Groups together outputs beginning at output n and any contiguous preceeding output
    that does not increase the latch support by a or more"""
    global f_name, max_bmc
    nlt = n_latches()
    extract(n,n)
    nli = n_latches()
    if n == 0:
        return n-1
    for J in range(1,n+1):
        abc('r %s_osavetemp.aig'%f_name)
        j = n-J
        #print 'trying %d to %d'%(j,n)
        extract(j,n)
        #print 'n_latches = %d'%n_latches()
        #if n_latches() >= nli + (nlt - nli)/2:
        if n_latches() == nli:
            continue
        if n_latches() > nli+a:
            break
    abc('r %s_osavetemp.aig'%f_name)
##    if j == 1:
##        j = j-1
    print 'extracting [%d-%d]'%(j,n)
    extract(j,n)
    ps()
    return j-1
        
def extract(n1,n2):
    """Extracts outputs n1 through n2"""
    no = n_pos()
    if n2 > no:
        return 'range exceeds number of POs'
    abc('cone -s -O %d -R %d'%(n1, 1+n2-n1))
    abc('scl')

def prove_0_ind():
    """Uses all other outputs as constraints to try to prove output 0 by induction"""
    abc('w %s_osavetemp.aig'%f_name)
    #ps()
    abc('constr -N %d'%(n_pos()-1))
    #ps()
    abc('fold')
    #ps()
    abc('ind -u -C 1000000 -F 20')
    status = get_status()
    abc('r %s_osavetemp.aig'%f_name)
    return status

def remove(list):
    """Removes outputs in list as well as easy output proved by fast interpolation"""
    zero(list)
    abc('scl')
    fast_int(1)

def zero(list):
    """Zeros out POs in list"""
    for j in list:
        run_command('zeropo -N %d'%j)

def sp():
    """Alias for super_prove"""
    print 'Executing super_prove'
    result = super_prove()
    return result

def super_prove():
    """Main proof technique now. Does original prove and if after speculation there are multiple output left
    if will try to prove each output separately, in reverse order. It will quit at the first output that fails
    to be proved, or any output that is proved SAT"""
    global max_bmc, init_initial_f_name, initial_f_name
    init_initial_f_name = initial_f_name
    if x_factor > 1:
        print 'x_factor = %d'%x_factor
        input_x_factor()
    max_bmc = -1
    x = time.clock()
    result = prove(0)
    k = 1
    print result
    if not result[:3] == 'UND':
        print 'Total time taken by super_prove = %f sec.'%(time.clock() - x)
        return result
    if n_pos() > 1:
        result = prove_g_pos(0)
        print result
        if result == 'UNSAT':
            print 'Total time taken by super_prove = %f sec.'%(time.clock() - x)
            return result
        if result == 'SAT':
            k = 0 #Don't try to prove UNSAT on an abstraction that had SAT
                    # should go back to backup 1 since probably spec was bad.
    y = time.clock()
    result = BMC_VER_result(k)
    print 'Total time taken by last gasp verification = %f sec.'%(time.clock() - y)
    print 'Total time for %s = %f sec.'%(init_initial_f_name,(time.clock() - x))
    return result

def reachm(t):
    run_command('&get;&reach -vcs -T %d;&put'%t)


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()
    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)
    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)
    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)
    return result

def try_split():
    abc('w %s_savetemp.aig'%f_name)
    na = n_ands()
    split(3)
    if n_ands()> 2*na:
        abc('r %s_savetemp.aig'%f_name)
    

def time_diff():
    global last_time
    new_time = time.clock()
    diff = new_time - last_time
    last_time = new_time
    result = 'Lapsed time = %.2f sec.'%diff
    return result
                         
def prove_all_ind():
    """Tries to prove output k by induction, using outputs > k as constraints. Removes proved outputs from POs."""
    abc('w %s_osavetemp.aig'%f_name)
    plist = []
    for j in range(n_pos()):
        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 '%d'%j,
    print '\nOutputs proved inductively = ',
    print plist
    abc('r %s_osavetemp.aig'%f_name)
    remove(plist) #remove the outputs proved
    return status

def split(n):
    abc('orpos;&get')
    abc('&posplit -v -N %d;&put;dc2;trm'%n)

def keep_splitting():
    for j in range(5):
        split(5+j)
        no = n_pos()
        status = prove_g_pos_split(0)
        if status <= Unsat:
            return status
        if no == n_pos():
            return Undecided

def drill(n):
    run_command('&get; &reach -vcs -H 5 -S %d -T 50 -C 40'%n)

def prove_1():
    """Proves all the outputs together. If ever an abstraction was done then if SAT is returned,
        we make RESULT return "undecided".
        """
    a = 1
    global x_factor,xfi,f_name
    x = time.clock()
    max_bmc = -1
    K = 0
    print 'Initial: ',
    print_circuit_stats()
    x_factor = xfi
    print 'x_factor = %f'%x_factor
    print '\nRunning pre_simp'
    set_globals()
    status = pre_simp()
    if status <= Unsat:
        print 'Time for proof = %f sec.'%(time.clock() - x)
        return RESULT[status]
    abc('trm')
    write_file('smp')
    abc('w %s_backup_%d.aig'%(initial_f_name,K))
    K = K +1
    set_globals()
    if ((n_ands() < 30000) and (a == 1) and (n_latches() < 300)):
        print '\nRunning 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'
    nl_b = n_latches()
    status = abstract()
    abc('trm')
    write_file('abs')
    status = process_status(status)
    if ((status <= Unsat)  or  status == Error):
        if  status < Unsat:
            print 'CEX in frame %d'%cex_frame()
            print 'Time for proof = %f sec.'%(time.clock() - x)
            return RESULT[status]
        print 'Time for proof = %f sec.'%(time.clock() - x)
        return RESULT[status]
    abc('w %s_backup_%d.aig'%(initial_f_name,K))
    status = final_verify_recur(2)
    abc('trm')
    write_file('final')
    print 'Time for proof = %f sec.'%(time.clock() - x)
    return RESULT[status]

def qprove():
    global x_factor
    x = time.clock()
    x_factor = 3
    print '\n*********pre_simp**********\n'
    pre_simp()
    print '\n*********absv**********\n'
    result = absv(3,1)
    x_factor = 2
    print '\n*********absv**********\n'
    result = absv(3,1)
    print '\n*********speculate**********\n'
    result = speculate()
    if result <= Unsat:
        return RESULT[result]
    print '\n*********absv**********\n'
    result = absv(3,1)
    print '\n*********prove_pos**********\n'
    result = prove_pos()
    if result == 'UNDECIDED':
        print '\n*********BMC_VER_result**********\n'
        result = BMC_VER_result(1)
    print 'Time for proof = %f sec.'%(time.clock() - x)
    return result