summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-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
-rw-r--r--src/opt/xyz/xyz.h2
-rw-r--r--src/opt/xyz/xyzCore.c348
-rw-r--r--src/opt/xyz/xyzInt.h77
-rw-r--r--src/opt/xyz/xyzMinEsop.c38
-rw-r--r--src/opt/xyz/xyzMinMan.c1
-rw-r--r--src/opt/xyz/xyzMinSop.c346
-rw-r--r--src/opt/xyz/xyzMinUtil.c56
-rw-r--r--src/opt/xyz/xyzTest.c370
-rw-r--r--src/sat/asat/solver.h5
-rw-r--r--src/sat/fraig/fraigCanon.c4
-rw-r--r--src/sat/fraig/fraigSat.c22
-rw-r--r--src/sat/msat/msat.h1
-rw-r--r--src/sat/msat/msatClause.c5
-rw-r--r--src/sat/msat/msatInt.h1
-rw-r--r--src/sat/msat/msatSolverApi.c1
-rw-r--r--src/sat/msat/msatSolverCore.c20
20 files changed, 1784 insertions, 110 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 );
diff --git a/src/opt/xyz/xyz.h b/src/opt/xyz/xyz.h
index f18686ff..ea488068 100644
--- a/src/opt/xyz/xyz.h
+++ b/src/opt/xyz/xyz.h
@@ -46,6 +46,8 @@ struct Xyz_Man_t_
Vec_Ptr_t * vObjStrs; // object structures
void * pMemory; // memory for the internal data strctures
Min_Man_t * pManMin; // the cub manager
+ int fUseEsop; // enables ESOPs
+ int fUseSop; // enables SOPs
// arrays to map local variables
Vec_Int_t * vComTo0; // mapping of common variables into first fanin
Vec_Int_t * vComTo1; // mapping of common variables into second fanin
diff --git a/src/opt/xyz/xyzCore.c b/src/opt/xyz/xyzCore.c
index a48f749e..e5089788 100644
--- a/src/opt/xyz/xyzCore.c
+++ b/src/opt/xyz/xyzCore.c
@@ -27,13 +27,19 @@
static void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose );
static int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose );
static void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary );
-
+/*
static int Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
static int Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
static int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
static int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
static int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
static int Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
+*/
+
+static int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj );
+static Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp );
+static Min_Cube_t * Abc_NodeXyzSum( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -59,6 +65,8 @@ Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUs
// create the manager
p = Xyz_ManAlloc( pNtk, nFaninMax );
+ p->fUseEsop = fUseEsop;
+ p->fUseSop = 1;//fUseSop;
pNtk->pManCut = p;
// perform mapping
@@ -69,6 +77,8 @@ Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUs
pNtkNew = Abc_NtkXyzDeriveClean( p, pNtk );
else
pNtkNew = Abc_NtkXyzDerive( p, pNtk );
+// pNtkNew = NULL;
+
Xyz_ManFree( p );
pNtk->pManCut = NULL;
@@ -164,7 +174,10 @@ int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose )
}
// traverse the cone starting from this node
- Abc_NtkXyzCovers_rec( p, pObj, vBoundary );
+ if ( Abc_ObjGetSupp(pObj) == NULL )
+ Abc_NtkXyzCovers_rec( p, pObj, vBoundary );
+
+ // count the number of solved cones
if ( Abc_ObjGetSupp(pObj) == NULL )
fStop = 0;
else
@@ -225,7 +238,7 @@ void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundar
{
Abc_Obj_t * pObj0, * pObj1;
// return if the support is already computed
- if ( pObj->fMarkB || pObj->fMarkA || Abc_ObjGetSupp(pObj) )
+ if ( pObj->fMarkB || pObj->fMarkA )//|| Abc_ObjGetSupp(pObj) ) // why do we need Supp check here???
return;
// mark as visited
pObj->fMarkB = 1;
@@ -236,9 +249,9 @@ void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundar
Abc_NtkXyzCovers_rec( p, pObj0, vBoundary );
Abc_NtkXyzCovers_rec( p, pObj1, vBoundary );
// skip the node that spaced out
- if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) || // fanin is not ready
- !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) || // fanin is not ready
- !Abc_NodeXyzPropagateEsop(p, pObj, pObj0, pObj1) ) // node's support or covers cannot be computed
+ if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) || // fanin is not ready
+ !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) || // fanin is not ready
+ !Abc_NodeXyzPropagate( p, pObj ) ) // node's support or covers cannot be computed
{
// save the nodes of the future boundary
if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) )
@@ -331,6 +344,321 @@ Vec_Int_t * Abc_NodeXyzSupport( Xyz_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * v
/**Function*************************************************************
+ Synopsis [Propagates all types of covers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj )
+{
+ Min_Cube_t * pCoverP = NULL, * pCoverN = NULL, * pCoverX = NULL;
+ Min_Cube_t * pCov0, * pCov1, * pCover0, * pCover1;
+ Vec_Int_t * vSupp, * vSupp0, * vSupp1;
+ Abc_Obj_t * pObj0, * pObj1;
+ int fCompl0, fCompl1;
+
+ pObj0 = Abc_ObjFanin0( pObj );
+ pObj1 = Abc_ObjFanin1( pObj );
+
+ if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id );
+ if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id );
+
+ // get the resulting support
+ vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0);
+ vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1);
+ vSupp = Abc_NodeXyzSupport( p, vSupp0, vSupp1 );
+
+ // quit if support if too large
+ if ( vSupp->nSize > p->nFaninMax )
+ {
+ Vec_IntFree( vSupp );
+ return 0;
+ }
+
+ // get the complemented attributes
+ fCompl0 = Abc_ObjFaninC0( pObj );
+ fCompl1 = Abc_ObjFaninC1( pObj );
+
+ // propagate ESOP
+ if ( p->fUseEsop )
+ {
+ // get the covers
+ pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0);
+ pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1);
+ if ( pCov0 && pCov1 )
+ {
+ // complement the first if needed
+ if ( !fCompl0 )
+ pCover0 = pCov0;
+ else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
+ pCover0 = pCov0->pNext;
+ else
+ pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0;
+
+ // complement the second if needed
+ if ( !fCompl1 )
+ pCover1 = pCov1;
+ else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
+ pCover1 = pCov1->pNext;
+ else
+ pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1;
+
+ // derive the new cover
+ pCoverX = Abc_NodeXyzProduct( p, pCover0, pCover1, 1, vSupp->nSize );
+ }
+ }
+ // propagate SOPs
+ if ( p->fUseSop )
+ {
+ // get the covers for the direct polarity
+ pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0);
+ pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1);
+ // derive the new cover
+ if ( pCover0 && pCover1 )
+ pCoverP = Abc_NodeXyzProduct( p, pCover0, pCover1, 0, vSupp->nSize );
+
+ // get the covers for the inverse polarity
+ pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0);
+ pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1);
+ // derive the new cover
+ if ( pCover0 && pCover1 )
+ pCoverN = Abc_NodeXyzSum( p, pCover0, pCover1, 0, vSupp->nSize );
+ }
+
+ // if none of the covers can be computed quit
+ if ( !pCoverX && !pCoverP && !pCoverN )
+ {
+ Vec_IntFree( vSupp );
+ return 0;
+ }
+
+ // set the covers
+ assert( Abc_ObjGetSupp(pObj) == NULL );
+ Abc_ObjSetSupp( pObj, vSupp );
+ Abc_ObjSetCover( pObj, pCoverP, 0 );
+ Abc_ObjSetCover( pObj, pCoverN, 1 );
+ Abc_ObjSetCover2( pObj, pCoverX );
+//printf( "%3d : %4d %4d %4d\n", pObj->Id, Min_CoverCountCubes(pCoverP), Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverX) );
+
+ // count statistics
+ p->nSupps++;
+ p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps );
+ return 1;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp )
+{
+ Min_Cube_t * pCube, * pCube0, * pCube1;
+ Min_Cube_t * pCover;
+ int i, Val0, Val1;
+ assert( pCover0 && pCover1 );
+
+ // clean storage
+ Min_ManClean( p->pManMin, nSupp );
+ // go through the cube pairs
+ Min_CoverForEachCube( pCover0, pCube0 )
+ Min_CoverForEachCube( pCover1, pCube1 )
+ {
+ // go through the support variables of the cubes
+ for ( i = 0; i < p->vPairs0->nSize; i++ )
+ {
+ Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] );
+ Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] );
+ if ( (Val0 & Val1) == 0 )
+ break;
+ }
+ // check disjointness
+ if ( i < p->vPairs0->nSize )
+ continue;
+
+ if ( p->pManMin->nCubes > p->nCubesMax )
+ {
+ pCover = Min_CoverCollect( p->pManMin, nSupp );
+//Min_CoverWriteFile( pCover, "large", 1 );
+ Min_CoverRecycle( p->pManMin, pCover );
+ return NULL;
+ }
+
+ // create the product cube
+ pCube = Min_CubeAlloc( p->pManMin );
+
+ // add the literals
+ pCube->nLits = 0;
+ for ( i = 0; i < nSupp; i++ )
+ {
+ if ( p->vComTo0->pArray[i] == -1 )
+ Val0 = 3;
+ else
+ Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
+
+ if ( p->vComTo1->pArray[i] == -1 )
+ Val1 = 3;
+ else
+ Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
+
+ if ( (Val0 & Val1) == 3 )
+ continue;
+
+ Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 );
+ pCube->nLits++;
+ }
+ // add the cube to storage
+ if ( fEsop )
+ Min_EsopAddCube( p->pManMin, pCube );
+ else
+ Min_SopAddCube( p->pManMin, pCube );
+ }
+
+ // minimize the cover
+ if ( fEsop )
+ Min_EsopMinimize( p->pManMin );
+ else
+ Min_SopMinimize( p->pManMin );
+ pCover = Min_CoverCollect( p->pManMin, nSupp );
+
+ // quit if the cover is too large
+ if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
+ {
+/*
+Min_CoverWriteFile( pCover, "large", 1 );
+ Min_CoverExpand( p->pManMin, pCover );
+ Min_EsopMinimize( p->pManMin );
+ Min_EsopMinimize( p->pManMin );
+ Min_EsopMinimize( p->pManMin );
+ Min_EsopMinimize( p->pManMin );
+ Min_EsopMinimize( p->pManMin );
+ Min_EsopMinimize( p->pManMin );
+ Min_EsopMinimize( p->pManMin );
+ Min_EsopMinimize( p->pManMin );
+ Min_EsopMinimize( p->pManMin );
+ pCover = Min_CoverCollect( p->pManMin, nSupp );
+*/
+ Min_CoverRecycle( p->pManMin, pCover );
+ return NULL;
+ }
+ return pCover;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeXyzSum( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp )
+{
+ Min_Cube_t * pCube, * pCube0, * pCube1;
+ Min_Cube_t * pCover;
+ int i, Val0, Val1;
+ assert( pCover0 && pCover1 );
+
+ // clean storage
+ Min_ManClean( p->pManMin, nSupp );
+ Min_CoverForEachCube( pCover0, pCube0 )
+ {
+ // create the cube
+ pCube = Min_CubeAlloc( p->pManMin );
+ pCube->nLits = 0;
+ for ( i = 0; i < p->vComTo0->nSize; i++ )
+ {
+ if ( p->vComTo0->pArray[i] == -1 )
+ continue;
+ Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
+ if ( Val0 == 3 )
+ continue;
+ Min_CubeXorVar( pCube, i, Val0 ^ 3 );
+ pCube->nLits++;
+ }
+ if ( p->pManMin->nCubes > p->nCubesMax )
+ {
+ pCover = Min_CoverCollect( p->pManMin, nSupp );
+ Min_CoverRecycle( p->pManMin, pCover );
+ return NULL;
+ }
+ // add the cube to storage
+ if ( fEsop )
+ Min_EsopAddCube( p->pManMin, pCube );
+ else
+ Min_SopAddCube( p->pManMin, pCube );
+ }
+ Min_CoverForEachCube( pCover1, pCube1 )
+ {
+ // create the cube
+ pCube = Min_CubeAlloc( p->pManMin );
+ pCube->nLits = 0;
+ for ( i = 0; i < p->vComTo1->nSize; i++ )
+ {
+ if ( p->vComTo1->pArray[i] == -1 )
+ continue;
+ Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
+ if ( Val1 == 3 )
+ continue;
+ Min_CubeXorVar( pCube, i, Val1 ^ 3 );
+ pCube->nLits++;
+ }
+ if ( p->pManMin->nCubes > p->nCubesMax )
+ {
+ pCover = Min_CoverCollect( p->pManMin, nSupp );
+ Min_CoverRecycle( p->pManMin, pCover );
+ return NULL;
+ }
+ // add the cube to storage
+ if ( fEsop )
+ Min_EsopAddCube( p->pManMin, pCube );
+ else
+ Min_SopAddCube( p->pManMin, pCube );
+ }
+
+ // minimize the cover
+ if ( fEsop )
+ Min_EsopMinimize( p->pManMin );
+ else
+ Min_SopMinimize( p->pManMin );
+ pCover = Min_CoverCollect( p->pManMin, nSupp );
+
+ // quit if the cover is too large
+ if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
+ {
+ Min_CoverRecycle( p->pManMin, pCover );
+ return NULL;
+ }
+ return pCover;
+}
+
+
+
+
+
+
+
+#if 0
+
+
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -581,7 +909,7 @@ int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pC
pCube->nLits++;
}
// add the cube to storage
- while ( Min_EsopAddCube( p->pManMin, pCube ) );
+ Min_EsopAddCube( p->pManMin, pCube );
}
return 1;
}
@@ -642,7 +970,7 @@ int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCov
if ( p->pManMin->nCubes >= p->nCubesMax )
return 0;
// add the cube to storage
- while ( Min_EsopAddCube( p->pManMin, pCube ) );
+ Min_EsopAddCube( p->pManMin, pCube );
}
}
if ( pCover1 )
@@ -665,7 +993,7 @@ int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCov
if ( p->pManMin->nCubes >= p->nCubesMax )
return 0;
// add the cube to storage
- while ( Min_EsopAddCube( p->pManMin, pCube ) );
+ Min_EsopAddCube( p->pManMin, pCube );
}
}
return 1;
@@ -688,7 +1016,7 @@ int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCove
}
-
+#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/opt/xyz/xyzInt.h b/src/opt/xyz/xyzInt.h
index 22950bfd..656612aa 100644
--- a/src/opt/xyz/xyzInt.h
+++ b/src/opt/xyz/xyzInt.h
@@ -81,10 +81,10 @@ static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uDa
/*=== xyzMinEsop.c ==========================================================*/
extern void Min_EsopMinimize( Min_Man_t * p );
-extern int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
+extern void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
/*=== xyzMinSop.c ==========================================================*/
extern void Min_SopMinimize( Min_Man_t * p );
-extern int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
+extern void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
/*=== xyzMinMan.c ==========================================================*/
extern Min_Man_t * Min_ManAlloc( int nVars );
extern void Min_ManClean( Min_Man_t * p, int nSupp );
@@ -92,8 +92,10 @@ extern void Min_ManFree( Min_Man_t * p );
/*=== xyzMinUtil.c ==========================================================*/
extern void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube );
extern void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover );
+extern void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p );
extern void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop );
extern void Min_CoverCheck( Min_Man_t * p );
+extern int Min_CubeCheck( Min_Cube_t * pCube );
extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize );
extern void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover );
extern int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover );
@@ -161,6 +163,7 @@ static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy )
Min_Cube_t * pCube;
pCube = Min_CubeAlloc( p );
memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords );
+ pCube->nLits = pCopy->nLits;
return pCube;
}
@@ -538,6 +541,24 @@ static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, M
}
}
+/**Function*************************************************************
+
+ Synopsis [Transforms the cube into the result of distance-1 merging.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Min_CubesTransformOr( Min_Cube_t * pCube, Min_Cube_t * pDist )
+{
+ int w;
+ for ( w = 0; w < (int)pCube->nWords; w++ )
+ pCube->uData[w] |= pDist->uData[w];
+}
+
/**Function*************************************************************
@@ -579,7 +600,7 @@ static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCove
/**Function*************************************************************
- Synopsis [Check if the cube is equal or dist1 or contained.]
+ Synopsis [Returns 1 if the given cube is contained in one of the cubes of the cover.]
Description []
@@ -588,42 +609,32 @@ static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCove
SeeAlso []
***********************************************************************/
-static inline int Min_CubeIsEqualOrSubsumed( Min_Man_t * p, Min_Cube_t * pNew )
+static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube )
{
- Min_Cube_t * pCube;
+ Min_Cube_t * pThis;
int i;
- // check identity
- Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube )
- if ( Min_CubesAreEqual( pCube, pNew ) )
+/*
+ // this cube cannot be equal to any cube
+ Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+ {
+ if ( Min_CubesAreEqual( pCube, pThis ) )
+ {
+ Min_CubeWrite( stdout, pCube );
+ assert( 0 );
+ }
+ }
+*/
+ // try to find a containing cube
+ for ( i = 0; i <= (int)pCube->nLits; i++ )
+ Min_CoverForEachCube( p->ppStore[i], pThis )
+ {
+ // skip the bubble
+ if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
return 1;
- // check containment
- for ( i = 0; i < (int)pNew->nLits; i++ )
- Min_CoverForEachCube( p->ppStore[i], pCube )
- if ( Min_CubeIsContained( pCube, pNew ) )
- return 1;
+ }
return 0;
}
-/**Function*************************************************************
-
- Synopsis [Check if the cube is equal or dist1 or contained.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Min_Cube_t * Min_CubeHasDistanceOne( Min_Man_t * p, Min_Cube_t * pNew )
-{
- Min_Cube_t * pCube;
- Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube )
- if ( Min_CubesDistOne( pCube, pNew, NULL ) )
- return pCube;
- return NULL;
-}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/xyz/xyzMinEsop.c b/src/opt/xyz/xyzMinEsop.c
index 114e28a6..839e2410 100644
--- a/src/opt/xyz/xyzMinEsop.c
+++ b/src/opt/xyz/xyzMinEsop.c
@@ -62,7 +62,11 @@ void Min_EsopMinimize( Min_Man_t * p )
Synopsis [Performs one round of rewriting using distance 2 cubes.]
- Description []
+ Description [The weakness of this procedure is that it tries each cube
+ with only one distance-2 cube. If this pair does not lead to improvement
+ the cube is inserted into the cover anyhow, and we try another pair.
+ A possible improvement would be to try this cube with all distance-2
+ cubes, until an improvement is found, or until all such cubes are tried.]
SideEffects []
@@ -162,8 +166,8 @@ void Min_EsopRewrite( Min_Man_t * p )
// add the cubes
nCubesOld = p->nCubes;
- while ( Min_EsopAddCube( p, pCube ) );
- while ( Min_EsopAddCube( p, pThis ) );
+ Min_EsopAddCube( p, pCube );
+ Min_EsopAddCube( p, pThis );
// check if the cubes were absorbed
if ( p->nCubes < nCubesOld + 2 )
continue;
@@ -191,8 +195,8 @@ void Min_EsopRewrite( Min_Man_t * p )
pThis->nLits += (v11 != 3);
// add them anyhow
- while ( Min_EsopAddCube( p, pCube ) );
- while ( Min_EsopAddCube( p, pThis ) );
+ Min_EsopAddCube( p, pCube );
+ Min_EsopAddCube( p, pThis );
}
// printf( "Pairs = %d ", nPairs );
}
@@ -201,8 +205,8 @@ void Min_EsopRewrite( Min_Man_t * p )
Synopsis [Adds the cube to storage.]
- Description [If the distance one cube is found, returns the transformed
- cube. If there is no distance one, adds the given cube to storage.
+ Description [Returns 0 if the cube is added or removed. Returns 1
+ if the cube is glued with some other cube and has to be added again.
Do not forget to clean the storage!]
SideEffects []
@@ -210,7 +214,7 @@ void Min_EsopRewrite( Min_Man_t * p )
SeeAlso []
***********************************************************************/
-int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+int Min_EsopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
{
Min_Cube_t * pThis, ** ppPrev;
// try to find the identical cube
@@ -270,6 +274,24 @@ int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
return 0;
}
+/**Function*************************************************************
+
+ Synopsis [Adds the cube to storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+{
+ assert( pCube != p->pBubble );
+ assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+ while ( Min_EsopAddCubeInt( p, pCube ) );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/xyz/xyzMinMan.c b/src/opt/xyz/xyzMinMan.c
index 423564c1..20314698 100644
--- a/src/opt/xyz/xyzMinMan.c
+++ b/src/opt/xyz/xyzMinMan.c
@@ -62,6 +62,7 @@ Min_Man_t * Min_ManAlloc( int nVars )
pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 );
pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 );
pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 );
+ Min_ManClean( pMan, nVars );
return pMan;
}
diff --git a/src/opt/xyz/xyzMinSop.c b/src/opt/xyz/xyzMinSop.c
index 1c5951fe..a5d57c66 100644
--- a/src/opt/xyz/xyzMinSop.c
+++ b/src/opt/xyz/xyzMinSop.c
@@ -52,10 +52,11 @@ void Min_SopMinimize( Min_Man_t * p )
nCubesOld = p->nCubes;
Min_SopRewrite( p );
nIter++;
+// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
}
while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
+// printf( "\n" );
-// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
}
/**Function*************************************************************
@@ -74,8 +75,17 @@ void Min_SopRewrite( Min_Man_t * p )
Min_Cube_t * pCube, ** ppPrev;
Min_Cube_t * pThis, ** ppPrevT;
Min_Cube_t * pTemp;
- int v00, v01, v10, v11, Var0, Var1, Index;
+ int v00, v01, v10, v11, Var0, Var1, Index, fCont0, fCont1, nCubesOld;
int nPairs = 0;
+/*
+ {
+ Min_Cube_t * pCover;
+ pCover = Min_CoverCollect( p, p->nVars );
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCover );
+ Min_CoverExpand( p, pCover );
+ }
+*/
// insert the bubble before the first cube
p->pBubble->pNext = p->ppStore[0];
@@ -127,7 +137,11 @@ void Min_SopRewrite( Min_Man_t * p )
continue;
}
nPairs++;
-
+/*
+printf( "\n" );
+Min_CubeWrite( stdout, pCube );
+Min_CubeWrite( stdout, pThis );
+*/
// remove the cubes, insert the bubble instead of pCube
*ppPrevT = pThis->pNext;
*ppPrev = p->pBubble;
@@ -135,6 +149,8 @@ void Min_SopRewrite( Min_Man_t * p )
p->pBubble->nLits = pCube->nLits;
p->nCubes -= 2;
+ assert( pCube != p->pBubble && pThis != p->pBubble );
+
// save the dist2 parameters
v00 = Min_CubeGetVar( pCube, Var0 );
@@ -145,22 +161,83 @@ void Min_SopRewrite( Min_Man_t * p )
assert( v00 != 3 || v01 != 3 );
assert( v10 != 3 || v11 != 3 );
- // skip the case when rewriting is impossible
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+ // consider the case when both cubes have non-empty literals
if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 )
+ {
+ assert( v00 == (v10 ^ 3) );
+ assert( v01 == (v11 ^ 3) );
+ // create the temporary cube equal to the first corner
+ Min_CubeXorVar( pCube, Var0, 3 );
+ // check if this cube is contained
+ fCont0 = Min_CoverContainsCube( p, pCube );
+ // create the temporary cube equal to the first corner
+ Min_CubeXorVar( pCube, Var0, 3 );
+ Min_CubeXorVar( pCube, Var1, 3 );
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+ // check if this cube is contained
+ fCont1 = Min_CoverContainsCube( p, pCube );
+ // undo the change
+ Min_CubeXorVar( pCube, Var1, 3 );
+
+ // check if the cubes can be overwritten
+ if ( fCont0 && fCont1 )
+ {
+ // one of the cubes can be recycled, the other expanded and added
+ Min_CubeRecycle( p, pThis );
+ // remove the literals
+ Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
+ Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+ pCube->nLits -= 2;
+ Min_SopAddCube( p, pCube );
+ }
+ else if ( fCont0 )
+ {
+ // expand both cubes and add them
+ Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
+ pCube->nLits--;
+ Min_SopAddCube( p, pCube );
+ Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
+ pThis->nLits--;
+ Min_SopAddCube( p, pThis );
+ }
+ else if ( fCont1 )
+ {
+ // expand both cubes and add them
+ Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+ pCube->nLits--;
+ Min_SopAddCube( p, pCube );
+ Min_CubeXorVar( pThis, Var0, v10 ^ 3 );
+ pThis->nLits--;
+ Min_SopAddCube( p, pThis );
+ }
+ else
+ {
+ Min_SopAddCube( p, pCube );
+ Min_SopAddCube( p, pThis );
+ }
+ // otherwise, no change is possible
continue;
+ }
// if one of them does not have DC lit, move it
if ( v00 != 3 && v01 != 3 )
{
+ assert( v10 == 3 || v11 == 3 );
pTemp = pCube; pCube = pThis; pThis = pTemp;
Index = v00; v00 = v10; v10 = Index;
Index = v01; v01 = v11; v11 = Index;
}
-//printf( "\n" );
-//Min_CubeWrite( stdout, pCube );
-//Min_CubeWrite( stdout, pThis );
-
// make sure the first cube has first var DC
if ( v00 != 3 )
{
@@ -174,13 +251,93 @@ void Min_SopRewrite( Min_Man_t * p )
if ( v00 == 3 && v11 == 3 )
{
assert( v01 != 3 && v10 != 3 );
- // try two reduced cubes
-
+ // try the remaining minterm
+ // create the temporary cube equal to the first corner
+ Min_CubeXorVar( pCube, Var0, v10 );
+ Min_CubeXorVar( pCube, Var1, 3 );
+ pCube->nLits++;
+ // check if this cube is contained
+ fCont0 = Min_CoverContainsCube( p, pCube );
+ // undo the cube transformations
+ Min_CubeXorVar( pCube, Var0, v10 );
+ Min_CubeXorVar( pCube, Var1, 3 );
+ pCube->nLits--;
+ // check the case when both are covered
+ if ( fCont0 )
+ {
+ // one of the cubes can be recycled, the other expanded and added
+ Min_CubeRecycle( p, pThis );
+ // remove the literals
+ Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+ pCube->nLits--;
+ Min_SopAddCube( p, pCube );
+ }
+ else
+ {
+ // try two reduced cubes
+ Min_CubeXorVar( pCube, Var0, v10 );
+ pCube->nLits++;
+ // remember the cubes
+ nCubesOld = p->nCubes;
+ Min_SopAddCube( p, pCube );
+ // check if the cube is absorbed
+ if ( p->nCubes < nCubesOld + 1 )
+ { // absorbed - add the second cube
+ Min_SopAddCube( p, pThis );
+ }
+ else
+ { // remove this cube, and try another one
+ assert( pCube == p->ppStore[pCube->nLits] );
+ p->ppStore[pCube->nLits] = pCube->pNext;
+ p->nCubes--;
+
+ // return the cube to the previous state
+ Min_CubeXorVar( pCube, Var0, v10 );
+ pCube->nLits--;
+
+ // generate another reduced cube
+ Min_CubeXorVar( pThis, Var1, v01 );
+ pThis->nLits++;
+
+ // add both cubes
+ Min_SopAddCube( p, pCube );
+ Min_SopAddCube( p, pThis );
+ }
+ }
}
else // the first cube has DC lit
{
assert( v01 != 3 && v10 != 3 && v11 != 3 );
- // try reduced and expanded cube
+ // try the remaining minterm
+ // create the temporary cube equal to the minterm
+ Min_CubeXorVar( pThis, Var0, 3 );
+ // check if this cube is contained
+ fCont0 = Min_CoverContainsCube( p, pThis );
+ // undo the cube transformations
+ Min_CubeXorVar( pThis, Var0, 3 );
+ // check the case when both are covered
+ if ( fCont0 )
+ {
+ // one of the cubes can be recycled, the other expanded and added
+ Min_CubeRecycle( p, pThis );
+ // remove the literals
+ Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
+ pCube->nLits--;
+ Min_SopAddCube( p, pCube );
+ }
+ else
+ {
+ // try reshaping the cubes
+ // reduce the first cube
+ Min_CubeXorVar( pCube, Var0, v10 );
+ pCube->nLits++;
+ // expand the second cube
+ Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
+ pThis->nLits--;
+ // add both cubes
+ Min_SopAddCube( p, pCube );
+ Min_SopAddCube( p, pThis );
+ }
}
}
// printf( "Pairs = %d ", nPairs );
@@ -188,26 +345,80 @@ void Min_SopRewrite( Min_Man_t * p )
/**Function*************************************************************
- Synopsis []
+ Synopsis [Adds cube to the SOP cover stored in the manager.]
- Description []
+ Description [Returns 0 if the cube is added or removed. Returns 1
+ if the cube is glued with some other cube and has to be added again.]
SideEffects []
SeeAlso []
***********************************************************************/
-int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+int Min_SopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
{
- return 1;
-}
-
+ Min_Cube_t * pThis, * pThis2, ** ppPrev;
+ int i;
+ // try to find the identical cube
+ Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
+ {
+ if ( Min_CubesAreEqual( pCube, pThis ) )
+ {
+ Min_CubeRecycle( p, pCube );
+ return 0;
+ }
+ }
+ // try to find a containing cube
+ for ( i = 0; i < (int)pCube->nLits; i++ )
+ Min_CoverForEachCube( p->ppStore[i], pThis )
+ {
+ if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
+ {
+ Min_CubeRecycle( p, pCube );
+ return 0;
+ }
+ }
+ // try to find distance one in the same bin
+ Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+ {
+ if ( Min_CubesDistOne( pCube, pThis, NULL ) )
+ {
+ *ppPrev = pThis->pNext;
+ Min_CubesTransformOr( pCube, pThis );
+ pCube->nLits--;
+ Min_CubeRecycle( p, pThis );
+ p->nCubes--;
+ return 1;
+ }
+ }
+ // clean the other cubes using this one
+ for ( i = pCube->nLits + 1; i <= (int)pCube->nVars; i++ )
+ {
+ ppPrev = &p->ppStore[i];
+ Min_CoverForEachCubeSafe( p->ppStore[i], pThis, pThis2 )
+ {
+ if ( pThis != p->pBubble && Min_CubeIsContained( pCube, pThis ) )
+ {
+ *ppPrev = pThis->pNext;
+ Min_CubeRecycle( p, pThis );
+ p->nCubes--;
+ }
+ else
+ ppPrev = &pThis->pNext;
+ }
+ }
+ // add the cube
+ pCube->pNext = p->ppStore[pCube->nLits];
+ p->ppStore[pCube->nLits] = pCube;
+ p->nCubes++;
+ return 0;
+}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Adds the cube to storage.]
Description []
@@ -216,27 +427,18 @@ int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
SeeAlso []
***********************************************************************/
-void Min_SopDist1Merge( Min_Man_t * p )
+void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
{
- Min_Cube_t * pCube, * pCube2, * pCubeNew;
- int i;
- for ( i = p->nVars; i >= 0; i-- )
- {
- Min_CoverForEachCube( p->ppStore[i], pCube )
- Min_CoverForEachCube( pCube->pNext, pCube2 )
- {
- assert( pCube->nLits == pCube2->nLits );
- if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
- continue;
- pCubeNew = Min_CubesXor( p, pCube, pCube2 );
- assert( pCubeNew->nLits == pCube->nLits - 1 );
- pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
- p->ppStore[pCubeNew->nLits] = pCubeNew;
- p->nCubes++;
- }
- }
+ assert( Min_CubeCheck( pCube ) );
+ assert( pCube != p->pBubble );
+ assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+ while ( Min_SopAddCubeInt( p, pCube ) );
}
+
+
+
+
/**Function*************************************************************
Synopsis []
@@ -286,6 +488,38 @@ void Min_SopContain( Min_Man_t * p )
SeeAlso []
***********************************************************************/
+void Min_SopDist1Merge( Min_Man_t * p )
+{
+ Min_Cube_t * pCube, * pCube2, * pCubeNew;
+ int i;
+ for ( i = p->nVars; i >= 0; i-- )
+ {
+ Min_CoverForEachCube( p->ppStore[i], pCube )
+ Min_CoverForEachCube( pCube->pNext, pCube2 )
+ {
+ assert( pCube->nLits == pCube2->nLits );
+ if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
+ continue;
+ pCubeNew = Min_CubesXor( p, pCube, pCube2 );
+ assert( pCubeNew->nLits == pCube->nLits - 1 );
+ pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
+ p->ppStore[pCubeNew->nLits] = pCubeNew;
+ p->nCubes++;
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp )
{
Vec_Int_t * vVars;
@@ -334,6 +568,46 @@ Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp )
return Min_CoverCollect( p, p->nVars );
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Min_SopCheck( Min_Man_t * p )
+{
+ Min_Cube_t * pCube, * pThis;
+ int i;
+
+ pCube = Min_CubeAlloc( p );
+ Min_CubeXorBit( pCube, 2*0+1 );
+ Min_CubeXorBit( pCube, 2*1+1 );
+ Min_CubeXorBit( pCube, 2*2+0 );
+ Min_CubeXorBit( pCube, 2*3+0 );
+ Min_CubeXorBit( pCube, 2*4+0 );
+ Min_CubeXorBit( pCube, 2*5+1 );
+ Min_CubeXorBit( pCube, 2*6+1 );
+ pCube->nLits = 7;
+
+// Min_CubeWrite( stdout, pCube );
+
+ // check that the cubes contain it
+ for ( i = 0; i <= p->nVars; i++ )
+ Min_CoverForEachCube( p->ppStore[i], pThis )
+ if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
+ {
+ Min_CubeRecycle( p, pCube );
+ return 1;
+ }
+ Min_CubeRecycle( p, pCube );
+ return 0;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/xyz/xyzMinUtil.c b/src/opt/xyz/xyzMinUtil.c
index 0aebb815..9ec5f83f 100644
--- a/src/opt/xyz/xyzMinUtil.c
+++ b/src/opt/xyz/xyzMinUtil.c
@@ -92,13 +92,44 @@ void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover )
SeeAlso []
***********************************************************************/
+void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p )
+{
+ Min_Cube_t * pCube;
+ int i;
+ for ( i = 0; i <= p->nVars; i++ )
+ {
+ Min_CoverForEachCube( p->ppStore[i], pCube )
+ {
+ printf( "%2d : ", i );
+ if ( pCube == p->pBubble )
+ {
+ printf( "Bubble\n" );
+ continue;
+ }
+ Min_CubeWrite( pFile, pCube );
+ }
+ }
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
{
char Buffer[1000];
Min_Cube_t * pCube;
FILE * pFile;
int i;
- sprintf( Buffer, "%s.esop", pName );
+ sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" );
for ( i = strlen(Buffer) - 1; i >= 0; i-- )
if ( Buffer[i] == '<' || Buffer[i] == '>' )
Buffer[i] = '_';
@@ -116,7 +147,7 @@ void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
/**Function*************************************************************
- Synopsis [Performs one round of rewriting using distance 2 cubes.]
+ Synopsis []
Description []
@@ -137,6 +168,26 @@ void Min_CoverCheck( Min_Man_t * p )
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Min_CubeCheck( Min_Cube_t * pCube )
+{
+ int i;
+ for ( i = 0; i < (int)pCube->nVars; i++ )
+ if ( Min_CubeGetVar( pCube, i ) == 0 )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Converts the cover from the sorted structure.]
Description []
@@ -158,6 +209,7 @@ Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize )
assert( i == (int)pCube->nLits );
*ppTail = pCube;
ppTail = &pCube->pNext;
+ assert( pCube->uData[0] ); // not a bubble
}
}
*ppTail = NULL;
diff --git a/src/opt/xyz/xyzTest.c b/src/opt/xyz/xyzTest.c
index 6c0a63f3..38580790 100644
--- a/src/opt/xyz/xyzTest.c
+++ b/src/opt/xyz/xyzTest.c
@@ -39,11 +39,377 @@
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk )
+Min_Cube_t * Abc_NodeDeriveCoverPro( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 )
{
- return NULL;
+ Min_Cube_t * pCover;
+ Min_Cube_t * pCube0, * pCube1, * pCube;
+ if ( pCover0 == NULL || pCover1 == NULL )
+ return NULL;
+ // clean storage
+ Min_ManClean( p, p->nVars );
+ // go through the cube pairs
+ Min_CoverForEachCube( pCover0, pCube0 )
+ Min_CoverForEachCube( pCover1, pCube1 )
+ {
+ if ( Min_CubesDisjoint( pCube0, pCube1 ) )
+ continue;
+ pCube = Min_CubesProduct( p, pCube0, pCube1 );
+ // add the cube to storage
+ Min_SopAddCube( p, pCube );
+ }
+ Min_SopMinimize( p );
+ pCover = Min_CoverCollect( p, p->nVars );
+ assert( p->nCubes == Min_CoverCountCubes(pCover) );
+ return pCover;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeDeriveCoverSum( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 )
+{
+ Min_Cube_t * pCover;
+ Min_Cube_t * pThis, * pCube;
+ if ( pCover0 == NULL || pCover1 == NULL )
+ return NULL;
+ // clean storage
+ Min_ManClean( p, p->nVars );
+ // add the cubes to storage
+ Min_CoverForEachCube( pCover0, pThis )
+ {
+ pCube = Min_CubeDup( p, pThis );
+ Min_SopAddCube( p, pCube );
+ }
+ Min_CoverForEachCube( pCover1, pThis )
+ {
+ pCube = Min_CubeDup( p, pThis );
+ Min_SopAddCube( p, pCube );
+ }
+ Min_SopMinimize( p );
+ pCover = Min_CoverCollect( p, p->nVars );
+ assert( p->nCubes == Min_CoverCountCubes(pCover) );
+ return pCover;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NodeDeriveSops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes )
+{
+ Min_Cube_t * pCov0[2], * pCov1[2];
+ Min_Cube_t * pCoverP, * pCoverN;
+ Abc_Obj_t * pObj;
+ int i, nCubes, fCompl0, fCompl1;
+
+ // set elementary vars
+ Vec_PtrForEachEntry( vSupp, pObj, i )
+ {
+ pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 );
+ pObj->pNext = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 1 );
+ }
+
+ // get the cover for each node in the array
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ // get the complements
+ fCompl0 = Abc_ObjFaninC0(pObj);
+ fCompl1 = Abc_ObjFaninC1(pObj);
+ // get the covers
+ pCov0[0] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy;
+ pCov0[1] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pNext;
+ pCov1[0] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy;
+ pCov1[1] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pNext;
+ // compute the covers
+ pCoverP = Abc_NodeDeriveCoverPro( p, pCov0[ fCompl0], pCov1[ fCompl1] );
+ pCoverN = Abc_NodeDeriveCoverSum( p, pCov0[!fCompl0], pCov1[!fCompl1] );
+ // set the covers
+ pObj->pCopy = (Abc_Obj_t *)pCoverP;
+ pObj->pNext = (Abc_Obj_t *)pCoverN;
+ }
+
+ nCubes = ABC_MIN( Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverP) );
+
+/*
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCoverP );
+printf( "\n\n" );
+Min_CoverWrite( stdout, pCoverN );
+*/
+
+// printf( "\n" );
+// Min_CoverWrite( stdout, pCoverP );
+
+// Min_CoverExpand( p, pCoverP );
+// Min_SopMinimize( p );
+// pCoverP = Min_CoverCollect( p, p->nVars );
+
+// printf( "\n" );
+// Min_CoverWrite( stdout, pCoverP );
+
+// nCubes = Min_CoverCountCubes(pCoverP);
+
+ // clean the copy fields
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ pObj->pCopy = pObj->pNext = NULL;
+ Vec_PtrForEachEntry( vSupp, pObj, i )
+ pObj->pCopy = pObj->pNext = NULL;
+
+// Min_CoverWriteFile( pCoverP, Abc_ObjName(pRoot), 0 );
+// printf( "\n" );
+// Min_CoverWrite( stdout, pCoverP );
+
+// printf( "\n" );
+// Min_CoverWrite( stdout, pCoverP );
+// printf( "\n" );
+// Min_CoverWrite( stdout, pCoverN );
+ return nCubes;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkTestSop( Abc_Ntk_t * pNtk )
+{
+ Min_Man_t * p;
+ Vec_Ptr_t * vSupp, * vNodes;
+ Abc_Obj_t * pObj;
+ int i, nCubes;
+ assert( Abc_NtkIsStrash(pNtk) );
+
+ Abc_NtkCleanCopy(pNtk);
+ Abc_NtkCleanNext(pNtk);
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ {
+ if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) )
+ {
+ printf( "%-20s : Trivial.\n", Abc_ObjName(pObj) );
+ continue;
+ }
+
+ vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+ vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+
+ printf( "%20s : Cone = %5d. Supp = %5d. ",
+ Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
+// if ( vSupp->nSize <= 128 )
+ {
+ p = Min_ManAlloc( vSupp->nSize );
+ nCubes = Abc_NodeDeriveSops( p, pObj, vSupp, vNodes );
+ printf( "Cubes = %5d. ", nCubes );
+ Min_ManFree( p );
+ }
+ printf( "\n" );
+
+
+ Vec_PtrFree( vNodes );
+ Vec_PtrFree( vSupp );
+ }
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Min_Cube_t * Abc_NodeDeriveCover( Min_Man_t * p, Min_Cube_t * pCov0, Min_Cube_t * pCov1, int fComp0, int fComp1 )
+{
+ Min_Cube_t * pCover0, * pCover1, * pCover;
+ Min_Cube_t * pCube0, * pCube1, * pCube;
+
+ // complement the first if needed
+ if ( !fComp0 )
+ pCover0 = pCov0;
+ else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
+ pCover0 = pCov0->pNext;
+ else
+ pCover0 = p->pOne0, p->pOne0->pNext = pCov0;
+
+ // complement the second if needed
+ if ( !fComp1 )
+ pCover1 = pCov1;
+ else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
+ pCover1 = pCov1->pNext;
+ else
+ pCover1 = p->pOne1, p->pOne1->pNext = pCov1;
+
+ if ( pCover0 == NULL || pCover1 == NULL )
+ return NULL;
+
+ // clean storage
+ Min_ManClean( p, p->nVars );
+ // go through the cube pairs
+ Min_CoverForEachCube( pCover0, pCube0 )
+ Min_CoverForEachCube( pCover1, pCube1 )
+ {
+ if ( Min_CubesDisjoint( pCube0, pCube1 ) )
+ continue;
+ pCube = Min_CubesProduct( p, pCube0, pCube1 );
+ // add the cube to storage
+ Min_EsopAddCube( p, pCube );
+ }
+
+ if ( p->nCubes > 10 )
+ {
+// printf( "(%d,", p->nCubes );
+ Min_EsopMinimize( p );
+// printf( "%d) ", p->nCubes );
+ }
+
+ pCover = Min_CoverCollect( p, p->nVars );
+ assert( p->nCubes == Min_CoverCountCubes(pCover) );
+
+// if ( p->nCubes > 1000 )
+// printf( "%d ", p->nCubes );
+ return pCover;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NodeDeriveEsops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes )
+{
+ Min_Cube_t * pCover, * pCube;
+ Abc_Obj_t * pObj;
+ int i;
+
+ // set elementary vars
+ Vec_PtrForEachEntry( vSupp, pObj, i )
+ pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 );
+
+ // get the cover for each node in the array
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ pCover = Abc_NodeDeriveCover( p,
+ (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy,
+ (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy,
+ Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+ pObj->pCopy = (Abc_Obj_t *)pCover;
+ if ( p->nCubes > 3000 )
+ return -1;
+ }
+
+ // add complement if needed
+ if ( Abc_ObjFaninC0(pRoot) )
+ {
+ if ( pCover && pCover->nLits == 0 ) // topmost one is the tautology cube
+ {
+ pCube = pCover;
+ pCover = pCover->pNext;
+ Min_CubeRecycle( p, pCube );
+ p->nCubes--;
+ }
+ else
+ {
+ pCube = Min_CubeAlloc( p );
+ pCube->pNext = pCover;
+ p->nCubes++;
+ }
+ }
+/*
+ Min_CoverExpand( p, pCover );
+ Min_EsopMinimize( p );
+ pCover = Min_CoverCollect( p, p->nVars );
+*/
+ // clean the copy fields
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ pObj->pCopy = NULL;
+ Vec_PtrForEachEntry( vSupp, pObj, i )
+ pObj->pCopy = NULL;
+
+// Min_CoverWriteFile( pCover, Abc_ObjName(pRoot), 1 );
+// Min_CoverWrite( stdout, pCover );
+ return p->nCubes;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkTestEsop( Abc_Ntk_t * pNtk )
+{
+ Min_Man_t * p;
+ Vec_Ptr_t * vSupp, * vNodes;
+ Abc_Obj_t * pObj;
+ int i, nCubes;
+ assert( Abc_NtkIsStrash(pNtk) );
+
+ Abc_NtkCleanCopy(pNtk);
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ {
+ if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) )
+ {
+ printf( "%-20s : Trivial.\n", Abc_ObjName(pObj) );
+ continue;
+ }
+
+ vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+ vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+
+ printf( "%20s : Cone = %5d. Supp = %5d. ",
+ Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
+// if ( vSupp->nSize <= 128 )
+ {
+ p = Min_ManAlloc( vSupp->nSize );
+ nCubes = Abc_NodeDeriveEsops( p, pObj, vSupp, vNodes );
+ printf( "Cubes = %5d. ", nCubes );
+ Min_ManFree( p );
+ }
+ printf( "\n" );
+
+
+ Vec_PtrFree( vNodes );
+ Vec_PtrFree( vSupp );
+ }
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index b82601c4..9618603c 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -52,8 +52,9 @@ static const lbool l_Undef = 0;
static const lbool l_True = 1;
static const lbool l_False = -1;
-static inline lit neg (lit l) { return l ^ 1; }
-static inline lit toLit (int v) { return v + v; }
+static inline lit neg (lit l) { return l ^ 1; }
+static inline lit toLit (int v) { return v + v; }
+static inline lit toLitCond (int v, int c) { return v + v + (int)(c != 0); }
//=================================================================================================
// Public interface:
diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c
index 97da413d..fab01368 100644
--- a/src/sat/fraig/fraigCanon.c
+++ b/src/sat/fraig/fraigCanon.c
@@ -68,7 +68,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
return p1;
return Fraig_Not(pMan->pConst1);
}
-
+/*
// check for less trivial cases
if ( Fraig_IsComplement(p1) )
{
@@ -125,7 +125,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
return Fraig_Not(pMan->pConst1);
}
}
-
+*/
// perform level-one structural hashing
if ( Fraig_HashTableLookupS( pMan, p1, p2, &pNodeNew ) ) // the node with these children is found
{
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index bc60e4e9..13f6b50b 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -41,6 +41,8 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i );
// The best way seems to be fanins followed by fanouts. Slight changes to this order
// leads to big degradation in quality.
+static int nMuxes;
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -105,7 +107,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
}
if ( p->fVerboseP )
{
- PRT( "Final miter proof time", clock() - clk );
+// PRT( "Final miter proof time", clock() - clk );
}
}
@@ -195,6 +197,8 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
}
*/
+ nMuxes = 0;
+
// get the logic cone
clk = clock();
@@ -202,6 +206,9 @@ clk = clock();
// Fraig_PrepareCones( p, pOld, pNew );
p->timeTrav += clock() - clk;
+// printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) );
+// PRT( "Time", clock() - clk );
+
if ( fVerbose )
printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
@@ -226,6 +233,8 @@ clk = clock();
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
p->timeSat += clock() - clk;
+Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
+
if ( RetValue1 == MSAT_FALSE )
{
//p->time1 += clock() - clk;
@@ -284,6 +293,7 @@ p->time3 += clock() - clk;
clk = clock();
RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
p->timeSat += clock() - clk;
+
if ( RetValue1 == MSAT_FALSE )
{
//p->time1 += clock() - clk;
@@ -552,6 +562,7 @@ void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t *
Fraig_PrepareCones_rec( pMan, pNew );
Fraig_PrepareCones_rec( pMan, pOld );
+
/*
nVars = Msat_IntVecReadSize( pMan->vVarsInt );
pVars = Msat_IntVecReadArray( pMan->vVarsInt );
@@ -715,6 +726,8 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t
Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) );
Fraig_SupergateAddClausesMux( pMan, pNode );
// Fraig_DetectFanoutFreeConeMux( pMan, pNode );
+
+ nMuxes++;
}
else
{
@@ -1057,6 +1070,12 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode )
// t + e + f'
// t' + e' + f
+ if ( VarT == VarE )
+ {
+// assert( fCompT == !fCompE );
+ return;
+ }
+
Msat_IntVecClear( p->vProj );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) );
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) );
@@ -1069,6 +1088,7 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode )
Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) );
RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
assert( RetValue );
+
}
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 37e0bbeb..40028784 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -87,6 +87,7 @@ extern void Msat_SolverPrintClauses( Msat_Solver_t * p );
extern void Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName );
// access to the solver internal data
extern int Msat_SolverReadVarNum( Msat_Solver_t * p );
+extern int Msat_SolverReadClauseNum( Msat_Solver_t * p );
extern int Msat_SolverReadVarAllocNum( Msat_Solver_t * p );
extern int * Msat_SolverReadAssignsArray( Msat_Solver_t * p );
extern int * Msat_SolverReadModelArray( Msat_Solver_t * p );
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
index f944ed81..62b9ecad 100644
--- a/src/sat/msat/msatClause.c
+++ b/src/sat/msat/msatClause.c
@@ -82,6 +82,10 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
// nSeenId - 1 stands for negative
// nSeenId stands for positive
// Remove false literals
+
+ // there is a bug here!!!!
+ // when the same var in opposite polarities is given, it drops one polarity!!!
+
for ( i = j = 0; i < nLits; i++ ) {
// get the corresponding variable
Var = MSAT_LIT2VAR(pLits[i]);
@@ -190,6 +194,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
{
Msat_SolverVarBumpActivity( p, pLits[i] );
// Msat_SolverVarBumpActivity( p, pLits[i] );
+ p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++;
}
}
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index ef2375a7..3dfe2109 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -151,6 +151,7 @@ struct Msat_Solver_t_
int nSeenId; // the id of current seeing
Msat_IntVec_t * vReason; // the temporary array of literals
Msat_IntVec_t * vTemp; // the temporary array of literals
+ int * pFreq; // the number of times each var participated in conflicts
// the memory manager
Msat_MmStep_t * pMem;
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index dd3a5a43..4a721487 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -42,6 +42,7 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
***********************************************************************/
int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; }
+int Msat_SolverReadClauseNum( Msat_Solver_t * p ) { return p->nClauses; }
int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc;}
int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); }
int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; }
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index ed228b33..5f13694b 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -140,6 +140,9 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
int64 nConflictsOld = p->Stats.nConflicts;
int64 nDecisionsOld = p->Stats.nDecisions;
+ p->pFreq = ALLOC( int, p->nVarsAlloc );
+ memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
+
if ( vAssumps )
{
int * pAssumps, nAssumps, i;
@@ -181,6 +184,23 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
}
Msat_SolverCancelUntil( p, 0 );
p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
+/*
+ PRT( "True solver runtime", clock() - timeStart );
+ // print the statistics
+ {
+ int i, Counter = 0;
+ for ( i = 0; i < p->nVars; i++ )
+ if ( p->pFreq[i] > 0 )
+ {
+ printf( "%d ", p->pFreq[i] );
+ Counter++;
+ }
+ if ( Counter )
+ printf( "\n" );
+ printf( "Total = %d. Used = %d. Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
+ PRT( "Time", clock() - timeStart );
+ }
+*/
return Status;
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 03:16:28 +0000