summaryrefslogtreecommitdiffstats
path: root/src/sat/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/aig')
-rw-r--r--src/sat/aig/aig.h3
-rw-r--r--src/sat/aig/aigNode.c23
-rw-r--r--src/sat/aig/fraigCore.c2
-rw-r--r--src/sat/aig/rwrMffc.c303
-rw-r--r--src/sat/aig/rwrTruth.c2
-rw-r--r--src/sat/aig/rwr_.c48
6 files changed, 377 insertions, 4 deletions
diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
index ee029789..c83af527 100644
--- a/src/sat/aig/aig.h
+++ b/src/sat/aig/aig.h
@@ -300,8 +300,9 @@ extern void Aig_ManStop( Aig_Man_t * p );
/*=== aigNode.c =============================================================*/
extern Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p );
extern Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p );
-extern Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin );
+extern Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p );
extern Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 );
+extern Aig_Node_t * Aig_NodeConnectPo( Aig_Man_t * p, Aig_Node_t * pNode, Aig_Node_t * pFanin );
extern void Aig_NodeConnectAnd( Aig_Node_t * pFanin0, Aig_Node_t * pFanin1, Aig_Node_t * pNode );
extern void Aig_NodeDisconnectAnd( Aig_Node_t * pNode );
extern void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot );
diff --git a/src/sat/aig/aigNode.c b/src/sat/aig/aigNode.c
index 991cc7e5..ce458353 100644
--- a/src/sat/aig/aigNode.c
+++ b/src/sat/aig/aigNode.c
@@ -104,12 +104,30 @@ Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p )
SeeAlso []
***********************************************************************/
-Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin )
+Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p )
{
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
pNode->Type = AIG_PO;
Vec_PtrPush( p->vPos, pNode );
+ return pNode;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates a primary output node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Node_t * Aig_NodeConnectPo( Aig_Man_t * p, Aig_Node_t * pNode, Aig_Node_t * pFanin )
+{
+ assert( Aig_NodeIsPo(pNode) );
+ assert( !Aig_IsComplement(pNode) );
// connect to the fanin
pNode->Fans[0].fComp = Aig_IsComplement(pFanin);
pNode->Fans[0].iNode = Aig_Regular(pFanin)->Id;
@@ -224,13 +242,14 @@ void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot )
assert( !Aig_IsComplement(pRoot) );
assert( pRoot->nRefs == 0 );
assert( Aig_NodeIsAnd(pRoot) );
- // save the children
+ // remember the children
pNode0 = Aig_NodeFanin0(pRoot);
pNode1 = Aig_NodeFanin1(pRoot);
// disconnect the node
Aig_NodeDisconnectAnd( pRoot );
// recycle the node
Vec_PtrWriteEntry( pMan->vNodes, pRoot->Id, NULL );
+ memset( pRoot, 0, sizeof(Aig_Node_t) ); // this is a temporary hack to skip dead children below!!!
Aig_MemFixedEntryRecycle( pMan->mmNodes, (char *)pRoot );
// call recursively
if ( Aig_NodeIsAnd(pNode0) && pNode0->nRefs == 0 )
diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c
index decf05ee..525d4a14 100644
--- a/src/sat/aig/fraigCore.c
+++ b/src/sat/aig/fraigCore.c
@@ -92,7 +92,7 @@ Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan )
// solve the miter
clk = clock();
pMan->pSat->verbosity = pMan->pParam->fSatVerbose;
- status = solver_solve( pMan->pSat, NULL, NULL, pMan->pParam->nSeconds );
+ status = solver_solve( pMan->pSat, NULL, NULL, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nImpLimit );
if ( status == l_Undef )
{
// printf( "The problem timed out.\n" );
diff --git a/src/sat/aig/rwrMffc.c b/src/sat/aig/rwrMffc.c
new file mode 100644
index 00000000..663534b3
--- /dev/null
+++ b/src/sat/aig/rwrMffc.c
@@ -0,0 +1,303 @@
+/**CFile****************************************************************
+
+ FileName [rwrMffc.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis [Procedures working with Maximum Fanout-Free Cones.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rwrMffc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+extern int Aig_NodeDeref_rec( Aig_Node_t * pNode );
+extern int Aig_NodeRef_rec( Aig_Node_t * pNode );
+extern void Aig_NodeMffsConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
+extern void Aig_NodeFactorConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_MffcTest( Aig_Man_t * pMan )
+{
+ Aig_Node_t * pNode, * pNodeA, * pNodeB, * pNodeC, * pLeaf;
+ Vec_Ptr_t * vCone, * vSupp;
+ int i, k;//, nNodes1, nNodes2;
+ int nSizes = 0;
+ int nCones = 0;
+ int nMuxes = 0;
+ int nExors = 0;
+
+ vCone = Vec_PtrAlloc( 100 );
+ vSupp = Vec_PtrAlloc( 100 );
+
+ // mark the multiple-fanout nodes
+ Aig_ManForEachAnd( pMan, pNode, i )
+ if ( pNode->nRefs > 1 )
+ pNode->fMarkA = 1;
+ // unmark the control inputs of MUXes and inputs of EXOR gates
+ Aig_ManForEachAnd( pMan, pNode, i )
+ {
+ if ( !Aig_NodeIsMuxType(pNode) )
+ continue;
+
+ pNodeC = Aig_NodeRecognizeMux( pNode, &pNodeA, &pNodeB );
+ // if real children are used, skip
+ if ( Aig_NodeFanin0(pNode)->nRefs > 1 || Aig_NodeFanin1(pNode)->nRefs > 1 )
+ continue;
+/*
+
+ if ( pNodeC->nRefs == 2 )
+ pNodeC->fMarkA = 0;
+ if ( Aig_Regular(pNodeA) == Aig_Regular(pNodeB) && Aig_Regular(pNodeA)->nRefs == 2 )
+ Aig_Regular(pNodeA)->fMarkA = 0;
+*/
+
+ if ( Aig_Regular(pNodeA) == Aig_Regular(pNodeB) )
+ nExors++;
+ else
+ nMuxes++;
+ }
+ // mark the PO drivers
+ Aig_ManForEachPo( pMan, pNode, i )
+ {
+ Aig_NodeFanin0(pNode)->fMarkA = 1;
+ Aig_NodeFanin0(pNode)->fMarkB = 1;
+ }
+
+
+ // print sizes of MFFCs
+ Aig_ManForEachAnd( pMan, pNode, i )
+ {
+ if ( !pNode->fMarkA )
+ continue;
+
+// nNodes1 = Aig_NodeDeref_rec( pNode );
+// Aig_NodeMffsConeSupp( pNode, vCone, vSupp );
+// nNodes2 = Aig_NodeRef_rec( pNode );
+// assert( nNodes1 == nNodes2 );
+
+ Aig_NodeFactorConeSupp( pNode, vCone, vSupp );
+
+ printf( "%6d : Fan = %4d. Co = %5d. Su = %5d. %s ",
+ pNode->Id, pNode->nRefs, Vec_PtrSize(vCone), Vec_PtrSize(vSupp), pNode->fMarkB? "po" : " " );
+
+ Vec_PtrForEachEntry( vSupp, pLeaf, k )
+ printf( " %d", pLeaf->Id );
+
+ printf( "\n" );
+
+ nSizes += Vec_PtrSize(vCone);
+ nCones++;
+ }
+ printf( "Nodes = %6d. MFFC sizes = %6d. Cones = %6d. nExors = %6d. Muxes = %6d.\n",
+ Aig_ManAndNum(pMan), nSizes, nCones, nExors, nMuxes );
+
+ // unmark the nodes
+ Aig_ManForEachNode( pMan, pNode, i )
+ {
+ pNode->fMarkA = 0;
+ pNode->fMarkB = 0;
+ pNode->fMarkC = 0;
+ }
+
+ Vec_PtrFree( vCone );
+ Vec_PtrFree( vSupp );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Dereferences the node's MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_NodeDeref_rec( Aig_Node_t * pNode )
+{
+ Aig_Node_t * pNode0, * pNode1;
+ int Counter = 1;
+ if ( Aig_NodeIsPi(pNode) )
+ return 0;
+ pNode0 = Aig_NodeFanin0(pNode);
+ pNode1 = Aig_NodeFanin1(pNode);
+ assert( pNode0->nRefs > 0 );
+ assert( pNode1->nRefs > 0 );
+ if ( --pNode0->nRefs == 0 )
+ Counter += Aig_NodeDeref_rec( pNode0 );
+ if ( --pNode1->nRefs == 0 )
+ Counter += Aig_NodeDeref_rec( pNode1 );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [References the node's MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_NodeRef_rec( Aig_Node_t * pNode )
+{
+ Aig_Node_t * pNode0, * pNode1;
+ int Counter = 1;
+ if ( Aig_NodeIsPi(pNode) )
+ return 0;
+ pNode0 = Aig_NodeFanin0(pNode);
+ pNode1 = Aig_NodeFanin1(pNode);
+ if ( pNode0->nRefs++ == 0 )
+ Counter += Aig_NodeRef_rec( pNode0 );
+ if ( pNode1->nRefs++ == 0 )
+ Counter += Aig_NodeRef_rec( pNode1 );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the internal and leaf nodes in the derefed MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_NodeMffsConeSupp_rec( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost )
+{
+ // skip visited nodes
+ if ( Aig_NodeIsTravIdCurrent(pNode) )
+ return;
+ Aig_NodeSetTravIdCurrent(pNode);
+ // add to the new support nodes
+ if ( !fTopmost && (Aig_NodeIsPi(pNode) || pNode->nRefs > 0) )
+ {
+ Vec_PtrPush( vSupp, pNode );
+ return;
+ }
+ // recur on the children
+ Aig_NodeMffsConeSupp_rec( Aig_NodeFanin0(pNode), vCone, vSupp, 0 );
+ Aig_NodeMffsConeSupp_rec( Aig_NodeFanin1(pNode), vCone, vSupp, 0 );
+ // collect the internal node
+ Vec_PtrPush( vCone, pNode );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the support of the derefed MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_NodeMffsConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp )
+{
+ assert( Aig_NodeIsAnd(pNode) );
+ assert( !Aig_IsComplement(pNode) );
+ Vec_PtrClear( vCone );
+ Vec_PtrClear( vSupp );
+ Aig_ManIncrementTravId( pNode->pMan );
+ Aig_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 );
+}
+
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Collects the internal and leaf nodes of the factor-cut of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_NodeFactorConeSupp_rec( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost )
+{
+ // skip visited nodes
+ if ( Aig_NodeIsTravIdCurrent(pNode) )
+ return;
+ Aig_NodeSetTravIdCurrent(pNode);
+ // add to the new support nodes
+ if ( !fTopmost && (Aig_NodeIsPi(pNode) || pNode->fMarkA) )
+ {
+ Vec_PtrPush( vSupp, pNode );
+ return;
+ }
+ // recur on the children
+ Aig_NodeFactorConeSupp_rec( Aig_NodeFanin0(pNode), vCone, vSupp, 0 );
+ Aig_NodeFactorConeSupp_rec( Aig_NodeFanin1(pNode), vCone, vSupp, 0 );
+ // collect the internal node
+ assert( fTopmost || !pNode->fMarkA );
+ Vec_PtrPush( vCone, pNode );
+
+ assert( pNode->fMarkC == 0 );
+ pNode->fMarkC = 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the support of the derefed MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_NodeFactorConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp )
+{
+ assert( Aig_NodeIsAnd(pNode) );
+ assert( !Aig_IsComplement(pNode) );
+ Vec_PtrClear( vCone );
+ Vec_PtrClear( vSupp );
+ Aig_ManIncrementTravId( pNode->pMan );
+ Aig_NodeFactorConeSupp_rec( pNode, vCone, vSupp, 1 );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/rwrTruth.c b/src/sat/aig/rwrTruth.c
index 2c402184..63a437ce 100644
--- a/src/sat/aig/rwrTruth.c
+++ b/src/sat/aig/rwrTruth.c
@@ -444,6 +444,8 @@ Aig_Node_t * Aig_TruthDecompose( Aig_Truth_t * p )
assert( 0 );
}
+
+ return NULL;
}
diff --git a/src/sat/aig/rwr_.c b/src/sat/aig/rwr_.c
new file mode 100644
index 00000000..45e76f75
--- /dev/null
+++ b/src/sat/aig/rwr_.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+ FileName [rwr_.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rwr_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 15:52:42 +0000