Limiting runtime limit checks in 'pdr'.

Makefile

@@ -23,7 +23,8 @@ MODULES := \
 	src/opt/ret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
 	src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/sfm \
 	src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \
-	src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky src/bool/rsb \
+	src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
+	src/bool/rsb src/bool/rpo \
 	src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \
 	src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \
 	src/proof/abs src/proof/ssc \

abclib.dsp

@@ -3886,6 +3886,10 @@ SOURCE=.\src\bool\rsb\rsbInt.h
 SOURCE=.\src\bool\rsb\rsbMan.c
 # End Source File
 # End Group
+# Begin Group "rpo"
+
+# PROP Default_Filter ""
+# End Group
 # End Group
 # Begin Group "prove"
 

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*************************************************************
 

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 \

src/base/main/mainInit.c

@@ -23,7 +23,7 @@
 
 ABC_NAMESPACE_IMPL_START
 
-//#define USE_ABC2
+#define USE_ABC2
 //#define USE_ABC85
  
 ////////////////////////////////////////////////////////////////////////

src/bool/rpo/literal.h

+/**CFile****************************************************************
+
+  FileName    [literal.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [RPO]
+
+  Synopsis    [Literal structure]
+
+  Author      [Mayler G. A. Martins / Vinicius Callegaro]
+  
+  Affiliation [UFRGS]
+
+  Date        [Ver. 1.0. Started - May 08, 2013.]
+
+  Revision    [$Id: literal.h,v 1.00 2013/05/08 00:00:00 mgamartins Exp $]
+
+ ***********************************************************************/
+
+#ifndef ABC__bool__rpo__literal_h
+#define ABC__bool__rpo__literal_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include "bool/kit/kit.h"
+#include "misc/vec/vec.h"
+#include "misc/util/abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+// associations
+typedef enum {
+    LIT_NONE = 0, // 0: unknown
+    LIT_AND, // 1: AND association
+    LIT_OR, // 2: OR association
+    LIT_XOR // 3: XOR association (not used yet)
+} Operator_t;
+
+
+typedef struct Literal_t_ Literal_t;
+
+struct Literal_t_ {
+    unsigned * transition;
+    unsigned * function;
+    Vec_Str_t * expression;
+};
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the positive transition]
+
+  Description [The inputs are a function, the number of variables and a variable index and the output is a function]
+               
+  SideEffects [Should this function be in kitTruth.c ?]
+
+  SeeAlso     []
+//
+***********************************************************************/
+
+static inline void Lit_TruthPositiveTransition( unsigned * pIn, unsigned * pOut, int nVars, int varIdx )
+{
+    unsigned * cof0 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) );
+    unsigned * cof1 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) );
+    unsigned * ncof0;
+    Kit_TruthCofactor0New(cof0, pIn,nVars,varIdx);
+    Kit_TruthCofactor1New(cof1, pIn,nVars,varIdx);
+    ncof0 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) );
+    Kit_TruthNot(ncof0,cof0,nVars);
+    Kit_TruthAnd(pOut,ncof0,cof1, nVars);
+    ABC_FREE(cof0);
+    ABC_FREE(ncof0);
+    ABC_FREE(cof1);
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the negative transition]
+
+  Description [The inputs are a function, the number of variables and a variable index and the output is a function]
+               
+  SideEffects [Should this function be in kitTruth.c ?]
+
+  SeeAlso     []
+
+***********************************************************************/
+
+static inline void Lit_TruthNegativeTransition( unsigned * pIn, unsigned * pOut, int nVars, int varIdx )
+{
+    unsigned * cof0 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) );
+    unsigned * cof1 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) );
+    unsigned * ncof1;
+    Kit_TruthCofactor0New(cof0, pIn,nVars,varIdx);
+    Kit_TruthCofactor1New(cof1, pIn,nVars,varIdx);
+    ncof1 = ABC_ALLOC (unsigned, Kit_TruthWordNum(nVars) );
+    Kit_TruthNot(ncof1,cof1,nVars);
+    Kit_TruthAnd(pOut,ncof1,cof0,nVars);
+    ABC_FREE(cof0);
+    ABC_FREE(cof1);
+    ABC_FREE(ncof1);
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Create a literal given a polarity ]
+
+  Description [The inputs are the function, index and its polarity and a the output is a literal]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+
+static inline Literal_t* Lit_Alloc(unsigned* pTruth, int nVars, int varIdx, char pol) {
+    unsigned * transition;
+    unsigned * function;
+    Vec_Str_t * exp;
+    Literal_t* lit;
+    assert(pol == '+' || pol == '-');
+    transition = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
+    if (pol == '+') {
+        Lit_TruthPositiveTransition(pTruth, transition, nVars, varIdx);
+    } else {
+        Lit_TruthNegativeTransition(pTruth, transition, nVars, varIdx);
+    }
+    if (!Kit_TruthIsConst0(transition,nVars)) {
+        function = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
+        Kit_TruthIthVar(function, nVars, varIdx);
+        //Abc_Print(-2, "Allocating function %X %d %c \n", *function, varIdx, pol);
+        exp = Vec_StrAlloc(5);
+        if (pol == '-') {
+            Kit_TruthNot(function, function, nVars);
+            Vec_StrPutC(exp, '!');
+        }
+        Vec_StrPutC(exp, (char)('a' + varIdx));
+        Vec_StrPutC(exp, '\0');
+        lit = ABC_ALLOC(Literal_t, 1);
+        lit->function = function;
+        lit->transition = transition;
+        lit->expression = exp;
+        return lit;
+    } else {
+        ABC_FREE(transition); // free the function.
+        return NULL;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Group 2 literals using AND or OR]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+
+static inline Literal_t* Lit_GroupLiterals(Literal_t* lit1, Literal_t* lit2, Operator_t op, int nVars) {
+    unsigned * newFunction = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
+    unsigned * newTransition = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
+    Vec_Str_t * newExp = Vec_StrAlloc(lit1->expression->nSize + lit2->expression->nSize + 3);
+    Literal_t* newLiteral;
+    char opChar = '%';
+    switch (op) {
+        case LIT_AND:
+        {
+            //Abc_Print(-2, "Grouping AND %X %X \n", *lit1->function, *lit2->function);
+            Kit_TruthAnd(newFunction, lit1->function, lit2->function, nVars);
+            opChar = '*';
+            break;
+        }
+        case LIT_OR:
+        {
+            //Abc_Print(-2, "Grouping OR %X %X \n", *lit1->function, *lit2->function);
+            Kit_TruthOr(newFunction, lit1->function, lit2->function, nVars);
+            opChar = '+';
+            break;
+        }
+        default:
+        {
+            Abc_Print(-2, "Lit_GroupLiterals with op not defined.");
+            //TODO Call ABC Abort
+        }
+    }
+
+    Kit_TruthOr(newTransition, lit1->transition, lit2->transition, nVars);
+    // create a new expression.
+    Vec_StrPutC(newExp, '(');
+    Vec_StrAppend(newExp, lit1->expression->pArray);
+    //Vec_StrPop(newExp); // pop the \0
+    Vec_StrPutC(newExp, opChar);
+    Vec_StrAppend(newExp, lit2->expression->pArray);
+    //Vec_StrPop(newExp); // pop the \0
+    Vec_StrPutC(newExp, ')');
+    Vec_StrPutC(newExp, '\0');
+
+    newLiteral = ABC_ALLOC(Literal_t, 1);
+    newLiteral->function = newFunction;
+    newLiteral->transition = newTransition;
+    newLiteral->expression = newExp;
+    return newLiteral;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Create a const literal ]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+
+static inline Literal_t* Lit_CreateLiteralConst(unsigned* pTruth, int nVars, int constant) {
+    Vec_Str_t * exp = Vec_StrAlloc(3);
+    Literal_t* lit;
+    Vec_StrPutC(exp, (char)('0' + constant));
+    Vec_StrPutC(exp, '\0');
+    lit = ABC_ALLOC(Literal_t, 1);
+    lit->expression = exp;
+    lit->function = pTruth;
+    lit->transition = pTruth; // wrong but no effect ###
+    return lit;
+}
+
+static inline Literal_t* Lit_Copy(Literal_t* lit, int nVars) {
+    Literal_t* newLit = ABC_ALLOC(Literal_t,1);
+    newLit->function = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
+    Kit_TruthCopy(newLit->function,lit->function,nVars);
+    newLit->transition = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
+    Kit_TruthCopy(newLit->transition,lit->transition,nVars);
+    newLit->expression = Vec_StrDup(lit->expression);
+//    Abc_Print(-2,"Copying: %s\n",newLit->expression->pArray); 
+    return newLit;
+}
+
+static inline void Lit_PrintTT(unsigned* tt, int nVars) {
+    int w;
+    for(w=nVars-1; w>=0; w--) {
+            Abc_Print(-2, "%08X", tt[w]);
+    }
+}
+
+static inline void Lit_PrintExp(Literal_t* lit) {
+    Abc_Print(-2, "%s", lit->expression->pArray);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delete the literal ]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+ ***********************************************************************/
+
+static inline void Lit_Free(Literal_t * lit) {
+    if(lit == NULL) {
+        return;
+    }
+//    Abc_Print(-2,"Freeing: %s\n",lit->expression->pArray); 
+    ABC_FREE(lit->function);
+    ABC_FREE(lit->transition);
+    Vec_StrFree(lit->expression);
+    ABC_FREE(lit);
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif    /* LITERAL_H */
+

src/bool/rpo/module.make

+SRC +=    src/bool/rpo/rpo.c
\ No newline at end of file

src/bool/rpo/rpo.h

+/**CFile****************************************************************
+
+  FileName    [rpo.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [RPO]
+
+  Synopsis    [Rpo Header]
+
+  Author      [Mayler G. A. Martins / Vinicius Callegaro]
+  
+  Affiliation [UFRGS]
+
+  Date        [Ver. 1.0. Started - May 08, 2013.]
+
+  Revision    [$Id: rpo.h,v 1.00 2013/05/08 00:00:00 mgamartins Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__bool__rpo__rpo_h
+#define ABC__bool__rpo__rpo_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "literal.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Rpo_LCI_Edge_t_ Rpo_LCI_Edge_t;
+
+struct Rpo_LCI_Edge_t_ {
+    unsigned long visited : 1;
+    unsigned long connectionType : 2;
+    unsigned long reserved : 1;
+    unsigned long idx1 : 30;
+    unsigned long idx2 : 30;
+};
+
+void Rpo_PrintEdge(Rpo_LCI_Edge_t* edge);
+int Rpo_CheckANDGroup(Literal_t* lit1, Literal_t* lit2, int nVars);
+int Rpo_CheckORGroup(Literal_t* lit1, Literal_t* lit2, int nVars);
+Literal_t* Rpo_Factorize(unsigned* target, int nVars, int nThreshold, int verbose);
+Literal_t* Rpo_Recursion(unsigned* target, Literal_t** vecLit, int nLit, int nLitCount, int nVars, int* thresholdCount, int thresholdMax, int verbose);
+Rpo_LCI_Edge_t* Rpo_CreateEdge(Operator_t op, int i, int j, int* vertexDegree);
+int Rpo_computeMinEdgeCost(Rpo_LCI_Edge_t** edges, int edgeCount, int* vertexDegree);
+
+ABC_NAMESPACE_HEADER_END
+        
+#endif
+  
\ No newline at end of file