summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw/sswCnf.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw/sswCnf.c')
-rw-r--r--src/aig/ssw/sswCnf.c124
1 files changed, 105 insertions, 19 deletions
diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c
index e4b8f9f6..d068bb78 100644
--- a/src/aig/ssw/sswCnf.c
+++ b/src/aig/ssw/sswCnf.c
@@ -30,6 +30,63 @@
/**Function*************************************************************
+ Synopsis [Starts the SAT manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ssw_Sat_t * Ssw_SatStart( int fPolarFlip )
+{
+ Ssw_Sat_t * p;
+ int Lit;
+ p = ALLOC( Ssw_Sat_t, 1 );
+ memset( p, 0, sizeof(Ssw_Sat_t) );
+ p->pAig = NULL;
+ p->fPolarFlip = fPolarFlip;
+ p->vSatVars = Vec_IntStart( 10000 );
+ p->vFanins = Vec_PtrAlloc( 100 );
+ p->vUsedPis = Vec_PtrAlloc( 100 );
+ p->pSat = sat_solver_new();
+ sat_solver_setnvars( p->pSat, 1000 );
+ // var 0 is not used
+ // var 1 is reserved for const1 node - add the clause
+ p->nSatVars = 1;
+ Lit = toLit( p->nSatVars );
+ if ( fPolarFlip )
+ Lit = lit_neg( Lit );
+ sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+// Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
+ Vec_IntWriteEntry( p->vSatVars, 0, p->nSatVars++ );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stop the SAT manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SatStop( Ssw_Sat_t * p )
+{
+ if ( p->pSat )
+ sat_solver_delete( p->pSat );
+ Vec_IntFree( p->vSatVars );
+ Vec_PtrFree( p->vFanins );
+ Vec_PtrFree( p->vUsedPis );
+ free( p );
+}
+
+/**Function*************************************************************
+
Synopsis [Addes clauses to the solver.]
Description []
@@ -39,7 +96,7 @@
SeeAlso []
***********************************************************************/
-void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
+void Ssw_AddClausesMux( Ssw_Sat_t * p, Aig_Obj_t * pNode )
{
Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
@@ -68,7 +125,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 1^fCompT);
pLits[2] = toLitCond(VarF, 0);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -79,7 +136,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 0^fCompT);
pLits[2] = toLitCond(VarF, 1);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -90,7 +147,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 1^fCompE);
pLits[2] = toLitCond(VarF, 0);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -101,7 +158,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 0^fCompE);
pLits[2] = toLitCond(VarF, 1);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -126,7 +183,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarT, 0^fCompT);
pLits[1] = toLitCond(VarE, 0^fCompE);
pLits[2] = toLitCond(VarF, 1);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -137,7 +194,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarT, 1^fCompT);
pLits[1] = toLitCond(VarE, 1^fCompE);
pLits[2] = toLitCond(VarF, 0);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -158,7 +215,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
+void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
{
Aig_Obj_t * pFanin;
int * pLits, nLits, RetValue, i;
@@ -173,7 +230,7 @@ void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
{
pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
pLits[1] = toLitCond(Ssw_ObjSatNum(p,pNode), 1);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
@@ -185,13 +242,13 @@ void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
Vec_PtrForEachEntry( vSuper, pFanin, i )
{
pLits[i] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
}
}
pLits[nLits-1] = toLitCond(Ssw_ObjSatNum(p,pNode), 0);
- if ( p->pPars->fPolarFlip )
+ if ( p->fPolarFlip )
{
if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
}
@@ -221,6 +278,7 @@ void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
Vec_PtrPushUnique( vSuper, pObj );
return;
}
+// pObj->fMarkA = 1;
// go through the branches
Ssw_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
Ssw_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
@@ -256,7 +314,7 @@ void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
SeeAlso []
***********************************************************************/
-void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+void Ssw_ObjAddToFrontier( Ssw_Sat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
{
assert( !Aig_IsComplement(pObj) );
if ( Ssw_ObjSatNum(p,pObj) )
@@ -264,12 +322,10 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
assert( Ssw_ObjSatNum(p,pObj) == 0 );
if ( Aig_ObjIsConst1(pObj) )
return;
- if ( p->pPars->fLatchCorrOpt )
- {
- Vec_PtrPush( p->vUsedNodes, pObj );
- if ( Aig_ObjIsPi(pObj) )
- Vec_PtrPush( p->vUsedPis, pObj );
- }
+// pObj->fMarkA = 1;
+ // save PIs (used by register correspondence)
+ if ( Aig_ObjIsPi(pObj) )
+ Vec_PtrPush( p->vUsedPis, pObj );
Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) );
if ( Aig_ObjIsNode(pObj) )
@@ -287,7 +343,7 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
SeeAlso []
***********************************************************************/
-void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj )
+void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj )
{
Vec_Ptr_t * vFrontier;
Aig_Obj_t * pNode, * pFanin;
@@ -327,6 +383,36 @@ void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj )
}
+/**Function*************************************************************
+
+ Synopsis [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj )
+{
+ int Value0, Value1, nVarNum;
+ assert( !Aig_IsComplement(pObj) );
+ nVarNum = Ssw_ObjSatNum( p, pObj );
+ if ( nVarNum > 0 )
+ return sat_solver_var_value( p->pSat, nVarNum );
+// if ( pObj->fMarkA == 1 )
+// return 0;
+ if ( Aig_ObjIsPi(pObj) )
+ return 0;
+ assert( Aig_ObjIsNode(pObj) );
+ Value0 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin0(pObj) );
+ Value0 ^= Aig_ObjFaninC0(pObj);
+ Value1 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin1(pObj) );
+ Value1 ^= Aig_ObjFaninC1(pObj);
+ return Value0 & Value1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-20 04:04:49 +0000