Skip to content

A
abc
Commit 17a0d944 by Alan Mishchenko
Options

SAT sweeping under constraints.

parent 613e8b2a
Showing with 96 additions and 37 deletions
src/base/abci/abc.c
......@@ -27186,14 +27186,15 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9CFraig(): There is no AIG.\n" );
return 1;
}
Abc_Print( 0, "Current AIG contains %d constraints.\n", pAbc->pGia->nConstrs );
pTemp = Ssc_PerformSweepingConstr( pAbc->pGia, pPars );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &cfraig [-WC <num>] [-rmdwvh]\n" );
Abc_Print( -2, "\t performs conditional combinational SAT sweeping\n" );
Abc_Print( -2, "\t performs combinational SAT sweeping under constraints\n" );
Abc_Print( -2, "\t which are present in the AIG or set manually using \"constr\"\n" );
Abc_Print( -2, "\t (constraints are listed as last POs and true when they are 0)\n" );
Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
......
src/proof/ssc/sscClass.c
......@@ -257,8 +257,8 @@ void Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs )
Vec_IntForEachEntryDouble( vDisPairs, iRepr, iObj, i )
if ( iRepr == Gia_ObjRepr(p, iObj) )
printf( "Pair (%d, %d) are still equivalent.\n", iRepr, iObj ), Result = 0;
if ( Result )
printf( "Classes are refined correctly.\n" );
// if ( Result )
// printf( "Classes are refined correctly.\n" );
}
......
src/proof/ssc/sscCore.c
......@@ -52,7 +52,6 @@ void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
p->fVerbose = 0; // verbose stats
}
/**Function*************************************************************
Synopsis []
......@@ -104,7 +103,7 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
return NULL;
}
sat_solver_bookmark( p->pSat );
Vec_IntPrint( p->vPivot );
// Vec_IntPrint( p->vPivot );
Gia_ManSetPhasePattern( p->pAig, p->vPivot );
Gia_ManSetPhasePattern( p->pCare, p->vPivot );
if ( Gia_ManCheckCoPhase(p->pCare) )
......@@ -121,6 +120,26 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
Ssc_GiaClassesInit( pAig );
return p;
}
void Ssc_ManPrintStats( Ssc_Man_t * p )
{
Abc_Print( 1, "Parameters: SimWords = %d. SatConfs = %d. SatVarMax = %d. CallsRec = %d. Verbose = %d.\n",
p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax, p->pPars->nCallsRecycle, p->pPars->fVerbose );
Abc_Print( 1, "SAT calls : Total = %d. Proof = %d. Cex = %d. Undec = %d.\n",
p->nSatCalls, p->nSatCallsUnsat, p->nSatCallsSat, p->nSatCallsUndec );
Abc_Print( 1, "SAT solver: Vars = %d. Clauses = %d. Recycles = %d. Sim rounds = %d.\n",
sat_solver_nvars(p->pSat), sat_solver_nclauses(p->pSat), p->nRecycles, p->nSimRounds );
p->timeOther = p->timeTotal - p->timeSimInit - p->timeSimSat - p->timeCnfGen - p->timeSatSat - p->timeSatUnsat - p->timeSatUndec;
ABC_PRTP( "Initialization ", p->timeSimInit, p->timeTotal );
ABC_PRTP( "SAT simulation ", p->timeSimSat, p->timeTotal );
ABC_PRTP( "CNF generation ", p->timeSimSat, p->timeTotal );
ABC_PRTP( "SAT solving ", p->timeSat-p->timeCnfGen, p->timeTotal );
ABC_PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
ABC_PRTP( " sat ", p->timeSatSat, p->timeTotal );
ABC_PRTP( " undecided ", p->timeSatUndec, p->timeTotal );
ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
}
/**Function*************************************************************
......@@ -140,6 +159,7 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
Gia_Obj_t * pObj, * pRepr;
clock_t clk, clkTotal = clock();
int i, fCompl, status;
clk = clock();
assert( Gia_ManRegNum(pCare) == 0 );
assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) );
assert( Gia_ManIsNormalized(pAig) );
......@@ -151,13 +171,13 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
if ( p == NULL )
return Gia_ManDup( pAig );
// perform simulation
clk = clock();
if ( Gia_ManAndNum(pCare) == 0 ) // no constraints
{
for ( i = 0; i < 16; i++ )
{
Ssc_GiaRandomPiPattern( pAig, 10, NULL );
Ssc_GiaSimRound( pAig );
if ( pPars->fVerbose )
Ssc_GiaClassesRefine( pAig );
Gia_ManEquivPrintClasses( pAig, 0, 0 );
}
......@@ -176,63 +196,86 @@ p->timeSimInit += clock() - clk;
{
if ( pAig->iPatsPi == 64 * pPars->nWords )
{
clk = clock();
Ssc_GiaSimRound( pAig );
Ssc_GiaClassesRefine( pAig );
if ( pPars->fVerbose )
Gia_ManEquivPrintClasses( pAig, 0, 0 );
Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
Vec_IntClear( p->vDisPairs );
// prepare next patterns
Ssc_GiaResetPiPattern( pAig, pPars->nWords );
Ssc_GiaSavePiPattern( pAig, p->vPivot );
Vec_IntClear( p->vDisPairs );
p->timeSimSat += clock() - clk;
}
if ( Gia_ObjIsAnd(pObj) )
pObj->Value = Gia_ManHashAnd( p->pFraig, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( !Gia_ObjHasRepr(pAig, i) )
continue;
pRepr = Gia_ObjReprObj(pAig, i);
if ( pRepr->Value == pObj->Value )
if ( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase ) )
continue;
assert( Abc_Lit2Var(pRepr->Value) != Abc_Lit2Var(pObj->Value) );
fCompl = pRepr->fPhase ^ pObj->fPhase ^ Abc_LitIsCompl(pRepr->Value) ^ Abc_LitIsCompl(pObj->Value);
// perform SAT call
clk = clock();
clk = clock();
p->nSatCalls++;
status = Ssc_ManCheckEquivalence( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl );
if ( status == l_False )
{
p->nSatCallsUnsat++;
p->timeSatUnsat += clock() - clk;
pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
}
else if ( status == l_True )
{
p->nSatCallsSat++;
p->timeSatSat += clock() - clk;
Ssc_GiaSavePiPattern( pAig, p->vPattern );
Vec_IntPush( p->vDisPairs, Gia_ObjRepr(p->pAig, i) );
Vec_IntPush( p->vDisPairs, i );
// printf( "Try %2d and %2d: ", Gia_ObjRepr(p->pAig, i), i );
// Vec_IntPrint( p->vPattern );
}
else if ( status == l_Undef )
{
p->nSatCallsUndec++;
p->timeSatUndec += clock() - clk;
}
else assert( 0 );
p->timeSat += clock() - clk;
}
if ( pAig->iPatsPi > 1 )
{
clk = clock();
while ( pAig->iPatsPi < 64 * pPars->nWords )
Ssc_GiaSavePiPattern( pAig, p->vPivot );
Ssc_GiaSimRound( pAig );
Ssc_GiaClassesRefine( pAig );
if ( pPars->fVerbose )
Gia_ManEquivPrintClasses( pAig, 0, 0 );
Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
Vec_IntClear( p->vDisPairs );
p->timeSimSat += clock() - clk;
}
// Gia_ManEquivPrintClasses( pAig, 1, 0 );
// remember the resulting AIG
// generate the resulting AIG
pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 );
if ( pResult == NULL )
{
printf( "There is no equivalences.\n" );
ABC_FREE( pAig->pReprs );
ABC_FREE( pAig->pNexts );
pResult = Gia_ManDup( pAig );
}
p->timeTotal = clock() - clkTotal;
if ( pPars->fVerbose )
Ssc_ManPrintStats( p );
Ssc_ManStop( p );
// count the number of representatives
if ( pPars->fVerbose )
{
Gia_ManEquivPrintClasses( pAig, 0, 0 );
Abc_Print( 1, "Reduction in AIG nodes:%8d ->%8d. ", Gia_ManAndNum(pAig), Gia_ManAndNum(pResult) );
// Gia_ManEquivPrintClasses( pAig, 0, 0 );
Abc_Print( 1, "Reduction in AIG nodes:%8d ->%8d (%6.2f %%). ",
Gia_ManAndNum(pAig), Gia_ManAndNum(pResult),
100.0 - 100.0 * Gia_ManAndNum(pResult) / Gia_ManAndNum(pAig) );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
return pResult;
......@@ -241,6 +284,8 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
{
Gia_Man_t * pAig, * pCare, * pResult;
int i;
if ( pPars->fVerbose )
Abc_Print( 0, "SAT sweeping AIG with %d constraints.\n", p->nConstrs );
if ( p->nConstrs == 0 )
{
pAig = Gia_ManDup( p );
......@@ -257,6 +302,14 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
pCare = Gia_ManDupCones( p, Vec_IntArray(vOuts) + Gia_ManPoNum(p) - p->nConstrs, p->nConstrs, 0 );
Vec_IntFree( vOuts );
}
if ( pPars->fVerbose )
{
printf( "User AIG: " );
Gia_ManPrintStats( pAig, 0, 0, 0 );
printf( "Care AIG: " );
Gia_ManPrintStats( pCare, 0, 0, 0 );
}
pAig = Gia_ManDupLevelized( pResult = pAig );
Gia_ManStop( pResult );
pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
......
src/proof/ssc/sscInt.h
......@@ -64,6 +64,7 @@ struct Ssc_Man_t_
Vec_Int_t * vPattern; // counter-example
Vec_Int_t * vDisPairs; // disproved pairs
// SAT calls statistics
int nSimRounds; // the number of simulation rounds
int nRecycles; // the number of times SAT solver was recycled
int nCallsSince; // the number of calls since the last recycle
int nSatCalls; // the number of SAT calls
......@@ -74,6 +75,7 @@ struct Ssc_Man_t_
clock_t timeSimInit; // simulation and class computation
clock_t timeSimSat; // simulation of the counter-examples
clock_t timeCnfGen; // generation of CNF
clock_t timeSat; // total SAT time
clock_t timeSatSat; // sat
clock_t timeSatUnsat; // unsat
clock_t timeSatUndec; // undecided
......
src/proof/ssc/sscSat.c
......@@ -210,8 +210,9 @@ static void Ssc_ManCnfNodeAddToSolver( Ssc_Man_t * p, int NodeId )
Gia_Obj_t * pNode;
int i, k, Id, Lit;
clock_t clk;
assert( NodeId > 0 );
// quit if CNF is ready
if ( NodeId == 0 || Ssc_ObjSatVar(p, NodeId) )
if ( Ssc_ObjSatVar(p, NodeId) )
return;
clk = clock();
// start the frontier
......@@ -345,33 +346,24 @@ Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p )
int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
{
int pLitsSat[2], RetValue;
clock_t clk;
assert( iRepr < iNode );
// if ( p->nTimeOut )
// sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + clock() );
// create CNF
if ( iRepr )
Ssc_ManCnfNodeAddToSolver( p, iRepr );
Ssc_ManCnfNodeAddToSolver( p, iNode );
sat_solver_compress( p->pSat );
// order the literals
pLitsSat[0] = Abc_Var2Lit( Ssc_ObjSatVar(p, iRepr), 0 );
pLitsSat[1] = Abc_Var2Lit( Ssc_ObjSatVar(p, iNode), 0 );
if ( pLitsSat[0] < pLitsSat[1] )
ABC_SWAP( int, pLitsSat[0], pLitsSat[1] );
// correct polarity
pLitsSat[1] = Abc_LitNotCond( pLitsSat[1], !fCompl ); // extra complement!
if ( !Abc_LitIsCompl(pLitsSat[1]) )
{
pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
}
assert( pLitsSat[0] > pLitsSat[1] );
assert( Abc_LitIsCompl(pLitsSat[1]) );
assert( pLitsSat[1] != 0 );
pLitsSat[1] = Abc_Var2Lit( Ssc_ObjSatVar(p, iNode), fCompl ^ (int)(iRepr > 0) );
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
// A = 1; B = 0
clk = clock();
RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_False )
{
......@@ -379,22 +371,27 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
pLitsSat[1] = Abc_LitNot( pLitsSat[1] ); // compl
RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
assert( RetValue );
p->timeSatUnsat += clock() - clk;
}
else if ( RetValue == l_True )
{
Ssc_ManCollectSatPattern( p, p->vPattern );
p->timeSatSat += clock() - clk;
return l_True;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatUndec += clock() - clk;
return l_Undef;
}
// if the old node was constant 0, we already know the answer
if ( pLitsSat[1] == 0 )
if ( iRepr == 0 )
return l_False;
assert( pLitsSat[1] > 1 );
// solve under assumptions
// A = 0; B = 1 OR A = 0; B = 0
// A = 0; B = 1
clk = clock();
RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_False )
{
......@@ -402,14 +399,19 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
assert( RetValue );
p->timeSatUnsat += clock() - clk;
}
else if ( RetValue == l_True )
{
Ssc_ManCollectSatPattern( p, p->vPattern );
p->timeSatSat += clock() - clk;
return l_True;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatUndec += clock() - clk;
return l_Undef;
}
return l_False;
}
......
src/proof/ssc/sscSim.c
......@@ -212,6 +212,7 @@ void Ssc_GiaSimRound( Gia_Man_t * p )
assert( pSim == Gia_ObjSimObj( p, pObj ) );
pSim0 = pSim - pObj->iDiff0 * nWords;
Ssc_SimDup( pSim, pSim0, nWords, Gia_ObjFaninC0(pObj) );
// Extra_PrintBinary( stdout, pSim, 64 ), printf( "\n" );
pSim += nWords;
}
}
......
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