diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/aig/aig/module.make | 1 | ||||
| -rw-r--r-- | src/sat/bsat/satProof.c | 11 |
3 files changed, 6 insertions, 10 deletions
@@ -3107,10 +3107,6 @@ SOURCE=.\src\aig\aig\aigPartSat.c # End Source File # Begin Source File -SOURCE=.\src\aig\aig\aigRepar.c -# End Source File -# Begin Source File - SOURCE=.\src\aig\aig\aigRepr.c # End Source File # Begin Source File diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make index aaf5bf6d..c291433f 100644 --- a/src/aig/aig/module.make +++ b/src/aig/aig/module.make @@ -17,7 +17,6 @@ SRC += src/aig/aig/aigCheck.c \ src/aig/aig/aigPart.c \ src/aig/aig/aigPartReg.c \ src/aig/aig/aigPartSat.c \ - src/aig/aig/aigRepar.c \ src/aig/aig/aigRepr.c \ src/aig/aig/aigRet.c \ src/aig/aig/aigRetF.c \ diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index a669d2be..680b1996 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -71,11 +71,12 @@ void Proof_ClauseSetEnts( Vec_Set_t* p, int h, int nEnts ) { Proof_Node // iterating through fanins of a proof node #define Proof_NodeForeachFanin( pProof, pNode, pFanin, i ) \ for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)), 1); i++ ) -//#define Proof_NodeForeachLeaf( pClauses, pNode, pLeaf, i ) \ -// for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ ) -//#define Proof_NodeForeachFaninLeaf( pProof, pClauses, pNode, pFanin, i ) \ -// for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)); i++ ) - +/* +#define Proof_NodeForeachLeaf( pClauses, pNode, pLeaf, i ) \ + for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ ) +#define Proof_NodeForeachFaninLeaf( pProof, pClauses, pNode, pFanin, i ) \ + for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)); i++ ) +*/ //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// |