summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satProof.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bsat/satProof.c')
-rw-r--r--src/sat/bsat/satProof.c11
1 files changed, 6 insertions, 5 deletions
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 ///