Limiting runtime limit checks in 'pdr'.

4 files changed, 522 insertions, 1 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ef973099..063388f7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -53,6 +53,7 @@
 #include "sat/bmc/bmc.h"
 #include "proof/ssc/ssc.h"
 #include "opt/sfm/sfm.h"
+#include "bool/rpo/rpo.h"
 
 #ifndef _WIN32
 #include <unistd.h>
@@ -113,6 +114,7 @@ static int Abc_CommandAddBuffs               ( Abc_Frame_t * pAbc, int argc, cha
 //static int Abc_CommandMerge                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestDec                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestNpn                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTestRPO                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandRewrite                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRefactor               ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -663,6 +665,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "Synthesis",    "merge",         Abc_CommandMerge,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "testdec",       Abc_CommandTestDec,          0 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "testnpn",       Abc_CommandTestNpn,          0 );
+    Cmd_CommandAdd( pAbc, "LogiCS",       "testrpo",       Abc_CommandTestRPO,          0 );
 
     Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
@@ -5323,6 +5326,81 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandTestRPO(Abc_Frame_t * pAbc, int argc, char ** argv) {
+    extern int Abc_RpoTest(char * pFileName, int nVarNum, int nThreshold, int fVerbose);
+    char * pFileName;
+    int c;
+    int nVarNum = -1;
+    int fVerbose = 0;
+    int nThreshold = -1;
+    Extra_UtilGetoptReset();
+    while ((c = Extra_UtilGetopt(argc, argv, "TNvh")) != EOF) {
+        switch (c) {
+            case 'N':
+                if (globalUtilOptind >= argc) {
+                    Abc_Print(-1, "Command line switch \"-N\" should be followed by an integer.\n");
+                    goto usage;
+                }
+                nVarNum = atoi(argv[globalUtilOptind]);
+                globalUtilOptind++;
+                if (nVarNum < 0)
+                    goto usage;
+                break;
+            case 'T':
+                if (globalUtilOptind >= argc) {
+                    Abc_Print(-1, "Command line switch \"-T\" should be followed by an integer.\n");
+                    goto usage;
+                }
+                nThreshold = atoi(argv[globalUtilOptind]);
+                globalUtilOptind++;
+                if (nThreshold < 0)
+                    goto usage;
+                break;
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if (argc != globalUtilOptind + 1) 
+    {
+        Abc_Print(1, "Input file is not given.\n");
+        goto usage;
+    }
+    // get the output file name
+    pFileName = argv[globalUtilOptind];
+    // call the testbench
+    Abc_RpoTest( pFileName, nVarNum, nThreshold, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print(-2, "usage: testrpo [-NT <num>] [-vh] <file>\n");
+    Abc_Print(-2, "\t           RPO algorithm developed and implemented by Mayler G. A. Martins,\n");
+    Abc_Print(-2, "\t           Vinicius Callegaro, Renato P. Ribas and Andre' I. Reis\n");
+    Abc_Print(-2, "\t           at Federal University of Rio Grande do Sul, Porto Alegre, Brazil\n");
+    Abc_Print(-2, "\t-N <num> : the number of support variables (binary files only) [default = unused]\n");
+    Abc_Print(-2, "\t-T <num> : the number of recursions accepted before abort [default = INFINITE]\n");
+    Abc_Print(-2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no");
+    Abc_Print(-2, "\t-h       : print the command usage\n");
+    Abc_Print(-2, "\t<file>   : a text file with truth tables in hexadecimal, listed one per line,\n");
+    Abc_Print(-2, "\t           or a binary file with an array of truth tables (in this case,\n");
+    Abc_Print(-2, "\t           -N <num> is required to determine how many functions are stored)\n");
+    return 1;
+}
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcRpo.c b/src/base/abci/abcRpo.c
new file mode 100644
index 00000000..286ef80b
--- /dev/null
+++ b/src/base/abci/abcRpo.c
@@ -0,0 +1,442 @@
+/**CFile****************************************************************
+
+  FileName    [abcRpo.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Rpo package.]
+
+  Synopsis    [Procedures for executing RPO.]
+
+  Author      [Mayler G. A. Martins / Vinicius Callegaro]
+  
+  Affiliation [UFRGS]
+
+  Date        [Ver. 1.0. Started - May 08, 2013.]
+
+  Revision    [$Id: abcRpo.c,v 1.00 2013/05/08 00:00:00 mgamartins Exp $]
+
+ ***********************************************************************/
+
+#include "misc/extra/extra.h"
+
+#include "bool/rpo/rpo.h"
+#include "bool/rpo/literal.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+// data-structure to store a bunch of truth tables
+typedef struct Rpo_TtStore_t_ Rpo_TtStore_t;
+
+struct Rpo_TtStore_t_ {
+    int nVars;
+    int nWords;
+    int nFuncs;
+    word ** pFuncs;
+};
+
+
+// read/write/flip i-th bit of a bit string table:
+
+static inline int Abc_TruthGetBit(word * p, int i) {
+    return (int) (p[i >> 6] >> (i & 63)) & 1;
+}
+
+static inline void Abc_TruthSetBit(word * p, int i) {
+    p[i >> 6] |= (((word) 1) << (i & 63));
+}
+
+static inline void Abc_TruthXorBit(word * p, int i) {
+    p[i >> 6] ^= (((word) 1) << (i & 63));
+}
+
+// read/write k-th digit d of a hexadecimal number:
+
+static inline int Abc_TruthGetHex(word * p, int k) {
+    return (int) (p[k >> 4] >> ((k << 2) & 63)) & 15;
+}
+
+static inline void Abc_TruthSetHex(word * p, int k, int d) {
+    p[k >> 4] |= (((word) d) << ((k << 2) & 63));
+}
+
+static inline void Abc_TruthXorHex(word * p, int k, int d) {
+    p[k >> 4] ^= (((word) d) << ((k << 2) & 63));
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+// read one hex character
+
+static inline int Abc_TruthReadHexDigit(char HexChar) {
+    if (HexChar >= '0' && HexChar <= '9')
+        return HexChar - '0';
+    if (HexChar >= 'A' && HexChar <= 'F')
+        return HexChar - 'A' + 10;
+    if (HexChar >= 'a' && HexChar <= 'f')
+        return HexChar - 'a' + 10;
+    assert(0); // not a hexadecimal symbol
+    return -1; // return value which makes no sense
+}
+
+// write one hex character
+
+static inline void Abc_TruthWriteHexDigit(FILE * pFile, int HexDigit) {
+    assert(HexDigit >= 0 && HexDigit < 16);
+    if (HexDigit < 10)
+        fprintf(pFile, "%d", HexDigit);
+    else
+        fprintf(pFile, "%c", 'A' + HexDigit - 10);
+}
+
+// read one truth table in hexadecimal
+
+static void Abc_TruthReadHex(word * pTruth, char * pString, int nVars) {
+    int nWords = (nVars < 7) ? 1 : (1 << (nVars - 6));
+    int k, Digit, nDigits = (nWords << 4);
+    char EndSymbol;
+    // skip the first 2 symbols if they are "0x"
+    if (pString[0] == '0' && pString[1] == 'x')
+        pString += 2;
+    // get the last symbol
+    EndSymbol = pString[nDigits];
+    // the end symbol of the TT (the one immediately following hex digits)
+    // should be one of the following: space, a new-line, or a zero-terminator
+    // (note that on Windows symbols '\r' can be inserted before each '\n')
+    assert(EndSymbol == ' ' || EndSymbol == '\n' || EndSymbol == '\r' || EndSymbol == '\0');
+    // read hexadecimal digits in the reverse order
+    // (the last symbol in the string is the least significant digit)
+    for (k = 0; k < nDigits; k++) {
+        Digit = Abc_TruthReadHexDigit(pString[nDigits - 1 - k]);
+        assert(Digit >= 0 && Digit < 16);
+        Abc_TruthSetHex(pTruth, k, Digit);
+    }
+}
+
+// write one truth table in hexadecimal (do not add end-of-line!)
+
+static void Abc_TruthWriteHex(FILE * pFile, word * pTruth, int nVars) {
+    int nDigits, Digit, k;
+    nDigits = (1 << (nVars - 2));
+    for (k = 0; k < nDigits; k++) {
+        Digit = Abc_TruthGetHex(pTruth, k);
+        assert(Digit >= 0 && Digit < 16);
+        Abc_TruthWriteHexDigit(pFile, Digit);
+    }
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate/Deallocate storage for truth tables..]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+static Rpo_TtStore_t * Abc_TruthStoreAlloc(int nVars, int nFuncs) {
+    Rpo_TtStore_t * p;
+    int i;
+    p = (Rpo_TtStore_t *) malloc(sizeof (Rpo_TtStore_t));
+    p->nVars = nVars;
+    p->nWords = (nVars < 7) ? 1 : (1 << (nVars - 6));
+    p->nFuncs = nFuncs;
+    // alloc storage for 'nFuncs' truth tables as one chunk of memory
+    p->pFuncs = (word **) malloc((sizeof (word *) + sizeof (word) * p->nWords) * p->nFuncs);
+    // assign and clean the truth table storage
+    p->pFuncs[0] = (word *) (p->pFuncs + p->nFuncs);
+    memset(p->pFuncs[0], 0, sizeof (word) * p->nWords * p->nFuncs);
+    // split it up into individual truth tables
+    for (i = 1; i < p->nFuncs; i++)
+        p->pFuncs[i] = p->pFuncs[i - 1] + p->nWords;
+    return p;
+}
+
+static Rpo_TtStore_t * Abc_TruthStoreAlloc2(int nVars, int nFuncs, word * pBuffer) {
+    Rpo_TtStore_t * p;
+    int i;
+    p = (Rpo_TtStore_t *) malloc(sizeof (Rpo_TtStore_t));
+    p->nVars = nVars;
+    p->nWords = (nVars < 7) ? 1 : (1 << (nVars - 6));
+    p->nFuncs = nFuncs;
+    // alloc storage for 'nFuncs' truth tables as one chunk of memory
+    p->pFuncs = (word **) malloc(sizeof (word *) * p->nFuncs);
+    // assign and clean the truth table storage
+    p->pFuncs[0] = pBuffer;
+    // split it up into individual truth tables
+    for (i = 1; i < p->nFuncs; i++)
+        p->pFuncs[i] = p->pFuncs[i - 1] + p->nWords;
+    return p;
+}
+
+static void Abc_TtStoreFree(Rpo_TtStore_t * p, int nVarNum) {
+    if (nVarNum >= 0)
+        ABC_FREE(p->pFuncs[0]);
+    ABC_FREE(p->pFuncs);
+    ABC_FREE(p);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read file contents.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+extern int Abc_FileSize(char * pFileName);
+
+/**Function*************************************************************
+
+  Synopsis    [Read file contents.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+extern char * Abc_FileRead(char * pFileName);
+
+/**Function*************************************************************
+
+  Synopsis    [Determine the number of variables by reading the first line.]
+
+  Description [Determine the number of functions by counting the lines.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+extern void Abc_TruthGetParams(char * pFileName, int * pnVars, int * pnTruths);
+
+
+/**Function*************************************************************
+
+  Synopsis    [Read truth tables from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+static void Abc_TruthStoreRead(char * pFileName, Rpo_TtStore_t * p) {
+    char * pContents;
+    int i, nLines;
+    pContents = Abc_FileRead(pFileName);
+    if (pContents == NULL)
+        return;
+    // here it is assumed (without checking!) that each line of the file 
+    // begins with a string of hexadecimal chars followed by space
+
+    // the file will be read till the first empty line (pContents[i] == '\n')
+    // (note that Abc_FileRead() added several empty lines at the end of the file contents)
+    for (nLines = i = 0; pContents[i] != '\n';) {
+        // read one line
+        Abc_TruthReadHex(p->pFuncs[nLines++], &pContents[i], p->nVars);
+        // skip till after the end-of-line symbol
+        // (note that end-of-line symbol is also skipped)
+        while (pContents[i++] != '\n');
+    }
+    // adjust the number of functions read 
+    // (we may have allocated more storage because some lines in the file were empty)
+    assert(p->nFuncs >= nLines);
+    p->nFuncs = nLines;
+    ABC_FREE(pContents);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Write truth tables into file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+static void Abc_TtStoreWrite(char * pFileName, Rpo_TtStore_t * p, int fBinary) {
+    FILE * pFile;
+    int i, nBytes = 8 * Abc_Truth6WordNum(p->nVars);
+    pFile = fopen(pFileName, "wb");
+    if (pFile == NULL) {
+        printf("Cannot open file \"%s\" for writing.\n", pFileName);
+        return;
+    }
+    for (i = 0; i < p->nFuncs; i++) {
+        if (fBinary)
+            fwrite(p->pFuncs[i], nBytes, 1, pFile);
+        else
+            Abc_TruthWriteHex(pFile, p->pFuncs[i], p->nVars), fprintf(pFile, "\n");
+    }
+    fclose(pFile);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read truth tables from input file and write them into output file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+static Rpo_TtStore_t * Abc_TtStoreLoad(char * pFileName, int nVarNum) {
+    Rpo_TtStore_t * p;
+    if (nVarNum < 0) {
+        int nVars, nTruths;
+        // figure out how many truth table and how many variables
+        Abc_TruthGetParams(pFileName, &nVars, &nTruths);
+        if (nVars < 2 || nVars > 16 || nTruths == 0)
+            return NULL;
+        // allocate data-structure
+        p = Abc_TruthStoreAlloc(nVars, nTruths);
+        // read info from file
+        Abc_TruthStoreRead(pFileName, p);
+    } else {
+        char * pBuffer;
+        int nFileSize = Abc_FileSize(pFileName);
+        int nBytes = (1 << (nVarNum - 3)); // why mishchencko put -3? ###
+        int nTruths = nFileSize / nBytes;
+        //Abc_Print(-2,"nFileSize=%d,nTruths=%d\n",nFileSize, nTruths);
+        if (nFileSize == -1)
+            return NULL;
+        assert(nVarNum >= 6);
+        if (nFileSize % nBytes != 0)
+            Abc_Print(0, "The file size (%d) is divided by the truth table size (%d) with remainder (%d).\n",
+                nFileSize, nBytes, nFileSize % nBytes);
+        // read file contents
+        pBuffer = Abc_FileRead(pFileName);
+        // allocate data-structure
+        p = Abc_TruthStoreAlloc2(nVarNum, nTruths, (word *) pBuffer);
+    }
+    return p;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Apply decomposition to the truth table.]
+
+  Description [Returns the number of AIG nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+void Abc_TruthRpoPerform(Rpo_TtStore_t * p, int nThreshold, int fVerbose) {
+    clock_t clk = clock();
+    int i;
+    int rpoCount = 0;
+    Literal_t* lit;
+    float percent;
+    for (i = 0; i < p->nFuncs; i++) {
+//        if(i>1000) {
+//            continue;
+//        }
+////        
+//        if(i!= 2196 ) { //5886
+//            continue;
+//        }
+        if(fVerbose) {
+            Abc_Print(-2,"%d: ", i+1);
+        }
+            
+        lit = Rpo_Factorize((unsigned *) p->pFuncs[i], p->nVars, nThreshold, fVerbose);
+        if (lit != NULL) {
+            if(fVerbose) {
+                Abc_Print(-2, "Solution : %s\n", lit->expression->pArray);
+                Abc_Print(-2, "\n\n");
+            }
+            Lit_Free(lit);
+            rpoCount++;
+        } else {
+            if(fVerbose) {
+                Abc_Print(-2, "null\n");
+                Abc_Print(-2, "\n\n");
+            }
+        }
+    }
+    percent = (rpoCount * 100.0) / p->nFuncs;
+    Abc_Print(-2,"%d of %d (%.2f %%) functions are RPO.\n", rpoCount,p->nFuncs,percent);
+    Abc_PrintTime(1, "Time", clock() - clk);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Apply decomposition to truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+void Abc_TruthRpoTest(char * pFileName, int nVarNum, int nThreshold, int fVerbose) {
+    Rpo_TtStore_t * p;
+
+    // allocate data-structure
+//    if (fVerbose) {
+//        Abc_Print(-2, "Number of variables = %d\n", nVarNum);
+//    }
+    p = Abc_TtStoreLoad(pFileName, nVarNum);
+
+    if (fVerbose) {
+        Abc_Print(-2, "Number of variables = %d\n", p->nVars);
+    }
+    // consider functions from the file
+    Abc_TruthRpoPerform(p, nThreshold, fVerbose);
+
+    // delete data-structure
+    Abc_TtStoreFree(p, nVarNum);
+    //    printf( "Finished decomposing truth tables from file \"%s\".\n", pFileName );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testbench for decomposition algorithms.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+int Abc_RpoTest(char * pFileName, int nVarNum,int nThreshold, int fVerbose) {
+    if (fVerbose) {
+        printf("Using truth tables from file \"%s\"...\n", pFileName);
+    }
+    Abc_TruthRpoTest(pFileName, nVarNum, nThreshold, fVerbose);
+    fflush(stdout);
+    return 0;
+}
+
+
+/////////////////////ert truth table to ///////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index c7645775..5554ea93 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -55,6 +55,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcRestruct.c \
     src/base/abci/abcResub.c \
     src/base/abci/abcRewrite.c \
+    src/base/abci/abcRpo.c \
     src/base/abci/abcRr.c \
     src/base/abci/abcSat.c \
     src/base/abci/abcScorr.c \
diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c
index bbe0bbd1..bdf0613e 100644
--- a/src/base/main/mainInit.c
+++ b/src/base/main/mainInit.c
@@ -23,7 +23,7 @@
 
 ABC_NAMESPACE_IMPL_START
 
-//#define USE_ABC2
+#define USE_ABC2
 //#define USE_ABC85
  
 ////////////////////////////////////////////////////////////////////////