Skip to content

A
abc
Commit a6aec18a by Alan Mishchenko
Options

Version abc51225

parent 457e243e
Showing with 382 additions and 61 deletions
abc.opt
No preview for this file type
abc.rc
......@@ -74,4 +74,5 @@ alias compress "b; rw -l; rwz -l; b; rwz -l; b"
alias compress2 "b; rw -l; rf -l; b; rw -l; rwz -l; b; rfz -l; rwz -l; b"
alias choice "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
alias choice2 "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
alias try "st; fpga; miter; fraig -rp"
mcnc_temp.genlib_temp 0 → 100644
# The genlib library "mcnc_temp.genlib".
GATE inv1 1.00 O=!a;
PIN a INV 1 999 0.90 0.00 0.90 0.00
GATE inv2 2.00 O=!a;
PIN a INV 2 999 1.00 0.00 1.00 0.00
GATE inv3 3.00 O=!a;
PIN a INV 3 999 1.10 0.00 1.10 0.00
GATE inv4 4.00 O=!a;
PIN a INV 4 999 1.20 0.00 1.20 0.00
GATE nand2 2.00 O=!(a*b);
PIN a INV 1 999 1.00 0.00 1.00 0.00
PIN b INV 1 999 1.00 0.00 1.00 0.00
GATE nand3 3.00 O=!(a*b*c);
PIN a INV 1 999 1.10 0.00 1.10 0.00
PIN b INV 1 999 1.10 0.00 1.10 0.00
PIN c INV 1 999 1.10 0.00 1.10 0.00
GATE nand4 4.00 O=!(a*b*c*d);
PIN a INV 1 999 1.40 0.00 1.40 0.00
PIN b INV 1 999 1.40 0.00 1.40 0.00
PIN c INV 1 999 1.40 0.00 1.40 0.00
PIN d INV 1 999 1.40 0.00 1.40 0.00
GATE nor2 2.00 O=!(a+b);
PIN a INV 1 999 1.40 0.00 1.40 0.00
PIN b INV 1 999 1.40 0.00 1.40 0.00
GATE nor3 3.00 O=!(a+b+c);
PIN a INV 1 999 2.40 0.00 2.40 0.00
PIN b INV 1 999 2.40 0.00 2.40 0.00
PIN c INV 1 999 2.40 0.00 2.40 0.00
GATE nor4 4.00 O=!(a+b+c+d);
PIN a INV 1 999 3.80 0.00 3.80 0.00
PIN b INV 1 999 3.80 0.00 3.80 0.00
PIN c INV 1 999 3.80 0.00 3.80 0.00
PIN d INV 1 999 3.80 0.00 3.80 0.00
GATE xora 5.00 O=a*!b+!a*b;
PIN a UNKNOWN 2 999 1.90 0.00 1.90 0.00
PIN b UNKNOWN 2 999 1.90 0.00 1.90 0.00
GATE xorb 5.00 O=!(a*b+!a*!b);
PIN a UNKNOWN 2 999 1.90 0.00 1.90 0.00
PIN b UNKNOWN 2 999 1.90 0.00 1.90 0.00
GATE xnora 5.00 O=a*b+!a*!b;
PIN a UNKNOWN 2 999 2.10 0.00 2.10 0.00
PIN b UNKNOWN 2 999 2.10 0.00 2.10 0.00
GATE xnorb 5.00 O=!(!a*b+a*!b);
PIN a UNKNOWN 2 999 2.10 0.00 2.10 0.00
PIN b UNKNOWN 2 999 2.10 0.00 2.10 0.00
GATE aoi21 3.00 O=!(a*b+c);
PIN a INV 1 999 1.60 0.00 1.60 0.00
PIN b INV 1 999 1.60 0.00 1.60 0.00
PIN c INV 1 999 1.60 0.00 1.60 0.00
GATE aoi22 4.00 O=!(a*b+c*d);
PIN a INV 1 999 2.00 0.00 2.00 0.00
PIN b INV 1 999 2.00 0.00 2.00 0.00
PIN c INV 1 999 2.00 0.00 2.00 0.00
PIN d INV 1 999 2.00 0.00 2.00 0.00
GATE oai21 3.00 O=!((a+b)*c);
PIN a INV 1 999 1.60 0.00 1.60 0.00
PIN b INV 1 999 1.60 0.00 1.60 0.00
PIN c INV 1 999 1.60 0.00 1.60 0.00
GATE oai22 4.00 O=!((a+b)*(c+d));
PIN a INV 1 999 2.00 0.00 2.00 0.00
PIN b INV 1 999 2.00 0.00 2.00 0.00
PIN c INV 1 999 2.00 0.00 2.00 0.00
PIN d INV 1 999 2.00 0.00 2.00 0.00
GATE buf 1.00 O=a;
PIN a NONINV 1 999 1.00 0.00 1.00 0.00
GATE zero 0.00 O=CONST0;
GATE one 0.00 O=CONST1;
mcnc_temp.super 0 → 100644
#
# Supergate library derived for "mcnc_temp.genlib_temp" on Sun Dec 25 06:29:48 2005.
#
# Command line: "super -i 5 -l 1 -d 10000000.00 -a 10000000.00 -t 100 mcnc_temp.genlib_temp".
#
# The number of inputs = 5.
# The number of levels = 1.
# The maximum delay = 10000000.00.
# The maximum area = 10000000.00.
# The maximum runtime (sec) = 100.
#
# The number of attempts = 860.
# The number of supergates = 20.
# The number of functions = 0.
# The total functions = 4294967296 (2^32).
#
# Generation time (sec) = 0.01.
#
mcnc_temp.genlib_temp
5
20
25
* xorb 1 0
* nor4 2 1 0 3
* nor3 2 1 0
* oai22 2 1 0 3
* oai22 2 0 1 3
* aoi21 1 0 2
* aoi22 2 3 1 0
* nor2 1 0
* oai22 2 3 1 0
* aoi21 2 0 1
* aoi22 2 0 1 3
* aoi21 2 1 0
* aoi22 2 1 0 3
* oai21 1 0 2
* oai21 2 0 1
* oai21 2 1 0
* nand2 1 0
* nand3 2 1 0
* nand4 2 1 0 3
* xnora 1 0
src/base/abc/abcAig.c
......@@ -572,7 +572,28 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
return Abc_AigOr( pMan, Abc_AigAnd(pMan, p0, Abc_ObjNot(p1)),
Abc_AigAnd(pMan, p1, Abc_ObjNot(p0)) );
}
/**Function*************************************************************
Synopsis [Implements the miter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_AigMiter_rec( Abc_Aig_t * pMan, Abc_Obj_t ** ppObjs, int nObjs )
{
Abc_Obj_t * pObj1, * pObj2;
if ( nObjs == 1 )
return ppObjs[0];
pObj1 = Abc_AigMiter_rec( pMan, ppObjs, nObjs/2 );
pObj2 = Abc_AigMiter_rec( pMan, ppObjs + nObjs/2, nObjs - nObjs/2 );
return Abc_AigOr( pMan, pObj1, pObj2 );
}
/**Function*************************************************************
Synopsis [Implements the miter.]
......@@ -586,6 +607,30 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
***********************************************************************/
Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
{
int i;
if ( vPairs->nSize == 0 )
return Abc_ObjNot( Abc_NtkConst1(pMan->pNtkAig) );
assert( vPairs->nSize % 2 == 0 );
// go through the cubes of the node's SOP
for ( i = 0; i < vPairs->nSize; i += 2 )
vPairs->pArray[i/2] = Abc_AigXor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] );
vPairs->nSize = vPairs->nSize/2;
return Abc_AigMiter_rec( pMan, (Abc_Obj_t **)vPairs->pArray, vPairs->nSize );
}
/**Function*************************************************************
Synopsis [Implements the miter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_AigMiter2( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
{
Abc_Obj_t * pMiter, * pXor;
int i;
assert( vPairs->nSize % 2 == 0 );
......
src/base/abci/abc.c
......@@ -2868,6 +2868,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
return 0;
}
if ( Abc_NtkIsSeq(pNtk) )
{
fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" );
return 0;
}
/*
if ( !Abc_NtkIsLogic(pNtk) )
{
fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" );
......@@ -2877,19 +2884,35 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkUnmap(pNtk);
if ( Abc_NtkIsSopLogic(pNtk) )
Abc_NtkSopToBdd(pNtk);
RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose );
if ( RetValue == -1 )
printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
else if ( RetValue == 0 )
printf( "The miter is SATISFIABLE.\n" );
*/
if ( Abc_NtkIsStrash(pNtk) )
{
RetValue = Abc_NtkMiterSat2( pNtk, nSeconds, fVerbose );
if ( RetValue == -1 )
printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
else if ( RetValue == 0 )
printf( "The miter is SATISFIABLE.\n" );
else
printf( "The miter is UNSATISFIABLE.\n" );
}
else
printf( "The miter is UNSATISFIABLE.\n" );
{
Abc_Ntk_t * pTemp;
pTemp = Abc_NtkStrash( pNtk, 0, 0 );
RetValue = Abc_NtkMiterSat2( pTemp, nSeconds, fVerbose );
if ( RetValue == -1 )
printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
else if ( RetValue == 0 )
printf( "The miter is SATISFIABLE.\n" );
else
printf( "The miter is UNSATISFIABLE.\n" );
Abc_NtkDelete( pTemp );
}
return 0;
usage:
fprintf( pErr, "usage: sat [-T num] [-vh]\n" );
fprintf( pErr, "\t solves the miter\n" );
fprintf( pErr, "\t solves the combinational miter\n" );
fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
......@@ -3722,11 +3745,11 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// run the command
pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 0, 0, fUseInvs, fVerbose );
pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
return 1;
return 0;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
......@@ -3788,9 +3811,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
// Abc_NtkDeriveEsops( pNtk );
// Abc_NtkXyz( pNtk, 128, 0, 0, 0 );
printf( "This command is currently not used.\n" );
Abc_NtkTestEsop( pNtk );
// Abc_NtkTestSop( pNtk );
// printf( "This command is currently not used.\n" );
/*
// run the command
......
src/base/abci/abcVerify.c
......@@ -148,6 +148,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
Fraig_ParamsSetDefault( &Params );
Params.fVerbose = fVerbose;
Params.nSeconds = nSeconds;
Params.fFuncRed = 0;
Params.nPatsRand = 0;
Params.nPatsDyna = 0;
pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 );
Fraig_ManProveMiter( pMan );
......@@ -325,6 +328,9 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
Fraig_ParamsSetDefault( &Params );
Params.fVerbose = fVerbose;
Params.nSeconds = nSeconds;
Params.fFuncRed = 0;
Params.nPatsRand = 0;
Params.nPatsDyna = 0;
pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 );
Fraig_ManProveMiter( pMan );
......
src/opt/xyz/xyz.h
......@@ -46,6 +46,8 @@ struct Xyz_Man_t_
Vec_Ptr_t * vObjStrs; // object structures
void * pMemory; // memory for the internal data strctures
Min_Man_t * pManMin; // the cub manager
int fUseEsop; // enables ESOPs
int fUseSop; // enables SOPs
// arrays to map local variables
Vec_Int_t * vComTo0; // mapping of common variables into first fanin
Vec_Int_t * vComTo1; // mapping of common variables into second fanin
......
src/opt/xyz/xyzInt.h
......@@ -81,10 +81,10 @@ static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uDa
/*=== xyzMinEsop.c ==========================================================*/
extern void Min_EsopMinimize( Min_Man_t * p );
extern int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
extern void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
/*=== xyzMinSop.c ==========================================================*/
extern void Min_SopMinimize( Min_Man_t * p );
extern int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
extern void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
/*=== xyzMinMan.c ==========================================================*/
extern Min_Man_t * Min_ManAlloc( int nVars );
extern void Min_ManClean( Min_Man_t * p, int nSupp );
......@@ -92,8 +92,10 @@ extern void Min_ManFree( Min_Man_t * p );
/*=== xyzMinUtil.c ==========================================================*/
extern void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube );
extern void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover );
extern void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p );
extern void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop );
extern void Min_CoverCheck( Min_Man_t * p );
extern int Min_CubeCheck( Min_Cube_t * pCube );
extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize );
extern void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover );
extern int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover );
......@@ -161,6 +163,7 @@ static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy )
Min_Cube_t * pCube;
pCube = Min_CubeAlloc( p );
memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords );
pCube->nLits = pCopy->nLits;
return pCube;
}
......@@ -538,6 +541,24 @@ static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, M
}
}
/**Function*************************************************************
Synopsis [Transforms the cube into the result of distance-1 merging.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Min_CubesTransformOr( Min_Cube_t * pCube, Min_Cube_t * pDist )
{
int w;
for ( w = 0; w < (int)pCube->nWords; w++ )
pCube->uData[w] |= pDist->uData[w];
}
/**Function*************************************************************
......@@ -579,7 +600,7 @@ static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCove
/**Function*************************************************************
Synopsis [Check if the cube is equal or dist1 or contained.]
Synopsis [Returns 1 if the given cube is contained in one of the cubes of the cover.]
Description []
......@@ -588,42 +609,32 @@ static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCove
SeeAlso []
***********************************************************************/
static inline int Min_CubeIsEqualOrSubsumed( Min_Man_t * p, Min_Cube_t * pNew )
static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube )
{
Min_Cube_t * pCube;
Min_Cube_t * pThis;
int i;
// check identity
Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube )
if ( Min_CubesAreEqual( pCube, pNew ) )
/*
// this cube cannot be equal to any cube
Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
{
if ( Min_CubesAreEqual( pCube, pThis ) )
{
Min_CubeWrite( stdout, pCube );
assert( 0 );
}
}
*/
// try to find a containing cube
for ( i = 0; i <= (int)pCube->nLits; i++ )
Min_CoverForEachCube( p->ppStore[i], pThis )
{
// skip the bubble
if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
return 1;
// check containment
for ( i = 0; i < (int)pNew->nLits; i++ )
Min_CoverForEachCube( p->ppStore[i], pCube )
if ( Min_CubeIsContained( pCube, pNew ) )
return 1;
}
return 0;
}
/**Function*************************************************************
Synopsis [Check if the cube is equal or dist1 or contained.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Min_Cube_t * Min_CubeHasDistanceOne( Min_Man_t * p, Min_Cube_t * pNew )
{
Min_Cube_t * pCube;
Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube )
if ( Min_CubesDistOne( pCube, pNew, NULL ) )
return pCube;
return NULL;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/opt/xyz/xyzMinEsop.c
......@@ -62,7 +62,11 @@ void Min_EsopMinimize( Min_Man_t * p )
Synopsis [Performs one round of rewriting using distance 2 cubes.]
Description []
Description [The weakness of this procedure is that it tries each cube
with only one distance-2 cube. If this pair does not lead to improvement
the cube is inserted into the cover anyhow, and we try another pair.
A possible improvement would be to try this cube with all distance-2
cubes, until an improvement is found, or until all such cubes are tried.]
SideEffects []
......@@ -162,8 +166,8 @@ void Min_EsopRewrite( Min_Man_t * p )
// add the cubes
nCubesOld = p->nCubes;
while ( Min_EsopAddCube( p, pCube ) );
while ( Min_EsopAddCube( p, pThis ) );
Min_EsopAddCube( p, pCube );
Min_EsopAddCube( p, pThis );
// check if the cubes were absorbed
if ( p->nCubes < nCubesOld + 2 )
continue;
......@@ -191,8 +195,8 @@ void Min_EsopRewrite( Min_Man_t * p )
pThis->nLits += (v11 != 3);
// add them anyhow
while ( Min_EsopAddCube( p, pCube ) );
while ( Min_EsopAddCube( p, pThis ) );
Min_EsopAddCube( p, pCube );
Min_EsopAddCube( p, pThis );
}
// printf( "Pairs = %d ", nPairs );
}
......@@ -201,8 +205,8 @@ void Min_EsopRewrite( Min_Man_t * p )
Synopsis [Adds the cube to storage.]
Description [If the distance one cube is found, returns the transformed
cube. If there is no distance one, adds the given cube to storage.
Description [Returns 0 if the cube is added or removed. Returns 1
if the cube is glued with some other cube and has to be added again.
Do not forget to clean the storage!]
SideEffects []
......@@ -210,7 +214,7 @@ void Min_EsopRewrite( Min_Man_t * p )
SeeAlso []
***********************************************************************/
int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
int Min_EsopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
{
Min_Cube_t * pThis, ** ppPrev;
// try to find the identical cube
......@@ -270,6 +274,24 @@ int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
return 0;
}
/**Function*************************************************************
Synopsis [Adds the cube to storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
{
assert( pCube != p->pBubble );
assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
while ( Min_EsopAddCubeInt( p, pCube ) );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/opt/xyz/xyzMinMan.c
......@@ -62,6 +62,7 @@ Min_Man_t * Min_ManAlloc( int nVars )
pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 );
pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 );
pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 );
Min_ManClean( pMan, nVars );
return pMan;
}
......
src/opt/xyz/xyzMinUtil.c
......@@ -92,13 +92,44 @@ void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover )
SeeAlso []
***********************************************************************/
void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p )
{
Min_Cube_t * pCube;
int i;
for ( i = 0; i <= p->nVars; i++ )
{
Min_CoverForEachCube( p->ppStore[i], pCube )
{
printf( "%2d : ", i );
if ( pCube == p->pBubble )
{
printf( "Bubble\n" );
continue;
}
Min_CubeWrite( pFile, pCube );
}
}
printf( "\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
{
char Buffer[1000];
Min_Cube_t * pCube;
FILE * pFile;
int i;
sprintf( Buffer, "%s.esop", pName );
sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" );
for ( i = strlen(Buffer) - 1; i >= 0; i-- )
if ( Buffer[i] == '<' || Buffer[i] == '>' )
Buffer[i] = '_';
......@@ -116,7 +147,7 @@ void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
/**Function*************************************************************
Synopsis [Performs one round of rewriting using distance 2 cubes.]
Synopsis []
Description []
......@@ -137,6 +168,26 @@ void Min_CoverCheck( Min_Man_t * p )
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Min_CubeCheck( Min_Cube_t * pCube )
{
int i;
for ( i = 0; i < (int)pCube->nVars; i++ )
if ( Min_CubeGetVar( pCube, i ) == 0 )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Converts the cover from the sorted structure.]
Description []
......@@ -158,6 +209,7 @@ Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize )
assert( i == (int)pCube->nLits );
*ppTail = pCube;
ppTail = &pCube->pNext;
assert( pCube->uData[0] ); // not a bubble
}
}
*ppTail = NULL;
......
src/sat/asat/solver.h
......@@ -52,8 +52,9 @@ static const lbool l_Undef = 0;
static const lbool l_True = 1;
static const lbool l_False = -1;
static inline lit neg (lit l) { return l ^ 1; }
static inline lit toLit (int v) { return v + v; }
static inline lit neg (lit l) { return l ^ 1; }
static inline lit toLit (int v) { return v + v; }
static inline lit toLitCond (int v, int c) { return v + v + (int)(c != 0); }
//=================================================================================================
// Public interface:
......
src/sat/fraig/fraigCanon.c
......@@ -68,7 +68,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
return p1;
return Fraig_Not(pMan->pConst1);
}
/*
// check for less trivial cases
if ( Fraig_IsComplement(p1) )
{
......@@ -125,7 +125,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
return Fraig_Not(pMan->pConst1);
}
}
*/
// perform level-one structural hashing
if ( Fraig_HashTableLookupS( pMan, p1, p2, &pNodeNew ) ) // the node with these children is found
{
......
src/sat/fraig/fraigSat.c
......@@ -41,6 +41,8 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i );
// The best way seems to be fanins followed by fanouts. Slight changes to this order
// leads to big degradation in quality.
static int nMuxes;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -105,7 +107,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
}
if ( p->fVerboseP )
{
PRT( "Final miter proof time", clock() - clk );
// PRT( "Final miter proof time", clock() - clk );
}
}
......@@ -195,6 +197,8 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
}
*/
nMuxes = 0;
// get the logic cone
clk = clock();
......@@ -202,6 +206,9 @@ clk = clock();
// Fraig_PrepareCones( p, pOld, pNew );
p->timeTrav += clock() - clk;
// printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) );
// PRT( "Time", clock() - clk );
if ( fVerbose )
printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
......@@ -226,6 +233,8 @@ clk = clock();
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
p->timeSat += clock() - clk;
Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
if ( RetValue1 == MSAT_FALSE )
{
//p->time1 += clock() - clk;
......@@ -284,6 +293,7 @@ p->time3 += clock() - clk;
clk = clock();
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
p->timeSat += clock() - clk;
if ( RetValue1 == MSAT_FALSE )
{
//p->time1 += clock() - clk;
......@@ -552,6 +562,7 @@ void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t *
Fraig_PrepareCones_rec( pMan, pNew );
Fraig_PrepareCones_rec( pMan, pOld );
/*
nVars = Msat_IntVecReadSize( pMan->vVarsInt );
pVars = Msat_IntVecReadArray( pMan->vVarsInt );
......@@ -715,6 +726,8 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t
Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) );
Fraig_SupergateAddClausesMux( pMan, pNode );
// Fraig_DetectFanoutFreeConeMux( pMan, pNode );
nMuxes++;
}
else
{
......@@ -1057,6 +1070,12 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode )
// t + e + f'
// t' + e' + f
if ( VarT == VarE )
{
// assert( fCompT == !fCompE );
return;
}
Msat_IntVecClear( p->vProj );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) );
......@@ -1069,6 +1088,7 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode )
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) );
RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
assert( RetValue );
}
......
src/sat/msat/msat.h
......@@ -87,6 +87,7 @@ extern void Msat_SolverPrintClauses( Msat_Solver_t * p );
extern void Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName );
// access to the solver internal data
extern int Msat_SolverReadVarNum( Msat_Solver_t * p );
extern int Msat_SolverReadClauseNum( Msat_Solver_t * p );
extern int Msat_SolverReadVarAllocNum( Msat_Solver_t * p );
extern int * Msat_SolverReadAssignsArray( Msat_Solver_t * p );
extern int * Msat_SolverReadModelArray( Msat_Solver_t * p );
......
src/sat/msat/msatClause.c
......@@ -82,6 +82,10 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
// nSeenId - 1 stands for negative
// nSeenId stands for positive
// Remove false literals
// there is a bug here!!!!
// when the same var in opposite polarities is given, it drops one polarity!!!
for ( i = j = 0; i < nLits; i++ ) {
// get the corresponding variable
Var = MSAT_LIT2VAR(pLits[i]);
......@@ -190,6 +194,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
{
Msat_SolverVarBumpActivity( p, pLits[i] );
// Msat_SolverVarBumpActivity( p, pLits[i] );
p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++;
}
}
......
src/sat/msat/msatInt.h
......@@ -151,6 +151,7 @@ struct Msat_Solver_t_
int nSeenId; // the id of current seeing
Msat_IntVec_t * vReason; // the temporary array of literals
Msat_IntVec_t * vTemp; // the temporary array of literals
int * pFreq; // the number of times each var participated in conflicts
// the memory manager
Msat_MmStep_t * pMem;
......
src/sat/msat/msatSolverApi.c
......@@ -42,6 +42,7 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
***********************************************************************/
int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; }
int Msat_SolverReadClauseNum( Msat_Solver_t * p ) { return p->nClauses; }
int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc;}
int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); }
int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; }
......
src/sat/msat/msatSolverCore.c
......@@ -140,6 +140,9 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
int64 nConflictsOld = p->Stats.nConflicts;
int64 nDecisionsOld = p->Stats.nDecisions;
p->pFreq = ALLOC( int, p->nVarsAlloc );
memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
if ( vAssumps )
{
int * pAssumps, nAssumps, i;
......@@ -181,6 +184,23 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
}
Msat_SolverCancelUntil( p, 0 );
p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
/*
PRT( "True solver runtime", clock() - timeStart );
// print the statistics
{
int i, Counter = 0;
for ( i = 0; i < p->nVars; i++ )
if ( p->pFreq[i] > 0 )
{
printf( "%d ", p->pFreq[i] );
Counter++;
}
if ( Counter )
printf( "\n" );
printf( "Total = %d. Used = %d. Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
PRT( "Time", clock() - timeStart );
}
*/
return Status;
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment