Skip to content

A
abc
Commit 689cbe90 by Alan Mishchenko
Options

Version abc80927

parent 91effd81
Showing with 2201 additions and 22 deletions
abc.dsp
......@@ -3270,6 +3270,10 @@ SOURCE=.\src\aig\saig\saig.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigAbs.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigBmc.c
# End Source File
# Begin Source File
......@@ -3290,6 +3294,10 @@ SOURCE=.\src\aig\saig\saigIoa.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigLoc.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigMiter.c
# End Source File
# Begin Source File
......@@ -3488,6 +3496,10 @@ SOURCE=.\src\aig\ssw\sswSimSat.c
SOURCE=.\src\aig\ssw\sswSweep.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswUnique.c
# End Source File
# End Group
# End Group
# End Group
......
src/aig/aig/aig.h
......@@ -480,6 +480,7 @@ extern int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper
/*=== aigDup.c ==========================================================*/
extern Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vPos );
extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p );
......
src/aig/aig/aigDup.c
......@@ -194,6 +194,43 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
/**Function*************************************************************
Synopsis [Duplicates part of the AIG manager.]
Description [Orders nodes as follows: PIs, ANDs, POs.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vPos )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjNew;
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
Vec_PtrForEachEntry( vPis, pObj, i )
pObj->pData = Aig_ObjCreatePi( pNew );
// duplicate internal nodes
Vec_PtrForEachEntry( vPos, pObj, i )
{
pObjNew = Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
Aig_ObjCreatePo( pNew, pObjNew );
}
Aig_ManSetRegNum( pNew, 0 );
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupSimple(): The check has failed.\n" );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager.]
Description [Assumes topological ordering of the nodes.]
......
src/aig/fra/fraSec.c
......@@ -56,6 +56,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
p->fInterpolation = 1; // enables interpolation
p->fReachability = 1; // enables BDD based reachability
p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove
p->fUseNewProver = 0; // enables new prover
p->fSilent = 0; // disables all output
p->fVerbose = 0; // enables verbose reporting of statistics
p->fVeryVerbose = 0; // enables very verbose reporting
......
src/aig/saig/module.make
SRC += src/aig/saig/saigBmc.c \
SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigBmc.c \
src/aig/saig/saigCone.c \
src/aig/saig/saigDup.c \
src/aig/saig/saigHaig.c \
src/aig/saig/saigIoa.c \
src/aig/saig/saigLoc.c \
src/aig/saig/saigMiter.c \
src/aig/saig/saigPhase.c \
src/aig/saig/saigRetFwd.c \
......
src/aig/saig/saig.h
......@@ -84,6 +84,7 @@ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int n
extern void Saig_ManPrintCones( Aig_Man_t * p );
/*=== saigDup.c ==========================================================*/
extern Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * p );
extern Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
/*=== saigHaig.c ==========================================================*/
extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
/*=== saigIoa.c ==========================================================*/
......
src/aig/saig/saigAbs.c 0 → 100644
/**CFile****************************************************************
FileName [saigAbs.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Proof-based abstraction.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
#include "cnf.h"
#include "satSolver.h"
#include "satStore.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline Aig_Obj_t * Saig_ObjFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i ) { return ppMap[nFrames*pObj->Id + i]; }
static inline void Saig_ObjSetFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + i] = pNode; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Create timeframes of the manager for BMC.]
Description [The resulting manager is combinational. The only PO is
the output of the last frame.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t *** pppMap )
{
Aig_Man_t * pFrames;
Aig_Obj_t ** ppMap;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, f;
assert( Saig_ManRegNum(pAig) > 0 );
// start the mapping
ppMap = *pppMap = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) * nFrames );
// start the manager
pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
// create variables for register outputs
Saig_ManForEachLo( pAig, pObj, i )
{
pObj->pData = Aig_ManConst0( pFrames );
Saig_ObjSetFrame( ppMap, nFrames, pObj, 0, pObj->pData );
}
// add timeframes
for ( f = 0; f < nFrames; f++ )
{
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
Saig_ObjSetFrame( ppMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pAig)->pData );
// create PI nodes for this frame
Saig_ManForEachPi( pAig, pObj, i )
{
pObj->pData = Aig_ObjCreatePi( pFrames );
Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
}
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
{
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
}
// create POs for this frame
if ( f == nFrames - 1 )
{
Saig_ManForEachPo( pAig, pObj, i )
{
pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
}
break;
}
// save register inputs
Saig_ManForEachLi( pAig, pObj, i )
{
pObj->pData = Aig_ObjChild0Copy(pObj);
Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
}
// transfer to register outputs
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
{
pObjLo->pData = pObjLi->pData;
Saig_ObjSetFrame( ppMap, nFrames, pObjLo, f, pObjLo->pData );
}
}
Aig_ManCleanup( pFrames );
// remove mapping for the nodes that are no longer there
for ( i = 0; i < Aig_ManObjNumMax(pAig) * nFrames; i++ )
if ( ppMap[i] && Aig_ObjIsNone( Aig_Regular(ppMap[i]) ) )
ppMap[i] = NULL;
return pFrames;
}
/**Function*************************************************************
Synopsis [Finds the set of variables involved in the UNSAT core.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nConfMax, int fVerbose )
{
void * pSatCnf;
Intp_Man_t * pManProof;
sat_solver * pSat;
Vec_Int_t * vCore;
int * pClause1, * pClause2, * pLit, * pVars, iClause, nVars;
int i, RetValue;
// create the SAT solver
pSat = sat_solver_new();
sat_solver_store_alloc( pSat );
sat_solver_setnvars( pSat, pCnf->nVars );
for ( i = 0; i < pCnf->nClauses; i++ )
{
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
{
printf( "The BMC problem is trivially UNSAT.\n" );
sat_solver_delete( pSat );
return NULL;
}
}
sat_solver_store_mark_roots( pSat );
// solve the problem
RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue == l_Undef )
{
printf( "Conflict limit is reached.\n" );
sat_solver_delete( pSat );
return NULL;
}
if ( RetValue == l_True )
{
printf( "The BMC problem is SAT.\n" );
sat_solver_delete( pSat );
return NULL;
}
printf( "SAT solver returned UNSAT after %d conflicts.\n", pSat->stats.conflicts );
assert( RetValue == l_False );
pSatCnf = sat_solver_store_release( pSat );
sat_solver_delete( pSat );
// derive the UNSAT core
pManProof = Intp_ManAlloc();
vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVerbose );
Intp_ManFree( pManProof );
Sto_ManFree( pSatCnf );
// derive the set of variables on which the core depends
// collect the variable numbers
nVars = 0;
pVars = ALLOC( int, pCnf->nVars );
memset( pVars, 0, sizeof(int) * pCnf->nVars );
Vec_IntForEachEntry( vCore, iClause, i )
{
pClause1 = pCnf->pClauses[iClause];
pClause2 = pCnf->pClauses[iClause+1];
for ( pLit = pClause1; pLit < pClause2; pLit++ )
{
if ( pVars[ (*pLit) >> 1 ] == 0 )
nVars++;
pVars[ (*pLit) >> 1 ] = 1;
if ( fVerbose )
printf( "%s%d ", ((*pLit) & 1)? "-" : "+", (*pLit) >> 1 );
}
if ( fVerbose )
printf( "\n" );
}
Vec_IntFree( vCore );
return pVars;
}
/**Function*************************************************************
Synopsis [Labels nodes with the given CNF variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManMarkIntoPresentVars_rec( Aig_Obj_t * pObj, Cnf_Dat_t * pCnf, int iVar )
{
int iVarThis = pCnf->pVarNums[pObj->Id];
if ( iVarThis >= 0 && iVarThis != iVar )
return;
assert( Aig_ObjIsNode(pObj) );
Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin0(pObj), pCnf, iVar );
Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin1(pObj), pCnf, iVar );
pCnf->pVarNums[pObj->Id] = iVar;
}
/**Function*************************************************************
Synopsis [Performs proof-based abstraction using BMC of the given depth.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose )
{
Cnf_Dat_t * pCnf;
Vec_Int_t * vFlops;
Aig_Man_t * pFrames, * pResult;
Aig_Obj_t ** ppAigToFrames;
Aig_Obj_t * pObj, * pObjFrame;
int f, i, * pUnsatCoreVars, clk = clock();
assert( Saig_ManPoNum(p) == 1 );
Aig_ManSetPioNumbers( p );
if ( fVerbose )
printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax );
// create the timeframes
pFrames = Saig_ManFramesBmcLast( p, nFrames, &ppAigToFrames );
// convert them into CNF
// pCnf = Cnf_Derive( pFrames, 0 );
pCnf = Cnf_DeriveSimple( pFrames, 0 );
// collect CNF variables involved in UNSAT core
pUnsatCoreVars = Saig_ManFindUnsatVariables( pCnf, nConfMax, 0 );
if ( pUnsatCoreVars == NULL )
{
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
return NULL;
}
if ( fVerbose )
{
int Counter = 0;
for ( i = 0; i < pCnf->nVars; i++ )
Counter += pUnsatCoreVars[i];
printf( "The number of variables in the UNSAT core is %d (out of %d).\n", Counter, pCnf->nVars );
}
// map other nodes into existing CNF variables
Aig_ManForEachNode( pFrames, pObj, i )
if ( pCnf->pVarNums[pObj->Id] >= 0 )
Saig_ManMarkIntoPresentVars_rec( pObj, pCnf, pCnf->pVarNums[pObj->Id] );
// collect relevant registers
for ( f = 0; f < nFrames; f++ )
{
Saig_ManForEachLo( p, pObj, i )
{
pObjFrame = Saig_ObjFrame( ppAigToFrames, nFrames, pObj, f );
if ( pObjFrame == NULL )
continue;
pObjFrame = Aig_Regular(pObjFrame);
if ( Aig_ObjIsConst1( pObjFrame ) )
continue;
assert( pCnf->pVarNums[pObjFrame->Id] >= 0 );
if ( pUnsatCoreVars[ pCnf->pVarNums[pObjFrame->Id] ] )
pObj->fMarkA = 1;
}
}
// collect the flops
vFlops = Vec_IntAlloc( 1000 );
Saig_ManForEachLo( p, pObj, i )
if ( pObj->fMarkA )
{
pObj->fMarkA = 0;
Vec_IntPush( vFlops, i );
}
if ( fVerbose )
{
printf( "The number of relevant registers is %d (out of %d).\n", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
PRT( "Time", clock() - clk );
}
// create the resulting AIG
pResult = Saig_ManAbstraction( p, vFlops );
// cleanup
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
free( ppAigToFrames );
free( pUnsatCoreVars );
Vec_IntFree( vFlops );
return pResult;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/saig/saigBmc.c
......@@ -34,8 +34,7 @@
Synopsis [Create timeframes of the manager for BMC.]
Description [The resulting manager is combinational. The primary inputs
corresponding to register outputs are ordered first. POs correspond to \
Description [The resulting manager is combinational. POs correspond to \
the property outputs in each time-frame.]
SideEffects []
......@@ -106,8 +105,7 @@ int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
Synopsis [Create timeframes of the manager for BMC.]
Description [The resulting manager is combinational. The primary inputs
corresponding to register outputs are ordered first. POs correspond to
Description [The resulting manager is combinational. POs correspond to
the property outputs in each time-frame.
The unrolling is stopped as soon as the number of nodes in the frames
exceeds the given maximum size.]
......
src/aig/saig/saigDup.c
......@@ -67,6 +67,66 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
return pAigNew;
}
/**Function*************************************************************
Synopsis [Numbers of flops included in the abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops )
{
Aig_Man_t * pAigNew;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, Entry;
// start the new manager
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
// label included flops
Vec_IntForEachEntry( vFlops, Entry, i )
{
pObjLi = Saig_ManLi( pAig, Entry );
assert( pObjLi->fMarkA == 0 );
pObjLi->fMarkA = 1;
pObjLo = Saig_ManLo( pAig, Entry );
assert( pObjLo->fMarkA == 0 );
pObjLo->fMarkA = 1;
}
// create variables for PIs
Aig_ManForEachPi( pAig, pObj, i )
if ( !pObj->fMarkA )
pObj->pData = Aig_ObjCreatePi( pAigNew );
// create variables for LOs
Aig_ManForEachPi( pAig, pObj, i )
if ( pObj->fMarkA )
{
pObj->fMarkA = 0;
pObj->pData = Aig_ObjCreatePi( pAigNew );
}
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create POs
Aig_ManForEachPo( pAig, pObj, i )
if ( !pObj->fMarkA )
Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
// create LIs
Aig_ManForEachPo( pAig, pObj, i )
if ( pObj->fMarkA )
{
pObj->fMarkA = 0;
Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
}
Aig_ManCleanup( pAigNew );
Aig_ManSetRegNum( pAigNew, Vec_IntSize(vFlops) );
return pAigNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/saig/saigLoc.c 0 → 100644
/**CFile****************************************************************
FileName [saigLoc.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Localization package.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigLoc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
#include "cnf.h"
#include "satSolver.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs localization by unrolling timeframes backward.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose )
{
sat_solver * pSat;
Vec_Int_t * vTopVarNums;
Vec_Ptr_t * vTop, * vBot;
Cnf_Dat_t * pCnfTop, * pCnfBot;
Aig_Man_t * pPartTop, * pPartBot;
Aig_Obj_t * pObj, * pObjBot;
int i, f, clk, Lits[2], status, RetValue, nSatVarNum, nConfPrev;
assert( Saig_ManPoNum(p) == 1 );
Aig_ManSetPioNumbers( p );
// start the top by including the PO
vBot = Vec_PtrAlloc( 100 );
vTop = Vec_PtrAlloc( 100 );
Vec_PtrPush( vTop, Aig_ManPo(p, 0) );
// create the manager composed of one PI/PO pair
pPartTop = Aig_ManStart( 10 );
Aig_ObjCreatePo( pPartTop, Aig_ObjCreatePi(pPartTop) );
pCnfTop = Cnf_Derive( pPartTop, 0 );
// start the array of CNF variables
vTopVarNums = Vec_IntAlloc( 100 );
Vec_IntPush( vTopVarNums, pCnfTop->pVarNums[Aig_ManPi(pPartTop,0)->Id] );
// start the solver
pSat = Cnf_DataWriteIntoSolver( pCnfTop, 1, 0 );
// iterate backward unrolling
RetValue = -1;
nSatVarNum = pCnfTop->nVars;
if ( fVerbose )
printf( "Localization parameters: FramesMax = %5d. ConflictMax = %6d.\n", nFramesMax, nConfMax );
for ( f = 0; ; f++ )
{
clk = clock();
// get the bottom
Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vTop), Vec_PtrSize(vTop), vBot );
// derive AIG for the part between top and bottom
pPartBot = Aig_ManDupSimpleDfsPart( p, vBot, vTop );
// convert it into CNF
pCnfBot = Cnf_Derive( pPartBot, Aig_ManPoNum(pPartBot) );
Cnf_DataLift( pCnfBot, nSatVarNum );
nSatVarNum += pCnfBot->nVars;
// stitch variables of top and bot
assert( Aig_ManPoNum(pPartBot) == Vec_IntSize(vTopVarNums) );
Aig_ManForEachPo( pPartBot, pObjBot, i )
{
Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i), 0 );
Lits[1] = toLitCond( pCnfBot->pVarNums[pObjBot->Id], 1 );
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
assert( 0 );
Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i), 1 );
Lits[1] = toLitCond( pCnfBot->pVarNums[pObjBot->Id], 0 );
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
assert( 0 );
}
// add CNF to the SAT solver
for ( i = 0; i < pCnfBot->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnfBot->pClauses[i], pCnfBot->pClauses[i+1] ) )
break;
if ( i < pCnfBot->nClauses )
{
// printf( "SAT solver became UNSAT after adding clauses.\n" );
RetValue = 1;
break;
}
// run the SAT solver
nConfPrev = pSat->stats.conflicts;
status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, 0, 0, 0 );
if ( fVerbose )
{
printf( "%3d : PI = %5d. PO = %5d. AIG = %5d. Var = %6d. Conf = %6d. ",
f+1, Aig_ManPiNum(pPartBot), Aig_ManPoNum(pPartBot), Aig_ManNodeNum(pPartBot),
nSatVarNum, pSat->stats.conflicts-nConfPrev );
PRT( "Time", clock() - clk );
}
if ( status == l_Undef )
break;
if ( status == l_False )
{
RetValue = 1;
break;
}
assert( status == l_True );
if ( f == nFramesMax - 1 )
break;
// the problem is SAT - add more clauses
// create new set of POs to derive new top
Vec_PtrClear( vTop );
Vec_IntClear( vTopVarNums );
Vec_PtrForEachEntry( vBot, pObj, i )
{
assert( Aig_ObjIsPi(pObj) );
if ( Saig_ObjIsLo(p, pObj) )
{
pObjBot = pObj->pData;
assert( pObjBot != NULL );
Vec_PtrPush( vTop, Saig_ObjLoToLi(p, pObj) );
Vec_IntPush( vTopVarNums, pCnfBot->pVarNums[pObjBot->Id] );
}
}
// remove old top and replace it by bottom
Aig_ManStop( pPartTop );
pPartTop = pPartBot;
pPartBot = NULL;
Cnf_DataFree( pCnfTop );
pCnfTop = pCnfBot;
pCnfBot = NULL;
}
// printf( "Completed %d interations.\n", f+1 );
// cleanup
sat_solver_delete( pSat );
Aig_ManStop( pPartTop );
Cnf_DataFree( pCnfTop );
Aig_ManStop( pPartBot );
Cnf_DataFree( pCnfBot );
Vec_IntFree( vTopVarNums );
Vec_PtrFree( vTop );
Vec_PtrFree( vBot );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ssw/module.make
......@@ -10,4 +10,5 @@ SRC += src/aig/ssw/sswAig.c \
src/aig/ssw/sswSat.c \
src/aig/ssw/sswSim.c \
src/aig/ssw/sswSimSat.c \
src/aig/ssw/sswSweep.c
src/aig/ssw/sswSweep.c \
src/aig/ssw/sswUnique.c
src/aig/ssw/ssw.h
......@@ -53,6 +53,7 @@ struct Ssw_Pars_t_
int fSkipCheck; // do not run equivalence check for unaffected cones
int fLatchCorr; // perform register correspondence
int fSemiFormal; // enable semiformal filtering
int fUniqueness; // enable uniqueness constraints
int fVerbose; // verbose stats
// optimized latch correspondence
int fLatchCorrOpt; // perform register correspondence (optimized)
......@@ -82,11 +83,15 @@ struct Ssw_Cex_t_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sswAbs.c ==========================================================*/
extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
/*=== sswCore.c ==========================================================*/
extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p );
extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswLoc.c ==========================================================*/
extern int Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose );
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPairs.c ===================================================*/
......
src/aig/ssw/sswCore.c
......@@ -45,7 +45,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->nPartSize = 0; // size of the partition
p->nOverSize = 0; // size of the overlap between partitions
p->nFramesK = 1; // the induction depth
p->nFramesAddSim = 2; // additional frames to simulate
p->nFramesAddSim = 0; // additional frames to simulate
p->nConstrs = 0; // treat the last nConstrs POs as seq constraints
p->nBTLimit = 1000; // conflict limit at a node
p->nMinDomSize = 100; // min clock domain considered for optimization
......@@ -53,6 +53,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->fSkipCheck = 0; // do not run equivalence check for unaffected cones
p->fLatchCorr = 0; // performs register correspondence
p->fSemiFormal = 0; // enable semiformal filtering
p->fUniqueness = 0; // enable uniqueness constraints
p->fVerbose = 0; // verbose stats
// latch correspondence
p->fLatchCorrOpt = 0; // performs optimized register correspondence
......@@ -153,9 +154,9 @@ clk = clock();
RetValue = Ssw_ManSweep( p );
if ( p->pPars->fVerbose )
{
printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ",
printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. U = %3d. F = %2d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nUniques, p->nSatFailsReal );
if ( p->pPars->fSkipCheck )
printf( "Use = %5d. Skip = %5d. ",
p->nRefUse, p->nRefSkip );
......@@ -165,7 +166,7 @@ clk = clock();
Ssw_ManCleanup( p );
if ( !RetValue )
break;
/*
{
static int Flag = 0;
if ( Flag++ == 4 && nIter == 4 )
......@@ -176,6 +177,7 @@ clk = clock();
Aig_ManStop( pSRed );
}
}
*/
}
p->pPars->nIters = nIter + 1;
......
src/aig/ssw/sswInt.h
......@@ -78,6 +78,10 @@ struct Ssw_Man_t_
int nRecycleCalls; // the number of calls since last recycling
int nRecycles; // the number of time SAT solver was recycled
int nConeMax; // the maximum cone size
// uniqueness
Vec_Ptr_t * vCommon; // the set of common variables in the logic cones
int iOutputLit; // the output literal of the uniqueness constaint
int nUniques; // the number of uniqueness constaints used
// sequential simulator
Ssw_Sml_t * pSml;
// counter example storage
......@@ -205,10 +209,13 @@ extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrame
extern void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
/*=== sswSweep.c ===================================================*/
extern int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc );
extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p );
/*=== sswUnique.c ===================================================*/
extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj );
extern int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 );
#ifdef __cplusplus
}
......
src/aig/ssw/sswMan.c
......@@ -59,6 +59,8 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// SAT solving (latch corr only)
p->vUsedNodes = Vec_PtrAlloc( 1000 );
p->vUsedPis = Vec_PtrAlloc( 1000 );
p->vCommon = Vec_PtrAlloc( 100 );
p->iOutputLit = -1;
// allocate storage for sim pattern
p->nPatWords = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
p->pPatWords = ALLOC( unsigned, p->nPatWords );
......@@ -190,6 +192,7 @@ void Ssw_ManStop( Ssw_Man_t * p )
Vec_PtrFree( p->vUsedNodes );
Vec_PtrFree( p->vUsedPis );
Vec_IntFree( p->vSatVars );
Vec_PtrFree( p->vCommon );
FREE( p->pNodeToFrames );
FREE( p->pPatWords );
free( p );
......
src/aig/ssw/sswSat.c
......@@ -42,7 +42,7 @@
int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
int nBTLimit = p->pPars->nBTLimit;
int pLits[2], RetValue, RetValue1, clk;//, status;
int pLits[3], nLits, RetValue, RetValue1, clk;//, status;
p->nSatCalls++;
// sanity checks
......@@ -59,8 +59,11 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
nLits = 2;
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
if ( p->iOutputLit > -1 )
pLits[nLits++] = p->iOutputLit;
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
......@@ -75,16 +78,19 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
}
clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
if ( nLits == 2 )
{
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
}
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
......@@ -109,8 +115,11 @@ p->timeSatUndec += clock() - clk;
// solve under assumptions
// A = 0; B = 1 OR A = 0; B = 0
nLits = 2;
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
if ( p->iOutputLit > -1 )
pLits[nLits++] = p->iOutputLit;
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
......@@ -124,16 +133,19 @@ p->timeSatUndec += clock() - clk;
}
clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
if ( nLits == 2 )
{
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
}
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
......
src/aig/ssw/sswSweep.c
......@@ -87,14 +87,15 @@ void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p )
SeeAlso []
***********************************************************************/
int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
{
Aig_Obj_t * pObjFraig;
int nVarNum, Value;
assert( Aig_ObjIsPi(pObj) );
// assert( Aig_ObjIsPi(pObj) );
pObjFraig = Ssw_ObjFrame( p, pObj, f );
nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
// Value = (Aig_IsComplement(pObjFraig) ^ ((!nVarNum)? 0 : sat_solver_var_value( p->pSat, nVarNum )));
// Value = (!nVarNum)? Aig_ManRandom(0) & 1 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
if ( p->pPars->fPolarFlip )
{
......@@ -120,7 +121,7 @@ void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Aig_ManForEachPi( p->pAig, pObj, i )
if ( Ssw_ManOriginalPiValue( p, pObj, f ) )
if ( Ssw_ManGetSatVarValue( p, pObj, f ) )
Aig_InfoSetBit( p->pPatWords, i );
}
......@@ -212,6 +213,18 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
// disproved the equivalence
Ssw_SmlSavePatternAig( p, f );
}
if ( !fBmc && p->pPars->fUniqueness && p->pPars->nFramesK > 1 &&
Ssw_ManUniqueOne( p, pObjRepr, pObj ) && p->iOutputLit == -1 )
{
if ( Ssw_ManUniqueAddConstraint( p, p->vCommon, 0, 1 ) )
{
int RetValue;
assert( p->iOutputLit > -1 );
RetValue = Ssw_ManSweepNode( p, pObj, f, 0 );
p->iOutputLit = -1;
return RetValue;
}
}
if ( p->pPars->nConstrs == 0 )
Ssw_ManResimulateWord( p, pObj, pObjRepr, f );
else
......@@ -300,6 +313,7 @@ int Ssw_ManSweep( Ssw_Man_t * p )
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
int nConstrPairs, clk, i, f;
int v;
// perform speculative reduction
clk = clock();
......@@ -330,6 +344,8 @@ clk = clock();
Ssw_ManSweepMarkRefinement( p );
p->timeMarkCones += clock() - clk;
//Ssw_ManUnique( p );
// map constants and PIs of the last frame
f = p->pPars->nFramesK;
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
......@@ -338,10 +354,18 @@ p->timeMarkCones += clock() - clk;
// make sure LOs are assigned
Saig_ManForEachLo( p->pAig, pObj, i )
assert( Ssw_ObjFrame( p, pObj, f ) != NULL );
////
// bring up the previous frames
if ( p->pPars->fUniqueness )
for ( v = 0; v < f; v++ )
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_CnfNodeAddToSolver( p, Aig_Regular(Ssw_ObjFrame(p, pObj, v)) );
////
// sweep internal nodes
p->fRefined = 0;
p->nSatFailsReal = 0;
p->nRefUse = p->nRefSkip = 0;
p->nUniques = 0;
Ssw_ClassesClearRefined( p->ppClasses );
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
......
src/aig/ssw/sswUnique.c 0 → 100644
/**CFile****************************************************************
FileName [sswSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [On-demand uniqueness constraints.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns the result of merging the two vectors.]
Description [Assumes that the vectors are sorted in the increasing order.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrTwoMerge( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
{
Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) );
pBeg = (Aig_Obj_t **)vArr->pArray;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
if ( (*pBeg1)->Id == (*pBeg2)->Id )
*pBeg++ = *pBeg1++, pBeg2++;
else if ( (*pBeg1)->Id < (*pBeg2)->Id )
*pBeg++ = *pBeg1++;
else
*pBeg++ = *pBeg2++;
}
while ( pBeg1 < pEnd1 )
*pBeg++ = *pBeg1++;
while ( pBeg2 < pEnd2 )
*pBeg++ = *pBeg2++;
vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
assert( vArr->nSize <= vArr->nCap );
assert( vArr->nSize >= vArr1->nSize );
assert( vArr->nSize >= vArr2->nSize );
}
/**Function*************************************************************
Synopsis [Returns the result of merging the two vectors.]
Description [Assumes that the vectors are sorted in the increasing order.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrTwoCommon( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
{
Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
Vec_PtrGrow( vArr, AIG_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
pBeg = (Aig_Obj_t **)vArr->pArray;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
if ( (*pBeg1)->Id == (*pBeg2)->Id )
*pBeg++ = *pBeg1++, pBeg2++;
else if ( (*pBeg1)->Id < (*pBeg2)->Id )
// *pBeg++ = *pBeg1++;
pBeg1++;
else
// *pBeg++ = *pBeg2++;
pBeg2++;
}
// while ( pBeg1 < pEnd1 )
// *pBeg++ = *pBeg1++;
// while ( pBeg2 < pEnd2 )
// *pBeg++ = *pBeg2++;
vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
assert( vArr->nSize <= vArr->nCap );
assert( vArr->nSize <= vArr1->nSize );
assert( vArr->nSize <= vArr2->nSize );
}
/**Function*************************************************************
Synopsis [Returns 1 if uniqueness constraints can be added.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
{
int fVerbose = 0;
Aig_Obj_t * ppObjs[2], * pTemp;
Vec_Ptr_t * vSupp, * vSupp2;
int i, k, Value0, Value1, RetValue;
assert( p->pPars->nFramesK > 1 );
vSupp = Vec_PtrAlloc( 100 );
vSupp2 = Vec_PtrAlloc( 100 );
Vec_PtrClear( p->vCommon );
// compute the first support in terms of LOs
ppObjs[0] = pRepr;
ppObjs[1] = pObj;
Aig_SupportNodes( p->pAig, ppObjs, 2, vSupp );
// modify support to be in terms of LIs
k = 0;
Vec_PtrForEachEntry( vSupp, pTemp, i )
if ( Saig_ObjIsLo(p->pAig, pTemp) )
Vec_PtrWriteEntry( vSupp, k++, Saig_ObjLoToLi(p->pAig, pTemp) );
Vec_PtrShrink( vSupp, k );
// compute the support of support
Aig_SupportNodes( p->pAig, (Aig_Obj_t **)Vec_PtrArray(vSupp), Vec_PtrSize(vSupp), vSupp2 );
// return support to LO
Vec_PtrForEachEntry( vSupp, pTemp, i )
Vec_PtrWriteEntry( vSupp, i, Saig_ObjLiToLo(p->pAig, pTemp) );
// find the number of common vars
Vec_PtrSort( vSupp, Aig_ObjCompareIdIncrease );
Vec_PtrSort( vSupp2, Aig_ObjCompareIdIncrease );
Vec_PtrTwoCommon( vSupp, vSupp2, p->vCommon );
/*
{
Vec_Ptr_t * vNew = Vec_PtrDup(vSupp);
Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp) )
printf( "Not unique!\n" );
}
{
Vec_Ptr_t * vNew = Vec_PtrDup(vSupp2);
Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp2) )
printf( "Not unique!\n" );
}
{
Vec_Ptr_t * vNew = Vec_PtrDup(p->vCommon);
Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
if ( Vec_PtrSize(vNew) != Vec_PtrSize(p->vCommon) )
printf( "Not unique!\n" );
}
*/
if ( fVerbose )
printf( "Node = %5d : One = %3d. Two = %3d. Common = %3d. ",
Aig_ObjId(pObj), Vec_PtrSize(vSupp), Vec_PtrSize(vSupp2), Vec_PtrSize(p->vCommon) );
// check the current values
RetValue = 1;
Vec_PtrForEachEntry( p->vCommon, pTemp, i )
{
Value0 = Ssw_ManGetSatVarValue( p, pTemp, 0 );
Value1 = Ssw_ManGetSatVarValue( p, pTemp, 1 );
if ( Value0 != Value1 )
RetValue = 0;
if ( fVerbose )
printf( "%d", Value0 ^ Value1 );
}
if ( Vec_PtrSize(p->vCommon) == 0 )
RetValue = 0;
if ( fVerbose )
printf( "\n" );
Vec_PtrFree( vSupp );
Vec_PtrFree( vSupp2 );
return RetValue;
}
/**Function*************************************************************
Synopsis [Returns the output of the uniqueness constraint.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 )
{
Aig_Obj_t * pObj, * pObj1New, * pObj2New, * pMiter, * pTotal;
int i, pLits[2];
// int RetValue;
assert( Vec_PtrSize(vCommon) > 0 );
// generate the constraint
pTotal = Aig_ManConst0(p->pFrames);
Vec_PtrForEachEntry( vCommon, pObj, i )
{
assert( Saig_ObjIsLo(p->pAig, pObj) );
pObj1New = Ssw_ObjFrame( p, pObj, f1 );
pObj2New = Ssw_ObjFrame( p, pObj, f2 );
pMiter = Aig_Exor( p->pFrames, pObj1New, pObj2New );
pTotal = Aig_Or( p->pFrames, pTotal, pMiter );
}
if ( Aig_ObjIsConst1(Aig_Regular(pTotal)) )
{
// printf( "Skipped\n" );
return 0;
}
p->nUniques++;
// create CNF
Ssw_CnfNodeAddToSolver( p, Aig_Regular(pTotal) );
// add output constraint
pLits[0] = toLitCond( Ssw_ObjSatNum(p,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) );
/*
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
assert( RetValue );
// simplify the solver
if ( p->pSat->qtail != p->pSat->qhead )
{
RetValue = sat_solver_simplify(p->pSat);
assert( RetValue != 0 );
}
*/
assert( p->iOutputLit == -1 );
p->iOutputLit = pLits[0];
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abci/abc.c
......@@ -215,6 +215,7 @@ static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandBmcInter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIndcut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandEnlarge ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLocalize ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -481,6 +482,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "int", Abc_CommandBmcInter, 0 );
Cmd_CommandAdd( pAbc, "Verification", "indcut", Abc_CommandIndcut, 0 );
Cmd_CommandAdd( pAbc, "Verification", "enlarge", Abc_CommandEnlarge, 1 );
Cmd_CommandAdd( pAbc, "Verification", "loc", Abc_CommandLocalize, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*r", Abc_CommandAbc8Read, 0 );
......@@ -3671,7 +3673,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Abc_NtkMfsParsDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraesvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraestvwh" ) ) != EOF )
{
switch ( c )
{
......@@ -3753,6 +3755,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
pPars->fSwapEdge ^= 1;
break;
case 't':
pPars->fOneHotness ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
......@@ -3786,7 +3791,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: mfs [-WFDMLC <num>] [-raesvh]\n" );
fprintf( pErr, "usage: mfs [-WFDMLC <num>] [-raestvh]\n" );
fprintf( pErr, "\t performs don't-care-based optimization of logic networks\n" );
fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
......@@ -3798,6 +3803,7 @@ usage:
fprintf( pErr, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
fprintf( pErr, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
fprintf( pErr, "\t-s : toggle evaluation of edge swapping [default = %s]\n", pPars->fSwapEdge? "yes": "no" );
fprintf( pErr, "\t-t : toggle using artificial one-hotness conditions [default = %s]\n", pPars->fOneHotness? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
......@@ -13535,7 +13541,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsfvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsfuvh" ) ) != EOF )
{
switch ( c )
{
......@@ -13628,6 +13634,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'f':
pPars->fSemiFormal ^= 1;
break;
case 'u':
pPars->fUniqueness ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
......@@ -13680,7 +13689,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsfvh]\n" );
fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsfuvh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
......@@ -13693,6 +13702,7 @@ usage:
fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
fprintf( pErr, "\t-s : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "yes": "no" );
fprintf( pErr, "\t-f : toggle filtering using interative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
fprintf( pErr, "\t-u : toggle using uniqueness constraints [default = %s]\n", pPars->fUniqueness? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
......@@ -16476,6 +16486,105 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandLocalize( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int nFramesMax;
int nConfMax;
int fVerbose;
int c;
extern void Abc_NtkDarLocalize( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFramesMax = 50;
nConfMax = 500;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFramesMax < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConfMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nConfMax < 0 )
goto usage;
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_NtkIsComb(pNtk) )
{
fprintf( pErr, "The network is combinational.\n" );
return 0;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
if ( Abc_NtkPoNum(pNtk) != 1 )
{
fprintf( pErr, "Currently this command works only for single-output miter.\n" );
return 0;
}
// modify the current network
Abc_NtkDarLocalize( pNtk, nFramesMax, nConfMax, fVerbose );
return 0;
usage:
fprintf( pErr, "usage: loc [-FC num] [-vh]\n" );
fprintf( pErr, "\t performs localization for single-output miter\n" );
fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
......
src/base/abci/abcDar.c
......@@ -1974,6 +1974,44 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
Aig_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Performs targe enlargement.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkDarLocalize( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
int clkTotal = clock();
int RetValue;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return;
RetValue = Saig_ManLocalization( pTemp = pMan, nFramesMax, nConfMax, fVerbose );
Aig_ManStop( pTemp );
if ( RetValue == 1 )
{
printf( "Networks are equivalent. " );
PRT( "Time", clock() - clkTotal );
}
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT. " );
PRT( "Time", clock() - clkTotal );
}
else
{
printf( "Networks are UNDECIDED. " );
PRT( "Time", clock() - clkTotal );
}
}
/**Function*************************************************************
......@@ -2453,6 +2491,7 @@ Aig_ManPrintStats( pMan );
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
{
/*
extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig );
Abc_Ntk_t * pNtkAig;
......@@ -2471,6 +2510,26 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Aig_ManStop( pMan );
return pNtkAig;
*/
Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
Aig_ManSetRegNum( pMan, pMan->nRegs );
pMan = Saig_ManProofAbstraction( pTemp = pMan, 10, 1000, 1 );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromAigPhase( pMan );
pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Aig_ManStop( pMan );
return pNtkAig;
}
////////////////////////////////////////////////////////////////////////
......
src/base/abci/abcStrash.c
......@@ -122,7 +122,15 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup )
// complement the 1-valued registers
Abc_NtkForEachLatch( pNtkAig, pObj, i )
if ( Abc_LatchIsInit1(pObj) )
{
Abc_ObjXorFaninC( Abc_ObjFanin0(pObj), 0 );
// if latch has PO as one of its fanouts change latch name
if ( Abc_NodeFindCoFanout( Abc_ObjFanout0(pObj) ) )
{
Nm_ManDeleteIdName( pObj->pNtk->pManName, Abc_ObjFanout0(pObj)->Id );
Abc_ObjAssignName( Abc_ObjFanout0(pObj), Abc_ObjName(Abc_ObjFanout0(pObj)), "_inv" );
}
}
// set all constant-0 values
Abc_NtkForEachLatch( pNtkAig, pObj, i )
Abc_LatchSetInit0( pObj );
......
src/opt/mfs/mfs.h
......@@ -52,6 +52,7 @@ struct Mfs_Par_t_
int fArea; // performs optimization for area
int fMoreEffort; // performs high-affort minimization
int fSwapEdge; // performs edge swapping
int fOneHotness; // adds one-hotness conditions
int fDelay; // performs optimization for delay
int fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats
......
src/opt/mfs/mfsCore.c
......@@ -41,6 +41,7 @@
***********************************************************************/
void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
{
memset( pPars, 0, sizeof(Mfs_Par_t) );
pPars->nWinTfoLevs = 2;
pPars->nFanoutsMax = 10;
pPars->nDepthMax = 20;
......@@ -52,6 +53,7 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
pPars->fArea = 0;
pPars->fMoreEffort = 0;
pPars->fSwapEdge = 0;
pPars->fOneHotness = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
}
......@@ -155,6 +157,8 @@ p->timeCnf += clock() - clk;
// create the SAT problem
clk = clock();
p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
if ( p->pSat && p->pPars->fOneHotness )
Abc_NtkAddOneHotness( p );
if ( p->pSat == NULL )
return 0;
// solve the SAT problem
......
src/opt/mfs/mfsInt.h
......@@ -141,6 +141,7 @@ extern int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsSat.c ==========================================================*/
extern int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern int Abc_NtkAddOneHotness( Mfs_Man_t * p );
/*=== mfsStrash.c ==========================================================*/
extern Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode );
......
src/opt/mfs/mfsInter.c
......@@ -123,6 +123,15 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
return NULL;
}
// add one-hotness constraints
if ( p->pPars->fOneHotness )
{
p->pSat = pSat;
if ( !Abc_NtkAddOneHotness( p ) )
return NULL;
p->pSat = NULL;
}
// bookmark the clauses of A
if ( pCands )
sat_solver_store_mark_clauses_a( pSat );
......@@ -139,6 +148,14 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
return NULL;
}
}
// add one-hotness constraints
if ( p->pPars->fOneHotness )
{
p->pSat = pSat;
if ( !Abc_NtkAddOneHotness( p ) )
return NULL;
p->pSat = NULL;
}
// transform the literals
for ( i = 0; i < p->pCnf->nLiterals; i++ )
p->pCnf->pClauses[0][i] -= 2 * p->pCnf->nVars;
......
src/opt/mfs/mfsSat.c
......@@ -133,6 +133,38 @@ int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
return 1;
}
/**Function*************************************************************
Synopsis [Adds one-hotness constraints for the window inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkAddOneHotness( Mfs_Man_t * p )
{
Aig_Obj_t * pObj1, * pObj2;
int i, k, Lits[2];
for ( i = 0; i < Vec_PtrSize(p->pAigWin->vPis); i++ )
for ( k = i+1; k < Vec_PtrSize(p->pAigWin->vPis); k++ )
{
pObj1 = Aig_ManPi( p->pAigWin, i );
pObj2 = Aig_ManPi( p->pAigWin, k );
Lits[0] = toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 );
Lits[1] = toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 );
if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
{
sat_solver_delete( p->pSat );
p->pSat = NULL;
return 0;
}
}
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/sat/bsat/satInterA_yu_hu.c 0 → 100644
/**CFile****************************************************************
FileName [satInter.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT sat_solver.]
Synopsis [Interpolation package.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
***********************************************************************/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "satStore.h"
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// variable assignments
static const lit LIT_UNDEF = 0xffffffff;
// interpolation manager
struct Inta_Man_t_
{
// clauses of the problems
Sto_Man_t * pCnf; // the set of CNF clauses for A and B
Vec_Int_t * vVarsAB; // the array of global variables
// various parameters
int fVerbose; // verbosiness flag
int fProofVerif; // verifies the proof
int fProofWrite; // writes the proof file
int nVarsAlloc; // the allocated size of var arrays
int nClosAlloc; // the allocated size of clause arrays
// internal BCP
int nRootSize; // the number of root level assignments
int nTrailSize; // the number of assignments made
lit * pTrail; // chronological order of assignments (size nVars)
lit * pAssigns; // assignments by variable (size nVars)
char * pSeens; // temporary mark (size nVars)
Sto_Cls_t ** pReasons; // reasons for each assignment (size nVars)
Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars)
// interpolation data
Aig_Man_t * pAig; // the AIG manager for recording the interpolant
int * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB]
Aig_Obj_t ** pInters; // storage for interpolants as truth tables (size nClauses)
int nIntersAlloc; // the allocated size of truth table array
// proof recording
int Counter; // counter of resolved clauses
int * pProofNums; // the proof numbers for each clause (size nClauses)
FILE * pFile; // the file for proof recording
// internal verification
lit * pResLits; // the literals of the resolvent
int nResLits; // the number of literals of the resolvent
int nResLitsAlloc;// the number of literals of the resolvent
// runtime stats
int timeBcp; // the runtime for BCP
int timeTrace; // the runtime of trace construction
int timeTotal; // the total runtime of interpolation
};
// procedure to get hold of the clauses' truth table
static inline Aig_Obj_t ** Inta_ManAigRead( Inta_Man_t * pMan, Sto_Cls_t * pCls ) { return pMan->pInters + pCls->Id; }
static inline void Inta_ManAigClear( Inta_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst0(pMan->pAig); }
static inline void Inta_ManAigFill( Inta_Man_t * pMan, Aig_Obj_t ** p ) { *p = Aig_ManConst1(pMan->pAig); }
static inline void Inta_ManAigCopy( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = *q; }
static inline void Inta_ManAigAnd( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_And(pMan->pAig, *p, *q); }
static inline void Inta_ManAigOr( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, *q); }
static inline void Inta_ManAigOrNot( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(*q)); }
static inline void Inta_ManAigOrVar( Inta_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_IthVar(pMan->pAig, v)); }
static inline void Inta_ManAigOrNotVar( Inta_Man_t * pMan, Aig_Obj_t ** p, int v ) { *p = Aig_Or(pMan->pAig, *p, Aig_Not(Aig_IthVar(pMan->pAig, v))); }
// reading/writing the proof for a clause
static inline int Inta_ManProofGet( Inta_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; }
static inline void Inta_ManProofSet( Inta_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocate proof manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Inta_Man_t * Inta_ManAlloc()
{
Inta_Man_t * p;
// allocate the manager
p = (Inta_Man_t *)malloc( sizeof(Inta_Man_t) );
memset( p, 0, sizeof(Inta_Man_t) );
// verification
p->nResLitsAlloc = (1<<16);
p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
// parameters
p->fProofWrite = 1;
p->fProofVerif = 1;
return p;
}
/**Function*************************************************************
Synopsis [Count common variables in the clauses of A and B.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Inta_ManGlobalVars( Inta_Man_t * p )
{
Sto_Cls_t * pClause;
int LargeNum = -100000000;
int Var, nVarsAB, v;
// mark the variable encountered in the clauses of A
Sto_ManForEachClauseRoot( p->pCnf, pClause )
{
if ( !pClause->fA )
break;
for ( v = 0; v < (int)pClause->nLits; v++ )
p->pVarTypes[lit_var(pClause->pLits[v])] = 1;
}
// check variables that appear in clauses of B
nVarsAB = 0;
Sto_ManForEachClauseRoot( p->pCnf, pClause )
{
if ( pClause->fA )
continue;
for ( v = 0; v < (int)pClause->nLits; v++ )
{
Var = lit_var(pClause->pLits[v]);
if ( p->pVarTypes[Var] == 1 ) // var of A
{
// change it into a global variable
nVarsAB++;
p->pVarTypes[Var] = LargeNum;
}
}
}
assert( nVarsAB <= Vec_IntSize(p->vVarsAB) );
// order global variables
nVarsAB = 0;
Vec_IntForEachEntry( p->vVarsAB, Var, v )
p->pVarTypes[Var] = -(1+nVarsAB++);
// check that there is no extra global variables
for ( v = 0; v < p->pCnf->nVars; v++ )
assert( p->pVarTypes[v] != LargeNum );
return nVarsAB;
}
/**Function*************************************************************
Synopsis [Resize proof manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Inta_ManResize( Inta_Man_t * p )
{
// check if resizing is needed
if ( p->nVarsAlloc < p->pCnf->nVars )
{
// find the new size
if ( p->nVarsAlloc == 0 )
p->nVarsAlloc = 1;
while ( p->nVarsAlloc < p->pCnf->nVars )
p->nVarsAlloc *= 2;
// resize the arrays
p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc );
p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc );
p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc );
p->pVarTypes = (int *) realloc( p->pVarTypes, sizeof(int) * p->nVarsAlloc );
p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc );
p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 );
}
// clean the free space
memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars );
memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars );
memset( p->pVarTypes, 0, sizeof(int) * p->pCnf->nVars );
memset( p->pReasons , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars );
memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 );
// compute the number of common variables
Inta_ManGlobalVars( p );
// check if resizing of clauses is needed
if ( p->nClosAlloc < p->pCnf->nClauses )
{
// find the new size
if ( p->nClosAlloc == 0 )
p->nClosAlloc = 1;
while ( p->nClosAlloc < p->pCnf->nClauses )
p->nClosAlloc *= 2;
// resize the arrays
p->pProofNums = (int *) realloc( p->pProofNums, sizeof(int) * p->nClosAlloc );
}
memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses );
// check if resizing of truth tables is needed
if ( p->nIntersAlloc < p->pCnf->nClauses )
{
p->nIntersAlloc = p->pCnf->nClauses;
p->pInters = (Aig_Obj_t **) realloc( p->pInters, sizeof(Aig_Obj_t *) * p->nIntersAlloc );
}
memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses );
}
/**Function*************************************************************
Synopsis [Deallocate proof manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Inta_ManFree( Inta_Man_t * p )
{
/*
printf( "Runtime stats:\n" );
PRT( "BCP ", p->timeBcp );
PRT( "Trace ", p->timeTrace );
PRT( "TOTAL ", p->timeTotal );
*/
free( p->pInters );
free( p->pProofNums );
free( p->pTrail );
free( p->pAssigns );
free( p->pSeens );
free( p->pVarTypes );
free( p->pReasons );
free( p->pWatches );
free( p->pResLits );
free( p );
}
/**Function*************************************************************
Synopsis [Prints the clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Inta_ManPrintClause( Inta_Man_t * p, Sto_Cls_t * pClause )
{
int i;
printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Inta_ManProofGet(p, pClause) );
for ( i = 0; i < (int)pClause->nLits; i++ )
printf( " %d", pClause->pLits[i] );
printf( " }\n" );
}
// Yu Hu
void Inta_ManPrintClauseEx( lit * pResLits, int nResLits )
{
int i;
printf( " {" );
for ( i = 0; i < nResLits; i++ )
printf( " %d", lit_print(pResLits[i]) );
printf( " }\n" );
}
/**Function*************************************************************
Synopsis [Prints the resolvent.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Inta_ManPrintResolvent( lit * pResLits, int nResLits )
{
int i;
printf( "Resolvent: {" );
for ( i = 0; i < nResLits; i++ )
printf( " %d", lit_print(pResLits[i]) );
printf( " }\n" );
}
/**Function*************************************************************
Synopsis [Prints the interpolant for one clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Inta_ManPrintInterOne( Inta_Man_t * p, Sto_Cls_t * pClause )
{
printf( "Clause %2d : ", pClause->Id );
// Extra_PrintBinary___( stdout, Inta_ManAigRead(p, pClause), (1 << p->nVarsAB) );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Adds one clause to the watcher list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Inta_ManWatchClause( Inta_Man_t * p, Sto_Cls_t * pClause, lit Lit )
{
assert( lit_check(Lit, p->pCnf->nVars) );
if ( pClause->pLits[0] == Lit )
pClause->pNext0 = p->pWatches[lit_neg(Lit)];
else
{
assert( pClause->pLits[1] == Lit );
pClause->pNext1 = p->pWatches[lit_neg(Lit)];
}
p->pWatches[lit_neg(Lit)] = pClause;
}
/**Function*************************************************************
Synopsis [Records implication.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Inta_ManEnqueue( Inta_Man_t * p, lit Lit, Sto_Cls_t * pReason )
{
int Var = lit_var(Lit);
if ( p->pAssigns[Var] != LIT_UNDEF )
return p->pAssigns[Var] == Lit;
p->pAssigns[Var] = Lit;
p->pReasons[Var] = pReason;
p->pTrail[p->nTrailSize++] = Lit;
//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) );
return 1;
}
/**Function*************************************************************
Synopsis [Records implication.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Inta_ManCancelUntil( Inta_Man_t * p, int Level )
{
lit Lit;
int i, Var;
for ( i = p->nTrailSize - 1; i >= Level; i-- )
{
Lit = p->pTrail[i];
Var = lit_var( Lit );
p->pReasons[Var] = NULL;
p->pAssigns[Var] = LIT_UNDEF;
//printf( "cancelling var %d\n", Var );
}
p->nTrailSize = Level;
}
/**Function*************************************************************
Synopsis [Propagate one assignment.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Sto_Cls_t * Inta_ManPropagateOne( Inta_Man_t * p, lit Lit )
{
Sto_Cls_t ** ppPrev, * pCur, * pTemp;
lit LitF = lit_neg(Lit);
int i;
// iterate through the literals
ppPrev = p->pWatches + Lit;
for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
{
// make sure the false literal is in the second literal of the clause
if ( pCur->pLits[0] == LitF )
{
pCur->pLits[0] = pCur->pLits[1];
pCur->pLits[1] = LitF;
pTemp = pCur->pNext0;
pCur->pNext0 = pCur->pNext1;
pCur->pNext1 = pTemp;
}
assert( pCur->pLits[1] == LitF );
// if the first literal is true, the clause is satisfied
if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
{
ppPrev = &pCur->pNext1;
continue;
}
// look for a new literal to watch
for ( i = 2; i < (int)pCur->nLits; i++ )
{
// skip the case when the literal is false
if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
continue;
// the literal is either true or unassigned - watch it
pCur->pLits[1] = pCur->pLits[i];
pCur->pLits[i] = LitF;
// remove this clause from the watch list of Lit
*ppPrev = pCur->pNext1;
// add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
Inta_ManWatchClause( p, pCur, pCur->pLits[1] );
break;
}
if ( i < (int)pCur->nLits ) // found new watch
continue;
// clause is unit - enqueue new implication
if ( Inta_ManEnqueue(p, pCur->pLits[0], pCur) )
{
ppPrev = &pCur->pNext1;
continue;
}
// conflict detected - return the conflict clause
return pCur;
}
return NULL;
}
/**Function*************************************************************
Synopsis [Propagate the current assignments.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Sto_Cls_t * Inta_ManPropagate( Inta_Man_t * p, int Start )
{
Sto_Cls_t * pClause;
int i;
int clk = clock();
for ( i = Start; i < p->nTrailSize; i++ )
{
pClause = Inta_ManPropagateOne( p, p->pTrail[i] );
if ( pClause )
{
p->timeBcp += clock() - clk;
return pClause;
}
}
p->timeBcp += clock() - clk;
return NULL;
}
/**Function*************************************************************
Synopsis [Writes one root clause into a file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Inta_ManProofWriteOne( Inta_Man_t * p, Sto_Cls_t * pClause )
{
Inta_ManProofSet( p, pClause, ++p->Counter );
if ( p->fProofWrite )
{
int v;
fprintf( p->pFile, "%d", Inta_ManProofGet(p, pClause) );
for ( v = 0; v < (int)pClause->nLits; v++ )
fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) );
fprintf( p->pFile, " 0 0\n" );
}
}
/**Function*************************************************************
Synopsis [Traces the proof for one clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal )
{
Sto_Cls_t * pReason;
int i, v, Var, PrevId;
int fPrint = 1; // Yu Hu
int clk = clock();
// collect resolvent literals
if ( p->fProofVerif )
{
assert( (int)pConflict->nLits <= p->nResLitsAlloc );
memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits );
p->nResLits = pConflict->nLits;
}
// mark all the variables in the conflict as seen
for ( v = 0; v < (int)pConflict->nLits; v++ )
p->pSeens[lit_var(pConflict->pLits[v])] = 1;
// start the anticedents
// pFinal->pAntis = Vec_PtrAlloc( 32 );
// Vec_PtrPush( pFinal->pAntis, pConflict );
if ( p->pCnf->nClausesA )
Inta_ManAigCopy( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pConflict) );
// follow the trail backwards
PrevId = Inta_ManProofGet(p, pConflict);
for ( i = p->nTrailSize - 1; i >= 0; i-- )
{
// skip literals that are not involved
Var = lit_var(p->pTrail[i]);
if ( !p->pSeens[Var] )
continue;
p->pSeens[Var] = 0;
// skip literals of the resulting clause
pReason = p->pReasons[Var];
if ( pReason == NULL )
continue;
assert( p->pTrail[i] == pReason->pLits[0] );
// add the variables to seen
for ( v = 1; v < (int)pReason->nLits; v++ )
p->pSeens[lit_var(pReason->pLits[v])] = 1;
// record the reason clause
assert( Inta_ManProofGet(p, pReason) > 0 );
p->Counter++;
if ( p->fProofWrite ) {
fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Inta_ManProofGet(p, pReason) );
// Yu Hu
printf( "%d * %d %d 0\n", p->Counter, PrevId, Inta_ManProofGet(p, pReason) );
}
PrevId = p->Counter;
if ( p->pCnf->nClausesA )
{
if ( p->pVarTypes[Var] == 1 ) // var of A
Inta_ManAigOr( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) );
else
Inta_ManAigAnd( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) );
}
// resolve the temporary resolvent with the reason clause
if ( p->fProofVerif )
{
int v1, v2;
// Yu Hu
// if ( fPrint )
// Inta_ManPrintResolvent( p->pResLits, p->nResLits );
if ( fPrint ) {
printf("pivot = %d,\n", lit_print(p->pTrail[i]));
Inta_ManPrintClauseEx( p->pResLits, p->nResLits);
}
// check that the var is present in the resolvent
for ( v1 = 0; v1 < p->nResLits; v1++ )
if ( lit_var(p->pResLits[v1]) == Var )
break;
if ( v1 == p->nResLits )
printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var );
if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) )
printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var );
// remove this variable from the resolvent
assert( lit_var(p->pResLits[v1]) == Var );
p->nResLits--;
for ( ; v1 < p->nResLits; v1++ )
p->pResLits[v1] = p->pResLits[v1+1];
// add variables of the reason clause
for ( v2 = 1; v2 < (int)pReason->nLits; v2++ )
{
for ( v1 = 0; v1 < p->nResLits; v1++ )
if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) )
break;
// if it is a new variable, add it to the resolvent
if ( v1 == p->nResLits )
{
if ( p->nResLits == p->nResLitsAlloc )
printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n", pFinal->Id );
p->pResLits[ p->nResLits++ ] = pReason->pLits[v2];
continue;
}
// if the variable is the same, the literal should be the same too
if ( p->pResLits[v1] == pReason->pLits[v2] )
continue;
// the literal is different
printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
}
// Yu Hu
if ( fPrint ) {
Inta_ManPrintClauseEx( pReason->pLits, pReason->nLits);
Inta_ManPrintResolvent( p->pResLits, p->nResLits );
}
}
// Vec_PtrPush( pFinal->pAntis, pReason );
}
// unmark all seen variables
// for ( i = p->nTrailSize - 1; i >= 0; i-- )
// p->pSeens[lit_var(p->pTrail[i])] = 0;
// check that the literals are unmarked
// for ( i = p->nTrailSize - 1; i >= 0; i-- )
// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 );
// use the resulting clause to check the correctness of resolution
if ( p->fProofVerif )
{
int v1, v2;
if ( fPrint ){
// Yu Hu
// Inta_ManPrintResolvent( p->pResLits, p->nResLits );
}
for ( v1 = 0; v1 < p->nResLits; v1++ )
{
for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
if ( pFinal->pLits[v2] == p->pResLits[v1] )
break;
if ( v2 < (int)pFinal->nLits )
continue;
break;
}
if ( v1 < p->nResLits )
{
printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id );
Inta_ManPrintClause( p, pConflict );
Inta_ManPrintResolvent( p->pResLits, p->nResLits );
Inta_ManPrintClause( p, pFinal );
}
}
p->timeTrace += clock() - clk;
// return the proof pointer
if ( p->pCnf->nClausesA )
{
// Inta_ManPrintInterOne( p, pFinal );
}
Inta_ManProofSet( p, pFinal, p->Counter );
return p->Counter;
}
/**Function*************************************************************
Synopsis [Records the proof for one clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Inta_ManProofRecordOne( Inta_Man_t * p, Sto_Cls_t * pClause )
{
Sto_Cls_t * pConflict;
int i;
// empty clause never ends up there
assert( pClause->nLits > 0 );
if ( pClause->nLits == 0 )
printf( "Error: Empty clause is attempted.\n" );
// add assumptions to the trail
assert( !pClause->fRoot );
assert( p->nTrailSize == p->nRootSize );
for ( i = 0; i < (int)pClause->nLits; i++ )
if ( !Inta_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
{
assert( 0 ); // impossible
return 0;
}
// propagate the assumptions
pConflict = Inta_ManPropagate( p, p->nRootSize );
if ( pConflict == NULL )
{
assert( 0 ); // cannot prove
return 0;
}
// construct the proof
Inta_ManProofTraceOne( p, pConflict, pClause );
// undo to the root level
Inta_ManCancelUntil( p, p->nRootSize );
// add large clauses to the watched lists
if ( pClause->nLits > 1 )
{
Inta_ManWatchClause( p, pClause, pClause->pLits[0] );
Inta_ManWatchClause( p, pClause, pClause->pLits[1] );
return 1;
}
assert( pClause->nLits == 1 );
// if the clause proved is unit, add it and propagate
if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) )
{
assert( 0 ); // impossible
return 0;
}
// propagate the assumption
pConflict = Inta_ManPropagate( p, p->nRootSize );
if ( pConflict )
{
// construct the proof
Inta_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty );
// if ( p->fVerbose )
// printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
return 0;
}
// update the root level
p->nRootSize = p->nTrailSize;
return 1;
}
/**Function*************************************************************
Synopsis [Propagate the root clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Inta_ManProcessRoots( Inta_Man_t * p )
{
Sto_Cls_t * pClause;
int Counter;
// make sure the root clauses are preceeding the learnt clauses
Counter = 0;
Sto_ManForEachClause( p->pCnf, pClause )
{
assert( (int)pClause->fA == (Counter < (int)p->pCnf->nClausesA) );
assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots) );
Counter++;
}
assert( p->pCnf->nClauses == Counter );
// make sure the last clause if empty
assert( p->pCnf->pTail->nLits == 0 );
// go through the root unit clauses
p->nTrailSize = 0;
Sto_ManForEachClauseRoot( p->pCnf, pClause )
{
// create watcher lists for the root clauses
if ( pClause->nLits > 1 )
{
Inta_ManWatchClause( p, pClause, pClause->pLits[0] );
Inta_ManWatchClause( p, pClause, pClause->pLits[1] );
}
// empty clause and large clauses
if ( pClause->nLits != 1 )
continue;
// unit clause
assert( lit_check(pClause->pLits[0], p->pCnf->nVars) );
if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) )
{
// detected root level conflict
// printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" );
// assert( 0 );
// detected root level conflict
Inta_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
if ( p->fVerbose )
printf( "Found root level conflict!\n" );
return 0;
}
}
// propagate the root unit clauses
pClause = Inta_ManPropagate( p, 0 );
if ( pClause )
{
// detected root level conflict
Inta_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
if ( p->fVerbose )
printf( "Found root level conflict!\n" );
return 0;
}
// set the root level
p->nRootSize = p->nTrailSize;
return 1;
}
/**Function*************************************************************
Synopsis [Records the proof.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Inta_ManPrepareInter( Inta_Man_t * p )
{
Sto_Cls_t * pClause;
int Var, VarAB, v;
// set interpolants for root clauses
Sto_ManForEachClauseRoot( p->pCnf, pClause )
{
if ( !pClause->fA ) // clause of B
{
Inta_ManAigFill( p, Inta_ManAigRead(p, pClause) );
// Inta_ManPrintInterOne( p, pClause );
continue;
}
// clause of A
Inta_ManAigClear( p, Inta_ManAigRead(p, pClause) );
for ( v = 0; v < (int)pClause->nLits; v++ )
{
Var = lit_var(pClause->pLits[v]);
if ( p->pVarTypes[Var] < 0 ) // global var
{
VarAB = -p->pVarTypes[Var]-1;
assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) );
if ( lit_sign(pClause->pLits[v]) ) // negative var
Inta_ManAigOrNotVar( p, Inta_ManAigRead(p, pClause), VarAB );
else
Inta_ManAigOrVar( p, Inta_ManAigRead(p, pClause), VarAB );
}
}
// Inta_ManPrintInterOne( p, pClause );
}
}
/**Function*************************************************************
Synopsis [Computes interpolant for the given CNF.]
Description [Takes the interpolation manager, the CNF deriving by the SAT
solver, which includes ClausesA, ClausesB, and learned clauses. Additional
arguments are the vector of variables common to AB and the verbosiness flag.
Returns the AIG manager with a single output, containing the interpolant.]
SideEffects []
SeeAlso []
***********************************************************************/
void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose )
{
Aig_Man_t * pRes;
Aig_Obj_t * pObj;
Sto_Cls_t * pClause;
int RetValue = 1;
int clkTotal = clock();
// check that the CNF makes sense
assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
p->pCnf = pCnf;
p->fVerbose = fVerbose;
p->vVarsAB = vVarsAB;
p->pAig = pRes = Aig_ManStart( 10000 );
Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 );
// adjust the manager
Inta_ManResize( p );
// prepare the interpolant computation
Inta_ManPrepareInter( p );
// construct proof for each clause
// start the proof
if ( p->fProofWrite )
{
p->pFile = fopen( "proof.cnf_", "w" );
p->Counter = 0;
}
// write the root clauses
Sto_ManForEachClauseRoot( p->pCnf, pClause )
Inta_ManProofWriteOne( p, pClause );
// propagate root level assignments
if ( Inta_ManProcessRoots( p ) )
{
// if there is no conflict, consider learned clauses
Sto_ManForEachClause( p->pCnf, pClause )
{
if ( pClause->fRoot )
continue;
if ( !Inta_ManProofRecordOne( p, pClause ) )
{
RetValue = 0;
break;
}
}
}
// stop the proof
if ( p->fProofWrite )
{
fclose( p->pFile );
p->pFile = NULL;
}
if ( fVerbose )
{
// PRT( "Interpo", clock() - clkTotal );
printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n",
p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
p->timeTotal += clock() - clkTotal;
}
pObj = *Inta_ManAigRead( p, p->pCnf->pTail );
Aig_ObjCreatePo( pRes, pObj );
Aig_ManCleanup( pRes );
p->pAig = NULL;
return pRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA )
{
Aig_Man_t * p;
Aig_Obj_t * pMiter, * pSum, * pLit;
Sto_Cls_t * pClause;
int Var, VarAB, v;
p = Aig_ManStart( 10000 );
pMiter = Aig_ManConst1(p);
Sto_ManForEachClauseRoot( pCnf, pClause )
{
if ( fClausesA ^ pClause->fA ) // clause of B
continue;
// clause of A
pSum = Aig_ManConst0(p);
for ( v = 0; v < (int)pClause->nLits; v++ )
{
Var = lit_var(pClause->pLits[v]);
if ( pMan->pVarTypes[Var] < 0 ) // global var
{
VarAB = -pMan->pVarTypes[Var]-1;
assert( VarAB >= 0 && VarAB < Vec_IntSize(pMan->vVarsAB) );
pLit = Aig_NotCond( Aig_IthVar(p, VarAB), lit_sign(pClause->pLits[v]) );
}
else
pLit = Aig_NotCond( Aig_IthVar(p, Vec_IntSize(pMan->vVarsAB)+1+Var), lit_sign(pClause->pLits[v]) );
pSum = Aig_Or( p, pSum, pLit );
}
pMiter = Aig_And( p, pMiter, pSum );
}
Aig_ObjCreatePo( p, pMiter );
return p;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/sat/bsat/satInterP.c
......@@ -796,7 +796,7 @@ void Intp_ManUnsatCore_rec( Vec_Int_t * vAnties, Vec_Int_t * vBreaks, int iThis,
Synopsis [Computes UNSAT core of the satisfiablity problem.]
Description [Takes the interpolation manager, the CNF deriving by the SAT
Description [Takes the interpolation manager, the CNF derived by the SAT
solver, which includes the root clauses and the learned clauses. Returns
the array of integers representing the number of root clauses that are in
the UNSAT core.]
......
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