summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2006-09-20 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2006-09-20 08:01:00 -0700
commit0da555cb481696efd78d9c5dc6293b6a95d1ffd5 (patch)
treebac6826fd2c8650225f237ca524b8b0276c9c224 /src
parent370578bf1c4504b65f49ab63fcf7ed9c88a15d69 (diff)
downloadabc-0da555cb481696efd78d9c5dc6293b6a95d1ffd5.tar.gz
abc-0da555cb481696efd78d9c5dc6293b6a95d1ffd5.tar.bz2
abc-0da555cb481696efd78d9c5dc6293b6a95d1ffd5.zip
Version abc60920
Diffstat (limited to 'src')
-rw-r--r--src/base/abc/abc.h2
-rw-r--r--src/base/abci/abc.c189
-rw-r--r--src/base/abci/abcIvy.c61
-rw-r--r--src/base/abci/abcStrash.c13
-rw-r--r--src/sat/asat/solver.c7
-rw-r--r--src/sat/asat/solver.h2
-rw-r--r--src/sat/fraig/fraigSat.c14
-rw-r--r--src/temp/ivy/ivy.h15
-rw-r--r--src/temp/ivy/ivyFraig.c1209
-rw-r--r--src/temp/ivy/satMem.c527
-rw-r--r--src/temp/ivy/satMem.h78
-rw-r--r--src/temp/ivy/satSolver.c93
-rw-r--r--src/temp/ivy/satSolver.h15
13 files changed, 1998 insertions, 227 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index c4dbb52f..b619e8b9 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -601,8 +601,8 @@ extern Abc_Obj_t * Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox,
extern Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode );
extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t * Abc_NtkFindTerm( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName );
+extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk );
extern Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b0ccae3a..2427146c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -97,7 +97,9 @@ static int Abc_CommandICut ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -224,7 +226,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "New AIG", "irw", Abc_CommandIRewrite, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "irws", Abc_CommandIRewriteSeq, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "iresyn", Abc_CommandIResyn, 1 );
+ Cmd_CommandAdd( pAbc, "New AIG", "isat", Abc_CommandISat, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "ifraig", Abc_CommandIFraig, 1 );
+ Cmd_CommandAdd( pAbc, "New AIG", "iprove", Abc_CommandIProve, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 );
@@ -3354,7 +3358,8 @@ int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
Abc_NtkDelete( pNtk2 );
-
+ // sweep dangling logic
+ Abc_AigCleanup( pNtk->pManFunc );
// replace the current network
// Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
@@ -5441,26 +5446,126 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandISat( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c, fUpdateLevel, fVerbose;
+ int nConfLimit;
+
+ extern Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nConfLimit = 100000;
+ fUpdateLevel = 1;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Clzvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfLimit < 0 )
+ goto usage;
+ break;
+ case 'l':
+ fUpdateLevel ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkIsSeq(pNtk) )
+ {
+ fprintf( pErr, "Only works for non-sequential networks.\n" );
+ return 1;
+ }
+
+ pNtkRes = Abc_NtkIvySat( pNtk, nConfLimit, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Command has failed.\n" );
+ return 0;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: isat [-C num] [-vh]\n" );
+ fprintf( pErr, "\t tries to prove the miter constant 0\n" );
+ fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+// fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c, fUpdateLevel, fVerbose;
+ int nConfLimit;
- extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk );
+ extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
+ nConfLimit = 100;
fUpdateLevel = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "lzvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Clzvh" ) ) != EOF )
{
switch ( c )
{
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfLimit < 0 )
+ goto usage;
+ break;
case 'l':
fUpdateLevel ^= 1;
break;
@@ -5484,7 +5589,7 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- pNtkRes = Abc_NtkIvyFraig( pNtk );
+ pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -5495,8 +5600,82 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: ifraig [-h]\n" );
+ fprintf( pErr, "usage: ifraig [-C num] [-vh]\n" );
fprintf( pErr, "\t performs fraiging using a new method\n" );
+ fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+// fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c, fUpdateLevel, fVerbose;
+
+ extern Abc_Ntk_t * Abc_NtkIvyProve( Abc_Ntk_t * pNtk );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fUpdateLevel = 1;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "lzvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'l':
+ fUpdateLevel ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkIsSeq(pNtk) )
+ {
+ fprintf( pErr, "Only works for non-sequential networks.\n" );
+ return 1;
+ }
+
+ pNtkRes = Abc_NtkIvyProve( pNtk );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Command has failed.\n" );
+ return 0;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: iprove [-h]\n" );
+ fprintf( pErr, "\t performs CEC using a new method\n" );
// fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
// fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 3a5333f4..320c76dd 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -338,7 +338,7 @@ Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
{
Ivy_FraigParams_t Params, * pParams = &Params;
Abc_Ntk_t * pNtkAig;
@@ -347,6 +347,38 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk )
if ( pMan == NULL )
return NULL;
Ivy_FraigParamsDefault( pParams );
+ pParams->nBTLimitMiter = nConfLimit;
+ pParams->fVerbose = fVerbose;
+// pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
+ pMan = Ivy_FraigMiter( pTemp = pMan, pParams );
+ Ivy_ManStop( pTemp );
+ pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
+ Ivy_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
+{
+ Ivy_FraigParams_t Params, * pParams = &Params;
+ Abc_Ntk_t * pNtkAig;
+ Ivy_Man_t * pMan, * pTemp;
+ pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
+ if ( pMan == NULL )
+ return NULL;
+ Ivy_FraigParamsDefault( pParams );
+ pParams->nBTLimitNode = nConfLimit;
+ pParams->fVerbose = fVerbose;
pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
Ivy_ManStop( pTemp );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
@@ -365,6 +397,33 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
+Abc_Ntk_t * Abc_NtkIvyProve( Abc_Ntk_t * pNtk )
+{
+ Ivy_FraigParams_t Params, * pParams = &Params;
+ Abc_Ntk_t * pNtkAig;
+ Ivy_Man_t * pMan, * pTemp;
+ pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
+ if ( pMan == NULL )
+ return NULL;
+ Ivy_FraigParamsDefault( pParams );
+ pMan = Ivy_FraigProve( pTemp = pMan, pParams );
+ Ivy_ManStop( pTemp );
+ pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
+ Ivy_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
{
// Abc_Ntk_t * pNtkAig;
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index a130c11f..e8dc9793 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -135,9 +135,8 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
Synopsis [Appends the second network to the first.]
Description [Modifies the first network by adding the logic of the second.
- Performs structural hashing while appending the networks. Does not add
- the COs of the second. Does not change the second network. Returns 0
- if the appending failed, 1 otherise.]
+ Performs structural hashing while appending the networks. Does not change
+ the second network. Returns 0 if the appending failed, 1 otherise.]
SideEffects []
@@ -159,11 +158,15 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
// check that the networks have the same PIs
// reorder PIs of pNtk2 according to pNtk1
if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1, 1 ) )
- return 0;
+ printf( "Abc_NtkAppend(): The union of the network PIs is computed (warning).\n" );
// perform strashing
Abc_NtkCleanCopy( pNtk2 );
Abc_NtkForEachCi( pNtk2, pObj, i )
- pObj->pCopy = Abc_NtkCi(pNtk1, i);
+ {
+ pObj->pCopy = Abc_NtkFindCi(pNtk1, Abc_ObjName(pObj));
+ if ( pObj->pCopy == NULL )
+ pObj->pCopy = Abc_NtkDupObj(pNtk1, pObj, 1);
+ }
// add pNtk2 to pNtk1 while strashing
if ( Abc_NtkIsLogic(pNtk2) )
Abc_NtkStrashPerform( pNtk2, pNtk1, 1 );
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index 34b4d233..6f8fe037 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -853,9 +853,16 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
// reset the activities
if ( s->factors )
+ {
+ s->var_inc = 1.0;
for ( i = 0; i < s->size; i++ )
+ {
s->activity[i] = (double)s->factors[i];
+// if ( s->orderpos[i] != -1 )
+// order_update(s, i );
+ }
// s->activity[i] = 1.0;
+ }
for (;;){
clause* confl = solver_propagate(s);
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index 7a5e5be6..bd6e8569 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -76,7 +76,7 @@ extern void solver_delete(solver* s);
extern bool solver_addclause(solver* s, lit* begin, lit* end);
extern bool solver_simplify(solver* s);
-extern int solver_solve(solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit );
+extern int solver_solve(solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit);
extern int * solver_get_model( solver * p, int * pVars, int nVars );
extern int solver_nvars(solver* s);
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index af0f13ce..53057fc3 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -300,6 +300,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
{
int RetValue, RetValue1, i, fComp, clk;
int fVerbose = 0;
+ int fSwitch = 0;
// make sure the nodes are not complemented
assert( !Fraig_IsComplement(pNew) );
@@ -318,6 +319,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
if ( nBTLimit <= 10 )
return 0;
nBTLimit = (int)sqrt(nBTLimit);
+// fSwitch = 1;
}
p->nSatCalls++;
@@ -417,6 +419,8 @@ PRT( "time", clock() - clk );
// if ( pOld->fFailTfo || pNew->fFailTfo )
// printf( "*" );
// printf( "s(%d)", pNew->Level );
+ if ( fSwitch )
+ printf( "s(%d)", pNew->Level );
p->nSatCounter++;
return 0;
}
@@ -433,6 +437,8 @@ p->time3 += clock() - clk;
pOld->fFailTfo = 1;
pNew->fFailTfo = 1;
// p->nSatFails++;
+ if ( fSwitch )
+ printf( "T(%d)", pNew->Level );
p->nSatFailsReal++;
return 0;
}
@@ -491,6 +497,8 @@ PRT( "time", clock() - clk );
// if ( pOld->fFailTfo || pNew->fFailTfo )
// printf( "*" );
// printf( "s(%d)", pNew->Level );
+ if ( fSwitch )
+ printf( "s(%d)", pNew->Level );
return 0;
}
else // if ( RetValue1 == MSAT_UNKNOWN )
@@ -500,6 +508,8 @@ p->time3 += clock() - clk;
// if ( pOld->fFailTfo || pNew->fFailTfo )
// printf( "*" );
// printf( "T(%d)", pNew->Level );
+ if ( fSwitch )
+ printf( "T(%d)", pNew->Level );
// mark the node as the failed node
pOld->fFailTfo = 1;
@@ -515,6 +525,10 @@ p->time3 += clock() - clk;
// if ( pOld->fFailTfo || pNew->fFailTfo )
// printf( "*" );
// printf( "u(%d)", pNew->Level );
+
+ if ( fSwitch )
+ printf( "u(%d)", pNew->Level );
+
return 1;
}
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index 5b684244..d9c17d80 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -128,8 +128,17 @@ struct Ivy_Man_t_
struct Ivy_FraigParams_t_
{
- int nSimWords; // the number of words in the simulation info
- double SimSatur; // the ratio of refined classes when saturation is reached
+ int nSimWords; // the number of words in the simulation info
+ double SimSatur; // the ratio of refined classes when saturation is reached
+ int fPatScores; // enables simulation pattern scoring
+ int MaxScore; // max score after which resimulation is used
+ int fVerbose; // verbose output
+ int nBTLimitNode; // conflict limit at a node
+ int nBTLimitMiter; // conflict limit at an output
+ int nBTLimitGlobal; // conflict limit global
+ int nInsLimitNode; // inspection limit at a node
+ int nInsLimitMiter; // inspection limit at an output
+ int nInsLimitGlobal; // inspection limit global
};
@@ -441,7 +450,9 @@ extern void Ivy_FastMapStop( Ivy_Man_t * pAig );
extern void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves );
extern void Ivy_FastMapReverseLevel( Ivy_Man_t * pAig );
/*=== ivyFraig.c ==========================================================*/
+extern Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
extern Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+extern Ivy_Man_t * Ivy_FraigProve( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
extern void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams );
/*=== ivyHaig.c ==========================================================*/
extern void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose );
diff --git a/src/temp/ivy/ivyFraig.c b/src/temp/ivy/ivyFraig.c
index a3a3b33a..88c726c7 100644
--- a/src/temp/ivy/ivyFraig.c
+++ b/src/temp/ivy/ivyFraig.c
@@ -20,13 +20,33 @@
#include "ivy.h"
#include "satSolver.h"
+#include "extra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-typedef struct Ivy_Fraig_t_ Ivy_Fraig_t;
-struct Ivy_Fraig_t_
+typedef struct Ivy_FraigMan_t_ Ivy_FraigMan_t;
+typedef struct Ivy_FraigSim_t_ Ivy_FraigSim_t;
+typedef struct Ivy_FraigList_t_ Ivy_FraigList_t;
+
+struct Ivy_FraigList_t_
+{
+ Ivy_Obj_t * pHead;
+ Ivy_Obj_t * pTail;
+ int nItems;
+};
+
+struct Ivy_FraigSim_t_
+{
+ int Type;
+ Ivy_FraigSim_t * pNext;
+ Ivy_FraigSim_t * pFanin0;
+ Ivy_FraigSim_t * pFanin1;
+ unsigned pData[0];
+};
+
+struct Ivy_FraigMan_t_
{
// general info
Ivy_FraigParams_t * pParams; // various parameters
@@ -34,23 +54,31 @@ struct Ivy_Fraig_t_
Ivy_Man_t * pManAig; // the starting AIG manager
Ivy_Man_t * pManFraig; // the final AIG manager
// simulation information
- int nWords; // the number of words
- unsigned * pWords; // the simulation info
+ int nSimWords; // the number of words
+ char * pSimWords; // the simulation info
+ Ivy_FraigSim_t * pSimStart; // the list of simulation info for internal nodes
// counter example storage
int nPatWords; // the number of words in the counter example
unsigned * pPatWords; // the counter example
+ int * pPatScores; // the scores of each pattern
// equivalence classes
- int nClasses; // the number of equivalence classes
- Ivy_Obj_t * pClassesHead; // the linked list of classes
- Ivy_Obj_t * pClassesTail; // the linked list of classes
+ Ivy_FraigList_t lClasses; // equivalence classes
+ Ivy_FraigList_t lCand; // candidatates
+ int nPairs; // the number of pairs of nodes
// equivalence checking
sat_solver * pSat; // SAT solver
int nSatVars; // the number of variables currently used
+ Vec_Ptr_t * vPiVars; // the PIs of the cone used
+ // other
+ ProgressBar * pProgress;
// statistics
int nSimRounds;
+ int nNodesMiter;
int nClassesZero;
int nClassesBeg;
int nClassesEnd;
+ int nPairsBeg;
+ int nPairsEnd;
int nSatCalls;
int nSatCallsSat;
int nSatCallsUnsat;
@@ -61,11 +89,16 @@ struct Ivy_Fraig_t_
int timeSim;
int timeTrav;
int timeSat;
+ int timeSatUnsat;
+ int timeSatSat;
+ int timeSatFail;
int timeRef;
int timeTotal;
+ int time1;
+ int time2;
};
-static inline unsigned * Ivy_ObjSim( Ivy_Obj_t * pObj ) { return (unsigned *)pObj->pFanout; }
+static inline Ivy_FraigSim_t * Ivy_ObjSim( Ivy_Obj_t * pObj ) { return (Ivy_FraigSim_t *)pObj->pFanout; }
static inline Ivy_Obj_t * Ivy_ObjClassNodeLast( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; }
static inline Ivy_Obj_t * Ivy_ObjClassNodeRepr( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; }
static inline Ivy_Obj_t * Ivy_ObjClassNodeNext( Ivy_Obj_t * pObj ) { return pObj->pNextFan1; }
@@ -76,7 +109,7 @@ static inline Ivy_Obj_t * Ivy_ObjFraig( Ivy_Obj_t * pObj )
static inline int Ivy_ObjSatNum( Ivy_Obj_t * pObj ) { return (int)pObj->pNextFan0; }
static inline Vec_Ptr_t * Ivy_ObjFaninVec( Ivy_Obj_t * pObj ) { return (Vec_Ptr_t *)pObj->pNextFan1; }
-static inline void Ivy_ObjSetSim( Ivy_Obj_t * pObj, unsigned * pSim ) { pObj->pFanout = (Ivy_Obj_t *)pSim; }
+static inline void Ivy_ObjSetSim( Ivy_Obj_t * pObj, Ivy_FraigSim_t * pSim ) { pObj->pFanout = (Ivy_Obj_t *)pSim; }
static inline void Ivy_ObjSetClassNodeLast( Ivy_Obj_t * pObj, Ivy_Obj_t * pLast ) { pObj->pNextFan0 = pLast; }
static inline void Ivy_ObjSetClassNodeRepr( Ivy_Obj_t * pObj, Ivy_Obj_t * pRepr ) { pObj->pNextFan0 = pRepr; }
static inline void Ivy_ObjSetClassNodeNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pNextFan1 = pNext; }
@@ -105,33 +138,26 @@ static inline unsigned Ivy_ObjRandomSim() { return (ran
for ( pEnt = pClass; \
pEnt; \
pEnt = Ivy_ObjClassNodeNext(pEnt) )
-#define Ivy_FraigForEachClassNodeSafe( pClass, pEnt, pEnt2 ) \
- for ( pEnt = pClass, \
- pEnt2 = pEnt? Ivy_ObjClassNodeNext(pEnt): NULL; \
- pEnt; \
- pEnt = pEnt2, \
- pEnt2 = pEnt? Ivy_ObjClassNodeNext(pEnt): NULL )
// iterate through nodes in the hash table
#define Ivy_FraigForEachBinNode( pBin, pEnt ) \
for ( pEnt = pBin; \
pEnt; \
pEnt = Ivy_ObjNodeHashNext(pEnt) )
-#define Ivy_FraigForEachBinNodeSafe( pBin, pEnt, pEnt2 ) \
- for ( pEnt = pBin, \
- pEnt2 = pEnt? Ivy_ObjNodeHashNext(pEnt): NULL; \
- pEnt; \
- pEnt = pEnt2, \
- pEnt2 = pEnt? Ivy_ObjNodeHashNext(pEnt): NULL )
-
-static Ivy_Fraig_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
-static void Ivy_FraigPrint( Ivy_Fraig_t * p );
-static void Ivy_FraigStop( Ivy_Fraig_t * p );
-static void Ivy_FraigSimulate( Ivy_Fraig_t * p );
-static void Ivy_FraigSweep( Ivy_Fraig_t * p );
-static Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld );
-static int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int nBTLimit );
-static void Ivy_FraigNodeAddToSolver( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
-static int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int * pTravIds, int TravId, double * pFactors, int LevelMax );
+
+static Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+static Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+static void Ivy_FraigPrint( Ivy_FraigMan_t * p );
+static void Ivy_FraigStop( Ivy_FraigMan_t * p );
+static void Ivy_FraigSimulate( Ivy_FraigMan_t * p );
+static void Ivy_FraigSweep( Ivy_FraigMan_t * p );
+static Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld );
+static int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
+static int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj );
+static void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
+static int Ivy_FraigMarkConeSetActivity( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew );
+static void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew );
+static int Ivy_FraigMiterStatus( Ivy_FraigMan_t * p );
+static void Ivy_FraigMiterProve( Ivy_FraigMan_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -148,9 +174,36 @@ static int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_
SeeAlso []
***********************************************************************/
+Ivy_Man_t * Ivy_FraigProve( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+ Ivy_FraigMan_t * p;
+ Ivy_Man_t * pManAigNew;
+ int clk;
+clk = clock();
+ assert( Ivy_ManLatchNum(pManAig) == 0 );
+ p = Ivy_FraigStart( pManAig, pParams );
+ Ivy_FraigSimulate( p );
+ Ivy_FraigSweep( p );
+ pManAigNew = p->pManFraig;
+p->timeTotal = clock() - clk;
+ Ivy_FraigStop( p );
+ return pManAigNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging of the initial AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
{
- Ivy_Fraig_t * p;
+ Ivy_FraigMan_t * p;
Ivy_Man_t * pManAigNew;
int clk;
clk = clock();
@@ -175,11 +228,62 @@ p->timeTotal = clock() - clk;
SeeAlso []
***********************************************************************/
+Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+ Ivy_FraigMan_t * p;
+ Ivy_Man_t * pManAigNew;
+ Ivy_Obj_t * pObj;
+ int i, clk;
+clk = clock();
+ assert( Ivy_ManLatchNum(pManAig) == 0 );
+ p = Ivy_FraigStartSimple( pManAig, pParams );
+ // duplicate internal nodes
+ Ivy_ManForEachNode( p->pManAig, pObj, i )
+ pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+ // try to prove each output of the miter
+ Ivy_FraigMiterProve( p );
+ // add the POs
+ Ivy_ManForEachPo( p->pManAig, pObj, i )
+ Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
+ // clean the new manager
+ Ivy_ManForEachObj( p->pManFraig, pObj, i )
+ {
+ if ( Ivy_ObjFaninVec(pObj) )
+ Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
+ pObj->pNextFan0 = pObj->pNextFan1 = NULL;
+ }
+ // remove dangling nodes
+ Ivy_ManCleanup( p->pManFraig );
+ pManAigNew = p->pManFraig;
+p->timeTotal = clock() - clk;
+ Ivy_FraigStop( p );
+ return pManAigNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging of the initial AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams )
{
memset( pParams, 0, sizeof(Ivy_FraigParams_t) );
- pParams->nSimWords = 32;
- pParams->SimSatur = 0.005;
+ pParams->nSimWords = 32;
+ pParams->SimSatur = 0.005;
+ pParams->fPatScores = 0;
+ pParams->MaxScore = 25;
+ pParams->nBTLimitNode = 100; // conflict limit at a node
+ pParams->nBTLimitMiter = 500000; // conflict limit at an output
+ pParams->nBTLimitGlobal = 0; // conflict limit global
+ pParams->nInsLimitNode = 0; // inspection limit at a node
+ pParams->nInsLimitMiter = 0; // inspection limit at an output
+ pParams->nInsLimitGlobal = 0; // inspection limit global
}
/**Function*************************************************************
@@ -193,31 +297,81 @@ void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams )
SeeAlso []
***********************************************************************/
-Ivy_Fraig_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
{
- Ivy_Fraig_t * p;
+ Ivy_FraigMan_t * p;
+ // allocat the fraiging manager
+ p = ALLOC( Ivy_FraigMan_t, 1 );
+ memset( p, 0, sizeof(Ivy_FraigMan_t) );
+ p->pParams = pParams;
+ p->pManAig = pManAig;
+ p->pManFraig = Ivy_ManStartFrom( pManAig );
+ p->vPiVars = Vec_PtrAlloc( 100 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+ Ivy_FraigMan_t * p;
+ Ivy_FraigSim_t * pSims;
Ivy_Obj_t * pObj;
- int i, k;
+ int i, k, EntrySize;
// clean the fanout representation
Ivy_ManForEachObj( pManAig, pObj, i )
// pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
assert( !pObj->pEquiv && !pObj->pFanout );
// allocat the fraiging manager
- p = ALLOC( Ivy_Fraig_t, 1 );
- memset( p, 0, sizeof(Ivy_Fraig_t) );
+ p = ALLOC( Ivy_FraigMan_t, 1 );
+ memset( p, 0, sizeof(Ivy_FraigMan_t) );
p->pParams = pParams;
p->pManAig = pManAig;
p->pManFraig = Ivy_ManStartFrom( pManAig );
// allocate simulation info
- p->nWords = pParams->nSimWords;
- p->pWords = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nWords );
+ p->nSimWords = pParams->nSimWords;
+// p->pSimWords = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nSimWords );
+ EntrySize = sizeof(Ivy_FraigSim_t) + sizeof(unsigned) * p->nSimWords;
+ p->pSimWords = (char *)malloc( Ivy_ManObjNum(pManAig) * EntrySize );
+ memset( p->pSimWords, 0, EntrySize );
k = 0;
Ivy_ManForEachObj( pManAig, pObj, i )
- Ivy_ObjSetSim( pObj, p->pWords + p->nWords * k++ );
+ {
+ pSims = (Ivy_FraigSim_t *)(p->pSimWords + EntrySize * k++);
+ pSims->pNext = NULL;
+ if ( Ivy_ObjIsNode(pObj) )
+ {
+ if ( p->pSimStart == NULL )
+ p->pSimStart = pSims;
+ else
+ ((Ivy_FraigSim_t *)(p->pSimWords + EntrySize * (k-2)))->pNext = pSims;
+ pSims->pFanin0 = Ivy_ObjSim( Ivy_ObjFanin0(pObj) );
+ pSims->pFanin1 = Ivy_ObjSim( Ivy_ObjFanin1(pObj) );
+ pSims->Type = (Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) << 2) | (Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)) << 1) | pObj->fPhase;
+ }
+ else
+ {
+ pSims->pFanin0 = NULL;
+ pSims->pFanin1 = NULL;
+ pSims->Type = 0;
+ }
+ Ivy_ObjSetSim( pObj, pSims );
+ }
assert( k == Ivy_ManObjNum(pManAig) );
// allocate storage for sim pattern
p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
p->pPatWords = ALLOC( unsigned, p->nPatWords );
+ p->pPatScores = ALLOC( int, 32 * p->nSimWords );
+ p->vPiVars = Vec_PtrAlloc( 100 );
// set random number generator
srand( 0xABCABC );
return p;
@@ -234,22 +388,27 @@ Ivy_Fraig_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
SeeAlso []
***********************************************************************/
-void Ivy_FraigPrint( Ivy_Fraig_t * p )
+void Ivy_FraigPrint( Ivy_FraigMan_t * p )
{
double nMemory;
- nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nWords*sizeof(unsigned)/(1<<20);
- printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nWords, p->nSimRounds, nMemory );
+ nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nSimWords*sizeof(unsigned)/(1<<20);
+ printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nSimWords, p->nSimRounds, nMemory );
printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
+ printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pParams->nBTLimitNode, p->pParams->nBTLimitMiter );
printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
- printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n",
- Ivy_ManNodeNum(p->pManFraig), Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
+ printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n",
+ Ivy_ManNodeNum(p->pManFraig), p->nNodesMiter, Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
PRT( "AIG simulation ", p->timeSim );
PRT( "AIG traversal ", p->timeTrav );
PRT( "SAT solving ", p->timeSat );
+ PRT( " Unsat ", p->timeSatUnsat );
+ PRT( " Sat ", p->timeSatSat );
+ PRT( " Fail ", p->timeSatFail );
PRT( "Class refining ", p->timeRef );
PRT( "TOTAL RUNTIME ", p->timeTotal );
+ PRT( "time1 ", p->time1 );
}
/**Function*************************************************************
@@ -263,15 +422,19 @@ void Ivy_FraigPrint( Ivy_Fraig_t * p )
SeeAlso []
***********************************************************************/
-void Ivy_FraigStop( Ivy_Fraig_t * p )
+void Ivy_FraigStop( Ivy_FraigMan_t * p )
{
- Ivy_FraigPrint( p );
+ if ( p->pParams->fVerbose )
+ Ivy_FraigPrint( p );
+ if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
if ( p->pSat ) sat_solver_delete( p->pSat );
- free( p->pPatWords );
- free( p->pWords );
+ FREE( p->pPatScores );
+ FREE( p->pPatWords );
+ FREE( p->pSimWords );
free( p );
}
+
/**Function*************************************************************
Synopsis [Simulates one node.]
@@ -283,13 +446,13 @@ void Ivy_FraigStop( Ivy_Fraig_t * p )
SeeAlso []
***********************************************************************/
-void Ivy_NodeAssignRandom( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
+void Ivy_NodeAssignRandom( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
{
- unsigned * pSims;
+ Ivy_FraigSim_t * pSims;
int i;
pSims = Ivy_ObjSim(pObj);
- for ( i = 0; i < p->nWords; i++ )
- pSims[i] = Ivy_ObjRandomSim();
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = Ivy_ObjRandomSim();
}
/**Function*************************************************************
@@ -303,13 +466,13 @@ void Ivy_NodeAssignRandom( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Ivy_NodeAssignConst( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int fConst1 )
+void Ivy_NodeAssignConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int fConst1 )
{
- unsigned * pSims;
+ Ivy_FraigSim_t * pSims;
int i;
pSims = Ivy_ObjSim(pObj);
- for ( i = 0; i < p->nWords; i++ )
- pSims[i] = fConst1? ~(unsigned)0 : 0;
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = fConst1? ~(unsigned)0 : 0;
}
/**Function*************************************************************
@@ -323,13 +486,13 @@ void Ivy_NodeAssignConst( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int fConst1 )
SeeAlso []
***********************************************************************/
-int Ivy_NodeHasZeroSim( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
+int Ivy_NodeHasZeroSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
{
- unsigned * pSims;
+ Ivy_FraigSim_t * pSims;
int i;
pSims = Ivy_ObjSim(pObj);
- for ( i = 0; i < p->nWords; i++ )
- if ( pSims[i] )
+ for ( i = 0; i < p->nSimWords; i++ )
+ if ( pSims->pData[i] )
return 0;
return 1;
}
@@ -345,14 +508,14 @@ int Ivy_NodeHasZeroSim( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-int Ivy_NodeCompareSims( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
+int Ivy_NodeCompareSims( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
{
- unsigned * pSims0, * pSims1;
+ Ivy_FraigSim_t * pSims0, * pSims1;
int i;
pSims0 = Ivy_ObjSim(pObj0);
pSims1 = Ivy_ObjSim(pObj1);
- for ( i = 0; i < p->nWords; i++ )
- if ( pSims0[i] != pSims1[i] )
+ for ( i = 0; i < p->nSimWords; i++ )
+ if ( pSims0->pData[i] != pSims1->pData[i] )
return 0;
return 1;
}
@@ -368,9 +531,64 @@ int Ivy_NodeCompareSims( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
SeeAlso []
***********************************************************************/
-void Ivy_NodeSimulate( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
+void Ivy_NodeSimulateSim( Ivy_FraigMan_t * p, Ivy_FraigSim_t * pSims )
{
- unsigned * pSims, * pSims0, * pSims1;
+ unsigned * pData, * pData0, * pData1;
+ int i;
+ pData = pSims->pData;
+ pData0 = pSims->pFanin0->pData;
+ pData1 = pSims->pFanin1->pData;
+ switch( pSims->Type )
+ {
+ case 0:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = (pData0[i] & pData1[i]);
+ break;
+ case 1:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = ~(pData0[i] & pData1[i]);
+ break;
+ case 2:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = (pData0[i] & ~pData1[i]);
+ break;
+ case 3:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = (~pData0[i] | pData1[i]);
+ break;
+ case 4:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = (~pData0[i] & pData1[i]);
+ break;
+ case 5:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = (pData0[i] | ~pData1[i]);
+ break;
+ case 6:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = ~(pData0[i] | pData1[i]);
+ break;
+ case 7:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = (pData0[i] | pData1[i]);
+ break;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodeSimulate( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+ Ivy_FraigSim_t * pSims, * pSims0, * pSims1;
int fCompl, fCompl0, fCompl1, i;
assert( !Ivy_IsComplement(pObj) );
// get hold of the simulation information
@@ -385,38 +603,38 @@ void Ivy_NodeSimulate( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
if ( fCompl0 && fCompl1 )
{
if ( fCompl )
- for ( i = 0; i < p->nWords; i++ )
- pSims[i] = (pSims0[i] | pSims1[i]);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = (pSims0->pData[i] | pSims1->pData[i]);
else
- for ( i = 0; i < p->nWords; i++ )
- pSims[i] = ~(pSims0[i] | pSims1[i]);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = ~(pSims0->pData[i] | pSims1->pData[i]);
}
else if ( fCompl0 && !fCompl1 )
{
if ( fCompl )
- for ( i = 0; i < p->nWords; i++ )
- pSims[i] = (pSims0[i] | ~pSims1[i]);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = (pSims0->pData[i] | ~pSims1->pData[i]);
else
- for ( i = 0; i < p->nWords; i++ )
- pSims[i] = (~pSims0[i] & pSims1[i]);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = (~pSims0->pData[i] & pSims1->pData[i]);
}
else if ( !fCompl0 && fCompl1 )
{
if ( fCompl )
- for ( i = 0; i < p->nWords; i++ )
- pSims[i] = (~pSims0[i] | pSims1[i]);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = (~pSims0->pData[i] | pSims1->pData[i]);
else
- for ( i = 0; i < p->nWords; i++ )
- pSims[i] = (pSims0[i] & ~pSims1[i]);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = (pSims0->pData[i] & ~pSims1->pData[i]);
}
else // if ( !fCompl0 && !fCompl1 )
{
if ( fCompl )
- for ( i = 0; i < p->nWords; i++ )
- pSims[i] = ~(pSims0[i] & pSims1[i]);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = ~(pSims0->pData[i] & pSims1->pData[i]);
else
- for ( i = 0; i < p->nWords; i++ )
- pSims[i] = (pSims0[i] & pSims1[i]);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = (pSims0->pData[i] & pSims1->pData[i]);
}
}
@@ -431,7 +649,7 @@ void Ivy_NodeSimulate( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-unsigned Ivy_NodeHash( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
+unsigned Ivy_NodeHash( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
{
static int s_FPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
@@ -448,13 +666,14 @@ unsigned Ivy_NodeHash( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
- unsigned uHash, * pSims;
+ Ivy_FraigSim_t * pSims;
+ unsigned uHash;
int i;
- assert( p->nWords <= 128 );
+ assert( p->nSimWords <= 128 );
uHash = 0;
pSims = Ivy_ObjSim(pObj);
- for ( i = 0; i < p->nWords; i++ )
- uHash ^= pSims[i] * s_FPrimes[i];
+ for ( i = 0; i < p->nSimWords; i++ )
+ uHash ^= pSims->pData[i] * s_FPrimes[i];
return uHash;
}
@@ -469,7 +688,7 @@ unsigned Ivy_NodeHash( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Ivy_FraigSimulateOne( Ivy_Fraig_t * p )
+void Ivy_FraigSimulateOne( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;
int i, clk;
@@ -501,7 +720,29 @@ p->nSimRounds++;
SeeAlso []
***********************************************************************/
-void Ivy_FraigAssignRandom( Ivy_Fraig_t * p )
+void Ivy_FraigSimulateOneSim( Ivy_FraigMan_t * p )
+{
+ Ivy_FraigSim_t * pSims;
+ int clk;
+clk = clock();
+ for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext )
+ Ivy_NodeSimulateSim( p, pSims );
+p->timeSim += clock() - clk;
+p->nSimRounds++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates AIG manager.]
+
+ Description [Assumes that the PI simulation info is attached.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigAssignRandom( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;
int i;
@@ -520,15 +761,15 @@ void Ivy_FraigAssignRandom( Ivy_Fraig_t * p )
SeeAlso []
***********************************************************************/
-void Ivy_FraigAssignDist1( Ivy_Fraig_t * p, unsigned * pPat )
+void Ivy_FraigAssignDist1( Ivy_FraigMan_t * p, unsigned * pPat )
{
Ivy_Obj_t * pObj;
int i, Limit;
Ivy_ManForEachPi( p->pManAig, pObj, i )
Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) );
- Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nWords * 32 - 1 );
+ Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
for ( i = 0; i < Limit; i++ )
- Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) ), i+1 );
+ Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 );
/*
for ( i = 0; i < Limit; i++ )
Extra_PrintBinary( stdout, Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) ), 30 ), printf( "\n" );
@@ -568,23 +809,23 @@ void Ivy_NodeAddToClass( Ivy_Obj_t * pClass, Ivy_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Ivy_FraigAddClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass )
+void Ivy_FraigAddClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass )
{
- if ( p->pClassesHead == NULL )
+ if ( pList->pHead == NULL )
{
- p->pClassesHead = pClass;
- p->pClassesTail = pClass;
+ pList->pHead = pClass;
+ pList->pTail = pClass;
Ivy_ObjSetEquivListPrev( pClass, NULL );
Ivy_ObjSetEquivListNext( pClass, NULL );
}
else
{
- Ivy_ObjSetEquivListNext( p->pClassesTail, pClass );
- Ivy_ObjSetEquivListPrev( pClass, p->pClassesTail );
+ Ivy_ObjSetEquivListNext( pList->pTail, pClass );
+ Ivy_ObjSetEquivListPrev( pClass, pList->pTail );
Ivy_ObjSetEquivListNext( pClass, NULL );
- p->pClassesTail = pClass;
+ pList->pTail = pClass;
}
- p->nClasses++;
+ pList->nItems++;
}
/**Function*************************************************************
@@ -598,16 +839,16 @@ void Ivy_FraigAddClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass )
SeeAlso []
***********************************************************************/
-void Ivy_FraigInsertClass( Ivy_Fraig_t * p, Ivy_Obj_t * pBase, Ivy_Obj_t * pClass )
+void Ivy_FraigInsertClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pBase, Ivy_Obj_t * pClass )
{
Ivy_ObjSetEquivListPrev( pClass, pBase );
Ivy_ObjSetEquivListNext( pClass, Ivy_ObjEquivListNext(pBase) );
if ( Ivy_ObjEquivListNext(pBase) )
Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pBase), pClass );
Ivy_ObjSetEquivListNext( pBase, pClass );
- if ( p->pClassesTail == pBase )
- p->pClassesTail = pClass;
- p->nClasses++;
+ if ( pList->pTail == pBase )
+ pList->pTail = pClass;
+ pList->nItems++;
}
/**Function*************************************************************
@@ -621,19 +862,47 @@ void Ivy_FraigInsertClass( Ivy_Fraig_t * p, Ivy_Obj_t * pBase, Ivy_Obj_t * pClas
SeeAlso []
***********************************************************************/
-void Ivy_FraigRemoveClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass )
+void Ivy_FraigRemoveClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass )
{
- if ( p->pClassesHead == pClass )
- p->pClassesHead = Ivy_ObjEquivListNext(pClass);
- if ( p->pClassesTail == pClass )
- p->pClassesTail = Ivy_ObjEquivListPrev(pClass);
+ if ( pList->pHead == pClass )
+ pList->pHead = Ivy_ObjEquivListNext(pClass);
+ if ( pList->pTail == pClass )
+ pList->pTail = Ivy_ObjEquivListPrev(pClass);
if ( Ivy_ObjEquivListPrev(pClass) )
Ivy_ObjSetEquivListNext( Ivy_ObjEquivListPrev(pClass), Ivy_ObjEquivListNext(pClass) );
if ( Ivy_ObjEquivListNext(pClass) )
Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pClass), Ivy_ObjEquivListPrev(pClass) );
Ivy_ObjSetEquivListNext( pClass, NULL );
Ivy_ObjSetEquivListPrev( pClass, NULL );
- p->nClasses--;
+ pClass->fMarkA = 0;
+ pList->nItems--;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Count the number of pairs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigCountPairsClasses( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pClass, * pNode;
+ int nPairs = 0, nNodes;
+ return nPairs;
+
+ Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
+ {
+ nNodes = 0;
+ Ivy_FraigForEachClassNode( pClass, pNode )
+ nNodes++;
+ nPairs += nNodes * (nNodes - 1) / 2;
+ }
+ return nPairs;
}
/**Function*************************************************************
@@ -647,10 +916,10 @@ void Ivy_FraigRemoveClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass )
SeeAlso []
***********************************************************************/
-void Ivy_FraigCreateClasses( Ivy_Fraig_t * p )
+void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p )
{
Ivy_Obj_t ** pTable;
- Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry, * pEntry2;
+ Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry;
int i, nTableSize;
unsigned Hash;
pConst1 = Ivy_ManConst1(p->pManAig);
@@ -684,21 +953,24 @@ void Ivy_FraigCreateClasses( Ivy_Fraig_t * p )
pTable[Hash % nTableSize] = pObj;
}
// collect non-trivial classes
- assert( p->pClassesHead == NULL );
- if ( Ivy_ObjClassNodeNext(pConst1) )
+ assert( p->lClasses.pHead == NULL );
+ Ivy_ManForEachObj( p->pManAig, pObj, i )
{
- Ivy_FraigAddClass( p, pConst1 );
- Ivy_ObjSetClassNodeLast( pConst1, NULL );
+ if ( !Ivy_ObjIsConst1(pObj) && !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
+ continue;
+ Ivy_ObjSetNodeHashNext( pObj, NULL );
+ if ( Ivy_ObjClassNodeRepr(pObj) == NULL )
+ {
+ assert( Ivy_ObjClassNodeNext(pObj) == NULL );
+ continue;
+ }
+ // recognize the head of the class
+ if ( Ivy_ObjClassNodeNext( Ivy_ObjClassNodeRepr(pObj) ) != NULL )
+ continue;
+ // clean the class representative and add it to the list
+ Ivy_ObjSetClassNodeRepr( pObj, NULL );
+ Ivy_FraigAddClass( &p->lClasses, pObj );
}
- for ( i = 0; i < nTableSize; i++ )
- Ivy_FraigForEachBinNodeSafe( pTable[i], pEntry, pEntry2 )
- if ( Ivy_ObjClassNodeNext(pEntry) )
- {
- Ivy_FraigAddClass( p, pEntry );
- Ivy_ObjSetClassNodeLast( pEntry, NULL );
- }
- else
- Ivy_ObjSetNodeHashNext( pEntry, NULL );
// free the table
free( pTable );
}
@@ -714,15 +986,20 @@ void Ivy_FraigCreateClasses( Ivy_Fraig_t * p )
SeeAlso []
***********************************************************************/
-int Ivy_FraigRefineClass_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pClass )
+int Ivy_FraigRefineClass_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass )
{
Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode;
+ int RetValue = 0;
// check if there is refinement
pListOld = pClass;
Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew )
{
if ( !Ivy_NodeCompareSims(p, pClass, pClassNew) )
+ {
+ if ( p->pParams->fPatScores )
+ Ivy_FraigAddToPatScores( p, pClass, pClassNew );
break;
+ }
pListOld = pClassNew;
}
if ( pClassNew == NULL )
@@ -749,16 +1026,16 @@ int Ivy_FraigRefineClass_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pClass )
Ivy_ObjSetClassNodeNext( pListNew, NULL );
Ivy_ObjSetClassNodeNext( pListOld, NULL );
// update the list of classes
- Ivy_FraigInsertClass( p, pClass, pClassNew );
+ Ivy_FraigInsertClass( &p->lClasses, pClass, pClassNew );
// if the old class is trivial, remove it
if ( Ivy_ObjClassNodeNext(pClass) == NULL )
- Ivy_FraigRemoveClass( p, pClass );
+ Ivy_FraigRemoveClass( &p->lClasses, pClass );
// if the new class is trivial, remove it; otherwise, try to refine it
if ( Ivy_ObjClassNodeNext(pClassNew) == NULL )
- Ivy_FraigRemoveClass( p, pClassNew );
+ Ivy_FraigRemoveClass( &p->lClasses, pClassNew );
else
- Ivy_FraigRefineClass_rec( p, pClassNew );
- return 1;
+ RetValue = Ivy_FraigRefineClass_rec( p, pClassNew );
+ return RetValue + 1;
}
/**Function*************************************************************
@@ -773,15 +1050,24 @@ int Ivy_FraigRefineClass_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pClass )
SeeAlso []
***********************************************************************/
-int Ivy_FraigRefineClasses( Ivy_Fraig_t * p )
+int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pClass, * pClass2;
- int clk, RetValue = 0;
+ int clk, RetValue, Counter = 0;
clk = clock();
- Ivy_FraigForEachEquivClassSafe( p->pClassesHead, pClass, pClass2 )
- RetValue += Ivy_FraigRefineClass_rec( p, pClass );
+ Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 )
+ {
+ if ( pClass->fMarkA )
+ continue;
+ RetValue = Ivy_FraigRefineClass_rec( p, pClass );
+ Counter += ( RetValue > 0 );
+//if ( Ivy_ObjIsConst1(pClass) )
+//printf( "%d ", RetValue );
+if ( Ivy_ObjIsConst1(pClass) )
+ p->time1 += clock() - clk;
+ }
p->timeRef += clock() - clk;
- return RetValue;
+ return Counter;
}
/**Function*************************************************************
@@ -835,18 +1121,20 @@ int Ivy_FraigCountClassNodes( Ivy_Obj_t * pClass )
SeeAlso []
***********************************************************************/
-int Ivy_FraigCountClasses( Ivy_Fraig_t * p )
+void Ivy_FraigPrintSimClasses( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pClass;
- int Counter = 0;
- Ivy_FraigForEachEquivClass( p->pClassesHead, pClass )
- Counter++;
- return Counter;
+ Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
+ {
+// Ivy_FraigPrintClass( pClass );
+ printf( "%d ", Ivy_FraigCountClassNodes( pClass ) );
+ }
+// printf( "\n" );
}
/**Function*************************************************************
- Synopsis [Stops the fraiging manager.]
+ Synopsis [Copy pattern from the solver into the internal storage.]
Description []
@@ -855,20 +1143,119 @@ int Ivy_FraigCountClasses( Ivy_Fraig_t * p )
SeeAlso []
***********************************************************************/
-void Ivy_FraigPrintSimClasses( Ivy_Fraig_t * p )
+void Ivy_FraigSavePattern0( Ivy_FraigMan_t * p )
{
- Ivy_Obj_t * pClass;
- Ivy_FraigForEachEquivClass( p->pClassesHead, pClass )
- {
-// Ivy_FraigPrintClass( pClass );
- printf( "%d ", Ivy_FraigCountClassNodes( pClass ) );
- }
-// printf( "\n" );
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSavePattern1( Ivy_FraigMan_t * p )
+{
+ memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSavePattern( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+ Ivy_ManForEachPi( p->pManFraig, pObj, i )
+// Vec_PtrForEachEntry( p->vPiVars, pObj, i )
+ if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
+ Ivy_InfoSetBit( p->pPatWords, i );
+// Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSavePattern2( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+// Ivy_ManForEachPi( p->pManFraig, pObj, i )
+ Vec_PtrForEachEntry( p->vPiVars, pObj, i )
+ if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
+// Ivy_InfoSetBit( p->pPatWords, i );
+ Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSavePattern3( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+ for ( i = 0; i < p->nPatWords; i++ )
+ p->pPatWords[i] = Ivy_ObjRandomSim();
+ Vec_PtrForEachEntry( p->vPiVars, pObj, i )
+ if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) )
+ Ivy_InfoXorBit( p->pPatWords, pObj->Id - 1 );
}
/**Function*************************************************************
+ Synopsis [Returns 1 if the one of the output is already non-constant 0.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+ Ivy_ManForEachPo( p->pManAig, pObj, i )
+ if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
Synopsis [Stops the fraiging manager.]
Description []
@@ -878,21 +1265,127 @@ void Ivy_FraigPrintSimClasses( Ivy_Fraig_t * p )
SeeAlso []
***********************************************************************/
-void Ivy_FraigSimulate( Ivy_Fraig_t * p )
+void Ivy_FraigSimulate( Ivy_FraigMan_t * p )
{
int nChanges, nClasses;
+ // start the classes
Ivy_FraigAssignRandom( p );
Ivy_FraigSimulateOne( p );
Ivy_FraigCreateClasses( p );
-//printf( "Starting classes = %5d.\n", p->nClasses );
+//printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Ivy_FraigCountPairsClasses(p) );
+ // refine classes by walking 0/1 patterns
+ Ivy_FraigSavePattern0( p );
+ Ivy_FraigAssignDist1( p, p->pPatWords );
+ Ivy_FraigSimulateOne( p );
+ nChanges = Ivy_FraigRefineClasses( p );
+//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
+ Ivy_FraigSavePattern1( p );
+ Ivy_FraigAssignDist1( p, p->pPatWords );
+ Ivy_FraigSimulateOne( p );
+ nChanges = Ivy_FraigRefineClasses( p );
+//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
+ // refine classes by random simulation
do {
Ivy_FraigAssignRandom( p );
Ivy_FraigSimulateOne( p );
- nClasses = p->nClasses;
+ nClasses = p->lClasses.nItems;
nChanges = Ivy_FraigRefineClasses( p );
-//printf( "Refined classes = %5d. Changes = %4d.\n", p->nClasses, nChanges );
+//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
} while ( (double)nChanges / nClasses > p->pParams->SimSatur );
// Ivy_FraigPrintSimClasses( p );
+ // check if some outputs already became non-constant
+ if ( Ivy_FraigCheckOutputSims(p) )
+ printf( "Special case: One of the POs is already non-const zero.\n" );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Cleans pattern scores.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigCleanPatScores( Ivy_FraigMan_t * p )
+{
+ int i, nLimit = p->nSimWords * 32;
+ for ( i = 0; i < nLimit; i++ )
+ p->pPatScores[i] = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds to pattern scores.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew )
+{
+ Ivy_FraigSim_t * pSims0, * pSims1;
+ unsigned uDiff;
+ int i, w;
+ // get hold of the simulation information
+ pSims0 = Ivy_ObjSim(pClass);
+ pSims1 = Ivy_ObjSim(pClassNew);
+ // iterate through the differences and record the score
+ for ( w = 0; w < p->nSimWords; w++ )
+ {
+ uDiff = pSims0->pData[w] ^ pSims1->pData[w];
+ if ( uDiff == 0 )
+ continue;
+ for ( i = 0; i < 32; i++ )
+ if ( uDiff & ( 1 << i ) )
+ p->pPatScores[w*32+i]++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Selects the best pattern.]
+
+ Description [Returns 1 if such pattern is found.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigSelectBestPat( Ivy_FraigMan_t * p )
+{
+ Ivy_FraigSim_t * pSims;
+ Ivy_Obj_t * pObj;
+ int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1;
+ for ( i = 1; i < nLimit; i++ )
+ {
+ if ( MaxScore < p->pPatScores[i] )
+ {
+ MaxScore = p->pPatScores[i];
+ BestPat = i;
+ }
+ }
+ if ( MaxScore == 0 )
+ return 0;
+// if ( MaxScore > p->pParams->MaxScore )
+// printf( "Max score is %3d. ", MaxScore );
+ // copy the best pattern into the selected pattern
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+ Ivy_ManForEachPi( p->pManAig, pObj, i )
+ {
+ pSims = Ivy_ObjSim(pObj);
+ if ( Ivy_InfoHasBit(pSims->pData, BestPat) )
+ Ivy_InfoSetBit(p->pPatWords, i);
+ }
+ return MaxScore;
}
/**Function*************************************************************
@@ -906,19 +1399,158 @@ void Ivy_FraigSimulate( Ivy_Fraig_t * p )
SeeAlso []
***********************************************************************/
-void Ivy_FraigResimulate( Ivy_Fraig_t * p )
+void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
{
int nChanges;
Ivy_FraigAssignDist1( p, p->pPatWords );
Ivy_FraigSimulateOne( p );
+ if ( p->pParams->fPatScores )
+ Ivy_FraigCleanPatScores( p );
nChanges = Ivy_FraigRefineClasses( p );
+ if ( nChanges < 1 )
+ printf( "Error: A counter-example did not refine classes!\n" );
assert( nChanges >= 1 );
-//printf( "Refined classes! = %5d. Changes = %4d.\n", p->nClasses, nChanges );
+//printf( "Refined classes! = %5d. Changes = %4d.\n", p->lClasses.nItems, nChanges );
+
+ if ( !p->pParams->fPatScores )
+ return;
+
+ // perform additional simulation using dist1 patterns derived from successful patterns
+ while ( Ivy_FraigSelectBestPat(p) > p->pParams->MaxScore )
+ {
+ Ivy_FraigAssignDist1( p, p->pPatWords );
+ Ivy_FraigSimulateOne( p );
+ Ivy_FraigCleanPatScores( p );
+ nChanges = Ivy_FraigRefineClasses( p );
+//printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
+ if ( nChanges == 0 )
+ break;
+ }
}
/**Function*************************************************************
+ Synopsis [Reports the status of the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigMiterStatus( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj, * pObjNew;
+ int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
+ Ivy_ManForEachPo( p->pManAig, pObj, i )
+ {
+ pObjNew = Ivy_ObjChild0Equiv(pObj);
+ // check if the output is constant 1
+ if ( pObjNew == p->pManFraig->pConst1 )
+ {
+ CountNonConst0++;
+ continue;
+ }
+ // check if the output is constant 0
+ if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) )
+ {
+ CountConst0++;
+ continue;
+ }
+ // check if the output can be constant 0
+ if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
+ {
+ CountNonConst0++;
+ continue;
+ }
+ CountUndecided++;
+ }
+ if ( p->pParams->fVerbose )
+ {
+ printf( "Miter has %d outputs. ", Ivy_ManPoNum(p->pManAig) );
+ printf( "Const0 = %d. ", CountConst0 );
+ printf( "NonConst0 = %d. ", CountNonConst0 );
+ printf( "Undecided = %d. ", CountUndecided );
+ printf( "\n" );
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Works on the miter.]
+
+ Description [Tries to prove each output until encountering a sat output.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj, * pObjNew;
+ int i, RetValue, clk = clock();
+ int fVerbose = p->pParams->fVerbose;
+ Ivy_ManForEachPo( p->pManAig, pObj, i )
+ {
+ if ( i && fVerbose )
+ {
+ PRT( "Time", clock() -clk );
+ }
+ pObjNew = Ivy_ObjChild0Equiv(pObj);
+ // check if the output is constant 1
+ if ( pObjNew == p->pManFraig->pConst1 )
+ {
+ if ( fVerbose )
+ printf( "Output %2d (out of %2d) is constant 1. ", i, Ivy_ManPoNum(p->pManAig) );
+ break;
+ }
+ // check if the output is constant 0
+ if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) )
+ {
+ if ( fVerbose )
+ printf( "Output %2d (out of %2d) is already constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
+ continue;
+ }
+ // check if the output can be constant 0
+ if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
+ {
+ if ( fVerbose )
+ printf( "Output %2d (out of %2d) cannot be constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
+ break;
+ }
+ // try to prove the output constant 0
+ RetValue = Ivy_FraigNodeIsConst( p, Ivy_Regular(pObjNew) );
+ if ( RetValue == 1 ) // proved equivalent
+ {
+ if ( fVerbose )
+ printf( "Output %2d (out of %2d) was proved constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
+ // set the constant miter
+ Ivy_ObjFanin0(pObj)->pEquiv = Ivy_NotCond( p->pManFraig->pConst1, !Ivy_IsComplement(pObj) );
+ continue;
+ }
+ if ( RetValue == -1 ) // failed
+ {
+ if ( fVerbose )
+ printf( "Output %2d (out of %2d) has timed out at %d backtracks. ", i, Ivy_ManPoNum(p->pManAig), p->pParams->nBTLimitMiter );
+ continue;
+ }
+ // proved satisfiable
+ if ( fVerbose )
+ printf( "Output %2d (out of %2d) was proved NOT a constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
+ break;
+ }
+ if ( fVerbose )
+ {
+ PRT( "Time", clock() -clk );
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Performs fraiging for the internal nodes.]
Description []
@@ -928,16 +1560,25 @@ void Ivy_FraigResimulate( Ivy_Fraig_t * p )
SeeAlso []
***********************************************************************/
-void Ivy_FraigSweep( Ivy_Fraig_t * p )
+void Ivy_FraigSweep( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;
- int i;
-p->nClassesZero = Ivy_ObjIsConst1(p->pClassesHead) ? Ivy_FraigCountClassNodes(p->pClassesHead) : 0;
-p->nClassesBeg = Ivy_FraigCountClasses(p);
+ int i, k = 0;
+p->nClassesZero = Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0;
+p->nClassesBeg = p->lClasses.nItems;
// duplicate internal nodes
+ p->pProgress = Extra_ProgressBarStart( stdout, Ivy_ManNodeNum(p->pManAig) );
Ivy_ManForEachNode( p->pManAig, pObj, i )
+ {
+ Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
pObj->pEquiv = Ivy_FraigAnd( p, pObj );
-p->nClassesEnd = Ivy_FraigCountClasses(p);
+ }
+ Extra_ProgressBarStop( p->pProgress );
+p->nClassesEnd = p->lClasses.nItems;
+ // try to prove the outputs of the miter
+ p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig);
+ Ivy_FraigMiterStatus( p );
+ Ivy_FraigMiterProve( p );
// add the POs
Ivy_ManForEachPo( p->pManAig, pObj, i )
Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
@@ -953,6 +1594,9 @@ p->nClassesEnd = Ivy_FraigCountClasses(p);
}
// remove dangling nodes
Ivy_ManCleanup( p->pManFraig );
+ // clean up the class marks
+ Ivy_FraigForEachEquivClass( p->lClasses.pHead, pObj )
+ pObj->fMarkA = 0;
}
/**Function*************************************************************
@@ -966,7 +1610,7 @@ p->nClassesEnd = Ivy_FraigCountClasses(p);
SeeAlso []
***********************************************************************/
-Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld )
+Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
{
Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew;
int RetValue;
@@ -988,10 +1632,16 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld )
// if the fraiged nodes are the same return
if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) )
return pObjNew;
+ assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) );
// they are different (the counter-example is in p->pPatWords)
- RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew), 1000 );
+ RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew) );
if ( RetValue == 1 ) // proved equivalent
+ {
+ // mark the class as proved
+ if ( Ivy_ObjClassNodeNext(pObjOld) == NULL )
+ Ivy_ObjClassNodeRepr(pObjOld)->fMarkA = 1;
return Ivy_NotCond( pObjReprNew, pObjOld->fPhase ^ Ivy_ObjClassNodeRepr(pObjOld)->fPhase );
+ }
if ( RetValue == -1 ) // failed
return pObjNew;
// simulate the counter-example and return the new node
@@ -1001,29 +1651,25 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld )
/**Function*************************************************************
- Synopsis [Copy pattern from the solver into the internal storage.]
+ Synopsis [Performs fraiging for one node.]
- Description []
+ Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
***********************************************************************/
-void Ivy_FraigSavePattern( Ivy_Fraig_t * p )
+void Ivy_FraigCleanActivity( Ivy_FraigMan_t * p )
{
- Ivy_Obj_t * pObj;
+ double * pActivity;
int i;
- memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
- Ivy_ManForEachPi( p->pManFraig, pObj, i )
- if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
- Ivy_InfoSetBit( p->pPatWords, i );
-/*
- // print sat variables
+ pActivity = sat_solver_activity(p->pSat);
for ( i = 0; i < p->nSatVars; i++ )
- printf( "%d=%d ", i, p->pSat->model.ptr[i] );
- printf( "\n" );
-*/
+ {
+ pActivity[i] = 0.0;
+ sat_solver_order_update( p->pSat, i );
+ }
}
/**Function*************************************************************
@@ -1037,11 +1683,30 @@ void Ivy_FraigSavePattern( Ivy_Fraig_t * p )
SeeAlso []
***********************************************************************/
-int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew, int nBTLimit )
+void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p )
{
- int pLits[4], RetValue, RetValue1, clk, Counter;
+ double * pActivity;
+ int i;
+ pActivity = sat_solver_activity(p->pSat);
+ for ( i = 0; i < p->nSatVars; i++ )
+ printf( "%d %.3f ", i, pActivity[i] );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
-// printf( "Trying to prove nodes %d and %d\n", pOld->Id, pNew->Id );
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
+{
+ int pLits[4], RetValue, RetValue1, nBTLimit, clk;
// make sure the nodes are not complemented
assert( !Ivy_IsComplement(pNew) );
@@ -1051,9 +1716,13 @@ int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew,
// if at least one of the nodes is a failed node, perform adjustments:
// if the backtrack limit is small, simply skip this node
// if the backtrack limit is > 10, take the quare root of the limit
+ nBTLimit = p->pParams->nBTLimitNode;
if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
{
p->nSatFails++;
+ // fail immediately
+ return -1;
+
if ( nBTLimit <= 10 )
return -1;
nBTLimit = (int)sqrt(nBTLimit);
@@ -1071,25 +1740,19 @@ int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew,
// if the nodes do not have SAT variables, allocate them
Ivy_FraigNodeAddToSolver( p, pOld, pNew );
- // prepare variable activity
-clk = clock();
- Ivy_ManIncrementTravId( p->pManFraig );
- Counter = Ivy_FraigMarkConeSetActivity_rec( p, pOld, NULL, 0, NULL, 0 );
- Counter += Ivy_FraigMarkConeSetActivity_rec( p, pNew, NULL, 0, NULL, 0 );
-// printf( "%d ", Counter );
-p->timeTrav += clock() - clk;
-
-
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
clk = clock();
pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 );
pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
- RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2 );
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
+ nBTLimit, p->pParams->nInsLimitNode,
+ p->pParams->nBTLimitGlobal, p->pParams->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
+p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
@@ -1099,12 +1762,14 @@ p->timeSat += clock() - clk;
}
else if ( RetValue1 == l_True )
{
+p->timeSatSat += clock() - clk;
Ivy_FraigSavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
+p->timeSatFail += clock() - clk;
// mark the node as the failed node
if ( pOld != p->pManFraig->pConst1 )
pOld->fFailTfo = 1;
@@ -1125,10 +1790,13 @@ p->timeSat += clock() - clk;
clk = clock();
pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 );
pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
- RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2 );
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
+ nBTLimit, p->pParams->nInsLimitNode,
+ p->pParams->nBTLimitGlobal, p->pParams->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
+p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
@@ -1137,12 +1805,14 @@ p->timeSat += clock() - clk;
}
else if ( RetValue1 == l_True )
{
+p->timeSatSat += clock() - clk;
Ivy_FraigSavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
+p->timeSatFail += clock() - clk;
// mark the node as the failed node
pOld->fFailTfo = 1;
pNew->fFailTfo = 1;
@@ -1157,6 +1827,77 @@ p->timeSat += clock() - clk;
/**Function*************************************************************
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
+{
+ int pLits[2], RetValue1, RetValue, clk;
+
+ // make sure the nodes are not complemented
+ assert( !Ivy_IsComplement(pNew) );
+ assert( pNew != p->pManFraig->pConst1 );
+ p->nSatCalls++;
+
+ // make sure the solver is allocated and has enough variables
+ if ( p->pSat == NULL )
+ {
+ p->pSat = sat_solver_new();
+ p->nSatVars = 1;
+ sat_solver_setnvars( p->pSat, 1000 );
+ }
+
+ // if the nodes do not have SAT variables, allocate them
+ Ivy_FraigNodeAddToSolver( p, NULL, pNew );
+
+ // prepare variable activity
+ Ivy_FraigMarkConeSetActivity( p, NULL, pNew );
+
+ // solve under assumptions
+clk = clock();
+ pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase );
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1,
+ p->pParams->nBTLimitMiter, p->pParams->nInsLimitMiter,
+ p->pParams->nBTLimitGlobal, p->pParams->nInsLimitGlobal );
+p->timeSat += clock() - clk;
+ if ( RetValue1 == l_False )
+ {
+p->timeSatUnsat += clock() - clk;
+ pLits[0] = lit_neg( pLits[0] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+ assert( RetValue );
+ // continue solving the other implication
+ p->nSatCallsUnsat++;
+ }
+ else if ( RetValue1 == l_True )
+ {
+p->timeSatSat += clock() - clk;
+ Ivy_FraigSavePattern( p );
+ p->nSatCallsSat++;
+ return 0;
+ }
+ else // if ( RetValue1 == l_Undef )
+ {
+p->timeSatFail += clock() - clk;
+ // mark the node as the failed node
+ pNew->fFailTfo = 1;
+ p->nSatFailsReal++;
+ return -1;
+ }
+
+ // return SAT proof
+ p->nSatProof++;
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Addes clauses to the solver.]
Description []
@@ -1166,7 +1907,7 @@ p->timeSat += clock() - clk;
SeeAlso []
***********************************************************************/
-void Ivy_FraigAddClausesMux( Ivy_Fraig_t * p, Ivy_Obj_t * pNode )
+void Ivy_FraigAddClausesMux( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode )
{
Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE;
int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
@@ -1249,7 +1990,7 @@ void Ivy_FraigAddClausesMux( Ivy_Fraig_t * p, Ivy_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-void Ivy_FraigAddClausesSuper( Ivy_Fraig_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t * vSuper )
+void Ivy_FraigAddClausesSuper( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t * vSuper )
{
Ivy_Obj_t * pFanin;
int * pLits, nLits, RetValue, i;
@@ -1333,7 +2074,7 @@ Vec_Ptr_t * Ivy_FraigCollectSuper( Ivy_Obj_t * pObj, int fUseMuxes )
SeeAlso []
***********************************************************************/
-void Ivy_FraigObjAddToFrontier( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+void Ivy_FraigObjAddToFrontier( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vFrontier )
{
assert( !Ivy_IsComplement(pObj) );
if ( Ivy_ObjSatNum(pObj) )
@@ -1359,18 +2100,19 @@ void Ivy_FraigObjAddToFrontier( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * v
SeeAlso []
***********************************************************************/
-void Ivy_FraigNodeAddToSolver( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
-{
+void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
+{
Vec_Ptr_t * vFrontier, * vFanins;
Ivy_Obj_t * pNode, * pFanin;
int i, k, fUseMuxes = 1;
+ assert( pOld || pNew );
// quit if CNF is ready
- if ( Ivy_ObjFaninVec(pOld) && Ivy_ObjFaninVec(pNew) )
+ if ( (!pOld || Ivy_ObjFaninVec(pOld)) && (!pNew || Ivy_ObjFaninVec(pNew)) )
return;
// start the frontier
vFrontier = Vec_PtrAlloc( 100 );
- Ivy_FraigObjAddToFrontier( p, pOld, vFrontier );
- Ivy_FraigObjAddToFrontier( p, pNew, vFrontier );
+ if ( pOld ) Ivy_FraigObjAddToFrontier( p, pOld, vFrontier );
+ if ( pNew ) Ivy_FraigObjAddToFrontier( p, pNew, vFrontier );
// explore nodes in the frontier
Vec_PtrForEachEntry( vFrontier, pNode, i )
{
@@ -1412,7 +2154,7 @@ void Ivy_FraigNodeAddToSolver( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
SeeAlso []
***********************************************************************/
-int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int * pTravIds, int TravId, double * pFactors, int LevelMax )
+int Ivy_FraigMarkConeSetActivity_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, double * pActivity, int LevelMax, Vec_Ptr_t * vPiVars )
{
Vec_Ptr_t * vFanins;
Ivy_Obj_t * pFanin;
@@ -1421,21 +2163,74 @@ int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int * p
if ( Ivy_ObjIsConst1(pObj) )
return 0;
assert( Ivy_ObjSatNum(pObj) );
-// if ( pTravIds[Ivy_ObjSatNum(pObj)] == TravId )
-// return;
-// pTravIds[Ivy_ObjSatNum(pObj)] = TravId;
-// pFactors[Ivy_ObjSatNum(pObj)] = pow( 0.97, LevelMax - pObj->Level );
if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) )
return 0;
Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj);
+
+ // add this variable to the decision
+ assert( Ivy_ObjSatNum(pObj) > 0 );
+// pActivity[Ivy_ObjSatNum(pObj)] = 3.0 * pow( 0.97, LevelMax - pObj->Level );
+// sat_solver_order_unassigned( p->pSat, Ivy_ObjSatNum(pObj) );
+
+// pActivity[Ivy_ObjSatNum(pObj)] += 3.0 * pObj->Level / LevelMax;
+// sat_solver_order_update( p->pSat, Ivy_ObjSatNum(pObj) );
+
+ if ( LevelMax > 150 && (int)pObj->Level > LevelMax - 100 )
+ sat_solver_act_var_bump_factor( p->pSat, Ivy_ObjSatNum(pObj), 1.0 + 10.0 * (pObj->Level - (LevelMax - 100)) / 100 );
+
+ // add the PI to the list
if ( Ivy_ObjIsPi(pObj) )
+ {
+ Vec_PtrPush( vPiVars, pObj );
return 0;
+ }
+ // explore the fanins
vFanins = Ivy_ObjFaninVec( pObj );
Counter = 1;
Vec_PtrForEachEntry( vFanins, pFanin, i )
- Counter += Ivy_FraigMarkConeSetActivity_rec( p, Ivy_Regular(pFanin), pTravIds, TravId, pFactors, LevelMax );
+ Counter += Ivy_FraigMarkConeSetActivity_rec( p, Ivy_Regular(pFanin), pActivity, LevelMax, vPiVars );
return Counter;
+
+// Counter = Ivy_FraigMarkConeSetActivity_rec( p, Ivy_ObjFanin0(pObj), pActivity, LevelMax, vPiVars );
+// Counter += Ivy_FraigMarkConeSetActivity_rec( p, Ivy_ObjFanin1(pObj), pActivity, LevelMax, vPiVars );
+// return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigMarkConeSetActivity( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
+{
+ int clk, LevelMax, Counter;
+ assert( pOld || pNew );
+clk = clock();
+ Vec_PtrClear( p->vPiVars );
+ Ivy_ManIncrementTravId( p->pManFraig );
+// Ivy_FraigCleanActivity( p );
+// sat_solver_order_clean( p->pSat );
+//printf( "\n" );
+//printf( "Adding\n" );
+ LevelMax = IVY_MAX( pNew ? pNew->Level : 0, pOld ? pOld->Level : 0 );
+ Counter = 0;
+ if ( pOld )
+ Counter += Ivy_FraigMarkConeSetActivity_rec( p, pOld, sat_solver_activity(p->pSat), LevelMax, p->vPiVars );
+ if ( pNew )
+ Counter += Ivy_FraigMarkConeSetActivity_rec( p, pNew, sat_solver_activity(p->pSat), LevelMax, p->vPiVars );
+//Ivy_FraigPrintActivity( p );
+//printf( "\n" );
+//printf( "Solving\n" );
+// printf( "%d ", Vec_PtrSize(p->vPiVars) );
+p->timeTrav += clock() - clk;
+ return 1;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/satMem.c b/src/temp/ivy/satMem.c
new file mode 100644
index 00000000..bb234f66
--- /dev/null
+++ b/src/temp/ivy/satMem.c
@@ -0,0 +1,527 @@
+/**CFile****************************************************************
+
+ FileName [satMem.c]
+
+ PackageName [SAT solver.]
+
+ Synopsis [Memory management.]
+
+ Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - January 1, 2004.]
+
+ Revision [$Id: satMem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "satMem.h"
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+struct Sat_MmFixed_t_
+{
+ // information about individual entries
+ int nEntrySize; // the size of one entry
+ int nEntriesAlloc; // the total number of entries allocated
+ int nEntriesUsed; // the number of entries in use
+ int nEntriesMax; // the max number of entries in use
+ char * pEntriesFree; // the linked list of free entries
+
+ // this is where the memory is stored
+ int nChunkSize; // the size of one chunk
+ int nChunksAlloc; // the maximum number of memory chunks
+ int nChunks; // the current number of memory chunks
+ char ** pChunks; // the allocated memory
+
+ // statistics
+ int nMemoryUsed; // memory used in the allocated entries
+ int nMemoryAlloc; // memory allocated
+};
+
+struct Sat_MmFlex_t_
+{
+ // information about individual entries
+ int nEntriesUsed; // the number of entries allocated
+ char * pCurrent; // the current pointer to free memory
+ char * pEnd; // the first entry outside the free memory
+
+ // this is where the memory is stored
+ int nChunkSize; // the size of one chunk
+ int nChunksAlloc; // the maximum number of memory chunks
+ int nChunks; // the current number of memory chunks
+ char ** pChunks; // the allocated memory
+
+ // statistics
+ int nMemoryUsed; // memory used in the allocated entries
+ int nMemoryAlloc; // memory allocated
+};
+
+struct Sat_MmStep_t_
+{
+ int nMems; // the number of fixed memory managers employed
+ Sat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc
+ int nMapSize; // the size of the memory array
+ Sat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocates memory pieces of fixed size.]
+
+ Description [The size of the chunk is computed as the minimum of
+ 1024 entries and 64K. Can only work with entry size at least 4 byte long.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize )
+{
+ Sat_MmFixed_t * p;
+
+ p = ALLOC( Sat_MmFixed_t, 1 );
+ memset( p, 0, sizeof(Sat_MmFixed_t) );
+
+ p->nEntrySize = nEntrySize;
+ p->nEntriesAlloc = 0;
+ p->nEntriesUsed = 0;
+ p->pEntriesFree = NULL;
+
+ if ( nEntrySize * (1 << 10) < (1<<16) )
+ p->nChunkSize = (1 << 10);
+ else
+ p->nChunkSize = (1<<16) / nEntrySize;
+ if ( p->nChunkSize < 8 )
+ p->nChunkSize = 8;
+
+ p->nChunksAlloc = 64;
+ p->nChunks = 0;
+ p->pChunks = ALLOC( char *, p->nChunksAlloc );
+
+ p->nMemoryUsed = 0;
+ p->nMemoryAlloc = 0;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose )
+{
+ int i;
+ if ( p == NULL )
+ return;
+ if ( fVerbose )
+ {
+ printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
+ p->nEntrySize, p->nChunkSize, p->nChunks );
+ printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
+ p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
+ }
+ for ( i = 0; i < p->nChunks; i++ )
+ free( p->pChunks[i] );
+ free( p->pChunks );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p )
+{
+ char * pTemp;
+ int i;
+
+ // check if there are still free entries
+ if ( p->nEntriesUsed == p->nEntriesAlloc )
+ { // need to allocate more entries
+ assert( p->pEntriesFree == NULL );
+ if ( p->nChunks == p->nChunksAlloc )
+ {
+ p->nChunksAlloc *= 2;
+ p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc );
+ }
+ p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
+ p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
+ // transform these entries into a linked list
+ pTemp = p->pEntriesFree;
+ for ( i = 1; i < p->nChunkSize; i++ )
+ {
+ *((char **)pTemp) = pTemp + p->nEntrySize;
+ pTemp += p->nEntrySize;
+ }
+ // set the last link
+ *((char **)pTemp) = NULL;
+ // add the chunk to the chunk storage
+ p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
+ // add to the number of entries allocated
+ p->nEntriesAlloc += p->nChunkSize;
+ }
+ // incrememt the counter of used entries
+ p->nEntriesUsed++;
+ if ( p->nEntriesMax < p->nEntriesUsed )
+ p->nEntriesMax = p->nEntriesUsed;
+ // return the first entry in the free entry list
+ pTemp = p->pEntriesFree;
+ p->pEntriesFree = *((char **)pTemp);
+ return pTemp;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry )
+{
+ // decrement the counter of used entries
+ p->nEntriesUsed--;
+ // add the entry to the linked list of free entries
+ *((char **)pEntry) = p->pEntriesFree;
+ p->pEntriesFree = pEntry;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description [Relocates all the memory except the first chunk.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_MmFixedRestart( Sat_MmFixed_t * p )
+{
+ int i;
+ char * pTemp;
+
+ // deallocate all chunks except the first one
+ for ( i = 1; i < p->nChunks; i++ )
+ free( p->pChunks[i] );
+ p->nChunks = 1;
+ // transform these entries into a linked list
+ pTemp = p->pChunks[0];
+ for ( i = 1; i < p->nChunkSize; i++ )
+ {
+ *((char **)pTemp) = pTemp + p->nEntrySize;
+ pTemp += p->nEntrySize;
+ }
+ // set the last link
+ *((char **)pTemp) = NULL;
+ // set the free entry list
+ p->pEntriesFree = p->pChunks[0];
+ // set the correct statistics
+ p->nMemoryAlloc = p->nEntrySize * p->nChunkSize;
+ p->nMemoryUsed = 0;
+ p->nEntriesAlloc = p->nChunkSize;
+ p->nEntriesUsed = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sat_MmFixedReadMemUsage( Sat_MmFixed_t * p )
+{
+ return p->nMemoryAlloc;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Allocates entries of flexible size.]
+
+ Description [Can only work with entry size at least 4 byte long.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sat_MmFlex_t * Sat_MmFlexStart()
+{
+ Sat_MmFlex_t * p;
+
+ p = ALLOC( Sat_MmFlex_t, 1 );
+ memset( p, 0, sizeof(Sat_MmFlex_t) );
+
+ p->nEntriesUsed = 0;
+ p->pCurrent = NULL;
+ p->pEnd = NULL;
+
+ p->nChunkSize = (1 << 12);
+ p->nChunksAlloc = 64;
+ p->nChunks = 0;
+ p->pChunks = ALLOC( char *, p->nChunksAlloc );
+
+ p->nMemoryUsed = 0;
+ p->nMemoryAlloc = 0;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose )
+{
+ int i;
+ if ( p == NULL )
+ return;
+ if ( fVerbose )
+ {
+ printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
+ p->nChunkSize, p->nChunks );
+ printf( " Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
+ p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
+ }
+ for ( i = 0; i < p->nChunks; i++ )
+ free( p->pChunks[i] );
+ free( p->pChunks );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes )
+{
+ char * pTemp;
+ // check if there are still free entries
+ if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
+ { // need to allocate more entries
+ if ( p->nChunks == p->nChunksAlloc )
+ {
+ p->nChunksAlloc *= 2;
+ p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc );
+ }
+ if ( nBytes > p->nChunkSize )
+ {
+ // resize the chunk size if more memory is requested than it can give
+ // (ideally, this should never happen)
+ p->nChunkSize = 2 * nBytes;
+ }
+ p->pCurrent = ALLOC( char, p->nChunkSize );
+ p->pEnd = p->pCurrent + p->nChunkSize;
+ p->nMemoryAlloc += p->nChunkSize;
+ // add the chunk to the chunk storage
+ p->pChunks[ p->nChunks++ ] = p->pCurrent;
+ }
+ assert( p->pCurrent + nBytes <= p->pEnd );
+ // increment the counter of used entries
+ p->nEntriesUsed++;
+ // keep track of the memory used
+ p->nMemoryUsed += nBytes;
+ // return the next entry
+ pTemp = p->pCurrent;
+ p->pCurrent += nBytes;
+ return pTemp;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p )
+{
+ return p->nMemoryAlloc;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Starts the hierarchical memory manager.]
+
+ Description [This manager can allocate entries of any size.
+ Iternally they are mapped into the entries with the number of bytes
+ equal to the power of 2. The smallest entry size is 8 bytes. The
+ next one is 16 bytes etc. So, if the user requests 6 bytes, he gets
+ 8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc.
+ The input parameters "nSteps" says how many fixed memory managers
+ are employed internally. Calling this procedure with nSteps equal
+ to 10 results in 10 hierarchically arranged internal memory managers,
+ which can allocate up to 4096 (1Kb) entries. Requests for larger
+ entries are handed over to malloc() and then free()ed.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sat_MmStep_t * Sat_MmStepStart( int nSteps )
+{
+ Sat_MmStep_t * p;
+ int i, k;
+ p = ALLOC( Sat_MmStep_t, 1 );
+ p->nMems = nSteps;
+ // start the fixed memory managers
+ p->pMems = ALLOC( Sat_MmFixed_t *, p->nMems );
+ for ( i = 0; i < p->nMems; i++ )
+ p->pMems[i] = Sat_MmFixedStart( (8<<i) );
+ // set up the mapping of the required memory size into the corresponding manager
+ p->nMapSize = (4<<p->nMems);
+ p->pMap = ALLOC( Sat_MmFixed_t *, p->nMapSize+1 );
+ p->pMap[0] = NULL;
+ for ( k = 1; k <= 4; k++ )
+ p->pMap[k] = p->pMems[0];
+ for ( i = 0; i < p->nMems; i++ )
+ for ( k = (4<<i)+1; k <= (8<<i); k++ )
+ p->pMap[k] = p->pMems[i];
+//for ( i = 1; i < 100; i ++ )
+//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the memory manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose )
+{
+ int i;
+ for ( i = 0; i < p->nMems; i++ )
+ Sat_MmFixedStop( p->pMems[i], fVerbose );
+ free( p->pMems );
+ free( p->pMap );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the entry.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes )
+{
+ if ( nBytes == 0 )
+ return NULL;
+ if ( nBytes > p->nMapSize )
+ {
+// printf( "Allocating %d bytes.\n", nBytes );
+ return ALLOC( char, nBytes );
+ }
+ return Sat_MmFixedEntryFetch( p->pMap[nBytes] );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Recycles the entry.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes )
+{
+ if ( nBytes == 0 )
+ return;
+ if ( nBytes > p->nMapSize )
+ {
+ free( pEntry );
+ return;
+ }
+ Sat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sat_MmStepReadMemUsage( Sat_MmStep_t * p )
+{
+ int i, nMemTotal = 0;
+ for ( i = 0; i < p->nMems; i++ )
+ nMemTotal += p->pMems[i]->nMemoryAlloc;
+ return nMemTotal;
+}
diff --git a/src/temp/ivy/satMem.h b/src/temp/ivy/satMem.h
new file mode 100644
index 00000000..5c5ddd9c
--- /dev/null
+++ b/src/temp/ivy/satMem.h
@@ -0,0 +1,78 @@
+/**CFile****************************************************************
+
+ FileName [satMem.h]
+
+ PackageName [SAT solver.]
+
+ Synopsis [Memory management.]
+
+ Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - January 1, 2004.]
+
+ Revision [$Id: satMem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __SAT_MEM_H__
+#define __SAT_MEM_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+//#include "leaks.h"
+#include <stdio.h>
+#include <stdlib.h>
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// STRUCTURE DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Sat_MmFixed_t_ Sat_MmFixed_t;
+typedef struct Sat_MmFlex_t_ Sat_MmFlex_t;
+typedef struct Sat_MmStep_t_ Sat_MmStep_t;
+
+////////////////////////////////////////////////////////////////////////
+/// GLOBAL VARIABLES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// fixed-size-block memory manager
+extern Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize );
+extern void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose );
+extern char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p );
+extern void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry );
+extern void Sat_MmFixedRestart( Sat_MmFixed_t * p );
+extern int Sat_MmFixedReadMemUsage( Sat_MmFixed_t * p );
+// flexible-size-block memory manager
+extern Sat_MmFlex_t * Sat_MmFlexStart();
+extern void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose );
+extern char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes );
+extern int Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p );
+// hierarchical memory manager
+extern Sat_MmStep_t * Sat_MmStepStart( int nSteps );
+extern void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose );
+extern char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes );
+extern void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes );
+extern int Sat_MmStepReadMemUsage( Sat_MmStep_t * p );
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/temp/ivy/satSolver.c b/src/temp/ivy/satSolver.c
index b8248df8..38e73c7d 100644
--- a/src/temp/ivy/satSolver.c
+++ b/src/temp/ivy/satSolver.c
@@ -26,6 +26,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "satSolver.h"
+//#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
+
//=================================================================================================
// Debug:
@@ -142,6 +144,7 @@ static inline void order_unassigned(sat_solver* s, int v) // undoorder
orderpos[v] = veci_size(&s->order);
veci_push(&s->order,v);
order_update(s,v);
+//printf( "+%d ", v );
}
}
@@ -202,6 +205,7 @@ static int order_select(sat_solver* s, float random_var_freq) // selectvar
orderpos[heap[i]] = i;
}
+//printf( "-%d ", next );
if (values[next] == l_Undef)
return next;
}
@@ -209,6 +213,21 @@ static int order_select(sat_solver* s, float random_var_freq) // selectvar
return var_Undef;
}
+void sat_solver_order_clean(sat_solver* s) // removes all variables from the queue
+{
+ while ( order_select(s, 0.0) != var_Undef );
+}
+
+void sat_solver_order_unassigned(sat_solver* s, int v) // undoorder
+{
+ order_unassigned(s, v);
+}
+
+void sat_solver_order_update(sat_solver* s, int v) // updateorder
+{
+ order_update(s, v);
+}
+
//=================================================================================================
// Activity functions:
@@ -232,6 +251,18 @@ static inline void act_var_bump(sat_solver* s, int v) {
}
+void sat_solver_act_var_bump_factor(sat_solver* s, int v, double factor) {
+ double* activity = s->activity;
+ if ((activity[v] += s->var_inc * factor) > 1e100)
+ act_var_rescale(s);
+
+ //printf("bump %d %f\n", v-1, activity[v]);
+
+ if (s->orderpos[v] != -1)
+ order_update(s,v);
+
+}
+
static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; }
static inline void act_clause_rescale(sat_solver* s) {
@@ -253,6 +284,7 @@ static inline void act_clause_bump(sat_solver* s, clause *c) {
static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; }
+double* sat_solver_activity(sat_solver* s) { return s->activity; }
//=================================================================================================
// Clause functions:
@@ -268,7 +300,13 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
assert(end - begin > 1);
assert(learnt >= 0 && learnt < 2);
size = end - begin;
- c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+// c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
+ c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+#else
+ c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
+#endif
+
c->size_learnt = (size << 1) | learnt;
assert(((unsigned int)c & 1) == 0);
@@ -317,7 +355,11 @@ static void clause_remove(sat_solver* s, clause* c)
s->stats.clauses_literals -= clause_size(c);
}
+#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
free(c);
+#else
+ Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
+#endif
}
@@ -833,6 +875,16 @@ static lbool sat_solver_search(sat_solver* s, int nof_conflicts, int nof_learnts
veci_delete(&learnt_clause);
return l_Undef; }
+ if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit ||
+ s->nInsLimit && s->stats.inspects > s->nInsLimit )
+ {
+ // Reached bound on number of conflicts:
+ s->progress_estimate = sat_solver_progress(s);
+ sat_solver_canceluntil(s,s->root_level);
+ veci_delete(&learnt_clause);
+ return l_Undef;
+ }
+
if (sat_solver_dlevel(s) == 0)
// Simplify the set of problem clauses:
sat_solver_simplify(s);
@@ -931,18 +983,27 @@ sat_solver* sat_solver_new(void)
s->stats.max_literals = 0;
s->stats.tot_literals = 0;
+#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
+ s->pMem = NULL;
+#else
+ s->pMem = Sat_MmStepStart( 10 );
+#endif
return s;
}
void sat_solver_delete(sat_solver* s)
{
+
+#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
int i;
for (i = 0; i < vecp_size(&s->clauses); i++)
free(vecp_begin(&s->clauses)[i]);
-
for (i = 0; i < vecp_size(&s->learnts); i++)
free(vecp_begin(&s->learnts)[i]);
+#else
+ Sat_MmStepStop( s->pMem, 0 );
+#endif
// delete vectors
vecp_delete(&s->clauses);
@@ -1065,14 +1126,26 @@ bool sat_solver_simplify(sat_solver* s)
}
-int sat_solver_solve(sat_solver* s, lit* begin, lit* end)
+int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal)
{
double nof_conflicts = 100;
double nof_learnts = sat_solver_nclauses(s) / 3;
lbool status = l_Undef;
lbool* values = s->assigns;
lit* i;
-
+
+ // set the external limits
+ s->nConfLimit = 0;
+ s->nInsLimit = 0;
+ if ( nConfLimit )
+ s->nConfLimit = s->stats.conflicts + nConfLimit;
+ if ( nInsLimit )
+ s->nInsLimit = s->stats.inspects + nInsLimit;
+ if ( nConfLimitGlobal && s->nConfLimit > nConfLimitGlobal )
+ s->nConfLimit = nConfLimitGlobal;
+ if ( nInsLimitGlobal && s->nInsLimit > nInsLimitGlobal )
+ s->nInsLimit = nInsLimitGlobal;
+
//printf("solve: "); printlits(begin, end); printf("\n");
for (i = begin; i < end; i++){
switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
@@ -1117,6 +1190,18 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end)
status = sat_solver_search(s,(int)nof_conflicts, (int)nof_learnts);
nof_conflicts *= 1.5;
nof_learnts *= 1.1;
+
+ // quit the loop if reached an external limit
+ if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
+ {
+// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
+ break;
+ }
+ if ( s->nInsLimit && s->stats.inspects > s->nInsLimit )
+ {
+// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
+ break;
+ }
}
if (s->verbosity >= 1)
printf("==============================================================================\n");
diff --git a/src/temp/ivy/satSolver.h b/src/temp/ivy/satSolver.h
index 401a28e7..a7ace8ed 100644
--- a/src/temp/ivy/satSolver.h
+++ b/src/temp/ivy/satSolver.h
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#endif
#include "satVec.h"
+#include "satMem.h"
//=================================================================================================
// Simple types:
@@ -70,7 +71,7 @@ extern void sat_solver_delete(sat_solver* s);
extern bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
extern bool sat_solver_simplify(sat_solver* s);
-extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end);
+extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal);
extern int sat_solver_nvars(sat_solver* s);
extern int sat_solver_nclauses(sat_solver* s);
@@ -78,6 +79,13 @@ extern int sat_solver_nconflicts(sat_solver* s);
extern void sat_solver_setnvars(sat_solver* s,int n);
+extern void sat_solver_order_clean(sat_solver* s);
+extern void sat_solver_order_unassigned(sat_solver* s, int v);
+extern void sat_solver_order_update(sat_solver* s, int v);
+
+extern double* sat_solver_activity(sat_solver* s);
+extern void sat_solver_act_var_bump_factor(sat_solver* s, int v, double factor);
+
struct stats_t
{
sint64 starts, decisions, propagations, inspects, conflicts;
@@ -136,6 +144,11 @@ struct sat_solver_t
int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
stats stats;
+
+ sint64 nConfLimit; // external limit on the number of conflicts
+ sint64 nInsLimit; // external limit on the number of implications
+
+ Sat_MmStep_t * pMem;
};
#endif
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-22 07:01:47 +0000