luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Extending sweeper to handle XORs.

This commit is contained in:
Alan Mishchenko 2020-11-15 19:02:41 -08:00
parent 28ea3adedb
commit dd07ec57be
6 changed files with 255 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/base/abci/abc.c
View File

@ -36292,9 +36292,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec_ManFraSetDefaultParams( pPars ); Cec_ManFraSetDefaultParams( pPars );
pPars->jType = 2; // solver type pPars->jType = 2; // solver type
pPars->fSatSweeping = 1; // conflict limit at a node pPars->fSatSweeping = 1; // conflict limit at a node
pPars->nWords = 8; // simulation words pPars->nWords = 4; // simulation words
pPars->nRounds = 10; // simulation rounds pPars->nRounds = 10; // simulation rounds
pPars->nItersMax = 1000000; // this is a miter pPars->nItersMax = 2000; // this is a miter
pPars->nBTLimit = 1000000; // use logic cones pPars->nBTLimit = 1000000; // use logic cones
pPars->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver pPars->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver
pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver

151
src/proof/cec/cecSatG2.c
View File

@ -32,6 +32,8 @@
#define sat_solver_start bmcg2_sat_solver_start #define sat_solver_start bmcg2_sat_solver_start
#define sat_solver_stop bmcg2_sat_solver_stop #define sat_solver_stop bmcg2_sat_solver_stop
#define sat_solver_addclause bmcg2_sat_solver_addclause #define sat_solver_addclause bmcg2_sat_solver_addclause
#define sat_solver_add_and bmcg2_sat_solver_add_and
#define sat_solver_add_xor bmcg2_sat_solver_add_xor
#define sat_solver_addvar bmcg2_sat_solver_addvar #define sat_solver_addvar bmcg2_sat_solver_addvar
#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue #define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
#define sat_solver_reset bmcg2_sat_solver_reset #define sat_solver_reset bmcg2_sat_solver_reset
@ -54,6 +56,8 @@
#define sat_solver_start bmcg_sat_solver_start #define sat_solver_start bmcg_sat_solver_start
#define sat_solver_stop bmcg_sat_solver_stop #define sat_solver_stop bmcg_sat_solver_stop
#define sat_solver_addclause bmcg_sat_solver_addclause #define sat_solver_addclause bmcg_sat_solver_addclause
#define sat_solver_add_and bmcg_sat_solver_add_and
#define sat_solver_add_xor bmcg_sat_solver_add_xor
#define sat_solver_addvar bmcg_sat_solver_addvar #define sat_solver_addvar bmcg_sat_solver_addvar
#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue #define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
#define sat_solver_reset bmcg_sat_solver_reset #define sat_solver_reset bmcg_sat_solver_reset
@ -94,6 +98,7 @@ struct Cec4_Man_t_
Vec_Int_t * vCands; Vec_Int_t * vCands;
Vec_Int_t * vVisit; Vec_Int_t * vVisit;
Vec_Int_t * vPat; Vec_Int_t * vPat;
Vec_Int_t * vDisprPairs;
Vec_Bit_t * vFails; Vec_Bit_t * vFails;
int iPosRead; // candidate reading position int iPosRead; // candidate reading position
int iPosWrite; // candidate writing position int iPosWrite; // candidate writing position
@ -167,6 +172,7 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
p->vCands = Vec_IntAlloc( 100 ); p->vCands = Vec_IntAlloc( 100 );
p->vVisit = Vec_IntAlloc( 100 ); p->vVisit = Vec_IntAlloc( 100 );
p->vPat = Vec_IntAlloc( 100 ); p->vPat = Vec_IntAlloc( 100 );
p->vDisprPairs = Vec_IntAlloc( 100 );
p->vFails = Vec_BitStart( Gia_ManObjNum(pAig) ); p->vFails = Vec_BitStart( Gia_ManObjNum(pAig) );
//pAig->pData = p->pSat; // point AIG manager to the solver //pAig->pData = p->pSat; // point AIG manager to the solver
return p; return p;
@ -207,6 +213,7 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
Vec_IntFreeP( &p->vCands ); Vec_IntFreeP( &p->vCands );
Vec_IntFreeP( &p->vVisit ); Vec_IntFreeP( &p->vVisit );
Vec_IntFreeP( &p->vPat ); Vec_IntFreeP( &p->vPat );
Vec_IntFreeP( &p->vDisprPairs );
Vec_BitFreeP( &p->vFails ); Vec_BitFreeP( &p->vFails );
Vec_IntFreeP( &p->vRefClasses ); Vec_IntFreeP( &p->vRefClasses );
Vec_IntFreeP( &p->vRefNodes ); Vec_IntFreeP( &p->vRefNodes );
@ -220,6 +227,8 @@ Gia_Man_t * Cec4_ManStartNew( Gia_Man_t * pAig )
Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(pAig) ); Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(pAig) );
pNew->pName = Abc_UtilStrsav( pAig->pName ); pNew->pName = Abc_UtilStrsav( pAig->pName );
pNew->pSpec = Abc_UtilStrsav( pAig->pSpec ); pNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
if ( pAig->pMuxes )
pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
Gia_ManFillValue( pAig ); Gia_ManFillValue( pAig );
Gia_ManConst0(pAig)->Value = 0; Gia_ManConst0(pAig)->Value = 0;
Gia_ManForEachCi( pAig, pObj, i ) Gia_ManForEachCi( pAig, pObj, i )
@ -437,7 +446,7 @@ void Cec4_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFronti
} }
int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj ) int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj )
{ {
int fUseAnd2 = 1; // enable simple CNF int fUseSimple = 1; // enable simple CNF
int fUseMuxes = 1; // enable MUXes when using complex CNF int fUseMuxes = 1; // enable MUXes when using complex CNF
Gia_Obj_t * pNode, * pFanin; Gia_Obj_t * pNode, * pFanin;
Gia_Obj_t * pObj = Gia_ManObj(p->pNew, iObj); Gia_Obj_t * pObj = Gia_ManObj(p->pNew, iObj);
@ -449,25 +458,29 @@ int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj )
if ( Gia_ObjIsCi(pObj) ) if ( Gia_ObjIsCi(pObj) )
return Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) ); return Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
assert( Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsAnd(pObj) );
if ( fUseAnd2 ) if ( fUseSimple )
{ {
Cec4_ObjGetCnfVar( p, Gia_ObjFaninId0(pObj, iObj) ); int iVar0 = Cec4_ObjGetCnfVar( p, Gia_ObjFaninId0(pObj, iObj) );
Cec4_ObjGetCnfVar( p, Gia_ObjFaninId1(pObj, iObj) ); int iVar1 = Cec4_ObjGetCnfVar( p, Gia_ObjFaninId1(pObj, iObj) );
Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) ); int iVar = Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
if( sat_solver_jftr( p->pSat ) < 2 ) if ( p->pPars->jType < 2 )
{ {
Vec_PtrClear( p->vFanins ); if ( Gia_ObjIsXor(pObj) )
Vec_PtrPush( p->vFanins, Gia_ObjChild0(pObj) ); sat_solver_add_xor( p->pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
Vec_PtrPush( p->vFanins, Gia_ObjChild1(pObj) ); else
Cec4_AddClausesSuper( p->pNew, pObj, p->vFanins, p->pSat ); sat_solver_add_and( p->pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
}
if ( 0 < p->pPars->jType )
{
int Lit0 = Abc_Var2Lit( iVar0, Gia_ObjFaninC0(pObj) );
int Lit1 = Abc_Var2Lit( iVar1, Gia_ObjFaninC1(pObj) );
if ( (Lit0 > Lit1) ^ Gia_ObjIsXor(pObj) )
Lit1 ^= Lit0, Lit0 ^= Lit1, Lit1 ^= Lit0;
sat_solver_set_var_fanin_lit( p->pSat, iVar, Lit0, Lit1 );
} }
if( 0 < sat_solver_jftr( p->pSat ) )
sat_solver_set_var_fanin_lit( p->pSat\
, Cec4_ObjSatId( p->pNew, pObj )\
, Abc_Var2Lit( Cec4_ObjSatId( p->pNew, Gia_ObjFanin0(pObj) ), Gia_ObjFaninC0(pObj) )\
, Abc_Var2Lit( Cec4_ObjSatId( p->pNew, Gia_ObjFanin1(pObj) ), Gia_ObjFaninC1(pObj) ) );
return Cec4_ObjSatId( p->pNew, pObj ); return Cec4_ObjSatId( p->pNew, pObj );
} }
assert( !Gia_ObjIsXor(pObj) );
// start the frontier // start the frontier
Vec_PtrClear( p->vFrontier ); Vec_PtrClear( p->vFrontier );
Cec4_ObjAddToFrontier( p->pNew, pObj, p->vFrontier, p->pSat ); Cec4_ObjAddToFrontier( p->pNew, pObj, p->vFrontier, p->pSat );
@ -728,6 +741,20 @@ static inline void Cec4_ObjSimAnd( Gia_Man_t * p, int iObj )
for ( w = 0; w < p->nSimWords; w++ ) for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = pSim0[w] & pSim1[w]; pSim[w] = pSim0[w] & pSim1[w];
} }
static inline void Cec4_ObjSimXor( Gia_Man_t * p, int iObj )
{
int w;
Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
word * pSim = Cec4_ObjSim( p, iObj );
word * pSim0 = Cec4_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) );
word * pSim1 = Cec4_ObjSim( p, Gia_ObjFaninId1(pObj, iObj) );
if ( Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = ~pSim0[w] ^ pSim1[w];
else
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = pSim0[w] ^ pSim1[w];
}
static inline void Cec4_ObjSimCi( Gia_Man_t * p, int iObj ) static inline void Cec4_ObjSimCi( Gia_Man_t * p, int iObj )
{ {
int w; int w;
@ -796,6 +823,9 @@ void Cec4_ManSimulate( Gia_Man_t * p, Cec4_Man_t * pMan )
Gia_ManForEachAnd( p, pObj, i ) Gia_ManForEachAnd( p, pObj, i )
{ {
int iRepr = Gia_ObjRepr( p, i ); int iRepr = Gia_ObjRepr( p, i );
if ( Gia_ObjIsXor(pObj) )
Cec4_ObjSimXor( p, i );
else
Cec4_ObjSimAnd( p, i ); Cec4_ObjSimAnd( p, i );
if ( iRepr == GIA_VOID || p->pReprs[iRepr].fColorA || Cec4_ObjSimEqual(p, iRepr, i) ) if ( iRepr == GIA_VOID || p->pReprs[iRepr].fColorA || Cec4_ObjSimEqual(p, iRepr, i) )
continue; continue;
@ -819,6 +849,9 @@ void Cec4_ManSimulate_rec( Gia_Man_t * p, Cec4_Man_t * pMan, int iObj )
assert( Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsAnd(pObj) );
Cec4_ManSimulate_rec( p, pMan, Gia_ObjFaninId0(pObj, iObj) ); Cec4_ManSimulate_rec( p, pMan, Gia_ObjFaninId0(pObj, iObj) );
Cec4_ManSimulate_rec( p, pMan, Gia_ObjFaninId1(pObj, iObj) ); Cec4_ManSimulate_rec( p, pMan, Gia_ObjFaninId1(pObj, iObj) );
if ( Gia_ObjIsXor(pObj) )
Cec4_ObjSimXor( p, iObj );
else
Cec4_ObjSimAnd( p, iObj ); Cec4_ObjSimAnd( p, iObj );
} }
void Cec4_ManSimAlloc( Gia_Man_t * p, int nWords ) void Cec4_ManSimAlloc( Gia_Man_t * p, int nWords )
@ -947,7 +980,7 @@ int Cec4_ManVerify_rec( Gia_Man_t * p, int iObj, sat_solver * pSat )
assert( Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsAnd(pObj) );
Value0 = Cec4_ManVerify_rec( p, Gia_ObjFaninId0(pObj, iObj), pSat ) ^ Gia_ObjFaninC0(pObj); Value0 = Cec4_ManVerify_rec( p, Gia_ObjFaninId0(pObj, iObj), pSat ) ^ Gia_ObjFaninC0(pObj);
Value1 = Cec4_ManVerify_rec( p, Gia_ObjFaninId1(pObj, iObj), pSat ) ^ Gia_ObjFaninC1(pObj); Value1 = Cec4_ManVerify_rec( p, Gia_ObjFaninId1(pObj, iObj), pSat ) ^ Gia_ObjFaninC1(pObj);
return pObj->fMark1 = Value0 & Value1; return pObj->fMark1 = Gia_ObjIsXor(pObj) ? Value0 ^ Value1 : Value0 & Value1;
} }
void Cec4_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, sat_solver * pSat ) void Cec4_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, sat_solver * pSat )
{ {
@ -986,7 +1019,7 @@ int Cec4_ManCexVerify_rec( Gia_Man_t * p, int iObj )
assert( Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsAnd(pObj) );
Value0 = Cec4_ManCexVerify_rec( p, Gia_ObjFaninId0(pObj, iObj) ) ^ Gia_ObjFaninC0(pObj); Value0 = Cec4_ManCexVerify_rec( p, Gia_ObjFaninId0(pObj, iObj) ) ^ Gia_ObjFaninC0(pObj);
Value1 = Cec4_ManCexVerify_rec( p, Gia_ObjFaninId1(pObj, iObj) ) ^ Gia_ObjFaninC1(pObj); Value1 = Cec4_ManCexVerify_rec( p, Gia_ObjFaninId1(pObj, iObj) ) ^ Gia_ObjFaninC1(pObj);
return pObj->fMark1 = Value0 & Value1; return pObj->fMark1 = Gia_ObjIsXor(pObj) ? Value0 ^ Value1 : Value0 & Value1;
} }
void Cec4_ManCexVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase ) void Cec4_ManCexVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase )
{ {
@ -1058,6 +1091,14 @@ int Cec4_ManPackAddPattern( Gia_Man_t * p, Vec_Int_t * vLits )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline int Cec4_ObjFan0IsAssigned( Gia_Obj_t * pObj )
{
return Gia_ObjFanin0(pObj)->fMark0 || Gia_ObjFanin0(pObj)->fMark1;
}
static inline int Cec4_ObjFan1IsAssigned( Gia_Obj_t * pObj )
{
return Gia_ObjFanin1(pObj)->fMark0 || Gia_ObjFanin1(pObj)->fMark1;
}
static inline int Cec4_ObjFan0HasValue( Gia_Obj_t * pObj, int v ) static inline int Cec4_ObjFan0HasValue( Gia_Obj_t * pObj, int v )
{ {
return (v ^ Gia_ObjFaninC0(pObj)) ? Gia_ObjFanin0(pObj)->fMark1 : Gia_ObjFanin0(pObj)->fMark0; return (v ^ Gia_ObjFaninC0(pObj)) ? Gia_ObjFanin0(pObj)->fMark1 : Gia_ObjFanin0(pObj)->fMark0;
@ -1095,7 +1136,43 @@ int Cec4_ManGeneratePatterns_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int Value, Ve
assert( Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsAnd(pObj) );
pFan0 = Gia_ObjFanin0(pObj); pFan0 = Gia_ObjFanin0(pObj);
pFan1 = Gia_ObjFanin1(pObj); pFan1 = Gia_ObjFanin1(pObj);
if ( Value ) if ( Gia_ObjIsXor(pObj) )
{
int Ass0 = Cec4_ObjFan0IsAssigned(pObj);
int Ass1 = Cec4_ObjFan1IsAssigned(pObj);
assert( Gia_ObjFaninC0(pObj) == 0 && Gia_ObjFaninC1(pObj) == 0 );
if ( Ass0 && Ass1 )
return Value == (Cec4_ObjFan0HasValue(pObj, 1) ^ Cec4_ObjFan1HasValue(pObj, 1));
if ( Ass0 )
{
int ValueInt = Value ^ Cec4_ObjFan0HasValue(pObj, 1);
if ( !Cec4_ManGeneratePatterns_rec(p, pFan1, ValueInt, vPat, vVisit) )
return 0;
}
else if ( Ass1 )
{
int ValueInt = Value ^ Cec4_ObjFan1HasValue(pObj, 1);
if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, ValueInt, vPat, vVisit) )
return 0;
}
else if ( Abc_Random(0) & 1 )
{
if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, 0, vPat, vVisit) )
return 0;
if ( Cec4_ObjFan1HasValue(pObj, !Value) || (!Cec4_ObjFan1HasValue(pObj, Value) && !Cec4_ManGeneratePatterns_rec(p, pFan1, Value, vPat, vVisit)) )
return 0;
}
else
{
if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, 1, vPat, vVisit) )
return 0;
if ( Cec4_ObjFan1HasValue(pObj, Value) || (!Cec4_ObjFan1HasValue(pObj, !Value) && !Cec4_ManGeneratePatterns_rec(p, pFan1, !Value, vPat, vVisit)) )
return 0;
}
assert( Value == (Cec4_ObjFan0HasValue(pObj, 1) ^ Cec4_ObjFan1HasValue(pObj, 1)) );
return 1;
}
else if ( Value )
{ {
if ( Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0) ) if ( Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0) )
return 0; return 0;
@ -1212,10 +1289,17 @@ int Cec4_ManCandIterNext( Cec4_Man_t * p )
int Cec4_ManGeneratePatterns( Cec4_Man_t * p ) int Cec4_ManGeneratePatterns( Cec4_Man_t * p )
{ {
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
int i, iCand, nPats = 64 * p->pAig->nSimWords, Count = 0, Packs = 0; int i, iCand, nPats = 100 * 64 * p->pAig->nSimWords, CountPat = 0, Packs = 0;
//int iRepr;
//Vec_IntForEachEntryDouble( p->vDisprPairs, iRepr, iCand, i )
// if ( iRepr == Gia_ObjRepr(p->pAig, iCand) )
// printf( "Pair %6d (%6d, %6d) (new repr = %9d) is FAILED to disprove.\n", i, iRepr, iCand, Gia_ObjRepr(p->pAig, iCand) );
// else
// printf( "Pair %6d (%6d, %6d) (new repr = %9d) is disproved.\n", i, iRepr, iCand, Gia_ObjRepr(p->pAig, iCand) );
//Vec_IntClear( p->vDisprPairs );
p->pAig->iPatsPi = 0; p->pAig->iPatsPi = 0;
Vec_WrdFill( p->pAig->vSimsPi, Vec_WrdSize(p->pAig->vSimsPi), 0 ); Vec_WrdFill( p->pAig->vSimsPi, Vec_WrdSize(p->pAig->vSimsPi), 0 );
for ( i = 0; i < 100 * nPats; i++ ) for ( i = 0; i < nPats; i++ )
if ( (iCand = Cec4_ManCandIterNext(p)) ) if ( (iCand = Cec4_ManCandIterNext(p)) )
{ {
int iRepr = Gia_ObjRepr( p->pAig, iCand ); int iRepr = Gia_ObjRepr( p->pAig, iCand );
@ -1227,20 +1311,22 @@ int Cec4_ManGeneratePatterns( Cec4_Man_t * p )
if ( Res ) if ( Res )
{ {
int Ret = Cec4_ManPackAddPattern( p->pAig, p->vPat ); int Ret = Cec4_ManPackAddPattern( p->pAig, p->vPat );
//Vec_IntPushTwo( p->vDisprPairs, iRepr, iCand );
Packs += Ret; Packs += Ret;
if ( Ret == 64 * p->pAig->nSimWords ) if ( Ret == 64 * p->pAig->nSimWords )
break; break;
if ( ++Count == 4 * 64 * p->pAig->nSimWords ) if ( ++CountPat == 8 * 64 * p->pAig->nSimWords )
break; break;
//Cec4_ManCexVerify( p->pAig, iRepr, iCand, iReprVal ^ iCandVal ); //Cec4_ManCexVerify( p->pAig, iRepr, iCand, iReprVal ^ iCandVal );
//Gia_ManCleanMark01( p->pAig ); //Gia_ManCleanMark01( p->pAig );
} }
} }
p->nSatSat += Count;
//printf( "%3d : %6.2f %% : Generated %d CEXs after trying %d pairs. Ave tries = %.2f. Ave packs = %.2f\n", p->nItersSim++, 100.0*Vec_IntSize(p->vCands)/Gia_ManAndNum(p->pAig),
// Count, 100 * nPats, (float)p->pPars->nGenIters * nPats / Abc_MaxInt(1, Count), (float)Packs / Abc_MaxInt(1, Count) );
p->timeGenPats += Abc_Clock() - clk; p->timeGenPats += Abc_Clock() - clk;
return Count >= 100 * nPats / 1000 / 2; p->nSatSat += CountPat;
//printf( "%3d : %6.2f %% : Generated %6d CEXs after trying %6d pairs. Ave packs = %9.2f Ave tries = %9.2f (Limit = %9.2f)\n",
// p->nItersSim++, 100.0*Vec_IntSize(p->vCands)/Gia_ManAndNum(p->pAig),
// CountPat, i, (float)Packs / Abc_MaxInt(1, CountPat), (float)i / Abc_MaxInt(1, CountPat), (float)nPats / p->pPars->nItersMax );
return CountPat >= i / p->pPars->nItersMax;
} }
@ -1291,7 +1377,7 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
clk = Abc_Clock(); clk = Abc_Clock();
iVar0 = Cec4_ObjGetCnfVar( p, iObj0 ); iVar0 = Cec4_ObjGetCnfVar( p, iObj0 );
iVar1 = Cec4_ObjGetCnfVar( p, iObj1 ); iVar1 = Cec4_ObjGetCnfVar( p, iObj1 );
if( sat_solver_jftr( p->pSat ) ) if( p->pPars->jType > 0 )
{ {
sat_solver_start_new_round( p->pSat ); sat_solver_start_new_round( p->pSat );
sat_solver_mark_cone( p->pSat, Cec4_ObjSatId(p->pNew, Gia_ManObj(p->pNew, iObj0)) ); sat_solver_mark_cone( p->pSat, Cec4_ObjSatId(p->pNew, Gia_ManObj(p->pNew, iObj0)) );
@ -1377,27 +1463,25 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose ); status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose );
if ( status == GLUCOSE_SAT ) if ( status == GLUCOSE_SAT )
{ {
int * pCex;
//printf( "Disproved: %d == %d.\n", Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value) ); //printf( "Disproved: %d == %d.\n", Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value) );
p->nSatSat++; p->nSatSat++;
p->nPatterns++; p->nPatterns++;
p->pAig->iPatsPi++; p->pAig->iPatsPi++;
assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
//Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
// Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) );
pCex = sat_solver_read_cex( p->pSat );
Vec_IntClear( p->vPat ); Vec_IntClear( p->vPat );
if ( pCex == NULL ) if ( 0 == p->pPars->jType )
{ {
Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i ) Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
Vec_IntPush( p->vPat, Abc_Var2Lit(IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat)) ); Vec_IntPush( p->vPat, Abc_Var2Lit(IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat)) );
} }
else else
{ {
int * pCex = sat_solver_read_cex( p->pSat );
int * pMap = Vec_IntArray(&p->pNew->vVarMap); int * pMap = Vec_IntArray(&p->pNew->vVarMap);
assert( p->pAig->pMuxes == NULL ); // no xors
for ( i = 0; i < pCex[0]; ) for ( i = 0; i < pCex[0]; )
Vec_IntPush( p->vPat, Abc_Lit2LitV(pMap, Abc_LitNot(pCex[++i])) ); Vec_IntPush( p->vPat, Abc_Lit2LitV(pMap, Abc_LitNot(pCex[++i])) );
} }
assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
Vec_IntForEachEntry( p->vPat, iLit, i ) Vec_IntForEachEntry( p->vPat, iLit, i )
Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) ); Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) );
if ( fEasy ) if ( fEasy )
@ -1549,6 +1633,9 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
{ {
Gia_Obj_t * pObjNew; Gia_Obj_t * pObjNew;
pMan->nAndNodes++; pMan->nAndNodes++;
if ( Gia_ObjIsXor(pObj) )
pObj->Value = Gia_ManHashXorReal( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
else
pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( pPars->nLevelMax && Gia_ObjLevel(p, pObj) > pPars->nLevelMax ) if ( pPars->nLevelMax && Gia_ObjLevel(p, pObj) > pPars->nLevelMax )
continue; continue;

64
src/sat/glucose/AbcGlucose.cpp
View File

@ -326,6 +326,38 @@ int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1
return 1; return 1;
} }
int bmcg_solver_add_xor( bmcg_sat_solver * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
{
int Lits[3];
int Cid;
assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 1 );
Lits[2] = Abc_Var2Lit( iVarC, 1 );
Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 0 );
Lits[2] = Abc_Var2Lit( iVarC, 0 );
Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
Lits[0] = Abc_Var2Lit( iVarA, fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 1 );
Lits[2] = Abc_Var2Lit( iVarC, 0 );
Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
Lits[0] = Abc_Var2Lit( iVarA, fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 0 );
Lits[2] = Abc_Var2Lit( iVarC, 1 );
Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
return 4;
}
int bmcg_sat_solver_jftr(bmcg_sat_solver* s) int bmcg_sat_solver_jftr(bmcg_sat_solver* s)
{ {
return ((Gluco::SimpSolver*)s)->jftr; return ((Gluco::SimpSolver*)s)->jftr;
@ -633,6 +665,38 @@ int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1
return 1; return 1;
} }
int bmcg_solver_add_xor( bmcg_sat_solver * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
{
int Lits[3];
int Cid;
assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 1 );
Lits[2] = Abc_Var2Lit( iVarC, 1 );
Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 0 );
Lits[2] = Abc_Var2Lit( iVarC, 0 );
Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
Lits[0] = Abc_Var2Lit( iVarA, fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 1 );
Lits[2] = Abc_Var2Lit( iVarC, 0 );
Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
Lits[0] = Abc_Var2Lit( iVarA, fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 0 );
Lits[2] = Abc_Var2Lit( iVarC, 1 );
Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
return 4;
}
int bmcg_sat_solver_jftr(bmcg_sat_solver* s) int bmcg_sat_solver_jftr(bmcg_sat_solver* s)
{ {
return ((Gluco::Solver*)s)->jftr; return ((Gluco::Solver*)s)->jftr;

1
src/sat/glucose/AbcGlucose.h
View File

@ -94,6 +94,7 @@ extern int bmcg_sat_solver_learntnum( bmcg_sat_solver* s );
extern int bmcg_sat_solver_conflictnum( bmcg_sat_solver* s ); extern int bmcg_sat_solver_conflictnum( bmcg_sat_solver* s );
extern int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot ); extern int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot );
extern int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl ); extern int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl );
extern int bmcg_sat_solver_add_xor( bmcg_sat_solver * s, int iVarA, int iVarB, int iVarC, int fCompl );
extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ); extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits );
extern int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv ); extern int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv );
extern Vec_Str_t * bmcg_sat_solver_sop( Gia_Man_t * p, int CubeLimit ); extern Vec_Str_t * bmcg_sat_solver_sop( Gia_Man_t * p, int CubeLimit );

64
src/sat/glucose2/AbcGlucose2.cpp
View File

@ -326,6 +326,38 @@ int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVa
return 1; return 1;
} }
int bmcg2_sat_solver_add_xor( bmcg2_sat_solver * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
{
int Lits[3];
int Cid;
assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 1 );
Lits[2] = Abc_Var2Lit( iVarC, 1 );
Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 0 );
Lits[2] = Abc_Var2Lit( iVarC, 0 );
Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
Lits[0] = Abc_Var2Lit( iVarA, fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 1 );
Lits[2] = Abc_Var2Lit( iVarC, 0 );
Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
Lits[0] = Abc_Var2Lit( iVarA, fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 0 );
Lits[2] = Abc_Var2Lit( iVarC, 1 );
Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
return 4;
}
int bmcg2_sat_solver_jftr(bmcg2_sat_solver* s) int bmcg2_sat_solver_jftr(bmcg2_sat_solver* s)
{ {
return ((Gluco2::SimpSolver*)s)->jftr; return ((Gluco2::SimpSolver*)s)->jftr;
@ -632,6 +664,38 @@ int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVa
return 1; return 1;
} }
int bmcg2_solver_add_xor( bmcg2_sat_solver * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
{
int Lits[3];
int Cid;
assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 1 );
Lits[2] = Abc_Var2Lit( iVarC, 1 );
Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 0 );
Lits[2] = Abc_Var2Lit( iVarC, 0 );
Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
Lits[0] = Abc_Var2Lit( iVarA, fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 1 );
Lits[2] = Abc_Var2Lit( iVarC, 0 );
Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
Lits[0] = Abc_Var2Lit( iVarA, fCompl );
Lits[1] = Abc_Var2Lit( iVarB, 0 );
Lits[2] = Abc_Var2Lit( iVarC, 1 );
Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
assert( Cid );
return 4;
}
int bmcg2_sat_solver_jftr(bmcg2_sat_solver* s) int bmcg2_sat_solver_jftr(bmcg2_sat_solver* s)
{ {
return ((Gluco2::Solver*)s)->jftr; return ((Gluco2::Solver*)s)->jftr;

1
src/sat/glucose2/AbcGlucose2.h
View File

@ -94,6 +94,7 @@ extern int bmcg2_sat_solver_learntnum( bmcg2_sat_solver* s );
extern int bmcg2_sat_solver_conflictnum( bmcg2_sat_solver* s ); extern int bmcg2_sat_solver_conflictnum( bmcg2_sat_solver* s );
extern int bmcg2_sat_solver_minimize_assumptions( bmcg2_sat_solver * s, int * plits, int nlits, int pivot ); extern int bmcg2_sat_solver_minimize_assumptions( bmcg2_sat_solver * s, int * plits, int nlits, int pivot );
extern int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl ); extern int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl );
extern int bmcg2_sat_solver_add_xor( bmcg2_sat_solver * s, int iVarA, int iVarB, int iVarC, int fCompl );
extern int bmcg2_sat_solver_quantify( bmcg2_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ); extern int bmcg2_sat_solver_quantify( bmcg2_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits );
extern int bmcg2_sat_solver_equiv_overlap_check( bmcg2_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv ); extern int bmcg2_sat_solver_equiv_overlap_check( bmcg2_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv );
extern Vec_Str_t * bmcg2_sat_solver_sop( Gia_Man_t * p, int CubeLimit ); extern Vec_Str_t * bmcg2_sat_solver_sop( Gia_Man_t * p, int CubeLimit );