summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abcAig.c45
-rw-r--r--src/base/abci/abc.c49
-rw-r--r--src/base/abci/abcSat.c497
-rw-r--r--src/base/abci/abcVerify.c6
4 files changed, 583 insertions, 14 deletions
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 53ad88c2..167e7552 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -572,7 +572,28 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
return Abc_AigOr( pMan, Abc_AigAnd(pMan, p0, Abc_ObjNot(p1)),
Abc_AigAnd(pMan, p1, Abc_ObjNot(p0)) );
}
+
+/**Function*************************************************************
+
+ Synopsis [Implements the miter.]
+
+ Description []
+
+ SideEffects []
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Abc_AigMiter_rec( Abc_Aig_t * pMan, Abc_Obj_t ** ppObjs, int nObjs )
+{
+ Abc_Obj_t * pObj1, * pObj2;
+ if ( nObjs == 1 )
+ return ppObjs[0];
+ pObj1 = Abc_AigMiter_rec( pMan, ppObjs, nObjs/2 );
+ pObj2 = Abc_AigMiter_rec( pMan, ppObjs + nObjs/2, nObjs - nObjs/2 );
+ return Abc_AigOr( pMan, pObj1, pObj2 );
+}
+
/**Function*************************************************************
Synopsis [Implements the miter.]
@@ -586,6 +607,30 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
***********************************************************************/
Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
{
+ int i;
+ if ( vPairs->nSize == 0 )
+ return Abc_ObjNot( Abc_NtkConst1(pMan->pNtkAig) );
+ assert( vPairs->nSize % 2 == 0 );
+ // go through the cubes of the node's SOP
+ for ( i = 0; i < vPairs->nSize; i += 2 )
+ vPairs->pArray[i/2] = Abc_AigXor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] );
+ vPairs->nSize = vPairs->nSize/2;
+ return Abc_AigMiter_rec( pMan, (Abc_Obj_t **)vPairs->pArray, vPairs->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Implements the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Abc_AigMiter2( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
+{
Abc_Obj_t * pMiter, * pXor;
int i;
assert( vPairs->nSize % 2 == 0 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 71b76cf6..70cd2e6c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2868,6 +2868,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
return 0;
}
+ if ( Abc_NtkIsSeq(pNtk) )
+ {
+ fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" );
+ return 0;
+ }
+
+/*
if ( !Abc_NtkIsLogic(pNtk) )
{
fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" );
@@ -2877,19 +2884,35 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkUnmap(pNtk);
if ( Abc_NtkIsSopLogic(pNtk) )
Abc_NtkSopToBdd(pNtk);
-
- RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose );
- if ( RetValue == -1 )
- printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
- else if ( RetValue == 0 )
- printf( "The miter is SATISFIABLE.\n" );
+*/
+ if ( Abc_NtkIsStrash(pNtk) )
+ {
+ RetValue = Abc_NtkMiterSat2( pNtk, nSeconds, fVerbose );
+ if ( RetValue == -1 )
+ printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
+ else if ( RetValue == 0 )
+ printf( "The miter is SATISFIABLE.\n" );
+ else
+ printf( "The miter is UNSATISFIABLE.\n" );
+ }
else
- printf( "The miter is UNSATISFIABLE.\n" );
+ {
+ Abc_Ntk_t * pTemp;
+ pTemp = Abc_NtkStrash( pNtk, 0, 0 );
+ RetValue = Abc_NtkMiterSat2( pTemp, nSeconds, fVerbose );
+ if ( RetValue == -1 )
+ printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
+ else if ( RetValue == 0 )
+ printf( "The miter is SATISFIABLE.\n" );
+ else
+ printf( "The miter is UNSATISFIABLE.\n" );
+ Abc_NtkDelete( pTemp );
+ }
return 0;
usage:
fprintf( pErr, "usage: sat [-T num] [-vh]\n" );
- fprintf( pErr, "\t solves the miter\n" );
+ fprintf( pErr, "\t solves the combinational miter\n" );
fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
@@ -3722,11 +3745,11 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// run the command
- pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 0, 0, fUseInvs, fVerbose );
+ pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
- return 1;
+ return 0;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -3788,9 +3811,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
-// Abc_NtkDeriveEsops( pNtk );
-// Abc_NtkXyz( pNtk, 128, 0, 0, 0 );
- printf( "This command is currently not used.\n" );
+ Abc_NtkTestEsop( pNtk );
+// Abc_NtkTestSop( pNtk );
+// printf( "This command is currently not used.\n" );
/*
// run the command
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 4a65659c..8c8636c5 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -27,6 +27,10 @@
static int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
static int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
+static solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk );
+
+static nMuxes;
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -129,7 +133,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
Vec_Str_t * vCube;
Vec_Int_t * vVars;
char * pSop0, * pSop1;
- int i;
+ int i, clk = clock();
assert( Abc_NtkIsBddLogic(pNtk) );
@@ -159,6 +163,8 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
}
// Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 );
+ PRT( "Creating solver", clock() - clk );
+
// delete
Vec_StrFree( vCube );
Vec_IntFree( vVars );
@@ -291,6 +297,495 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
}
+
+
+
+
+
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Attempts to solve the miter using an internal SAT solver.]
+
+ Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
+{
+ solver * pSat;
+ lbool status;
+ int RetValue, clk;
+
+ assert( Abc_NtkIsStrash(pNtk) );
+ assert( Abc_NtkLatchNum(pNtk) == 0 );
+
+ if ( Abc_NtkPoNum(pNtk) > 1 )
+ fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
+
+ // load clauses into the solver
+ clk = clock();
+ pSat = Abc_NtkMiterSatCreate2( pNtk );
+ if ( pSat == NULL )
+ return 1;
+// printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
+// PRT( "Time", clock() - clk );
+
+ // simplify the problem
+ clk = clock();
+ status = solver_simplify(pSat);
+// printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
+// PRT( "Time", clock() - clk );
+ if ( status == 0 )
+ {
+ solver_delete( pSat );
+// printf( "The problem is UNSATISFIABLE after simplification.\n" );
+ return 1;
+ }
+
+ // solve the miter
+ clk = clock();
+ if ( fVerbose )
+ pSat->verbosity = 1;
+ status = solver_solve( pSat, NULL, NULL, nSeconds );
+ if ( status == l_Undef )
+ {
+// printf( "The problem timed out.\n" );
+ RetValue = -1;
+ }
+ else if ( status == l_True )
+ {
+// printf( "The problem is SATISFIABLE.\n" );
+ RetValue = 0;
+ }
+ else if ( status == l_False )
+ {
+// printf( "The problem is UNSATISFIABLE.\n" );
+ RetValue = 1;
+ }
+ else
+ assert( 0 );
+ PRT( "SAT solver time", clock() - clk );
+
+ // if the problem is SAT, get the counterexample
+ if ( status == l_True )
+ {
+ Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
+ pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize );
+ Vec_IntFree( vCiIds );
+ }
+ // free the solver
+ solver_delete( pSat );
+ return RetValue;
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Adds trivial clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+{
+//printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->solver_stats.clauses );
+ vVars->nSize = 0;
+ Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
+// Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
+ return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds trivial clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_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( !Abc_ObjIsComplement( pNode ) );
+ assert( Abc_ObjIsNode( pNode ) );
+
+// nVars = solver_nvars(pSat);
+ Var = (int)pNode->pCopy;
+// 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 = Abc_ObjIsComplement(vSuper->pArray[i]);
+ // determine the variable numbers
+ Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
+// Var1 = (int)Abc_ObjRegular(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 = Abc_ObjIsComplement(vSuper->pArray[i]);
+ // determine the variable numbers
+ Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
+// Var1 = (int)Abc_ObjRegular(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 Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_Obj_t * pNodeT, Abc_Obj_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( !Abc_ObjIsComplement( pNode ) );
+ assert( Abc_NodeIsMuxType( pNode ) );
+ // get the variable numbers
+ VarF = (int)pNode->pCopy;
+ VarI = (int)pNodeC->pCopy;
+ VarT = (int)Abc_ObjRegular(pNodeT)->pCopy;
+ VarE = (int)Abc_ObjRegular(pNodeE)->pCopy;
+// VarF = (int)pNode->Id;
+// VarI = (int)pNodeC->Id;
+// VarT = (int)Abc_ObjRegular(pNodeT)->Id;
+// VarE = (int)Abc_ObjRegular(pNodeE)->Id;
+
+ // get the complementation flags
+ fCompT = Abc_ObjIsComplement(pNodeT);
+ fCompE = Abc_ObjIsComplement(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 Abc_NtkCollectSupergate_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, int fFirst, int fStopAtMux )
+{
+ int RetValue1, RetValue2, i;
+ // check if the node is visited
+ if ( Abc_ObjRegular(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] == Abc_ObjNot(pNode) )
+ return -1;
+ assert( 0 );
+ return 0;
+ }
+ // if the new node is complemented or a PI, another gate begins
+ if ( !fFirst )
+ if ( Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || Abc_ObjFanoutNum(pNode) > 1 || fStopAtMux && Abc_NodeIsMuxType(pNode) )
+ {
+ Vec_PtrPush( vSuper, pNode );
+ Abc_ObjRegular(pNode)->fMarkB = 1;
+ return 0;
+ }
+ assert( !Abc_ObjIsComplement(pNode) );
+ assert( Abc_ObjIsNode(pNode) );
+ // go through the branches
+ RetValue1 = Abc_NtkCollectSupergate_rec( Abc_ObjChild0(pNode), vSuper, 0, fStopAtMux );
+ RetValue2 = Abc_NtkCollectSupergate_rec( Abc_ObjChild1(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 Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNodes )
+{
+ int RetValue, i;
+ assert( !Abc_ObjIsComplement(pNode) );
+ // collect the nodes in the implication supergate
+ Vec_PtrClear( vNodes );
+ RetValue = Abc_NtkCollectSupergate_rec( pNode, vNodes, 1, fStopAtMux );
+ assert( vNodes->nSize > 1 );
+ // unmark the visited nodes
+ for ( i = 0; i < vNodes->nSize; i++ )
+ Abc_ObjRegular((Abc_Obj_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 Abc_NtkMiterSatCreate2Int( solver * pSat, Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
+ Vec_Ptr_t * vNodes, * vSuper;
+ Vec_Int_t * vVars;
+ int i, k, fUseMuxes = 1;
+
+ assert( Abc_NtkIsStrash(pNtk) );
+
+ // 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 = Abc_NtkConst1(pNtk);
+ pNode->fMarkA = 1;
+ pNode->pCopy = (Abc_Obj_t *)vNodes->nSize;
+ Vec_PtrPush( vNodes, pNode );
+ Abc_NtkClauseTriv( pSat, pNode, vVars );
+
+ // collect the nodes that need clauses and top-level assignments
+ Abc_NtkForEachCo( pNtk, pNode, i )
+ {
+ // get the fanin
+ pFanin = Abc_ObjFanin0(pNode);
+ // create the node's variable
+ if ( pFanin->fMarkA == 0 )
+ {
+ pFanin->fMarkA = 1;
+ pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize;
+ Vec_PtrPush( vNodes, pFanin );
+ }
+ // add the trivial clause
+ if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) )
+ return 0;
+ }
+
+ // add the clauses
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ assert( !Abc_ObjIsComplement(pNode) );
+ if ( !Abc_NodeIsAigAnd(pNode) )
+ continue;
+//printf( "%d ", pNode->Id );
+
+ // add the clauses
+ if ( fUseMuxes && Abc_NodeIsMuxType(pNode) )
+ {
+ nMuxes++;
+
+ pNodeC = Abc_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 = Abc_ObjRegular(pFanin);
+ if ( pFanin->fMarkA == 0 )
+ {
+ pFanin->fMarkA = 1;
+ pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize;
+ Vec_PtrPush( vNodes, pFanin );
+ }
+ }
+ // add the clauses
+ if ( !Abc_NtkClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) )
+ return 0;
+ }
+ else
+ {
+ // get the supergate
+ Abc_NtkCollectSupergate( pNode, fUseMuxes, vSuper );
+ // add the fanin nodes to explore
+ Vec_PtrForEachEntry( vSuper, pFanin, k )
+ {
+ pFanin = Abc_ObjRegular(pFanin);
+ if ( pFanin->fMarkA == 0 )
+ {
+ pFanin->fMarkA = 1;
+ pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize;
+ Vec_PtrPush( vNodes, pFanin );
+ }
+ }
+ // add the clauses
+ if ( vSuper->nSize == 0 )
+ {
+ if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) )
+ return 0;
+ }
+ else
+ {
+ if ( !Abc_NtkClauseAnd( 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 * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk )
+{
+ solver * pSat;
+ Abc_Obj_t * pNode;
+ int RetValue, i, clk = clock();
+
+ nMuxes = 0;
+
+ pSat = solver_new();
+ RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk );
+ Abc_NtkForEachObj( pNtk, pNode, i )
+ pNode->fMarkA = 0;
+ Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
+ if ( RetValue == 0 )
+ {
+ solver_delete(pSat);
+ return NULL;
+ }
+ printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
+ PRT( "Creating solver", clock() - clk );
+ return pSat;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 070c871d..b30a6452 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -148,6 +148,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
Fraig_ParamsSetDefault( &Params );
Params.fVerbose = fVerbose;
Params.nSeconds = nSeconds;
+ Params.fFuncRed = 0;
+ Params.nPatsRand = 0;
+ Params.nPatsDyna = 0;
pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 );
Fraig_ManProveMiter( pMan );
@@ -325,6 +328,9 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
Fraig_ParamsSetDefault( &Params );
Params.fVerbose = fVerbose;
Params.nSeconds = nSeconds;
+ Params.fFuncRed = 0;
+ Params.nPatsRand = 0;
+ Params.nPatsDyna = 0;
pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 );
Fraig_ManProveMiter( pMan );
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-15 20:33:29 +0000