summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/ssc/sscClass.c50
-rw-r--r--src/proof/ssc/sscCore.c125
-rw-r--r--src/proof/ssc/sscInt.h42
-rw-r--r--src/proof/ssc/sscSat.c334
-rw-r--r--src/proof/ssc/sscSim.c78
5 files changed, 518 insertions, 111 deletions
diff --git a/src/proof/ssc/sscClass.c b/src/proof/ssc/sscClass.c
index a6d2b5e3..308fbada 100644
--- a/src/proof/ssc/sscClass.c
+++ b/src/proof/ssc/sscClass.c
@@ -208,23 +208,26 @@ void Ssc_GiaSimProcessRefined( Gia_Man_t * p, Vec_Int_t * vRefined )
SeeAlso []
***********************************************************************/
+void Ssc_GiaClassesInit( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj;
+ int i;
+ assert( p->pReprs == NULL );
+ p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+ p->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
+ Gia_ManForEachObj( p, pObj, i )
+ Gia_ObjSetRepr( p, i, Gia_ObjIsCand(pObj) ? 0 : GIA_VOID );
+ if ( p->vClassOld == NULL )
+ p->vClassOld = Vec_IntAlloc( 100 );
+ if ( p->vClassNew == NULL )
+ p->vClassNew = Vec_IntAlloc( 100 );
+}
int Ssc_GiaClassesRefine( Gia_Man_t * p )
{
Vec_Int_t * vRefinedC;
Gia_Obj_t * pObj;
int i;
- if ( p->pReprs == NULL )
- {
- assert( p->pReprs == NULL );
- p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
- p->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
- Gia_ManForEachObj( p, pObj, i )
- Gia_ObjSetRepr( p, i, Gia_ObjIsCand(pObj) ? 0 : GIA_VOID );
- if ( p->vClassOld == NULL )
- p->vClassOld = Vec_IntAlloc( 100 );
- if ( p->vClassNew == NULL )
- p->vClassNew = Vec_IntAlloc( 100 );
- }
+ if ( p->pReprs != NULL );
vRefinedC = Vec_IntAlloc( 100 );
Gia_ManForEachCand( p, pObj, i )
if ( Gia_ObjIsTail(p, i) )
@@ -236,6 +239,29 @@ int Ssc_GiaClassesRefine( Gia_Man_t * p )
return 0;
}
+
+/**Function*************************************************************
+
+ Synopsis [Check if the pairs have been disproved.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs )
+{
+ int i, iRepr, iObj, Result = 1;
+ 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" );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index f2cd810a..1aada663 100644
--- a/src/proof/ssc/sscCore.c
+++ b/src/proof/ssc/sscCore.c
@@ -45,13 +45,14 @@ ABC_NAMESPACE_IMPL_START
void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
{
memset( p, 0, sizeof(Ssc_Pars_t) );
- p->nWords = 4; // the number of simulation words
+ p->nWords = 1; // the number of simulation words
p->nBTLimit = 1000; // conflict limit at a node
p->nSatVarMax = 5000; // the max number of SAT variables
p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
p->fVerbose = 0; // verbose stats
}
+
/**Function*************************************************************
Synopsis []
@@ -65,11 +66,15 @@ void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
***********************************************************************/
void Ssc_ManStop( Ssc_Man_t * p )
{
- if ( p->pSat )
- sat_solver_delete( p->pSat );
- Vec_IntFreeP( &p->vSatVars );
- Gia_ManStopP( &p->pFraig );
+ Vec_IntFreeP( &p->vFront );
+ Vec_IntFreeP( &p->vFanins );
+ Vec_IntFreeP( &p->vPattern );
+ Vec_IntFreeP( &p->vDisPairs );
Vec_IntFreeP( &p->vPivot );
+ Vec_IntFreeP( &p->vId2Var );
+ Vec_IntFreeP( &p->vVar2Id );
+ if ( p->pSat ) sat_solver_delete( p->pSat );
+ Gia_ManStopP( &p->pFraig );
ABC_FREE( p );
}
Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
@@ -80,33 +85,48 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
p->pAig = pAig;
p->pCare = pCare;
p->pFraig = Gia_ManDup( p->pCare );
+ Gia_ManHashStart( p->pFraig );
Gia_ManInvertPos( p->pFraig );
Ssc_ManStartSolver( p );
if ( p->pSat == NULL )
{
- printf( "Constraints are UNSAT after propagation.\n" );
+ printf( "Constraints are UNSAT after propagation (likely a bug!).\n" );
Ssc_ManStop( p );
return NULL;
}
- p->vPivot = Ssc_GiaFindPivotSim( p->pFraig );
+// p->vPivot = Ssc_GiaFindPivotSim( p->pFraig );
// Vec_IntFreeP( &p->vPivot );
- if ( p->vPivot == NULL )
- p->vPivot = Ssc_ManFindPivotSat( p );
+ p->vPivot = Ssc_ManFindPivotSat( p );
if ( p->vPivot == NULL )
{
printf( "Constraints are UNSAT or conflict limit is too low.\n" );
Ssc_ManStop( p );
return NULL;
}
+ sat_solver_bookmark( p->pSat );
Vec_IntPrint( p->vPivot );
+ Gia_ManSetPhasePattern( p->pAig, p->vPivot );
+ Gia_ManSetPhasePattern( p->pCare, p->vPivot );
+ if ( Gia_ManCheckCoPhase(p->pCare) )
+ {
+ printf( "Computed reference pattern violates %d constraints (this is a bug!).\n", Gia_ManCheckCoPhase(p->pCare) );
+ Ssc_ManStop( p );
+ return NULL;
+ }
+ // other things
+ p->vDisPairs = Vec_IntAlloc( 100 );
+ p->vPattern = Vec_IntAlloc( 100 );
+ p->vFanins = Vec_IntAlloc( 100 );
+ p->vFront = Vec_IntAlloc( 100 );
+ Ssc_GiaClassesInit( pAig );
return p;
}
/**Function*************************************************************
- Synopsis [Performs computation of AIGs with choices.]
+ Synopsis []
- Description [Takes several AIGs and performs choicing.]
+ Description []
SideEffects []
@@ -117,10 +137,11 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
{
Ssc_Man_t * p;
Gia_Man_t * pResult;
+ Gia_Obj_t * pObj, * pRepr;
clock_t clk, clkTotal = clock();
- int i;
+ int i, fCompl, status;
assert( Gia_ManRegNum(pCare) == 0 );
- assert( Gia_ManPiNum(pAig) == Gia_ManPiNum(pCare) );
+ assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) );
assert( Gia_ManIsNormalized(pAig) );
assert( Gia_ManIsNormalized(pCare) );
// reset random numbers
@@ -131,14 +152,74 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
return Gia_ManDup( pAig );
// perform simulation
clk = clock();
- for ( i = 0; i < 16; i++ )
+ if ( Gia_ManAndNum(pCare) == 0 ) // no constraints
{
- Ssc_GiaRandomPiPattern( pAig, 10, NULL );
- Ssc_GiaSimRound( pAig );
- Ssc_GiaClassesRefine( pAig );
- Gia_ManEquivPrintClasses( pAig, 0, 0 );
+ for ( i = 0; i < 16; i++ )
+ {
+ Ssc_GiaRandomPiPattern( pAig, 10, NULL );
+ Ssc_GiaSimRound( pAig );
+ Ssc_GiaClassesRefine( pAig );
+ Gia_ManEquivPrintClasses( pAig, 0, 0 );
+ }
}
p->timeSimInit += clock() - clk;
+
+ // prepare user's AIG
+ Gia_ManFillValue(pAig);
+ Gia_ManConst0(pAig)->Value = 0;
+ Gia_ManForEachCi( pAig, pObj, i )
+ pObj->Value = Gia_Obj2Lit( p->pFraig, Gia_ManCi(p->pFraig, i) );
+ // perform sweeping
+ Ssc_GiaResetPiPattern( pAig, pPars->nWords );
+ Ssc_GiaSavePiPattern( pAig, p->vPivot );
+ Gia_ManForEachCand( pAig, pObj, i )
+ {
+ if ( pAig->iPatsPi == 64 * pPars->nWords )
+ {
+ Ssc_GiaSimRound( pAig );
+ Ssc_GiaClassesRefine( pAig );
+ Gia_ManEquivPrintClasses( pAig, 0, 0 );
+ Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
+ Ssc_GiaResetPiPattern( pAig, pPars->nWords );
+ Ssc_GiaSavePiPattern( pAig, p->vPivot );
+ Vec_IntClear( p->vDisPairs );
+ }
+ 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 )
+ 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();
+ 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 );
+ }
+ else if ( status == l_Undef )
+ {
+ p->nSatCallsUndec++;
+ p->timeSatUndec += clock() - clk;
+ }
+ else assert( 0 );
+ }
+
// remember the resulting AIG
pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 );
if ( pResult == NULL )
@@ -163,11 +244,11 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
if ( p->nConstrs == 0 )
{
pAig = Gia_ManDup( p );
- pCare = Gia_ManStart( Gia_ManPiNum(p) + 2 );
+ pCare = Gia_ManStart( Gia_ManCiNum(p) + 2 );
pCare->pName = Abc_UtilStrsav( "care" );
- for ( i = 0; i < Gia_ManPiNum(p); i++ )
+ for ( i = 0; i < Gia_ManCiNum(p); i++ )
Gia_ManAppendCi( pCare );
- Gia_ManAppendCo( pCare, 1 );
+ Gia_ManAppendCo( pCare, 0 );
}
else
{
@@ -176,6 +257,8 @@ 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 );
}
+ pAig = Gia_ManDupLevelized( pResult = pAig );
+ Gia_ManStop( pResult );
pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
Gia_ManStop( pAig );
Gia_ManStop( pCare );
diff --git a/src/proof/ssc/sscInt.h b/src/proof/ssc/sscInt.h
index 21f5afc2..7e710c19 100644
--- a/src/proof/ssc/sscInt.h
+++ b/src/proof/ssc/sscInt.h
@@ -35,7 +35,6 @@
////////////////////////////////////////////////////////////////////////
-
ABC_NAMESPACE_HEADER_START
@@ -47,33 +46,37 @@ ABC_NAMESPACE_HEADER_START
typedef struct Ssc_Man_t_ Ssc_Man_t;
struct Ssc_Man_t_
{
- // parameters
+ // user data
Ssc_Pars_t * pPars; // choicing parameters
Gia_Man_t * pAig; // subject AIG
Gia_Man_t * pCare; // care set AIG
+ // internal data
Gia_Man_t * pFraig; // resulting AIG
- Vec_Int_t * vPivot; // one SAT pattern
- // SAT solving
sat_solver * pSat; // recyclable SAT solver
- Vec_Int_t * vSatVars; // mapping of each node into its SAT var
- Vec_Int_t * vUsedNodes; // nodes whose SAT vars are assigned
+ Vec_Int_t * vId2Var; // mapping of each node into its SAT var
+ Vec_Int_t * vVar2Id; // mapping of each SAT var into its node
+ Vec_Int_t * vPivot; // one SAT pattern
+ int nSatVarsPivot; // the number of variables for constraints
+ int nSatVars; // the current number of variables
+ // temporary storage
+ Vec_Int_t * vFront; // supergate fanins
+ Vec_Int_t * vFanins; // supergate fanins
+ Vec_Int_t * vPattern; // counter-example
+ Vec_Int_t * vDisPairs; // disproved pairs
+ // SAT calls statistics
int nRecycles; // the number of times SAT solver was recycled
int nCallsSince; // the number of calls since the last recycle
- Vec_Int_t * vFanins; // fanins of the CNF node
- // SAT calls statistics
int nSatCalls; // the number of SAT calls
- int nSatProof; // the number of proofs
- int nSatFailsReal; // the number of timeouts
int nSatCallsUnsat; // the number of unsat SAT calls
int nSatCallsSat; // the number of sat SAT calls
+ int nSatCallsUndec; // the number of undec SAT calls
// runtime stats
clock_t timeSimInit; // simulation and class computation
clock_t timeSimSat; // simulation of the counter-examples
- clock_t timeSat; // solving SAT
+ clock_t timeCnfGen; // generation of CNF
clock_t timeSatSat; // sat
clock_t timeSatUnsat; // unsat
clock_t timeSatUndec; // undecided
- clock_t timeChoice; // choice computation
clock_t timeOther; // other runtime
clock_t timeTotal; // total runtime
};
@@ -82,28 +85,33 @@ struct Ssc_Man_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-static inline int Ssc_ObjSatNum( Ssc_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vSatVars, Gia_ObjId(p->pFraig, pObj)); }
-static inline void Ssc_ObjSetSatNum( Ssc_Man_t * p, Gia_Obj_t * pObj, int Num ) { Vec_IntWriteEntry(p->vSatVars, Gia_ObjId(p->pFraig, pObj), Num); }
+static inline int Ssc_ObjSatVar( Ssc_Man_t * p, int iObj ) { return Vec_IntEntry(p->vId2Var, iObj); }
+static inline void Ssc_ObjSetSatVar( Ssc_Man_t * p, int iObj, int Num ) { Vec_IntWriteEntry(p->vId2Var, iObj, Num); Vec_IntWriteEntry(p->vVar2Id, Num, iObj); }
+static inline void Ssc_ObjCleanSatVar( Ssc_Man_t * p, int Num ) { Vec_IntWriteEntry(p->vId2Var, Vec_IntEntry(p->vVar2Id, Num), Num); Vec_IntWriteEntry(p->vVar2Id, Num, 0); }
-static inline int Ssc_ObjFraig( Ssc_Man_t * p, Gia_Obj_t * pObj ) { return pObj->Value; }
-static inline void Ssc_ObjSetFraig( Gia_Obj_t * pObj, int iNode ) { pObj->Value = iNode; }
+static inline int Ssc_ObjFraig( Ssc_Man_t * p, Gia_Obj_t * pObj ) { return pObj->Value; }
+static inline void Ssc_ObjSetFraig( Gia_Obj_t * pObj, int iNode ) { pObj->Value = iNode; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sscClass.c =================================================*/
+extern void Ssc_GiaClassesInit( Gia_Man_t * p );
extern int Ssc_GiaClassesRefine( Gia_Man_t * p );
+extern void Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs );
/*=== sscCnf.c ===================================================*/
extern void Ssc_CnfNodeAddToSolver( Ssc_Man_t * p, Gia_Obj_t * pObj );
/*=== sscCore.c ==================================================*/
/*=== sscSat.c ===================================================*/
-extern int Ssc_NodesAreEquiv( Ssc_Man_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
extern void Ssc_ManSatSolverRecycle( Ssc_Man_t * p );
extern void Ssc_ManStartSolver( Ssc_Man_t * p );
extern Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p );
+extern int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iObj, int fCompl );
/*=== sscSim.c ===================================================*/
+extern void Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords );
extern void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot );
+extern void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat );
extern void Ssc_GiaSimRound( Gia_Man_t * p );
extern Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p );
/*=== sscUtil.c ===================================================*/
diff --git a/src/proof/ssc/sscSat.c b/src/proof/ssc/sscSat.c
index 1519b89e..ea9c599f 100644
--- a/src/proof/ssc/sscSat.c
+++ b/src/proof/ssc/sscSat.c
@@ -29,6 +29,7 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+static inline int Ssc_ObjSatLit( Ssc_Man_t * p, int Lit ) { return Abc_Var2Lit( Ssc_ObjSatVar(p, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) ); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -36,6 +37,217 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
+ Synopsis [Addes clauses to the solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static void Gia_ManAddClausesMux( Ssc_Man_t * p, Gia_Obj_t * pNode )
+{
+ Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
+ int pLits[4], LitF, LitI, LitT, LitE, RetValue;
+ assert( !Gia_IsComplement( pNode ) );
+ assert( Gia_ObjIsMuxType( pNode ) );
+ // get nodes (I = if, T = then, E = else)
+ pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+ // get the Litiable numbers
+ LitF = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNode) );
+ LitI = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeI) );
+ LitT = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeT) );
+ LitE = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeE) );
+
+ // f = ITE(i, t, e)
+
+ // i' + t' + f
+ // i' + t + f'
+ // i + e' + f
+ // i + e + f'
+
+ // create four clauses
+ pLits[0] = Abc_LitNotCond(LitI, 1);
+ pLits[1] = Abc_LitNotCond(LitT, 1);
+ pLits[2] = Abc_LitNotCond(LitF, 0);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+ pLits[0] = Abc_LitNotCond(LitI, 1);
+ pLits[1] = Abc_LitNotCond(LitT, 0);
+ pLits[2] = Abc_LitNotCond(LitF, 1);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+ pLits[0] = Abc_LitNotCond(LitI, 0);
+ pLits[1] = Abc_LitNotCond(LitE, 1);
+ pLits[2] = Abc_LitNotCond(LitF, 0);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+ pLits[0] = Abc_LitNotCond(LitI, 0);
+ pLits[1] = Abc_LitNotCond(LitE, 0);
+ pLits[2] = Abc_LitNotCond(LitF, 1);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+
+ // two additional clauses
+ // t' & e' -> f'
+ // t & e -> f
+
+ // t + e + f'
+ // t' + e' + f
+
+ if ( LitT == LitE )
+ {
+// assert( fCompT == !fCompE );
+ return;
+ }
+
+ pLits[0] = Abc_LitNotCond(LitT, 0);
+ pLits[1] = Abc_LitNotCond(LitE, 0);
+ pLits[2] = Abc_LitNotCond(LitF, 1);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+ pLits[0] = Abc_LitNotCond(LitT, 1);
+ pLits[1] = Abc_LitNotCond(LitE, 1);
+ pLits[2] = Abc_LitNotCond(LitF, 0);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Addes clauses to the solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static void Gia_ManAddClausesSuper( Ssc_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSuper )
+{
+ int i, RetValue, Lit, LitNode, pLits[2];
+ assert( !Gia_IsComplement(pNode) );
+ assert( Gia_ObjIsAnd( pNode ) );
+ // suppose AND-gate is A & B = C
+ // add !A => !C or A + !C
+ // add !B => !C or B + !C
+ LitNode = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNode) );
+ Vec_IntForEachEntry( vSuper, Lit, i )
+ {
+ pLits[0] = Ssc_ObjSatLit( p, Lit );
+ pLits[1] = Abc_LitNot( LitNode );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ // update literals
+ Vec_IntWriteEntry( vSuper, i, Abc_LitNot(pLits[0]) );
+ }
+ // add A & B => C or !A + !B + C
+ Vec_IntPush( vSuper, LitNode );
+ RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vSuper), Vec_IntArray(vSuper) + Vec_IntSize(vSuper) );
+ assert( RetValue );
+ (void) RetValue;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Collects the supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static void Ssc_ManCollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
+{
+ // stop at complements, PIs, and MUXes
+ if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) || Gia_ObjIsMuxType(pObj) )
+ {
+ Vec_IntPushUnique( vSuper, Gia_Obj2Lit(p, pObj) );
+ return;
+ }
+ Ssc_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
+ Ssc_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
+}
+static void Ssc_ManCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
+{
+ assert( !Gia_IsComplement(pObj) );
+ assert( Gia_ObjIsAnd(pObj) );
+ Vec_IntClear( vSuper );
+ Ssc_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
+ Ssc_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the solver clause database.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static void Ssc_ManCnfAddToFrontier( Ssc_Man_t * p, int Id, Vec_Int_t * vFront )
+{
+ Gia_Obj_t * pObj;
+ assert( Id > 0 );
+ if ( Ssc_ObjSatVar(p, Id) )
+ return;
+ pObj = Gia_ManObj( p->pFraig, Id );
+ Ssc_ObjSetSatVar( p, Id, p->nSatVars++ );
+ sat_solver_setnvars( p->pSat, p->nSatVars + 100 );
+ if ( Gia_ObjIsAnd(pObj) )
+ Vec_IntPush( vFront, Id );
+}
+static void Ssc_ManCnfNodeAddToSolver( Ssc_Man_t * p, int NodeId )
+{
+ Gia_Obj_t * pNode;
+ int i, k, Id, Lit;
+ clock_t clk;
+ // quit if CNF is ready
+ if ( NodeId == 0 || Ssc_ObjSatVar(p, NodeId) )
+ return;
+clk = clock();
+ // start the frontier
+ Vec_IntClear( p->vFront );
+ Ssc_ManCnfAddToFrontier( p, NodeId, p->vFront );
+ // explore nodes in the frontier
+ Gia_ManForEachObjVec( p->vFront, p->pFraig, pNode, i )
+ {
+ // create the supergate
+ assert( Ssc_ObjSatVar(p, Gia_ObjId(p->pFraig, pNode)) );
+ if ( Gia_ObjIsMuxType(pNode) )
+ {
+ Vec_IntClear( p->vFanins );
+ Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pFraig, Gia_ObjFanin0(pNode) ) );
+ Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pFraig, Gia_ObjFanin1(pNode) ) );
+ Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pFraig, Gia_ObjFanin0(pNode) ) );
+ Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pFraig, Gia_ObjFanin1(pNode) ) );
+ Vec_IntForEachEntry( p->vFanins, Id, k )
+ Ssc_ManCnfAddToFrontier( p, Id, p->vFront );
+ Gia_ManAddClausesMux( p, pNode );
+ }
+ else
+ {
+ Ssc_ManCollectSuper( p->pFraig, pNode, p->vFanins );
+ Vec_IntForEachEntry( p->vFanins, Lit, k )
+ Ssc_ManCnfAddToFrontier( p, Abc_Lit2Var(Lit), p->vFront );
+ Gia_ManAddClausesSuper( p, pNode, p->vFanins );
+ }
+ assert( Vec_IntSize(p->vFanins) > 1 );
+ }
+p->timeCnfGen += clock() - clk;
+}
+
+
+/**Function*************************************************************
+
Synopsis [Starts the SAT solver for constraints.]
Description []
@@ -47,16 +259,25 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
void Ssc_ManStartSolver( Ssc_Man_t * p )
{
- Aig_Man_t * pAig = Gia_ManToAig( p->pFraig, 0 );
- Cnf_Dat_t * pDat = Cnf_Derive( pAig, 0 );
+ Aig_Man_t * pMan = Gia_ManToAig( p->pFraig, 0 );
+ Cnf_Dat_t * pDat = Cnf_Derive( pMan, 0 );
+ Gia_Obj_t * pObj;
sat_solver * pSat;
int i, status;
- assert( p->pSat == NULL && p->vSatVars == NULL );
- assert( Aig_ManObjNumMax(pAig) == Gia_ManObjNum(p->pFraig) );
- Aig_ManStop( pAig );
-//Cnf_DataWriteIntoFile( pDat, "dump.cnf", 1, NULL, NULL );
+ assert( p->pSat == NULL && p->vId2Var == NULL );
+ assert( Aig_ManObjNumMax(pMan) == Gia_ManObjNum(p->pFraig) );
+ Aig_ManStop( pMan );
// save variable mapping
- p->vSatVars = Vec_IntAllocArray( pDat->pVarNums, Gia_ManObjNum(p->pFraig) ); pDat->pVarNums = NULL;
+ p->nSatVarsPivot = p->nSatVars = pDat->nVars;
+ p->vId2Var = Vec_IntStart( Gia_ManCandNum(p->pAig) + Gia_ManCandNum(p->pCare) + 10 ); // mapping of each node into its SAT var
+ p->vVar2Id = Vec_IntStart( Gia_ManCandNum(p->pAig) + Gia_ManCandNum(p->pCare) + 10 ); // mapping of each SAT var into its node
+ Ssc_ObjSetSatVar( p, 0, pDat->pVarNums[0] );
+ Gia_ManForEachCi( p->pFraig, pObj, i )
+ {
+ int iObj = Gia_ObjId( p->pFraig, pObj );
+ Ssc_ObjSetSatVar( p, iObj, pDat->pVarNums[iObj] );
+ }
+//Cnf_DataWriteIntoFile( pDat, "dump.cnf", 1, NULL, NULL );
// start the SAT solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pDat->nVars + 1000 );
@@ -90,20 +311,109 @@ void Ssc_ManStartSolver( Ssc_Man_t * p )
SeeAlso []
***********************************************************************/
+void Ssc_ManCollectSatPattern( Ssc_Man_t * p, Vec_Int_t * vPattern )
+{
+ Gia_Obj_t * pObj;
+ int i;
+ Vec_IntClear( vPattern );
+ Gia_ManForEachCi( p->pFraig, pObj, i )
+ Vec_IntPush( vPattern, sat_solver_var_value(p->pSat, Ssc_ObjSatVar(p, Gia_ObjId(p->pFraig, pObj))) );
+}
Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p )
{
Vec_Int_t * vInit;
- Gia_Obj_t * pObj;
- int i, status;
+ int status;
status = sat_solver_solve( p->pSat, NULL, NULL, p->pPars->nBTLimit, 0, 0, 0 );
if ( status != l_True ) // unsat or undec
return NULL;
- vInit = Vec_IntAlloc( Gia_ManPiNum(p->pFraig) );
- Gia_ManForEachPi( p->pFraig, pObj, i )
- Vec_IntPush( vInit, sat_solver_var_value(p->pSat, Ssc_ObjSatNum(p, pObj)) );
+ vInit = Vec_IntAlloc( Gia_ManCiNum(p->pFraig) );
+ Ssc_ManCollectSatPattern( p, vInit );
return vInit;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
+{
+ int pLitsSat[2], RetValue;
+// if ( p->nTimeOut )
+// sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + clock() );
+
+ // create CNF
+ 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 );
+
+ // solve under assumptions
+ // A = 1; B = 0 OR A = 1; B = 1
+ 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 )
+ {
+ pLitsSat[0] = Abc_LitNot( pLitsSat[0] ); // compl
+ pLitsSat[1] = Abc_LitNot( pLitsSat[1] ); // compl
+ RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
+ assert( RetValue );
+ }
+ else if ( RetValue == l_True )
+ {
+ Ssc_ManCollectSatPattern( p, p->vPattern );
+ return l_True;
+ }
+ else // if ( RetValue1 == l_Undef )
+ return l_Undef;
+
+ // if the old node was constant 0, we already know the answer
+ if ( pLitsSat[1] == 0 )
+ return l_False;
+ assert( pLitsSat[1] > 1 );
+
+ // solve under assumptions
+ // A = 0; B = 1 OR A = 0; B = 0
+ 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 )
+ {
+ pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
+ pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
+ RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
+ assert( RetValue );
+ }
+ else if ( RetValue == l_True )
+ {
+ Ssc_ManCollectSatPattern( p, p->vPattern );
+ return l_True;
+ }
+ else // if ( RetValue1 == l_Undef )
+ return l_Undef;
+ return l_False;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/ssc/sscSim.c b/src/proof/ssc/sscSim.c
index 86837000..89585ba6 100644
--- a/src/proof/ssc/sscSim.c
+++ b/src/proof/ssc/sscSim.c
@@ -34,51 +34,31 @@ static inline word Ssc_Random2() { return ((word)Gia_ManRandom(0) << 3
static inline void Ssc_SimAnd( word * pSim, word * pSim0, word * pSim1, int nWords, int fComp0, int fComp1 )
{
int w;
- if ( fComp0 && fComp1 )
- for ( w = 0; w < nWords; w++ )
- pSim[w] = ~(pSim0[w] | pSim1[w]);
- else if ( fComp0 )
- for ( w = 0; w < nWords; w++ )
- pSim[w] = ~pSim0[w] & pSim1[w];
- else if ( fComp1 )
- for ( w = 0; w < nWords; w++ )
- pSim[w] = pSim0[w] & ~pSim1[w];
- else
- for ( w = 0; w < nWords; w++ )
- pSim[w] = pSim0[w] & pSim1[w];
+ if ( fComp0 && fComp1 ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] | pSim1[w]);
+ else if ( fComp0 ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~pSim0[w] & pSim1[w];
+ else if ( fComp1 ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] &~pSim1[w];
+ else for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] & pSim1[w];
}
static inline void Ssc_SimDup( word * pSim, word * pSim0, int nWords, int fComp0 )
{
int w;
- if ( fComp0 )
- for ( w = 0; w < nWords; w++ )
- pSim[w] = ~pSim0[w];
- else
- for ( w = 0; w < nWords; w++ )
- pSim[w] = pSim0[w];
+ if ( fComp0 ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~pSim0[w];
+ else for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w];
}
static inline void Ssc_SimConst( word * pSim, int nWords, int fComp0 )
{
int w;
- if ( fComp0 )
- for ( w = 0; w < nWords; w++ )
- pSim[w] = ~(word)0;
- else
- for ( w = 0; w < nWords; w++ )
- pSim[w] = 0;
+ if ( fComp0 ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(word)0;
+ else for ( w = 0; w < nWords; w++ ) pSim[w] = 0;
}
static inline void Ssc_SimOr( word * pSim, word * pSim0, int nWords, int fComp0 )
{
int w;
- if ( fComp0 )
- for ( w = 0; w < nWords; w++ )
- pSim[w] |= ~pSim0[w];
- else
- for ( w = 0; w < nWords; w++ )
- pSim[w] |= pSim0[w];
+ if ( fComp0 ) for ( w = 0; w < nWords; w++ ) pSim[w] |= ~pSim0[w];
+ else for ( w = 0; w < nWords; w++ ) pSim[w] |= pSim0[w];
}
static inline int Ssc_SimFindBitWord( word t )
@@ -145,9 +125,23 @@ void Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords )
p->iPatsPi = 0;
if ( p->vSimsPi == NULL )
p->vSimsPi = Vec_WrdStart(0);
- Vec_WrdFill( p->vSimsPi, nWords * Gia_ManPiNum(p), 0 );
+ Vec_WrdFill( p->vSimsPi, nWords * Gia_ManCiNum(p), 0 );
assert( nWords == Gia_ObjSimWords( p ) );
}
+void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat )
+{
+ word * pSimPi;
+ int i;
+ assert( Vec_IntSize(vPat) == Gia_ManCiNum(p) );
+ if ( p->iPatsPi == 64 * Gia_ObjSimWords(p) )
+ Vec_WrdDoubleSimInfo( p->vSimsPi, Gia_ManCiNum(p) );
+ assert( p->iPatsPi < 64 * Gia_ObjSimWords(p) );
+ pSimPi = Gia_ObjSimPi( p, 0 );
+ for ( i = 0; i < Gia_ManCiNum(p); i++, pSimPi += Gia_ObjSimWords(p) )
+ if ( Vec_IntEntry(vPat, i) )
+ Abc_InfoSetBit( (unsigned *)pSimPi, p->iPatsPi );
+ p->iPatsPi++;
+}
void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot )
{
word * pSimPi;
@@ -163,20 +157,6 @@ void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot )
// Extra_PrintBinary( stdout, (unsigned *)pSimPi, 64 ), printf( "\n" );
}
}
-void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat )
-{
- word * pSimPi;
- int i;
- assert( Vec_IntSize(vPat) == Gia_ManPiNum(p) );
- if ( p->iPatsPi == 64 * Gia_ObjSimWords(p) )
- Vec_WrdDoubleSimInfo( p->vSimsPi, Gia_ManPiNum(p) );
- assert( p->iPatsPi < 64 * Gia_ObjSimWords(p) );
- pSimPi = Gia_ObjSimPi( p, 0 );
- for ( i = 0; i < Gia_ManPiNum(p); i++, pSimPi += Gia_ObjSimWords(p) )
- if ( Vec_IntEntry(vPat, i) )
- Abc_InfoSetBit( (unsigned *)pSimPi, p->iPatsPi );
- p->iPatsPi++;
-}
/**Function*************************************************************
@@ -191,7 +171,7 @@ void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat )
***********************************************************************/
void Ssc_GiaResetSimInfo( Gia_Man_t * p )
{
- assert( Vec_WrdSize(p->vSimsPi) % Gia_ManPiNum(p) == 0 );
+ assert( Vec_WrdSize(p->vSimsPi) % Gia_ManCiNum(p) == 0 );
if ( p->vSims == NULL )
p->vSims = Vec_WrdAlloc(0);
Vec_WrdFill( p->vSims, Gia_ObjSimWords(p) * Gia_ManObjNum(p), 0 );
@@ -208,7 +188,7 @@ void Ssc_GiaSimRound( Gia_Man_t * p )
// primary inputs
pSim = Gia_ObjSim( p, 1 );
pSim0 = Gia_ObjSimPi( p, 0 );
- Gia_ManForEachPi( p, pObj, i )
+ Gia_ManForEachCi( p, pObj, i )
{
assert( pSim == Gia_ObjSimObj( p, pObj ) );
Ssc_SimDup( pSim, pSim0, nWords, 0 );
@@ -216,7 +196,7 @@ void Ssc_GiaSimRound( Gia_Man_t * p )
pSim0 += nWords;
}
// intermediate nodes
- pSim = Gia_ObjSim( p, 1+Gia_ManPiNum(p) );
+ pSim = Gia_ObjSim( p, 1+Gia_ManCiNum(p) );
Gia_ManForEachAnd( p, pObj, i )
{
assert( pSim == Gia_ObjSim( p, i ) );
@@ -260,7 +240,7 @@ Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p )
if ( iBit == -1 )
return NULL;
vInit = Vec_IntAlloc( 100 );
- Gia_ManForEachPi( p, pObj, i )
+ Gia_ManForEachCi( p, pObj, i )
Vec_IntPush( vInit, Abc_InfoHasBit((unsigned *)Gia_ObjSimObj(p, pObj), iBit) );
return vInit;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-20 00:13:46 +0000