summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c13
-rw-r--r--src/base/abci/abcNewAig.c376
-rw-r--r--src/base/abci/abcSat.c6
-rw-r--r--src/bdd/dsd/dsdCheck.c2
-rw-r--r--src/misc/extra/extraBddSymm.c2
-rw-r--r--src/misc/extra/extraUtilMemory.c2
-rw-r--r--src/opt/dec/decAbc.c35
-rw-r--r--src/opt/fxu/fxu.c2
-rw-r--r--src/sat/aig/aig.h64
-rw-r--r--src/sat/aig/aigMan.c15
-rw-r--r--src/sat/aig/aigMem.c2
-rw-r--r--src/sat/aig/aigNode.c7
-rw-r--r--src/sat/aig/aigTable.c19
-rw-r--r--src/sat/aig/aigUtil.c130
-rw-r--r--src/sat/aig/fraigClass.c60
-rw-r--r--src/sat/aig/fraigCnf.c476
-rw-r--r--src/sat/aig/fraigCore.c86
-rw-r--r--src/sat/aig/fraigEngine.c131
-rw-r--r--src/sat/aig/fraigProve.c4
-rw-r--r--src/sat/aig/fraigSim.c184
-rw-r--r--src/sat/aig/fraigSolver.c47
-rw-r--r--src/sat/aig/fraigTrav.c47
-rw-r--r--src/sat/csat/csat_apis.c182
-rw-r--r--src/sat/csat/csat_apis.h106
-rw-r--r--src/sat/fraig/fraigMem.c2
-rw-r--r--src/sat/msat/msatMem.c2
26 files changed, 1757 insertions, 245 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 259187bf..5f5c4b49 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3782,8 +3782,9 @@ usage:
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk;//, * pNtkRes;
+ Abc_Ntk_t * pNtk, * pNtkRes;
int c;
+ extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -3807,19 +3808,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( !Abc_NtkIsStrash(pNtk) )
+ if ( Abc_NtkIsSeq(pNtk) )
{
- fprintf( pErr, "Only works for strashed networks.\n" );
+ fprintf( pErr, "Only works for non-sequential networks.\n" );
return 1;
}
// Abc_NtkTestEsop( pNtk );
// Abc_NtkTestSop( pNtk );
// printf( "This command is currently not used.\n" );
-
-/*
// run the command
- pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
+// pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
+ pNtkRes = Abc_NtkNewAig( pNtk );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -3827,7 +3827,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
return 0;
usage:
diff --git a/src/base/abci/abcNewAig.c b/src/base/abci/abcNewAig.c
new file mode 100644
index 00000000..33f58135
--- /dev/null
+++ b/src/base/abci/abcNewAig.c
@@ -0,0 +1,376 @@
+/**CFile****************************************************************
+
+ FileName [aigNewAig.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Strashing of the current network.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: aigNewAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "extra.h"
+#include "dec.h"
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan );
+static Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld );
+
+static void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Aig_Man_t * pMan );
+static Aig_Node_t * Abc_NodeStrashAig( Aig_Man_t * pMan, Abc_Obj_t * pNode );
+static Aig_Node_t * Abc_NodeStrashAigSopAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
+static Aig_Node_t * Abc_NodeStrashAigExorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
+static Aig_Node_t * Abc_NodeStrashAigFactorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
+extern char * Mio_GateReadSop( void * pGate );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk )
+{
+ Aig_Man_t * pMan;
+ Abc_Ntk_t * pNtkAig;
+ Aig_ProofType_t RetValue;
+ int fCleanup = 1;
+ int nNodes;
+
+ assert( !Abc_NtkIsNetlist(pNtk) );
+ assert( !Abc_NtkIsSeq(pNtk) );
+ if ( Abc_NtkIsBddLogic(pNtk) )
+ Abc_NtkBddToSop(pNtk);
+ // print warning about choice nodes
+ if ( Abc_NtkGetChoiceNum( pNtk ) )
+ printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
+
+ // convert to the AIG manager
+ pMan = Abc_NtkToAig( pNtk );
+ // execute a command in the AIG manager
+ RetValue = Aig_FraigProve( pMan );
+ if ( RetValue == AIG_PROOF_SAT )
+ printf( "Satisfiable.\n" );
+ else if ( RetValue == AIG_PROOF_UNSAT )
+ printf( "Unsatisfiable.\n" );
+ else if ( RetValue == AIG_PROOF_TIMEOUT )
+ printf( "Undecided.\n" );
+ else
+ assert( 0 );
+
+ // convert from the AIG manager
+ pNtkAig = Abc_NtkFromAig( pNtk, pMan );
+ Aig_ManStop( pMan );
+
+ // report the cleanup results
+ if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
+ printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
+ // duplicate EXDC
+ if ( pNtk->pExdc )
+ pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
+ // make sure everything is okay
+ if ( !Abc_NtkCheck( pNtkAig ) )
+ {
+ printf( "Abc_NtkStrash: The network check has failed.\n" );
+ Abc_NtkDelete( pNtkAig );
+ return NULL;
+ }
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts the network from the AIG manager into ABC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
+{
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
+ Aig_Node_t * pAnd;
+ int i;
+ // perform strashing
+ pNtk = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+ // transfer the pointers to the basic nodes
+ Aig_ManConst1(pMan)->Data = Abc_NtkConst1(pNtk)->Id;
+ Abc_NtkForEachCi( pNtkOld, pObj, i )
+ Aig_ManPi(pMan, i)->Data = pObj->pCopy->Id;
+ // rebuild the AIG
+ Aig_ManForEachAnd( pMan, pAnd, i )
+ {
+ // add the first fanins
+ pFaninNew0 = Abc_NtkObj( pNtk, Aig_NodeFanin0(pAnd)->Data );
+ pFaninNew0 = Abc_ObjNotCond( pFaninNew0, Aig_NodeFaninC0(pAnd) );
+ // add the first second
+ pFaninNew1 = Abc_NtkObj( pNtk, Aig_NodeFanin1(pAnd)->Data );
+ pFaninNew1 = Abc_ObjNotCond( pFaninNew1, Aig_NodeFaninC1(pAnd) );
+ // create the new node
+ pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
+ pAnd->Data = pObjNew->Id;
+ }
+ // connect the PO nodes
+ Abc_NtkForEachCo( pNtkOld, pObj, i )
+ {
+ pAnd = Aig_ManPo( pMan, i );
+ pFaninNew = Abc_NtkObj( pNtk, Aig_NodeFanin0(pAnd)->Data );
+ pFaninNew = Abc_ObjNotCond( pFaninNew, Aig_NodeFaninC0(pAnd) );
+ Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+ }
+ return pNtk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts the network from the AIG manager into ABC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld )
+{
+ Aig_Param_t Params;
+ Aig_Man_t * pMan;
+ Abc_Obj_t * pObj;
+ Aig_Node_t * pFanin;
+ int i;
+ // create the manager
+ Aig_ManSetDefaultParams( &Params );
+ pMan = Aig_ManStart( &Params );
+ // create the PIs
+ Abc_NtkConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
+ Abc_NtkForEachCi( pNtkOld, pObj, i )
+ pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePi(pMan);
+ // perform the conversion of the internal nodes
+ Abc_NtkStrashPerformAig( pNtkOld, pMan );
+ // create the POs
+ Abc_NtkForEachCo( pNtkOld, pObj, i )
+ {
+ pFanin = (Aig_Node_t *)Abc_ObjFanin0(pObj)->pCopy;
+ pFanin = Aig_NotCond( pFanin, Abc_ObjFaninC0(pObj) );
+ pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePo( pMan, pFanin );
+ }
+ return pMan;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the network for strashing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Aig_Man_t * pMan )
+{
+// ProgressBar * pProgress;
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pNode;
+ int i;
+ vNodes = Abc_NtkDfs( pNtk, 0 );
+// pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+// Extra_ProgressBarUpdate( pProgress, i, NULL );
+ pNode->pCopy = (Abc_Obj_t *)Abc_NodeStrashAig( pMan, pNode );
+ }
+// Extra_ProgressBarStop( pProgress );
+ Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Strashes one logic node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Node_t * Abc_NodeStrashAig( Aig_Man_t * pMan, Abc_Obj_t * pNode )
+{
+ int fUseFactor = 1;
+ char * pSop;
+ Aig_Node_t * pFanin0, * pFanin1;
+ extern int Abc_SopIsExorType( char * pSop );
+
+ assert( Abc_ObjIsNode(pNode) );
+
+ // consider the case when the graph is an AIG
+ if ( Abc_NtkIsStrash(pNode->pNtk) )
+ {
+ if ( Abc_NodeIsConst(pNode) )
+ return Aig_ManConst1(pMan);
+ pFanin0 = (Aig_Node_t *)Abc_ObjFanin0(pNode)->pCopy;
+ pFanin0 = Aig_NotCond( pFanin0, Abc_ObjFaninC0(pNode) );
+ pFanin1 = (Aig_Node_t *)Abc_ObjFanin1(pNode)->pCopy;
+ pFanin1 = Aig_NotCond( pFanin1, Abc_ObjFaninC1(pNode) );
+ return Aig_And( pMan, pFanin0, pFanin1 );
+ }
+
+ // get the SOP of the node
+ if ( Abc_NtkHasMapping(pNode->pNtk) )
+ pSop = Mio_GateReadSop(pNode->pData);
+ else
+ pSop = pNode->pData;
+
+ // consider the constant node
+ if ( Abc_NodeIsConst(pNode) )
+ return Aig_NotCond( Aig_ManConst1(pMan), Abc_SopIsConst0(pSop) );
+
+ // consider the special case of EXOR function
+ if ( Abc_SopIsExorType(pSop) )
+ return Abc_NodeStrashAigExorAig( pMan, pNode, pSop );
+
+ // decide when to use factoring
+ if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
+ return Abc_NodeStrashAigFactorAig( pMan, pNode, pSop );
+ return Abc_NodeStrashAigSopAig( pMan, pNode, pSop );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Strashes one logic node using its SOP.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Node_t * Abc_NodeStrashAigSopAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop )
+{
+ Abc_Obj_t * pFanin;
+ Aig_Node_t * pAnd, * pSum;
+ char * pCube;
+ int i, nFanins;
+
+ // get the number of node's fanins
+ nFanins = Abc_ObjFaninNum( pNode );
+ assert( nFanins == Abc_SopGetVarNum(pSop) );
+ // go through the cubes of the node's SOP
+ pSum = Aig_Not( Aig_ManConst1(pMan) );
+ Abc_SopForEachCube( pSop, nFanins, pCube )
+ {
+ // create the AND of literals
+ pAnd = Aig_ManConst1(pMan);
+ Abc_ObjForEachFanin( pNode, pFanin, i ) // pFanin can be a net
+ {
+ if ( pCube[i] == '1' )
+ pAnd = Aig_And( pMan, pAnd, (Aig_Node_t *)pFanin->pCopy );
+ else if ( pCube[i] == '0' )
+ pAnd = Aig_And( pMan, pAnd, Aig_Not((Aig_Node_t *)pFanin->pCopy) );
+ }
+ // add to the sum of cubes
+ pSum = Aig_Or( pMan, pSum, pAnd );
+ }
+ // decide whether to complement the result
+ if ( Abc_SopIsComplement(pSop) )
+ pSum = Aig_Not(pSum);
+ return pSum;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Strashed n-input XOR function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Node_t * Abc_NodeStrashAigExorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop )
+{
+ Abc_Obj_t * pFanin;
+ Aig_Node_t * pSum;
+ int i, nFanins;
+ // get the number of node's fanins
+ nFanins = Abc_ObjFaninNum( pNode );
+ assert( nFanins == Abc_SopGetVarNum(pSop) );
+ // go through the cubes of the node's SOP
+ pSum = Aig_Not( Aig_ManConst1(pMan) );
+ for ( i = 0; i < nFanins; i++ )
+ {
+ pFanin = Abc_ObjFanin( pNode, i );
+ pSum = Aig_Xor( pMan, pSum, (Aig_Node_t *)pFanin->pCopy );
+ }
+ if ( Abc_SopIsComplement(pSop) )
+ pSum = Aig_Not(pSum);
+ return pSum;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Strashes one logic node using its SOP.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Node_t * Abc_NodeStrashAigFactorAig( Aig_Man_t * pMan, Abc_Obj_t * pRoot, char * pSop )
+{
+ Dec_Graph_t * pFForm;
+ Dec_Node_t * pNode;
+ Aig_Node_t * pAnd;
+ int i;
+ extern Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph );
+
+ // perform factoring
+ pFForm = Dec_Factor( pSop );
+ // collect the fanins
+ Dec_GraphForEachLeaf( pFForm, pNode, i )
+ pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy;
+ // perform strashing
+ pAnd = Dec_GraphToNetworkAig( pMan, pFForm );
+ Dec_GraphFree( pFForm );
+ return pAnd;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 8c8636c5..f7b9892e 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -534,10 +534,10 @@ int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_
Vec_IntPush( vVars, toLitCond(VarF, 1) );
if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
-
+
if ( VarT == VarE )
{
- assert( fCompT == !fCompE );
+// assert( fCompT == !fCompE );
return 1;
}
@@ -774,7 +774,7 @@ solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk )
RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk );
Abc_NtkForEachObj( pNtk, pNode, i )
pNode->fMarkA = 0;
- Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
+// Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
if ( RetValue == 0 )
{
solver_delete(pSat);
diff --git a/src/bdd/dsd/dsdCheck.c b/src/bdd/dsd/dsdCheck.c
index 865cd830..58b824d2 100644
--- a/src/bdd/dsd/dsdCheck.c
+++ b/src/bdd/dsd/dsdCheck.c
@@ -82,7 +82,7 @@ void Dsd_CheckCacheAllocate( int nEntries )
/**Function********************************************************************
- Synopsis [Delocates the local cache.]
+ Synopsis [Deallocates the local cache.]
Description []
diff --git a/src/misc/extra/extraBddSymm.c b/src/misc/extra/extraBddSymm.c
index 474f663f..358402b0 100644
--- a/src/misc/extra/extraBddSymm.c
+++ b/src/misc/extra/extraBddSymm.c
@@ -223,7 +223,7 @@ Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars )
/**Function********************************************************************
- Synopsis [Delocates symmetry information structure.]
+ Synopsis [Deallocates symmetry information structure.]
Description []
diff --git a/src/misc/extra/extraUtilMemory.c b/src/misc/extra/extraUtilMemory.c
index af1128ac..c9137c56 100644
--- a/src/misc/extra/extraUtilMemory.c
+++ b/src/misc/extra/extraUtilMemory.c
@@ -257,7 +257,7 @@ void Extra_MmFixedRestart( Extra_MmFixed_t * p )
int i;
char * pTemp;
- // delocate all chunks except the first one
+ // deallocate all chunks except the first one
for ( i = 1; i < p->nChunks; i++ )
free( p->pChunks[i] );
p->nChunks = 1;
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index 1416cf0d..b24773be 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -18,6 +18,7 @@
#include "abc.h"
#include "dec.h"
+#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -201,6 +202,40 @@ void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpda
assert( nGain <= nNodesOld - nNodesNew );
}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the decomposition graph into the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
+{
+ Dec_Node_t * pNode;
+ Aig_Node_t * pAnd0, * pAnd1;
+ int i;
+ // check for constant function
+ if ( Dec_GraphIsConst(pGraph) )
+ return Aig_NotCond( Aig_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
+ // check for a literal
+ if ( Dec_GraphIsVar(pGraph) )
+ return Aig_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+ // build the AIG nodes corresponding to the AND gates of the graph
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ pAnd0 = Aig_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ pAnd1 = Aig_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+ pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 );
+ }
+ // complement the result if necessary
+ return Aig_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index 9da34fde..169fb218 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -159,7 +159,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
if ( pData->nNodesNew )
Fxu_CreateCovers( p, pData );
Fxu_MatrixDelete( p );
-// printf( "Memory usage after delocation: Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
+// printf( "Memory usage after deallocation: Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
if ( pData->nNodesNew == pData->nNodesExt )
printf( "Warning: The limit on the number of extracted divisors has been reached.\n" );
return pData->nNodesNew;
diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
index 009a17bb..55a75cf5 100644
--- a/src/sat/aig/aig.h
+++ b/src/sat/aig/aig.h
@@ -48,6 +48,7 @@
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
+#include "solver.h"
#include "vec.h"
////////////////////////////////////////////////////////////////////////
@@ -70,6 +71,7 @@ typedef struct Aig_Edge_t_ Aig_Edge_t;
typedef struct Aig_MemFixed_t_ Aig_MemFixed_t;
typedef struct Aig_SimInfo_t_ Aig_SimInfo_t;
typedef struct Aig_Table_t_ Aig_Table_t;
+typedef struct Aig_Pattern_t_ Aig_Pattern_t;
// network types
typedef enum {
@@ -79,12 +81,25 @@ typedef enum {
AIG_AND // 3: internal node
} Aig_NodeType_t;
+// proof outcomes
+typedef enum {
+ AIG_PROOF_NONE = 0, // 0: unknown
+ AIG_PROOF_SAT, // 1: primary input
+ AIG_PROOF_UNSAT, // 2: primary output
+ AIG_PROOF_TIMEOUT, // 3: primary output
+ AIG_PROOF_FAIL // 4: internal node
+} Aig_ProofType_t;
+
+
+
// the AIG parameters
struct Aig_Param_t_
{
int nPatsRand; // the number of random patterns
int nBTLimit; // backtrack limit at the intermediate nodes
int nSeconds; // the runtime limit at the final miter
+ int fVerbose; // verbosity
+ int fSatVerbose; // verbosity of SAT
};
// the AIG edge
@@ -127,6 +142,13 @@ struct Aig_Man_t_
Vec_Ptr_t * vPos; // all POs
Aig_Table_t * pTable; // structural hash table
int nLevelMax; // the maximum level
+ // SAT solver and related structures
+ solver * pSat;
+ Vec_Int_t * vVar2Sat; // mapping of nodes into their SAT var numbers (for each node num)
+ Vec_Int_t * vSat2Var; // mapping of the SAT var numbers into nodes (for each SAT var)
+ Vec_Int_t * vPiSatNums; // the SAT variable numbers (for each PI)
+ int * pModel; // the satisfying assignment (for each PI)
+ int nMuxes; // the number of MUXes
// fanout representation
Vec_Ptr_t * vFanPivots; // fanout pivots
Vec_Ptr_t * vFanFans0; // the next fanout of the first fanin
@@ -136,6 +158,7 @@ struct Aig_Man_t_
int nTravIds; // the traversal ID
// simulation info
Aig_SimInfo_t * pInfo; // random and systematic sim info for PIs
+ Aig_SimInfo_t * pInfoPi; // temporary sim info for the PI nodes
Aig_SimInfo_t * pInfoTemp; // temporary sim info for all nodes
// simulation patterns
int nPiWords; // the number of words in the PI info
@@ -148,6 +171,14 @@ struct Aig_Man_t_
Vec_Ptr_t * vToReplace; // the nodes to replace
};
+// the simulation patter
+struct Aig_Pattern_t_
+{
+ int nBits;
+ int nWords;
+ unsigned * pData;
+};
+
// the AIG simulation info
struct Aig_SimInfo_t_
{
@@ -166,9 +197,9 @@ struct Aig_SimInfo_t_
for ( i = 0; (i < Aig_ManPiNum(pMan)) && (((pNode) = Aig_ManPi(pMan, i)), 1); i++ )
#define Aig_ManForEachPo( pMan, pNode, i ) \
for ( i = 0; (i < Aig_ManPoNum(pMan)) && (((pNode) = Aig_ManPo(pMan, i)), 1); i++ )
-#define Aig_ManForEachAnd( pNtk, pNode, i ) \
+#define Aig_ManForEachAnd( pMan, pNode, i ) \
for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ ) \
- if ( Aig_NodeIsAnd(pNode) ) {} else
+ if ( !Aig_NodeIsAnd(pNode) ) {} else
// maximum/minimum operators
#define AIG_MIN(a,b) (((a) < (b))? (a) : (b))
@@ -178,8 +209,12 @@ struct Aig_SimInfo_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); }
+static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); }
+static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
+static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
+static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
+static inline Aig_Node_t * Aig_ManConst1( Aig_Man_t * pMan ) { return pMan->pConst1; }
static inline Aig_Node_t * Aig_ManNode( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vNodes, i); }
static inline Aig_Node_t * Aig_ManPi( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vPis, i); }
static inline Aig_Node_t * Aig_ManPo( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vPos, i); }
@@ -216,7 +251,8 @@ static inline Aig_Node_t * Aig_NodeChild0( Aig_Node_t * pNode ) { return Aig_N
static inline Aig_Node_t * Aig_NodeChild1( Aig_Node_t * pNode ) { return Aig_NotCond( Aig_NodeFanin1(pNode), Aig_NodeFaninC1(pNode) ); }
static inline Aig_Node_t * Aig_NodeNextH( Aig_Node_t * pNode ) { return pNode->NextH? Aig_ManNode(pNode->pMan, pNode->NextH) : NULL; }
static inline int Aig_NodeWhatFanin( Aig_Node_t * pNode, Aig_Node_t * pFanin ) { if ( Aig_NodeFaninId0(pNode) == pFanin->Id ) return 0; if ( Aig_NodeFaninId1(pNode) == pFanin->Id ) return 1; assert(0); return -1; }
-static inline int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); }
+static inline int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); }
+static inline int Aig_NodeRequiredLevel( Aig_Node_t * pNode ) { return pNode->pMan->nLevelMax + 1 - pNode->LevelR; }
static inline unsigned * Aig_SimInfoForNode( Aig_SimInfo_t * p, Aig_Node_t * pNode ) { assert( p->Type ); return p->pData + p->nWords * pNode->Id; }
static inline unsigned * Aig_SimInfoForPi( Aig_SimInfo_t * p, int Num ) { assert( !p->Type ); return p->pData + p->nWords * Num; }
@@ -268,6 +304,7 @@ extern void Aig_NodeDisconnectAnd( Aig_Node_t * pNode );
extern void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot );
extern void Aig_NodePrint( Aig_Node_t * pNode );
extern char * Aig_NodeName( Aig_Node_t * pNode );
+extern void Aig_PrintNode( Aig_Node_t * pNode );
/*=== aigOper.c ==========================================================*/
extern Aig_Node_t * Aig_And( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
extern Aig_Node_t * Aig_Or( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
@@ -287,18 +324,33 @@ extern void Aig_TableResize( Aig_Man_t * pMan );
extern void Aig_TableRehash( Aig_Man_t * pMan );
/*=== aigUtil.c ==========================================================*/
extern void Aig_ManIncrementTravId( Aig_Man_t * pMan );
-extern void Aig_PrintNode( Aig_Node_t * pNode );
+extern bool Aig_NodeIsMuxType( Aig_Node_t * pNode );
+extern Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t ** ppNodeT, Aig_Node_t ** ppNodeE );
+/*=== fraigCore.c ==========================================================*/
+extern Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan );
/*=== fraigClasses.c ==========================================================*/
extern Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfoAll );
+extern void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses );
+/*=== fraigCnf.c ==========================================================*/
+extern Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan );
+/*=== fraigEngine.c ==========================================================*/
+extern void Aig_EngineSimulateFirst( Aig_Man_t * p );
+extern int Aig_EngineSimulate( Aig_Man_t * p );
+extern void Aig_EngineSimulateRandomFirst( Aig_Man_t * p );
/*=== fraigSim.c ==========================================================*/
extern Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type );
extern void Aig_SimInfoClean( Aig_SimInfo_t * p );
extern void Aig_SimInfoRandom( Aig_SimInfo_t * p );
+extern void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat );
extern void Aig_SimInfoResize( Aig_SimInfo_t * p );
extern void Aig_SimInfoFree( Aig_SimInfo_t * p );
-extern Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi );
+extern void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll );
+extern Aig_Pattern_t * Aig_PatternAlloc( int nBits );
+extern void Aig_PatternClean( Aig_Pattern_t * pPat );
+extern void Aig_PatternRandom( Aig_Pattern_t * pPat );
+extern void Aig_PatternFree( Aig_Pattern_t * pPat );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/sat/aig/aigMan.c b/src/sat/aig/aigMan.c
index 2058f6b0..3807d28a 100644
--- a/src/sat/aig/aigMan.c
+++ b/src/sat/aig/aigMan.c
@@ -66,10 +66,11 @@ Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam )
// start the manager
p = ALLOC( Aig_Man_t, 1 );
memset( p, 0, sizeof(Aig_Man_t) );
- p->pParam = &p->Param;
- p->nTravIds = 1;
+ p->pParam = &p->Param;
+ p->nTravIds = 1;
+ p->nPatsMax = 20;
// set the defaults
- *p->pParam = *pParam;
+ *p->pParam = *pParam;
// start memory managers
p->mmNodes = Aig_MemFixedStart( sizeof(Aig_Node_t) );
// allocate node arrays
@@ -121,14 +122,22 @@ int Aig_ManCleanup( Aig_Man_t * pMan )
***********************************************************************/
void Aig_ManStop( Aig_Man_t * p )
{
+ // SAT solver
+ if ( p->pSat ) solver_delete( p->pSat );
+ if ( p->vVar2Sat ) Vec_IntFree( p->vVar2Sat );
+ if ( p->vSat2Var ) Vec_IntFree( p->vSat2Var );
+ if ( p->vPiSatNums ) Vec_IntFree( p->vPiSatNums );
+ // fanouts
if ( p->vFanPivots ) Vec_PtrFree( p->vFanPivots );
if ( p->vFanFans0 ) Vec_PtrFree( p->vFanFans0 );
if ( p->vFanFans1 ) Vec_PtrFree( p->vFanFans1 );
if ( p->vClasses ) Vec_VecFree( p->vClasses );
+ // nodes
Aig_MemFixedStop( p->mmNodes, 0 );
Vec_PtrFree( p->vNodes );
Vec_PtrFree( p->vPis );
Vec_PtrFree( p->vPos );
+ // temporary
Vec_PtrFree( p->vFanouts );
Vec_PtrFree( p->vToReplace );
Aig_TableFree( p->pTable );
diff --git a/src/sat/aig/aigMem.c b/src/sat/aig/aigMem.c
index 280cf98b..32709bf6 100644
--- a/src/sat/aig/aigMem.c
+++ b/src/sat/aig/aigMem.c
@@ -201,7 +201,7 @@ void Aig_MemFixedRestart( Aig_MemFixed_t * p )
int i;
char * pTemp;
- // delocate all chunks except the first one
+ // deallocate all chunks except the first one
for ( i = 1; i < p->nChunks; i++ )
free( p->pChunks[i] );
p->nChunks = 1;
diff --git a/src/sat/aig/aigNode.c b/src/sat/aig/aigNode.c
index afccd985..991cc7e5 100644
--- a/src/sat/aig/aigNode.c
+++ b/src/sat/aig/aigNode.c
@@ -46,6 +46,7 @@ static inline Aig_Node_t * Aig_NodeCreate( Aig_Man_t * p )
pNode = (Aig_Node_t *)Aig_MemFixedEntryFetch( p->mmNodes );
memset( pNode, 0, sizeof(Aig_Node_t) );
// assign the number and add to the array of nodes
+ pNode->pMan = p;
pNode->Id = p->vNodes->nSize;
Vec_PtrPush( p->vNodes, pNode );
return pNode;
@@ -66,6 +67,7 @@ Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p )
{
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
+ pNode->Type = AIG_NONE;
pNode->fPhase = 1; // sim value for 000... pattern
return pNode;
}
@@ -86,7 +88,8 @@ Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p )
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
Vec_PtrPush( p->vPis, pNode );
- pNode->fPhase = 0; // sim value for 000... pattern
+ pNode->Type = AIG_PI;
+ pNode->fPhase = 0; // sim value for 000... pattern
return pNode;
}
@@ -105,6 +108,7 @@ Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin )
{
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
+ pNode->Type = AIG_PO;
Vec_PtrPush( p->vPos, pNode );
// connect to the fanin
pNode->Fans[0].fComp = Aig_IsComplement(pFanin);
@@ -134,6 +138,7 @@ Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t
{
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
+ pNode->Type = AIG_AND;
Aig_NodeConnectAnd( pFanin0, pFanin1, pNode );
return pNode;
}
diff --git a/src/sat/aig/aigTable.c b/src/sat/aig/aigTable.c
index cfc94f6b..e6fe87d6 100644
--- a/src/sat/aig/aigTable.c
+++ b/src/sat/aig/aigTable.c
@@ -36,7 +36,7 @@ struct Aig_Table_t_
#define Aig_TableBinForEachEntry( pBin, pEnt ) \
for ( pEnt = pBin; \
pEnt; \
- pEnt = pEnt->NextH? Aig_ManNode(pEnt->pMan, pEnt->NextH) : NULL )
+ pEnt = Aig_NodeNextH(pEnt) )
#define Aig_TableBinForEachEntrySafe( pBin, pEnt, pEnt2 ) \
for ( pEnt = pBin, \
pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL; \
@@ -127,9 +127,8 @@ Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t
Aig_Node_t * pAnd;
unsigned Key;
assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id );
- assert( p0->pMan == p1->pMan );
// get the hash key for these two nodes
- Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
+ Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
// find the matching node in the table
Aig_TableBinForEachEntry( pMan->pTable->pBins[Key], pAnd )
if ( p0 == Aig_NodeChild0(pAnd) && p1 == Aig_NodeChild1(pAnd) )
@@ -157,8 +156,8 @@ Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t
Aig_TableResize( pMan );
// add the node to the corresponding linked list in the table
Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
- pAnd->NextH = pMan->pTable->pBins[Key]->Id;
- pMan->pTable->pBins[Key]->NextH = pAnd->Id;
+ pAnd->NextH = pMan->pTable->pBins[Key]? pMan->pTable->pBins[Key]->Id : 0;
+ pMan->pTable->pBins[Key] = pAnd;
pMan->pTable->nEntries++;
return pAnd;
}
@@ -195,7 +194,7 @@ void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis )
if ( pPlace == NULL )
pMan->pTable->pBins[Key] = Aig_NodeNextH(pThis);
else
- pPlace->NextH = pThis->Id;
+ pPlace->NextH = pThis->NextH;
break;
}
assert( pThis == pAnd );
@@ -232,8 +231,8 @@ clk = clock();
Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 )
{
Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), nBinsNew );
- pEnt->NextH = pBinsNew[Key]->Id;
- pBinsNew[Key]->NextH = pEnt->Id;
+ pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0;
+ pBinsNew[Key] = pEnt;
Counter++;
}
assert( Counter == pMan->pTable->nEntries );
@@ -282,8 +281,8 @@ void Aig_TableRehash( Aig_Man_t * pMan )
}
// rehash the node
Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), pMan->pTable->nBins );
- pEnt->NextH = pBinsNew[Key]->Id;
- pBinsNew[Key]->NextH = pEnt->Id;
+ pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0;
+ pBinsNew[Key] = pEnt;
Counter++;
}
assert( Counter == pMan->pTable->nEntries );
diff --git a/src/sat/aig/aigUtil.c b/src/sat/aig/aigUtil.c
index a1c9ca44..40f7aba1 100644
--- a/src/sat/aig/aigUtil.c
+++ b/src/sat/aig/aigUtil.c
@@ -53,6 +53,136 @@ void Aig_ManIncrementTravId( Aig_Man_t * pMan )
}
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+bool Aig_NodeIsMuxType( Aig_Node_t * pNode )
+{
+ Aig_Node_t * pNode0, * pNode1;
+ // check that the node is regular
+ assert( !Aig_IsComplement(pNode) );
+ // if the node is not AND, this is not MUX
+ if ( !Aig_NodeIsAnd(pNode) )
+ return 0;
+ // if the children are not complemented, this is not MUX
+ if ( !Aig_NodeFaninC0(pNode) || !Aig_NodeFaninC1(pNode) )
+ return 0;
+ // get children
+ pNode0 = Aig_NodeFanin0(pNode);
+ pNode1 = Aig_NodeFanin1(pNode);
+ // if the children are not ANDs, this is not MUX
+ if ( !Aig_NodeIsAnd(pNode0) || !Aig_NodeIsAnd(pNode1) )
+ return 0;
+ // otherwise the node is MUX iff it has a pair of equal grandchildren
+ return (Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC0(pNode1))) ||
+ (Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC1(pNode1))) ||
+ (Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC0(pNode1))) ||
+ (Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC1(pNode1)));
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recognizes what nodes are control and data inputs of a MUX.]
+
+ Description [If the node is a MUX, returns the control variable C.
+ Assigns nodes T and E to be the then and else variables of the MUX.
+ Node C is never complemented. Nodes T and E can be complemented.
+ This function also recognizes EXOR/NEXOR gates as MUXes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t ** ppNodeT, Aig_Node_t ** ppNodeE )
+{
+ Aig_Node_t * pNode0, * pNode1;
+ assert( !Aig_IsComplement(pNode) );
+ assert( Aig_NodeIsMuxType(pNode) );
+ // get children
+ pNode0 = Aig_NodeFanin0(pNode);
+ pNode1 = Aig_NodeFanin1(pNode);
+ // find the control variable
+// if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
+ if ( Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC0(pNode1)) )
+ {
+// if ( Fraig_IsComplement(pNode1->p1) )
+ if ( Aig_NodeFaninC0(pNode0) )
+ { // pNode2->p1 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
+ *ppNodeE = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
+ return Aig_NodeChild0(pNode1);//pNode2->p1;
+ }
+ else
+ { // pNode1->p1 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
+ *ppNodeE = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
+ return Aig_NodeChild0(pNode0);//pNode1->p1;
+ }
+ }
+// else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
+ else if ( Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC1(pNode1)) )
+ {
+// if ( Fraig_IsComplement(pNode1->p1) )
+ if ( Aig_NodeFaninC0(pNode0) )
+ { // pNode2->p2 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
+ *ppNodeE = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
+ return Aig_NodeChild1(pNode1);//pNode2->p2;
+ }
+ else
+ { // pNode1->p1 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
+ *ppNodeE = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
+ return Aig_NodeChild0(pNode0);//pNode1->p1;
+ }
+ }
+// else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
+ else if ( Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC0(pNode1)) )
+ {
+// if ( Fraig_IsComplement(pNode1->p2) )
+ if ( Aig_NodeFaninC1(pNode0) )
+ { // pNode2->p1 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
+ *ppNodeE = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
+ return Aig_NodeChild0(pNode1);//pNode2->p1;
+ }
+ else
+ { // pNode1->p2 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
+ *ppNodeE = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
+ return Aig_NodeChild1(pNode0);//pNode1->p2;
+ }
+ }
+// else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
+ else if ( Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC1(pNode1)) )
+ {
+// if ( Fraig_IsComplement(pNode1->p2) )
+ if ( Aig_NodeFaninC1(pNode0) )
+ { // pNode2->p2 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
+ *ppNodeE = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
+ return Aig_NodeChild1(pNode1);//pNode2->p2;
+ }
+ else
+ { // pNode1->p2 is positive phase of C
+ *ppNodeT = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
+ *ppNodeE = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
+ return Aig_NodeChild1(pNode0);//pNode1->p2;
+ }
+ }
+ assert( 0 ); // this is not MUX
+ return NULL;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/aig/fraigClass.c b/src/sat/aig/fraigClass.c
index b3040e2a..2f2d3e0c 100644
--- a/src/sat/aig/fraigClass.c
+++ b/src/sat/aig/fraigClass.c
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [aigFraig.c]
+ FileName [fraigClass.c]
SystemName [ABC: Logic synthesis and verification system.]
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: fraigClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@@ -25,7 +25,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static unsigned Aig_ManHashKey( unsigned * pData, int nWords );
+static unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -44,20 +44,24 @@ static unsigned Aig_ManHashKey( unsigned * pData, int nWords );
***********************************************************************/
Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
{
- Vec_Vec_t * vClasses; // equivalence classes
+ Vec_Vec_t * vClasses; // equivalence classes
stmm_table * tSim2Node; // temporary hash table hashing key into the class number
Aig_Node_t * pNode;
unsigned uKey;
- int i, * pSpot, ClassNum;
+ int i, * pSpot, Entry, ClassNum;
assert( pInfo->Type == 1 );
// fill in the hash table
tSim2Node = stmm_init_table( stmm_numcmp, stmm_numhash );
vClasses = Vec_VecAlloc( 100 );
- Aig_ManForEachNode( p, pNode, i )
+ // enumerate the nodes considered in the equivalence classes
+// Aig_ManForEachNode( p, pNode, i )
+ Vec_IntForEachEntry( p->vSat2Var, Entry, i )
{
+ pNode = Aig_ManNode( p, Entry );
+
if ( Aig_NodeIsPo(pNode) )
continue;
- uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords );
+ uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords, pNode->fPhase );
if ( !stmm_find_or_add( tSim2Node, (char *)uKey, (char ***)&pSpot ) ) // does not exist
*pSpot = (pNode->Id << 1) | 1; // save the node, and do nothing
else if ( (*pSpot) & 1 ) // this is a node
@@ -71,11 +75,24 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
}
else // this is a class
{
- ClassNum = (*pSpot) >> 1;
+ ClassNum = ((*pSpot) >> 1);
Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id );
}
}
stmm_free_table( tSim2Node );
+
+ // print the classes
+ {
+ Vec_Ptr_t * vVec;
+ printf( "PI/PO = %4d/%4d. Nodes = %7d. SatVars = %7d. Non-trivial classes = %5d: \n",
+ Aig_ManPiNum(p), Aig_ManPoNum(p),
+ Aig_ManNodeNum(p) - Aig_ManPoNum(p),
+ Vec_IntSize(p->vSat2Var), Vec_VecSize(vClasses) );
+
+ Vec_VecForEachLevel( vClasses, vVec, i )
+ printf( "%d ", Vec_PtrSize(vVec) );
+ printf( "\n" );
+ }
return vClasses;
}
@@ -90,17 +107,38 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
SeeAlso []
***********************************************************************/
-unsigned Aig_ManHashKey( unsigned * pData, int nWords )
+unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase )
{
static int Primes[10] = { 1009, 2207, 3779, 4001, 4877, 5381, 6427, 6829, 7213, 7919 };
unsigned uKey;
int i;
uKey = 0;
- for ( i = 0; i < nWords; i++ )
- uKey ^= pData[i] * Primes[i%10];
+ if ( fPhase )
+ for ( i = 0; i < nWords; i++ )
+ uKey ^= Primes[i%10] * pData[i];
+ else
+ for ( i = 0; i < nWords; i++ )
+ uKey ^= Primes[i%10] * ~pData[i];
return uKey;
}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the equivalence classes using the simulation info.]
+
+ Description [Records successful simulation patterns into the pattern
+ storage.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses )
+{
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/aig/fraigCnf.c b/src/sat/aig/fraigCnf.c
new file mode 100644
index 00000000..913165b2
--- /dev/null
+++ b/src/sat/aig/fraigCnf.c
@@ -0,0 +1,476 @@
+/**CFile****************************************************************
+
+ FileName [fraigCnf.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: fraigCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Adds trivial clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ClauseTriv( solver * pSat, Aig_Node_t * pNode, Vec_Int_t * vVars )
+{
+//printf( "Adding triv %d. %d\n", Aig_Regular(pNode)->Id, (int)pSat->solver_stats.clauses );
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond( Aig_Regular(pNode)->Data, Aig_IsComplement(pNode) ) );
+// Vec_IntPush( vVars, toLitCond( (int)Aig_Regular(pNode)->Id, Aig_IsComplement(pNode) ) );
+ return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds trivial clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ClauseAnd( solver * pSat, Aig_Node_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars )
+{
+ int fComp1, Var, Var1, i;
+//printf( "Adding AND %d. (%d) %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->solver_stats.clauses );
+
+ assert( !Aig_IsComplement( pNode ) );
+ assert( Aig_NodeIsAnd( pNode ) );
+
+// nVars = solver_nvars(pSat);
+ Var = pNode->Data;
+// Var = pNode->Id;
+
+// assert( Var < nVars );
+ for ( i = 0; i < vSuper->nSize; i++ )
+ {
+ // get the predecessor nodes
+ // get the complemented attributes of the nodes
+ fComp1 = Aig_IsComplement(vSuper->pArray[i]);
+ // determine the variable numbers
+ Var1 = Aig_Regular(vSuper->pArray[i])->Data;
+// Var1 = (int)Aig_Regular(vSuper->pArray[i])->Id;
+
+ // check that the variables are in the SAT manager
+// assert( Var1 < nVars );
+
+ // suppose the AND-gate is A * B = C
+ // add !A => !C or A + !C
+ // fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 );
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(Var1, fComp1) );
+ Vec_IntPush( vVars, toLitCond(Var, 1 ) );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
+ }
+
+ // add A & B => C or !A + !B + C
+// fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 );
+ vVars->nSize = 0;
+ for ( i = 0; i < vSuper->nSize; i++ )
+ {
+ // get the predecessor nodes
+ // get the complemented attributes of the nodes
+ fComp1 = Aig_IsComplement(vSuper->pArray[i]);
+ // determine the variable numbers
+ Var1 = Aig_Regular(vSuper->pArray[i])->Data;
+// Var1 = (int)Aig_Regular(vSuper->pArray[i])->Id;
+ // add this variable to the array
+ Vec_IntPush( vVars, toLitCond(Var1, !fComp1) );
+ }
+ Vec_IntPush( vVars, toLitCond(Var, 0) );
+ return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds trivial clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ClauseMux( solver * pSat, Aig_Node_t * pNode, Aig_Node_t * pNodeC, Aig_Node_t * pNodeT, Aig_Node_t * pNodeE, Vec_Int_t * vVars )
+{
+ int VarF, VarI, VarT, VarE, fCompT, fCompE;
+//printf( "Adding mux %d. %d\n", pNode->Id, (int)pSat->solver_stats.clauses );
+
+ assert( !Aig_IsComplement( pNode ) );
+ assert( Aig_NodeIsMuxType( pNode ) );
+ // get the variable numbers
+ VarF = pNode->Data;
+ VarI = pNodeC->Data;
+ VarT = Aig_Regular(pNodeT)->Data;
+ VarE = Aig_Regular(pNodeE)->Data;
+// VarF = (int)pNode->Id;
+// VarI = (int)pNodeC->Id;
+// VarT = (int)Aig_Regular(pNodeT)->Id;
+// VarE = (int)Aig_Regular(pNodeE)->Id;
+
+ // get the complementation flags
+ fCompT = Aig_IsComplement(pNodeT);
+ fCompE = Aig_IsComplement(pNodeE);
+
+ // f = ITE(i, t, e)
+ // i' + t' + f
+ // i' + t + f'
+ // i + e' + f
+ // i + e + f'
+ // create four clauses
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(VarI, 1) );
+ Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) );
+ Vec_IntPush( vVars, toLitCond(VarF, 0) );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(VarI, 1) );
+ Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) );
+ Vec_IntPush( vVars, toLitCond(VarF, 1) );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(VarI, 0) );
+ Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) );
+ Vec_IntPush( vVars, toLitCond(VarF, 0) );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(VarI, 0) );
+ Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) );
+ Vec_IntPush( vVars, toLitCond(VarF, 1) );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
+
+ if ( VarT == VarE )
+ {
+// assert( fCompT == !fCompE );
+ return 1;
+ }
+
+ // two additional clauses
+ // t' & e' -> f' t + e + f'
+ // t & e -> f t' + e' + f
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) );
+ Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) );
+ Vec_IntPush( vVars, toLitCond(VarF, 1) );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) );
+ Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) );
+ Vec_IntPush( vVars, toLitCond(VarF, 0) );
+ return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ClauseCollectSupergate_rec( Aig_Node_t * pNode, Vec_Ptr_t * vSuper, int fFirst, int fStopAtMux )
+{
+ int RetValue1, RetValue2, i;
+ // check if the node is visited
+ if ( Aig_Regular(pNode)->fMarkB )
+ {
+ // check if the node occurs in the same polarity
+ for ( i = 0; i < vSuper->nSize; i++ )
+ if ( vSuper->pArray[i] == pNode )
+ return 1;
+ // check if the node is present in the opposite polarity
+ for ( i = 0; i < vSuper->nSize; i++ )
+ if ( vSuper->pArray[i] == Aig_Not(pNode) )
+ return -1;
+ assert( 0 );
+ return 0;
+ }
+ // if the new node is complemented or a PI, another gate begins
+ if ( !fFirst )
+ if ( Aig_IsComplement(pNode) || !Aig_NodeIsAnd(pNode) || Aig_NodeRefs(pNode) > 1 || fStopAtMux && Aig_NodeIsMuxType(pNode) )
+ {
+ Vec_PtrPush( vSuper, pNode );
+ Aig_Regular(pNode)->fMarkB = 1;
+ return 0;
+ }
+ assert( !Aig_IsComplement(pNode) );
+ assert( Aig_NodeIsAnd(pNode) );
+ // go through the branches
+ RetValue1 = Aig_ClauseCollectSupergate_rec( Aig_NodeChild0(pNode), vSuper, 0, fStopAtMux );
+ RetValue2 = Aig_ClauseCollectSupergate_rec( Aig_NodeChild1(pNode), vSuper, 0, fStopAtMux );
+ if ( RetValue1 == -1 || RetValue2 == -1 )
+ return -1;
+ // return 1 if at least one branch has a duplicate
+ return RetValue1 || RetValue2;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ClauseCollectSupergate( Aig_Node_t * pNode, int fStopAtMux, Vec_Ptr_t * vNodes )
+{
+ int RetValue, i;
+ assert( !Aig_IsComplement(pNode) );
+ // collect the nodes in the implication supergate
+ Vec_PtrClear( vNodes );
+ RetValue = Aig_ClauseCollectSupergate_rec( pNode, vNodes, 1, fStopAtMux );
+ assert( vNodes->nSize > 1 );
+ // unmark the visited nodes
+ for ( i = 0; i < vNodes->nSize; i++ )
+ Aig_Regular((Aig_Node_t *)vNodes->pArray[i])->fMarkB = 0;
+ // if we found the node and its complement in the same implication supergate,
+ // return empty set of nodes (meaning that we should use constant-0 node)
+ if ( RetValue == -1 )
+ vNodes->nSize = 0;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Sets up the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ClauseCreateCnfInt( solver * pSat, Aig_Man_t * pNtk )
+{
+ Aig_Node_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
+ Vec_Ptr_t * vNodes, * vSuper;
+ Vec_Int_t * vVars;
+ int i, k, fUseMuxes = 1;
+
+ // start the data structures
+ vNodes = Vec_PtrAlloc( 1000 ); // the nodes corresponding to vars in the solver
+ vSuper = Vec_PtrAlloc( 100 ); // the nodes belonging to the given implication supergate
+ vVars = Vec_IntAlloc( 100 ); // the temporary array for variables in the clause
+
+ // add the clause for the constant node
+ pNode = Aig_ManConst1(pNtk);
+ pNode->fMarkA = 1;
+ pNode->Data = vNodes->nSize;
+ Vec_PtrPush( vNodes, pNode );
+ Aig_ClauseTriv( pSat, pNode, vVars );
+
+ // collect the nodes that need clauses and top-level assignments
+ Aig_ManForEachPo( pNtk, pNode, i )
+ {
+ // get the fanin
+ pFanin = Aig_NodeFanin0(pNode);
+ // create the node's variable
+ if ( pFanin->fMarkA == 0 )
+ {
+ pFanin->fMarkA = 1;
+ pFanin->Data = vNodes->nSize;
+ Vec_PtrPush( vNodes, pFanin );
+ }
+ // add the trivial clause
+ if ( !Aig_ClauseTriv( pSat, Aig_NodeChild0(pNode), vVars ) )
+ return 0;
+ }
+
+ // add the clauses
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ assert( !Aig_IsComplement(pNode) );
+ if ( !Aig_NodeIsAnd(pNode) )
+ continue;
+//printf( "%d ", pNode->Id );
+
+ // add the clauses
+ if ( fUseMuxes && Aig_NodeIsMuxType(pNode) )
+ {
+ pNode->pMan->nMuxes++;
+ pNodeC = Aig_NodeRecognizeMux( pNode, &pNodeT, &pNodeE );
+ Vec_PtrClear( vSuper );
+ Vec_PtrPush( vSuper, pNodeC );
+ Vec_PtrPush( vSuper, pNodeT );
+ Vec_PtrPush( vSuper, pNodeE );
+ // add the fanin nodes to explore
+ Vec_PtrForEachEntry( vSuper, pFanin, k )
+ {
+ pFanin = Aig_Regular(pFanin);
+ if ( pFanin->fMarkA == 0 )
+ {
+ pFanin->fMarkA = 1;
+ pFanin->Data = vNodes->nSize;
+ Vec_PtrPush( vNodes, pFanin );
+ }
+ }
+ // add the clauses
+ if ( !Aig_ClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) )
+ return 0;
+ }
+ else
+ {
+ // get the supergate
+ Aig_ClauseCollectSupergate( pNode, fUseMuxes, vSuper );
+ // add the fanin nodes to explore
+ Vec_PtrForEachEntry( vSuper, pFanin, k )
+ {
+ pFanin = Aig_Regular(pFanin);
+ if ( pFanin->fMarkA == 0 )
+ {
+ pFanin->fMarkA = 1;
+ pFanin->Data = vNodes->nSize;
+ Vec_PtrPush( vNodes, pFanin );
+ }
+ }
+ // add the clauses
+ if ( vSuper->nSize == 0 )
+ {
+ if ( !Aig_ClauseTriv( pSat, Aig_Not(pNode), vVars ) )
+ return 0;
+ }
+ else
+ {
+ if ( !Aig_ClauseAnd( pSat, pNode, vSuper, vVars ) )
+ return 0;
+ }
+ }
+ }
+
+ // delete
+ Vec_IntFree( vVars );
+ Vec_PtrFree( vNodes );
+ Vec_PtrFree( vSuper );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets up the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+solver * Aig_ClauseCreateCnf( Aig_Man_t * pMan )
+{
+ solver * pSat;
+ Aig_Node_t * pNode;
+ int RetValue, i, clk = clock();
+ // clean the marks
+ Aig_ManForEachNode( pMan, pNode, i )
+ pNode->fMarkA = 0, pNode->Data = -1;
+ // create the solver
+ pMan->nMuxes = 0;
+ pSat = solver_new();
+ RetValue = Aig_ClauseCreateCnfInt( pSat, pMan );
+// Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
+ if ( RetValue == 0 )
+ {
+ solver_delete(pSat);
+ Aig_ManForEachNode( pMan, pNode, i )
+ pNode->fMarkA = 0;
+ return NULL;
+ }
+ printf( "The number of MUXes detected = %d (%5.2f %% of logic). ",
+ pNode->pMan->nMuxes, 300.0*pNode->pMan->nMuxes/Aig_ManNodeNum(pMan) );
+ PRT( "Creating solver", clock() - clk );
+ return pSat;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan )
+{
+ Aig_Node_t * pNode;
+ int i;
+
+ // make sure it has one PO
+ if ( Aig_ManPoNum(pMan) != 1 )
+ {
+ printf( "The miter has other than 1 output.\n" );
+ return AIG_PROOF_FAIL;
+ }
+
+ // get the solver
+ assert( pMan->pSat == NULL );
+ pMan->pSat = Aig_ClauseCreateCnf( pMan );
+ if ( pMan->pSat == NULL )
+ return AIG_PROOF_UNSAT;
+
+ // get the variable mappings
+ pMan->vVar2Sat = Vec_IntStart( Aig_ManNodeNum(pMan) );
+ pMan->vSat2Var = Vec_IntStart( solver_nvars(pMan->pSat) );
+ Aig_ManForEachNode( pMan, pNode, i )
+ {
+ Vec_IntWriteEntry( pMan->vVar2Sat, i, pNode->Data );
+ if ( pNode->Data >= 0 ) Vec_IntWriteEntry( pMan->vSat2Var, pNode->Data, i );
+ }
+ // get the SAT var numbers of the primary inputs
+ pMan->vPiSatNums = Vec_IntAlloc( Aig_ManPiNum(pMan) );
+ Aig_ManForEachPi( pMan, pNode, i )
+ Vec_IntPush( pMan->vPiSatNums, (pNode->Data >= 0)? pNode->Data : 0 );
+ return AIG_PROOF_NONE;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c
index 6187538b..e7df1335 100644
--- a/src/sat/aig/fraigCore.c
+++ b/src/sat/aig/fraigCore.c
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [aigFraig.c]
+ FileName [fraigCore.c]
SystemName [ABC: Logic synthesis and verification system.]
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: fraigCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@@ -24,13 +24,56 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+static Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis []
+ Synopsis [Top-level equivalence checking procedure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan )
+{
+ Aig_ProofType_t RetValue;
+ int clk, status;
+
+ // create the solver
+ RetValue = Aig_ClauseSolverStart( pMan );
+ if ( RetValue != AIG_PROOF_NONE )
+ return RetValue;
+ // perform solving
+
+ // simplify the problem
+ clk = clock();
+ status = solver_simplify(pMan->pSat);
+ if ( status == 0 )
+ {
+// printf( "The problem is UNSATISFIABLE after simplification.\n" );
+ return AIG_PROOF_UNSAT;
+ }
+
+ // try to prove the output
+ RetValue = Aig_FraigProveOutput( pMan );
+ if ( RetValue != AIG_PROOF_TIMEOUT )
+ return RetValue;
+
+ // create equivalence classes
+ Aig_EngineSimulateRandomFirst( pMan );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Top-level equivalence checking procedure.]
Description []
@@ -39,6 +82,43 @@
SeeAlso []
***********************************************************************/
+Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan )
+{
+ Aig_ProofType_t RetValue;
+ int clk, status;
+
+ // solve the miter
+ clk = clock();
+ pMan->pSat->verbosity = pMan->pParam->fSatVerbose;
+ status = solver_solve( pMan->pSat, NULL, NULL, pMan->pParam->nSeconds );
+ if ( status == l_Undef )
+ {
+// printf( "The problem timed out.\n" );
+ RetValue = AIG_PROOF_TIMEOUT;
+ }
+ else if ( status == l_True )
+ {
+// printf( "The problem is SATISFIABLE.\n" );
+ RetValue = AIG_PROOF_SAT;
+ }
+ else if ( status == l_False )
+ {
+// printf( "The problem is UNSATISFIABLE.\n" );
+ RetValue = AIG_PROOF_UNSAT;
+ }
+ else
+ assert( 0 );
+// PRT( "SAT solver time", clock() - clk );
+
+ // if the problem is SAT, get the counterexample
+ if ( status == l_True )
+ {
+ if ( pMan->pModel ) free( pMan->pModel );
+ pMan->pModel = solver_get_model( pMan->pSat, pMan->vPiSatNums->pArray, pMan->vPiSatNums->nSize );
+ printf( "%d %d %d %d\n", pMan->pModel[0], pMan->pModel[1], pMan->pModel[2], pMan->pModel[3] );
+ }
+ return RetValue;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/sat/aig/fraigEngine.c b/src/sat/aig/fraigEngine.c
new file mode 100644
index 00000000..6214bf3b
--- /dev/null
+++ b/src/sat/aig/fraigEngine.c
@@ -0,0 +1,131 @@
+/**CFile****************************************************************
+
+ FileName [fraigEngine.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: fraigEngine.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Starts the simulation engine for the first time.]
+
+ Description [Tries several random patterns and their distance-1
+ minterms hoping to get simulation started.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_EngineSimulateFirst( Aig_Man_t * p )
+{
+ Aig_Pattern_t * pPat;
+ int i;
+ assert( Vec_PtrSize(p->vPats) == 0 );
+ for ( i = 0; i < p->nPatsMax; i++ )
+ {
+ pPat = Aig_PatternAlloc( Aig_ManPiNum(p) );
+ Aig_PatternRandom( pPat );
+ Vec_PtrPush( p->vPats, pPat );
+ if ( !Aig_EngineSimulate( p ) )
+ return;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Implements intelligent simulation engine.]
+
+ Description [Assumes that the good simulation patterns have been
+ assigned (p->vPats). Simulates until all of them are gone. Returns 1
+ if some classes are left. Returns 0 if there is no more classes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_EngineSimulate( Aig_Man_t * p )
+{
+ Aig_Pattern_t * pPat;
+ if ( Vec_VecSize(p->vClasses) == 0 )
+ return 0;
+ assert( Vec_PtrSize(p->vPats) > 0 );
+ // process patterns
+ while ( Vec_PtrSize(p->vPats) > 0 && Vec_VecSize(p->vClasses) > 0 )
+ {
+ // get the pattern and create new siminfo
+ pPat = Vec_PtrPop(p->vPats);
+ // create the new siminfo
+ Aig_SimInfoFromPattern( p->pInfoPi, pPat );
+ // free the patter
+ Aig_PatternFree( pPat );
+
+ // simulate this info
+ Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
+ // split the classes and collect the new patterns
+ Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses );
+ }
+ return Vec_VecSize(p->vClasses) > 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates all nodes using random simulation for the first time.]
+
+ Description [Assigns the original simulation info and the storage for the
+ future simulation info.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_EngineSimulateRandomFirst( Aig_Man_t * p )
+{
+ Aig_SimInfo_t * pInfoPi, * pInfoAll;
+ assert( !p->pInfo && !p->pInfoTemp );
+ // create random PI info
+ pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 );
+ Aig_SimInfoRandom( pInfoPi );
+ // allocate sim info for all nodes
+ pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 );
+ // simulate though the circuit
+ Aig_ManSimulateInfo( p, pInfoPi, pInfoAll );
+ // detect classes
+ p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
+ Aig_SimInfoFree( pInfoAll );
+ // save simulation info
+ p->pInfo = pInfoPi;
+ p->pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->vPis->nSize), 0 );
+ p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigProve.c b/src/sat/aig/fraigProve.c
index b5cce582..901f2fe2 100644
--- a/src/sat/aig/fraigProve.c
+++ b/src/sat/aig/fraigProve.c
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [aigProve.c]
+ FileName [fraigProve.c]
SystemName [ABC: Logic synthesis and verification system.]
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: aigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: fraigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
diff --git a/src/sat/aig/fraigSim.c b/src/sat/aig/fraigSim.c
index 1d547621..415b6918 100644
--- a/src/sat/aig/fraigSim.c
+++ b/src/sat/aig/fraigSim.c
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [aigSim.c]
+ FileName [fraigSim.c]
SystemName [ABC: Logic synthesis and verification system.]
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: aigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: fraigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@@ -30,59 +30,28 @@
/**Function*************************************************************
- Synopsis [Simulates all nodes using random simulation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManSimulateRandomFirst( Aig_Man_t * p )
-{
- Aig_SimInfo_t * pInfoPi, * pInfoAll;
- assert( p->pInfo && p->pInfoTemp );
- // create random PI info
- pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 );
- Aig_SimInfoRandom( pInfoPi );
- // simulate it though the circuit
- pInfoAll = Aig_ManSimulateInfo( p, pInfoPi );
- // detect classes
- p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
- Aig_SimInfoFree( pInfoAll );
- // save simulation info
- p->pInfo = pInfoPi;
- p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 );
-}
-
-/**Function*************************************************************
-
Synopsis [Simulates all nodes using the given simulation info.]
- Description []
+ Description [Returns the simulation info for all nodes.]
SideEffects []
SeeAlso []
***********************************************************************/
-Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
+void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll )
{
- Aig_SimInfo_t * pInfoAll;
Aig_Node_t * pNode;
- unsigned * pDataPi, * pData0, * pData1, * pDataAnd;
+ unsigned * pDataPi, * pDataPo, * pData0, * pData1, * pDataAnd;
int i, k, fComp0, fComp1;
assert( !pInfoPi->Type ); // PI siminfo
- // allocate sim info for all nodes
- pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 );
// set the constant sim info
pData1 = Aig_SimInfoForNode( pInfoAll, p->pConst1 );
for ( k = 0; k < pInfoPi->nWords; k++ )
pData1[k] = ~((unsigned)0);
- // copy the PI siminfo
- Vec_PtrForEachEntry( p->vPis, pNode, i )
+ // set the PI siminfo
+ Aig_ManForEachPi( p, pNode, i )
{
pDataPi = Aig_SimInfoForPi( pInfoPi, i );
pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode );
@@ -90,10 +59,8 @@ Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
pDataAnd[k] = pDataPi[k];
}
// simulate the nodes
- Vec_PtrForEachEntry( p->vNodes, pNode, i )
+ Aig_ManForEachAnd( p, pNode, i )
{
- if ( !Aig_NodeIsAnd(pNode) )
- continue;
pData0 = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) );
pData1 = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin1(pNode) );
pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode );
@@ -112,13 +79,25 @@ Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
for ( k = 0; k < pInfoPi->nWords; k++ )
pDataAnd[k] = pData0[k] & pData1[k];
}
- return pInfoAll;
+ // derive the PO siminfo
+ Aig_ManForEachPi( p, pNode, i )
+ {
+ pDataPo = Aig_SimInfoForNode( pInfoAll, pNode );
+ pDataAnd = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) );
+ if ( Aig_NodeFaninC0(pNode) )
+ for ( k = 0; k < pInfoPi->nWords; k++ )
+ pDataPo[k] = ~pDataAnd[k];
+ else
+ for ( k = 0; k < pInfoPi->nWords; k++ )
+ pDataPo[k] = pDataAnd[k];
+ }
}
+
/**Function*************************************************************
- Synopsis []
+ Synopsis [Allocates the simulation info.]
Description []
@@ -142,7 +121,7 @@ Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type )
/**Function*************************************************************
- Synopsis []
+ Synopsis [Sets the simulation info to zero.]
Description []
@@ -161,7 +140,7 @@ void Aig_SimInfoClean( Aig_SimInfo_t * p )
/**Function*************************************************************
- Synopsis []
+ Synopsis [Sets the random simulation info.]
Description []
@@ -187,7 +166,40 @@ void Aig_SimInfoRandom( Aig_SimInfo_t * p )
/**Function*************************************************************
- Synopsis []
+ Synopsis [Sets the random simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat )
+{
+ unsigned * pData;
+ int i, k;
+ assert( p->Type == 0 );
+ assert( p->nNodes == pPat->nBits );
+ for ( i = 0; i < p->nNodes; i++ )
+ {
+ // get the pointer to the bitdata for node i
+ pData = p->pData + p->nWords * i;
+ // fill in the bit data according to the pattern
+ if ( Aig_InfoHasBit(pPat->pData, i) ) // PI has bit set to 1
+ for ( k = 0; k < p->nWords; k++ )
+ pData[k] = ~((unsigned)0);
+ else
+ for ( k = 0; k < p->nWords; k++ )
+ pData[k] = 0;
+ // flip one bit
+ Aig_InfoXorBit( pData, i );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resizes the simulation info.]
Description []
@@ -209,13 +221,15 @@ void Aig_SimInfoResize( Aig_SimInfo_t * p )
for ( k = 0; k < p->nWords; k++ )
pData[2 * p->nWords * i + k + p->nWords] = 0;
}
- p->nPatsMax *= 2;
p->nWords *= 2;
+ p->nPatsMax *= 2;
+ free( p->pData );
+ p->pData = pData;
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Deallocates the simulation info.]
Description []
@@ -231,6 +245,80 @@ void Aig_SimInfoFree( Aig_SimInfo_t * p )
}
+/**Function*************************************************************
+
+ Synopsis [Allocates the simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Pattern_t * Aig_PatternAlloc( int nBits )
+{
+ Aig_Pattern_t * pPat;
+ pPat = ALLOC( Aig_Pattern_t, 1 );
+ memset( pPat, 0, sizeof(Aig_Pattern_t) );
+ pPat->nBits = nBits;
+ pPat->nWords = Aig_BitWordNum(nBits);
+ pPat->pData = ALLOC( unsigned, pPat->nWords );
+ return pPat;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Cleans the pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_PatternClean( Aig_Pattern_t * pPat )
+{
+ memset( pPat->pData, 0, sizeof(unsigned) * pPat->nWords );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets the random pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_PatternRandom( Aig_Pattern_t * pPat )
+{
+ int i;
+ for ( i = 0; i < pPat->nWords; i++ )
+ pPat->pData[i] = ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()));
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates the pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_PatternFree( Aig_Pattern_t * pPat )
+{
+ free( pPat->pData );
+ free( pPat );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/aig/fraigSolver.c b/src/sat/aig/fraigSolver.c
new file mode 100644
index 00000000..12502951
--- /dev/null
+++ b/src/sat/aig/fraigSolver.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+ FileName [fraigSolver.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: fraigSolver.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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/aig/fraigTrav.c b/src/sat/aig/fraigTrav.c
new file mode 100644
index 00000000..d5a09259
--- /dev/null
+++ b/src/sat/aig/fraigTrav.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+ FileName [fraigTrav.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: fraigTrav.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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index eb1c5374..3fadd457 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -26,7 +26,7 @@
#define ABC_DEFAULT_TIMEOUT 60 // 60 seconds
-struct CSAT_ManagerStruct_t
+struct ABC_ManagerStruct_t
{
// information about the problem
stmm_table * tName2Node; // the hash table mapping names to nodes
@@ -43,11 +43,11 @@ struct CSAT_ManagerStruct_t
Vec_Ptr_t * vNodes; // the gates in the target
Vec_Int_t * vValues; // the values of gate's outputs in the target
// solution
- CSAT_Target_ResultT * pResult; // the result of solving the target
+ ABC_Target_ResultT * pResult; // the result of solving the target
};
-static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars );
-static char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode );
+static ABC_Target_ResultT * ABC_TargetResAlloc( int nVars );
+static char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode );
// some external procedures
extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
@@ -67,11 +67,11 @@ extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
SeeAlso []
***********************************************************************/
-CSAT_Manager CSAT_InitManager()
+ABC_Manager ABC_InitManager()
{
- CSAT_Manager_t * mng;
- mng = ALLOC( CSAT_Manager_t, 1 );
- memset( mng, 0, sizeof(CSAT_Manager_t) );
+ ABC_Manager_t * mng;
+ mng = ALLOC( ABC_Manager_t, 1 );
+ memset( mng, 0, sizeof(ABC_Manager_t) );
mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
mng->pNtk->pName = util_strsav("csat_network");
mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
@@ -93,7 +93,7 @@ CSAT_Manager CSAT_InitManager()
SeeAlso []
***********************************************************************/
-void CSAT_QuitManager( CSAT_Manager mng )
+void ABC_QuitManager( ABC_Manager mng )
{
if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name );
if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
@@ -116,15 +116,15 @@ void CSAT_QuitManager( CSAT_Manager mng )
SeeAlso []
***********************************************************************/
-void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option )
+void ABC_SetSolveOption( ABC_Manager mng, enum ABC_OptionT option )
{
mng->mode = option;
if ( option == 0 )
- printf( "CSAT_SetSolveOption: Setting brute-force SAT mode.\n" );
+ printf( "ABC_SetSolveOption: Setting brute-force SAT mode.\n" );
else if ( option == 1 )
- printf( "CSAT_SetSolveOption: Setting resource-aware FRAIG mode.\n" );
+ printf( "ABC_SetSolveOption: Setting resource-aware FRAIG mode.\n" );
else
- printf( "CSAT_SetSolveOption: Unknown solving mode.\n" );
+ printf( "ABC_SetSolveOption: Unknown solving mode.\n" );
}
@@ -143,7 +143,7 @@ void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option )
SeeAlso []
***********************************************************************/
-int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr )
+int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr )
{
Abc_Obj_t * pObj, * pFanin;
char * pSop;
@@ -151,82 +151,82 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c
switch( type )
{
- case CSAT_BPI:
- case CSAT_BPPI:
+ case ABC_BPI:
+ case ABC_BPPI:
if ( nofi != 0 )
- { printf( "CSAT_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; }
// create the PI
pObj = Abc_NtkCreatePi( mng->pNtk );
stmm_insert( mng->tNode2Name, (char *)pObj, name );
break;
- case CSAT_CONST:
- case CSAT_BAND:
- case CSAT_BNAND:
- case CSAT_BOR:
- case CSAT_BNOR:
- case CSAT_BXOR:
- case CSAT_BXNOR:
- case CSAT_BINV:
- case CSAT_BBUF:
+ case ABC_CONST:
+ case ABC_BAND:
+ case ABC_BNAND:
+ case ABC_BOR:
+ case ABC_BNOR:
+ case ABC_BXOR:
+ case ABC_BXNOR:
+ case ABC_BINV:
+ case ABC_BBUF:
// create the node
pObj = Abc_NtkCreateNode( mng->pNtk );
// create the fanins
for ( i = 0; i < nofi; i++ )
{
if ( !stmm_lookup( mng->tName2Node, fanins[i], (char **)&pFanin ) )
- { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; }
+ { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; }
Abc_ObjAddFanin( pObj, pFanin );
}
// create the node function
switch( type )
{
- case CSAT_CONST:
+ case ABC_CONST:
if ( nofi != 0 )
- { printf( "CSAT_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; }
pSop = Abc_SopCreateConst1( mng->pNtk->pManFunc );
break;
- case CSAT_BAND:
+ case ABC_BAND:
if ( nofi < 1 )
- { printf( "CSAT_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL );
break;
- case CSAT_BNAND:
+ case ABC_BNAND:
if ( nofi < 1 )
- { printf( "CSAT_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; }
pSop = Abc_SopCreateNand( mng->pNtk->pManFunc, nofi );
break;
- case CSAT_BOR:
+ case ABC_BOR:
if ( nofi < 1 )
- { printf( "CSAT_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; }
pSop = Abc_SopCreateOr( mng->pNtk->pManFunc, nofi, NULL );
break;
- case CSAT_BNOR:
+ case ABC_BNOR:
if ( nofi < 1 )
- { printf( "CSAT_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; }
pSop = Abc_SopCreateNor( mng->pNtk->pManFunc, nofi );
break;
- case CSAT_BXOR:
+ case ABC_BXOR:
if ( nofi < 1 )
- { printf( "CSAT_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; }
if ( nofi > 2 )
- { printf( "CSAT_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
pSop = Abc_SopCreateXor( mng->pNtk->pManFunc, nofi );
break;
- case CSAT_BXNOR:
+ case ABC_BXNOR:
if ( nofi < 1 )
- { printf( "CSAT_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; }
if ( nofi > 2 )
- { printf( "CSAT_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
pSop = Abc_SopCreateNxor( mng->pNtk->pManFunc, nofi );
break;
- case CSAT_BINV:
+ case ABC_BINV:
if ( nofi != 1 )
- { printf( "CSAT_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
pSop = Abc_SopCreateInv( mng->pNtk->pManFunc );
break;
- case CSAT_BBUF:
+ case ABC_BBUF:
if ( nofi != 1 )
- { printf( "CSAT_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
pSop = Abc_SopCreateBuf( mng->pNtk->pManFunc );
break;
default :
@@ -234,24 +234,24 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c
}
Abc_ObjSetData( pObj, pSop );
break;
- case CSAT_BPPO:
- case CSAT_BPO:
+ case ABC_BPPO:
+ case ABC_BPO:
if ( nofi != 1 )
- { printf( "CSAT_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
// create the PO
pObj = Abc_NtkCreatePo( mng->pNtk );
stmm_insert( mng->tNode2Name, (char *)pObj, name );
// connect to the PO fanin
if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) )
- { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; }
+ { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; }
Abc_ObjAddFanin( pObj, pFanin );
break;
default:
- printf( "CSAT_AddGate: Unknown gate type.\n" );
+ printf( "ABC_AddGate: Unknown gate type.\n" );
break;
}
if ( stmm_insert( mng->tName2Node, name, (char *)pObj ) )
- { printf( "CSAT_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; }
+ { printf( "ABC_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; }
return 1;
}
@@ -267,7 +267,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c
SeeAlso []
***********************************************************************/
-int CSAT_Check_Integrity( CSAT_Manager mng )
+int ABC_Check_Integrity( ABC_Manager mng )
{
Abc_Ntk_t * pNtk = mng->pNtk;
Abc_Obj_t * pObj;
@@ -276,15 +276,15 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
// this procedure also finalizes construction of the ABC network
Abc_NtkFixNonDrivenNets( pNtk );
Abc_NtkForEachPi( pNtk, pObj, i )
- Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) );
+ Abc_NtkLogicStoreName( pObj, ABC_GetNodeName(mng, pObj) );
Abc_NtkForEachPo( pNtk, pObj, i )
- Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) );
+ Abc_NtkLogicStoreName( pObj, ABC_GetNodeName(mng, pObj) );
assert( Abc_NtkLatchNum(pNtk) == 0 );
// make sure everything is okay with the network structure
if ( !Abc_NtkDoCheck( pNtk ) )
{
- printf( "CSAT_Check_Integrity: The internal network check has failed.\n" );
+ printf( "ABC_Check_Integrity: The internal network check has failed.\n" );
return 0;
}
@@ -295,7 +295,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
continue;
if ( Abc_ObjFanoutNum(pObj) == 0 )
{
- printf( "CSAT_Check_Integrity: The network has dangling nodes.\n" );
+ printf( "ABC_Check_Integrity: The network has dangling nodes.\n" );
return 0;
}
}
@@ -313,7 +313,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
SeeAlso []
***********************************************************************/
-void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime )
+void ABC_SetTimeLimit( ABC_Manager mng, int runtime )
{
mng->nSeconds = runtime;
}
@@ -329,9 +329,9 @@ void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime )
SeeAlso []
***********************************************************************/
-void CSAT_SetLearnLimit( CSAT_Manager mng, int num )
+void ABC_SetLearnLimit( ABC_Manager mng, int num )
{
- printf( "CSAT_SetLearnLimit: The resource limit is not implemented (warning).\n" );
+ printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" );
}
/**Function*************************************************************
@@ -345,9 +345,9 @@ void CSAT_SetLearnLimit( CSAT_Manager mng, int num )
SeeAlso []
***********************************************************************/
-void CSAT_SetSolveBacktrackLimit( CSAT_Manager mng, int num )
+void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num )
{
- printf( "CSAT_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" );
+ printf( "ABC_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" );
}
/**Function*************************************************************
@@ -361,9 +361,9 @@ void CSAT_SetSolveBacktrackLimit( CSAT_Manager mng, int num )
SeeAlso []
***********************************************************************/
-void CSAT_SetLearnBacktrackLimit( CSAT_Manager mng, int num )
+void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num )
{
- printf( "CSAT_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
+ printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
}
/**Function*************************************************************
@@ -377,7 +377,7 @@ void CSAT_SetLearnBacktrackLimit( CSAT_Manager mng, int num )
SeeAlso []
***********************************************************************/
-void CSAT_EnableDump( CSAT_Manager mng, char * dump_file )
+void ABC_EnableDump( ABC_Manager mng, char * dump_file )
{
FREE( mng->pDumpFileName );
mng->pDumpFileName = util_strsav( dump_file );
@@ -398,12 +398,12 @@ void CSAT_EnableDump( CSAT_Manager mng, char * dump_file )
SeeAlso []
***********************************************************************/
-int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values )
+int ABC_AddTarget( ABC_Manager mng, int nog, char ** names, int * values )
{
Abc_Obj_t * pObj;
int i;
if ( nog < 1 )
- { printf( "CSAT_AddTarget: The target has no gates.\n" ); return 0; }
+ { printf( "ABC_AddTarget: The target has no gates.\n" ); return 0; }
// clear storage for the target
mng->nog = 0;
Vec_PtrClear( mng->vNodes );
@@ -412,10 +412,10 @@ int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values )
for ( i = 0; i < nog; i++ )
{
if ( !stmm_lookup( mng->tName2Node, names[i], (char **)&pObj ) )
- { printf( "CSAT_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; }
+ { printf( "ABC_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; }
Vec_PtrPush( mng->vNodes, pObj );
if ( values[i] < 0 || values[i] > 1 )
- { printf( "CSAT_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; }
+ { printf( "ABC_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; }
Vec_IntPush( mng->vValues, values[i] );
}
mng->nog = nog;
@@ -427,14 +427,14 @@ int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values )
Synopsis [Initialize the solver internal data structure.]
Description [Prepares the solver to work on one specific target
- set by calling CSAT_AddTarget before.]
+ set by calling ABC_AddTarget before.]
SideEffects []
SeeAlso []
***********************************************************************/
-void CSAT_SolveInit( CSAT_Manager mng )
+void ABC_SolveInit( ABC_Manager mng )
{
Fraig_Params_t * pParams = &mng->Params;
int nWords1, nWords2, nWordsMin;
@@ -442,7 +442,7 @@ void CSAT_SolveInit( CSAT_Manager mng )
// check if the target is available
assert( mng->nog == Vec_PtrSize(mng->vNodes) );
if ( mng->nog == 0 )
- { printf( "CSAT_SolveInit: Target is not specified by CSAT_AddTarget().\n" ); return; }
+ { printf( "ABC_SolveInit: Target is not specified by ABC_AddTarget().\n" ); return; }
// free the previous target network if present
if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
@@ -485,13 +485,13 @@ void CSAT_SolveInit( CSAT_Manager mng )
SeeAlso []
***********************************************************************/
-void CSAT_AnalyzeTargets( CSAT_Manager mng )
+void ABC_AnalyzeTargets( ABC_Manager mng )
{
}
/**Function*************************************************************
- Synopsis [Solves the targets added by CSAT_AddTarget().]
+ Synopsis [Solves the targets added by ABC_AddTarget().]
Description []
@@ -500,7 +500,7 @@ void CSAT_AnalyzeTargets( CSAT_Manager mng )
SeeAlso []
***********************************************************************/
-enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
+enum ABC_StatusT ABC_Solve( ABC_Manager mng )
{
Fraig_Man_t * pMan;
Abc_Ntk_t * pCnf;
@@ -509,7 +509,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
// check if the target network is available
if ( mng->pTarget == NULL )
- { printf( "CSAT_Solve: Target network is not derived by CSAT_SolveInit().\n" ); return UNDETERMINED; }
+ { printf( "ABC_Solve: Target network is not derived by ABC_SolveInit().\n" ); return UNDETERMINED; }
// optimizations of the target go here
// for example, to enable one pass of rewriting, uncomment this line
@@ -522,7 +522,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
RetValue = Abc_NtkMiterSat( pCnf, mng->nSeconds, 0 );
// analyze the result
- mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
+ mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
if ( RetValue == -1 )
mng->pResult->status = UNDETERMINED;
else if ( RetValue == 1 )
@@ -533,7 +533,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
// create the array of PI names and values
for ( i = 0; i < mng->pResult->no_sig; i++ )
{
- mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
+ mng->pResult->names[i] = ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
mng->pResult->values[i] = pCnf->pModel[i];
}
FREE( mng->pTarget->pModel );
@@ -549,7 +549,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
RetValue = Fraig_ManCheckMiter( pMan );
// analyze the result
- mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
+ mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
if ( RetValue == -1 )
mng->pResult->status = UNDETERMINED;
else if ( RetValue == 1 )
@@ -562,7 +562,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
// create the array of PI names and values
for ( i = 0; i < mng->pResult->no_sig; i++ )
{
- mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
+ mng->pResult->names[i] = ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
mng->pResult->values[i] = pModel[i];
}
}
@@ -584,14 +584,14 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
Synopsis [Gets the solve status of a target.]
- Description [TargetID: the target id returned by CSAT_AddTarget().]
+ Description [TargetID: the target id returned by ABC_AddTarget().]
SideEffects []
SeeAlso []
***********************************************************************/
-CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID )
+ABC_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID )
{
return mng->pResult;
}
@@ -607,7 +607,7 @@ CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID )
SeeAlso []
***********************************************************************/
-void CSAT_Dump_Bench_File( CSAT_Manager mng )
+void ABC_Dump_Bench_File( ABC_Manager mng )
{
Abc_Ntk_t * pNtkTemp, * pNtkAig;
char * pFileName;
@@ -617,7 +617,7 @@ void CSAT_Dump_Bench_File( CSAT_Manager mng )
pNtkTemp = Abc_NtkLogicToNetlistBench( pNtkAig );
Abc_NtkDelete( pNtkAig );
if ( pNtkTemp == NULL )
- { printf( "CSAT_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }
+ { printf( "ABC_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }
pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench";
Io_WriteBench( pNtkTemp, pFileName );
Abc_NtkDelete( pNtkTemp );
@@ -636,11 +636,11 @@ void CSAT_Dump_Bench_File( CSAT_Manager mng )
SeeAlso []
***********************************************************************/
-CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars )
+ABC_Target_ResultT * ABC_TargetResAlloc( int nVars )
{
- CSAT_Target_ResultT * p;
- p = ALLOC( CSAT_Target_ResultT, 1 );
- memset( p, 0, sizeof(CSAT_Target_ResultT) );
+ ABC_Target_ResultT * p;
+ p = ALLOC( ABC_Target_ResultT, 1 );
+ memset( p, 0, sizeof(ABC_Target_ResultT) );
p->no_sig = nVars;
p->names = ALLOC( char *, nVars );
p->values = ALLOC( int, nVars );
@@ -660,7 +660,7 @@ CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars )
SeeAlso []
***********************************************************************/
-void CSAT_TargetResFree( CSAT_Target_ResultT * p )
+void ABC_TargetResFree( ABC_Target_ResultT * p )
{
if ( p == NULL )
return;
@@ -680,7 +680,7 @@ void CSAT_TargetResFree( CSAT_Target_ResultT * p )
SeeAlso []
***********************************************************************/
-char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode )
+char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode )
{
char * pName = NULL;
if ( !stmm_lookup( mng->tNode2Name, (char *)pNode, (char **)&pName ) )
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h
index e567241f..3e04c7df 100644
--- a/src/sat/csat/csat_apis.h
+++ b/src/sat/csat/csat_apis.h
@@ -16,8 +16,8 @@
***********************************************************************/
-#ifndef __CSAT_APIS_H__
-#define __CSAT_APIS_H__
+#ifndef __ABC_APIS_H__
+#define __ABC_APIS_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
@@ -32,37 +32,37 @@
////////////////////////////////////////////////////////////////////////
-typedef struct CSAT_ManagerStruct_t CSAT_Manager_t;
-typedef struct CSAT_ManagerStruct_t * CSAT_Manager;
+typedef struct ABC_ManagerStruct_t ABC_Manager_t;
+typedef struct ABC_ManagerStruct_t * ABC_Manager;
// GateType defines the gate type that can be added to circuit by
-// CSAT_AddGate();
-#ifndef _CSAT_GATE_TYPE_
-#define _CSAT_GATE_TYPE_
+// ABC_AddGate();
+#ifndef _ABC_GATE_TYPE_
+#define _ABC_GATE_TYPE_
enum GateType
{
- CSAT_CONST = 0, // constant gate
- CSAT_BPI, // boolean PI
- CSAT_BPPI, // bit level PSEUDO PRIMARY INPUT
- CSAT_BAND, // bit level AND
- CSAT_BNAND, // bit level NAND
- CSAT_BOR, // bit level OR
- CSAT_BNOR, // bit level NOR
- CSAT_BXOR, // bit level XOR
- CSAT_BXNOR, // bit level XNOR
- CSAT_BINV, // bit level INVERTER
- CSAT_BBUF, // bit level BUFFER
- CSAT_BPPO, // bit level PSEUDO PRIMARY OUTPUT
- CSAT_BPO // boolean PO
+ ABC_CONST = 0, // constant gate
+ ABC_BPI, // boolean PI
+ ABC_BPPI, // bit level PSEUDO PRIMARY INPUT
+ ABC_BAND, // bit level AND
+ ABC_BNAND, // bit level NAND
+ ABC_BOR, // bit level OR
+ ABC_BNOR, // bit level NOR
+ ABC_BXOR, // bit level XOR
+ ABC_BXNOR, // bit level XNOR
+ ABC_BINV, // bit level INVERTER
+ ABC_BBUF, // bit level BUFFER
+ ABC_BPPO, // bit level PSEUDO PRIMARY OUTPUT
+ ABC_BPO // boolean PO
};
#endif
-//CSAT_StatusT defines the return value by CSAT_Solve();
-#ifndef _CSAT_STATUS_
-#define _CSAT_STATUS_
-enum CSAT_StatusT
+//ABC_StatusT defines the return value by ABC_Solve();
+#ifndef _ABC_STATUS_
+#define _ABC_STATUS_
+enum ABC_StatusT
{
UNDETERMINED = 0,
UNSATISFIABLE,
@@ -76,11 +76,11 @@ enum CSAT_StatusT
#endif
-// CSAT_OptionT defines the solver option about learning
-// which is used by CSAT_SetSolveOption();
-#ifndef _CSAT_OPTION_
-#define _CSAT_OPTION_
-enum CSAT_OptionT
+// ABC_OptionT defines the solver option about learning
+// which is used by ABC_SetSolveOption();
+#ifndef _ABC_OPTION_
+#define _ABC_OPTION_
+enum ABC_OptionT
{
BASE_LINE = 0,
IMPLICT_LEARNING, //default
@@ -89,12 +89,12 @@ enum CSAT_OptionT
#endif
-#ifndef _CSAT_Target_Result
-#define _CSAT_Target_Result
-typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT;
-struct _CSAT_Target_ResultT
+#ifndef _ABC_Target_Result
+#define _ABC_Target_Result
+typedef struct _ABC_Target_ResultT ABC_Target_ResultT;
+struct _ABC_Target_ResultT
{
- enum CSAT_StatusT status; // solve status of the target
+ enum ABC_StatusT status; // solve status of the target
int num_dec; // num of decisions to solve the target
int num_imp; // num of implications to solve the target
int num_cftg; // num of conflict gates learned
@@ -118,10 +118,10 @@ struct _CSAT_Target_ResultT
////////////////////////////////////////////////////////////////////////
// create a new manager
-extern CSAT_Manager CSAT_InitManager(void);
+extern ABC_Manager ABC_InitManager(void);
// set solver options for learning
-extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_OptionT option);
+extern void ABC_SetSolveOption(ABC_Manager mng, enum ABC_OptionT option);
// add a gate to the circuit
// the meaning of the parameters are:
@@ -129,7 +129,7 @@ extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_Opt
// name: the name of the gate to be added, name should be unique in a circuit.
// nofi: number of fanins of the gate to be added;
// fanins: the name array of fanins of the gate to be added
-extern int CSAT_AddGate(CSAT_Manager mng,
+extern int ABC_AddGate(ABC_Manager mng,
enum GateType type,
char* name,
int nofi,
@@ -138,38 +138,38 @@ extern int CSAT_AddGate(CSAT_Manager mng,
// check if there are gates that are not used by any primary ouput.
// if no such gates exist, return 1 else return 0;
-extern int CSAT_Check_Integrity(CSAT_Manager mng);
+extern int ABC_Check_Integrity(ABC_Manager mng);
// set time limit for solving a target.
// runtime: time limit (in second).
-extern void CSAT_SetTimeLimit(CSAT_Manager mng, int runtime);
-extern void CSAT_SetLearnLimit(CSAT_Manager mng, int num);
-extern void CSAT_SetSolveBacktrackLimit(CSAT_Manager mng, int num);
-extern void CSAT_SetLearnBacktrackLimit(CSAT_Manager mng, int num);
-extern void CSAT_EnableDump(CSAT_Manager mng, char* dump_file);
+extern void ABC_SetTimeLimit(ABC_Manager mng, int runtime);
+extern void ABC_SetLearnLimit(ABC_Manager mng, int num);
+extern void ABC_SetSolveBacktrackLimit(ABC_Manager mng, int num);
+extern void ABC_SetLearnBacktrackLimit(ABC_Manager mng, int num);
+extern void ABC_EnableDump(ABC_Manager mng, char* dump_file);
// the meaning of the parameters are:
// nog: number of gates that are in the targets
// names: name array of gates
// values: value array of the corresponding gates given in "names" to be
// solved. the relation of them is AND.
-extern int CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values);
+extern int ABC_AddTarget(ABC_Manager mng, int nog, char**names, int* values);
// initialize the solver internal data structure.
-extern void CSAT_SolveInit(CSAT_Manager mng);
-extern void CSAT_AnalyzeTargets(CSAT_Manager mng);
+extern void ABC_SolveInit(ABC_Manager mng);
+extern void ABC_AnalyzeTargets(ABC_Manager mng);
-// solve the targets added by CSAT_AddTarget()
-extern enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng);
+// solve the targets added by ABC_AddTarget()
+extern enum ABC_StatusT ABC_Solve(ABC_Manager mng);
// get the solve status of a target
-// TargetID: the target id returned by CSAT_AddTarget().
-extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID);
-extern void CSAT_Dump_Bench_File(CSAT_Manager mng);
+// TargetID: the target id returned by ABC_AddTarget().
+extern ABC_Target_ResultT * ABC_Get_Target_Result(ABC_Manager mng, int TargetID);
+extern void ABC_Dump_Bench_File(ABC_Manager mng);
// ADDED PROCEDURES:
-extern void CSAT_QuitManager( CSAT_Manager mng );
-extern void CSAT_TargetResFree( CSAT_Target_ResultT * p );
+extern void ABC_QuitManager( ABC_Manager mng );
+extern void ABC_TargetResFree( ABC_Target_ResultT * p );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/sat/fraig/fraigMem.c b/src/sat/fraig/fraigMem.c
index 7dc46430..500431c6 100644
--- a/src/sat/fraig/fraigMem.c
+++ b/src/sat/fraig/fraigMem.c
@@ -201,7 +201,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_t * p )
int i;
char * pTemp;
- // delocate all chunks except the first one
+ // deallocate all chunks except the first one
for ( i = 1; i < p->nChunks; i++ )
free( p->pChunks[i] );
p->nChunks = 1;
diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c
index 40aa223b..30bf4a96 100644
--- a/src/sat/msat/msatMem.c
+++ b/src/sat/msat/msatMem.c
@@ -231,7 +231,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p )
int i;
char * pTemp;
- // delocate all chunks except the first one
+ // deallocate all chunks except the first one
for ( i = 1; i < p->nChunks; i++ )
free( p->pChunks[i] );
p->nChunks = 1;
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-02 02:43:26 +0000