summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw')
-rw-r--r--src/aig/ssw/module.make3
-rw-r--r--src/aig/ssw/ssw.h5
-rw-r--r--src/aig/ssw/sswCore.c10
-rw-r--r--src/aig/ssw/sswInt.h9
-rw-r--r--src/aig/ssw/sswMan.c3
-rw-r--r--src/aig/ssw/sswSat.c34
-rw-r--r--src/aig/ssw/sswSweep.c32
-rw-r--r--src/aig/ssw/sswUnique.c254
8 files changed, 329 insertions, 21 deletions
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index 6b748598..625d72d1 100644
--- a/src/aig/ssw/module.make
+++ b/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
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 98e8c9d7..766407d4 100644
--- a/src/aig/ssw/ssw.h
+++ b/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 ===================================================*/
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 424e3531..8052ffcd 100644
--- a/src/aig/ssw/sswCore.c
+++ b/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;
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 5daffc75..636bd139 100644
--- a/src/aig/ssw/sswInt.h
+++ b/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
}
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index ba19d46e..d4a26f64 100644
--- a/src/aig/ssw/sswMan.c
+++ b/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 );
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c
index 264b39d1..af3bf80e 100644
--- a/src/aig/ssw/sswSat.c
+++ b/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;
- pLits[0] = lit_neg( pLits[0] );
- pLits[1] = lit_neg( pLits[1] );
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
- assert( RetValue );
+ 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;
- pLits[0] = lit_neg( pLits[0] );
- pLits[1] = lit_neg( pLits[1] );
- RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
- assert( RetValue );
+ 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 )
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index add00a88..b971a13a 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/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 );
}
@@ -179,7 +180,7 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
{
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
- return 0;
+ return 0;
// count the number of skipped calls
if ( !pObj->fMarkA && !pObjRepr->fMarkA )
p->nRefSkip++;
@@ -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) );
diff --git a/src/aig/ssw/sswUnique.c b/src/aig/ssw/sswUnique.c
new file mode 100644
index 00000000..888ed3da
--- /dev/null
+++ b/src/aig/ssw/sswUnique.c
@@ -0,0 +1,254 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-21 01:01:49 +0000