Skip to content

A
abc
Commit 3d01abf4 by Alan Mishchenko
Options

Experiment with 'pdr'.

parent 35273eae
Showing with 188 additions and 33 deletions
src/proof/pdr/pdrCnf.c
......@@ -67,6 +67,8 @@ static inline int Pdr_ObjSatVar1( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
//#define USE_PG
#ifdef USE_PG
static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
{
Vec_Int_t * vId2Vars = p->pvId2Vars + Aig_ObjId(pObj);
......@@ -80,7 +82,7 @@ static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pOb
int iVarNew = Vec_IntSize( vVar2Ids );
assert( iVarNew > 0 );
Vec_IntPush( vVar2Ids, Aig_ObjId(pObj) );
Vec_IntWriteEntry( vId2Vars, k, iVarNew );
Vec_IntWriteEntry( vId2Vars, k, iVarNew << 2 );
sat_solver_setnvars( pSat, iVarNew + 1 );
if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
{
......@@ -93,42 +95,128 @@ static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pOb
}
return Vec_IntEntry( vId2Vars, k );
}
/**Function*************************************************************
Synopsis [Recursively adds CNF for the given object.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level )
int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level, int Pol )
{
Vec_Int_t * vLits;
sat_solver * pSat;
Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, k);
int nVarCount = Vec_IntSize(vVar2Ids);
int iVarThis = Pdr_ObjSatVar2FindOrAdd( p, k, pObj );
int * pLit, i, iVar, nClauses, iFirstClause, RetValue;
if ( nVarCount == Vec_IntSize(vVar2Ids) )
int * pLit, i, iVar, iClaBeg, iClaEnd, RetValue;
int PolPres = (iVarThis & 3);
iVarThis >>= 2;
if ( Aig_ObjIsCi(pObj) )
return iVarThis;
// Pol = 3;
// if ( nVarCount != Vec_IntSize(vVar2Ids) || (Pol & ~PolPres) )
if ( (Pol & ~PolPres) )
{
*Vec_IntEntryP( p->pvId2Vars + Aig_ObjId(pObj), k ) |= Pol;
iClaBeg = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
iClaEnd = iClaBeg + p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
assert( iClaBeg < iClaEnd );
/*
if ( (Pol & ~PolPres) != 3 )
for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
{
printf( "Clause %5d : ", i );
for ( iVar = 0; iVar < 4; iVar++ )
printf( "%d ", ((unsigned)p->pCnf2->pClaPols[i] >> (2*iVar)) & 3 );
printf( " " );
for ( pLit = p->pCnf2->pClauses[i]; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
printf( "%6d ", *pLit );
printf( "\n" );
}
*/
pSat = Pdr_ManSolver(p, k);
vLits = Vec_WecEntry( p->vVLits, Level );
if ( (Pol & ~PolPres) == 3 )
{
assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) );
if ( Aig_ObjIsCi(pObj) )
for ( i = iClaBeg; i < iClaEnd; i++ )
{
Vec_IntClear( vLits );
Vec_IntPush( vLits, toLitCond( iVarThis, lit_sign(p->pCnf2->pClauses[i][0]) ) );
for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
{
iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, 3 );
Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
}
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
assert( RetValue );
(void) RetValue;
}
}
else // if ( (Pol & ~PolPres) == 2 || (Pol & ~PolPres) == 1 ) // write pos/neg polarity
{
assert( (Pol & ~PolPres) );
for ( i = iClaBeg; i < iClaEnd; i++ )
if ( 2 - !Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) == (Pol & ~PolPres) ) // taking opposite literal
{
Vec_IntClear( vLits );
Vec_IntPush( vLits, toLitCond( iVarThis, Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) ) );
for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
{
iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, ((unsigned)p->pCnf2->pClaPols[i] >> (2*(pLit-p->pCnf2->pClauses[i]-1))) & 3 );
Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
}
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
assert( RetValue );
(void) RetValue;
}
}
}
return iVarThis;
nClauses = p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
iFirstClause = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
assert( nClauses > 0 );
}
#else
static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int * pfNewVar )
{
Vec_Int_t * vId2Vars = p->pvId2Vars + Aig_ObjId(pObj);
assert( p->pCnf2->pObj2Count[Aig_ObjId(pObj)] >= 0 );
if ( Vec_IntSize(vId2Vars) == 0 )
Vec_IntGrow(vId2Vars, 2 * k + 1);
if ( Vec_IntGetEntry(vId2Vars, k) == 0 )
{
sat_solver * pSat = Pdr_ManSolver(p, k);
Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, k);
int iVarNew = Vec_IntSize( vVar2Ids );
assert( iVarNew > 0 );
Vec_IntPush( vVar2Ids, Aig_ObjId(pObj) );
Vec_IntWriteEntry( vId2Vars, k, iVarNew );
sat_solver_setnvars( pSat, iVarNew + 1 );
if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
{
int Lit = toLitCond( iVarNew, 1 );
int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue == 1 );
(void) RetValue;
sat_solver_compress( pSat );
}
*pfNewVar = 1;
}
return Vec_IntEntry( vId2Vars, k );
}
int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level, int Pol )
{
Vec_Int_t * vLits;
sat_solver * pSat;
int fNewVar = 0, iVarThis = Pdr_ObjSatVar2FindOrAdd( p, k, pObj, &fNewVar );
int * pLit, i, iVar, iClaBeg, iClaEnd, RetValue;
if ( Aig_ObjIsCi(pObj) || !fNewVar )
return iVarThis;
iClaBeg = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
iClaEnd = iClaBeg + p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
assert( iClaBeg < iClaEnd );
pSat = Pdr_ManSolver(p, k);
vLits = Vec_WecEntry( p->vVLits, Level );
for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
for ( i = iClaBeg; i < iClaEnd; i++ )
{
Vec_IntClear( vLits );
for ( pLit = p->pCnf2->pClauses[i]; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
Vec_IntPush( vLits, toLitCond( iVarThis, lit_sign(p->pCnf2->pClauses[i][0]) ) );
for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
{
iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1 );
iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)), Level+1, Pol );
Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
}
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
......@@ -137,6 +225,7 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level )
}
return iVarThis;
}
#endif
/**Function*************************************************************
......@@ -149,12 +238,12 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj, int Level )
SeeAlso []
***********************************************************************/
int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
int Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj )
{
if ( p->pPars->fMonoCnf )
return Pdr_ObjSatVar1( p, k, pObj );
else
return Pdr_ObjSatVar2( p, k, pObj, 0 );
return Pdr_ObjSatVar2( p, k, pObj, 0, Pol );
}
......@@ -277,7 +366,7 @@ static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p,
assert( p->vVar2Reg == NULL );
p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars );
Saig_ManForEachLi( p->pAig, pObj, i )
Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, pObj), i );
Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, 3, pObj), i );
}
pSat = (sat_solver *)Cnf_DataWriteIntoSolverInt( pSat, p->pCnf1, 1, fInit );
sat_solver_set_runtime_limit( pSat, p->timeToStop );
......@@ -303,6 +392,9 @@ static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p,
if ( p->pCnf2 == NULL )
{
p->pCnf2 = Cnf_DeriveOtherWithMan( p->pCnfMan, p->pAig, 0 );
#ifdef USE_PG
p->pCnf2->pClaPols = Cnf_DataDeriveLitPolarities( p->pCnf2 );
#endif
p->pvId2Vars = ABC_CALLOC( Vec_Int_t, Aig_ManObjNumMax(p->pAig) );
Vec_PtrGrow( &p->vVar2Ids, 256 );
}
......
src/proof/pdr/pdrInt.h
......@@ -156,7 +156,7 @@ static inline abctime Pdr_ManTimeLimit( Pdr_Man_t * p )
/*=== pdrCex.c ==========================================================*/
extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p );
/*=== pdrCnf.c ==========================================================*/
extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj );
extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj );
extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar );
extern int Pdr_ManFreeVar( Pdr_Man_t * p, int k );
extern sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit );
......
src/proof/pdr/pdrSat.c
......@@ -57,9 +57,8 @@ sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
Vec_VecExpand( p->vClauses, k );
Vec_IntPush( p->vActVars, 0 );
// add property cone
// Pdr_ObjSatVar( p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) );
Saig_ManForEachPo( p->pAig, pObj, i )
Pdr_ObjSatVar( p, k, pObj );
Pdr_ObjSatVar( p, k, 1, pObj );
return pSat;
}
......@@ -146,6 +145,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom
int i, iVar, iVarMax = 0;
abctime clk = Abc_Clock();
Vec_IntClear( p->vLits );
assert( !(fNext && fCompl) );
for ( i = 0; i < pCube->nLits; i++ )
{
if ( pCube->Lits[i] == -1 )
......@@ -154,7 +154,7 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom
pObj = Saig_ManLi( p->pAig, lit_var(pCube->Lits[i]) );
else
pObj = Saig_ManLo( p->pAig, lit_var(pCube->Lits[i]) );
iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 );
iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - lit_sign(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
iVarMax = Abc_MaxInt( iVarMax, iVar );
Vec_IntPush( p->vLits, toLitCond( iVar, fCompl ^ lit_sign(pCube->Lits[i]) ) );
}
......@@ -185,7 +185,7 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
// skip solved outputs
if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
continue;
Lit = toLitCond( Pdr_ObjSatVar(p, k, pObj), 1 ); // neg literal
Lit = toLitCond( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue == 1 );
}
......@@ -235,7 +235,7 @@ void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t
pSat = Pdr_ManSolver(p, k);
Aig_ManForEachObjVec( vObjIds, p->pAig, pObj, i )
{
iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 );
iVar = Pdr_ObjSatVar( p, k, 3, pObj ); assert( iVar >= 0 );
Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
}
}
......@@ -293,7 +293,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
if ( pCube == NULL ) // solve the property
{
clk = Abc_Clock();
Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
Lit = toLit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
sat_solver_set_runtime_limit( pSat, Limit );
......
src/sat/cnf/cnf.h
......@@ -63,6 +63,7 @@ struct Cnf_Dat_t_
int * pVarNums; // the number of CNF variable for each node ID (-1 if unused)
int * pObj2Clause; // the mapping of objects into clauses
int * pObj2Count; // the mapping of objects into clause number
unsigned char * pClaPols; // polarity of input literals in each clause
Vec_Int_t * vMapping; // mapping of internal nodes
};
......@@ -176,6 +177,7 @@ extern Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect );
extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder );
extern Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p );
/*=== cnfWrite.c ========================================================*/
extern Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped );
extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
......
src/sat/cnf/cnfMan.c
......@@ -182,6 +182,7 @@ void Cnf_DataFree( Cnf_Dat_t * p )
if ( p == NULL )
return;
Vec_IntFreeP( &p->vMapping );
ABC_FREE( p->pClaPols );
ABC_FREE( p->pObj2Clause );
ABC_FREE( p->pObj2Count );
ABC_FREE( p->pClauses[0] );
......
src/sat/cnf/cnfUtil.c
......@@ -229,6 +229,66 @@ Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
return vCoIds;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p )
{
int i, c, iClaBeg, iClaEnd, * pLit;
unsigned * pPols0 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) );
unsigned * pPols1 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) );
unsigned char * pPres = ABC_CALLOC( unsigned char, p->nClauses );
for ( i = 0; i < Aig_ManObjNumMax(p->pMan); i++ )
{
if ( p->pObj2Count[i] == 0 )
continue;
iClaBeg = p->pObj2Clause[i];
iClaEnd = p->pObj2Clause[i] + p->pObj2Count[i];
// go through the negative polarity clauses
for ( c = iClaBeg; c < iClaEnd; c++ )
for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
if ( Abc_LitIsCompl(p->pClauses[c][0]) )
pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
else
pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
// record these clauses
for ( c = iClaBeg; c < iClaEnd; c++ )
for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
if ( Abc_LitIsCompl(p->pClauses[c][0]) )
pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) );
else
pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) );
// clean negative polarity
for ( c = iClaBeg; c < iClaEnd; c++ )
for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
pPols0[Abc_Lit2Var(*pLit)] = pPols1[Abc_Lit2Var(*pLit)] = 0;
}
ABC_FREE( pPols0 );
ABC_FREE( pPols1 );
/*
// for ( c = 0; c < p->nClauses; c++ )
for ( c = 0; c < 100; c++ )
{
printf( "Clause %6d : ", c );
for ( i = 0; i < 4; i++ )
printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 );
printf( " " );
for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ )
printf( "%6d ", *pLit );
printf( "\n" );
}
*/
return pPres;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
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