diff options
Diffstat (limited to 'src/sat/bsat/satProof.c')
| -rw-r--r-- | src/sat/bsat/satProof.c | 517 |
1 files changed, 299 insertions, 218 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 5b3901a1..e2f907bb 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "satSolver.h" +#include "satSolver2.h" #include "vec.h" #include "aig.h" @@ -33,30 +33,41 @@ ABC_NAMESPACE_IMPL_START Label is initialized to 0. Root clauses are 1-based. They are marked by prepending bit 1; */ +/* + +typedef struct satset_t satset; +struct satset_t +{ + unsigned learnt : 1; + unsigned mark : 1; + unsigned partA : 1; + unsigned nEnts : 29; + int Id; + lit pEnts[0]; +}; + +#define satset_foreach_entry( p, c, h, s ) \ + for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) ) +*/ //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -typedef struct Sat_Set_t_ Sat_Set_t; -struct Sat_Set_t_ -{ - int nEnts; - int Label; - int pEnts[0]; -}; +static inline satset* Proof_NodeRead (Vec_Int_t* p, cla h ) { return satset_read( (veci*)p, h ); } +static inline cla Proof_NodeHandle (Vec_Int_t* p, satset* c) { return satset_handle( (veci*)p, c ); } +static inline int Proof_NodeCheck (Vec_Int_t* p, satset* c) { return satset_check( (veci*)p, c ); } +static inline int Proof_NodeSize (int nEnts) { return sizeof(satset)/4 + nEnts; } -static inline int Sat_SetCheck( Vec_Int_t * p, Sat_Set_t * pNode ) { return (int *)pNode > Vec_IntArray(p) && (int *)pNode < Vec_IntLimit(p); } -static inline int Sat_SetId( Vec_Int_t * p, Sat_Set_t * pNode ) { return (int *)pNode - Vec_IntArray(p); } -static inline Sat_Set_t * Sat_SetFromId( Vec_Int_t * p, int i ) { return (Sat_Set_t *)(Vec_IntArray(p) + i); } -static inline int Sat_SetSize( Sat_Set_t * pNode ) { return pNode->nEnts + 2; } +#define Proof_ForeachNode( p, pNode, hNode ) \ + satset_foreach_entry( ((veci*)p), pNode, hNode, 1 ) +#define Proof_ForeachNodeVec( pVec, p, pNode, i ) \ + for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ ) +#define Proof_NodeForeachFanin( p, pNode, pFanin, i ) \ + for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = ((pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 1))), 1); i++ ) +#define Proof_NodeForeachFanin2( p, pNode, pFanin, iFanin, i ) \ + for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = ((pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 1))), ((iFanin) = ((pNode->pEnts[i] & 1) ? pNode->pEnts[i] >> 1 : 0)), 1); i++ ) -#define Sat_PoolForEachSet( p, pNode, i ) \ - for ( i = 1; (i < Vec_IntSize(p)) && ((pNode) = Sat_SetFromId(p, Vec_IntEntry(p,i))); i += Sat_SetSize(pNode) ) -#define Sat_SetForEachSet( p, pSet, pNode, i ) \ - for ( i = 0; (i < pSet->nEnts) && (((pNode) = ((pSet->pEnts[i] & 1) ? NULL : Sat_SetFromId(p, pSet->pEnts[i]))), 1); i++ ) -#define Sat_VecForEachSet( pVec, p, pNode, i ) \ - for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Sat_SetFromId(p, Vec_IntEntry(pVec,i))); i++ ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -64,7 +75,7 @@ static inline int Sat_SetSize( Sat_Set_t * pNode ) { re /**Function************************************************************* - Synopsis [Recursively visits useful proof nodes.] + Synopsis [Collects all resolution nodes belonging to the proof.] Description [] @@ -73,48 +84,20 @@ static inline int Sat_SetSize( Sat_Set_t * pNode ) { re SeeAlso [] ***********************************************************************/ -int Sat_ProofReduceOne( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize, Vec_Int_t * vStack ) +Vec_Int_t * Proof_CollectAll( Vec_Int_t * p ) { - Sat_Set_t * pNext; - int i, NodeId; - if ( pNode->Label ) - return pNode->Label; - // start with node - pNode->Label = 1; - Vec_IntPush( vStack, Sat_SetId(p, pNode) ); - // perform DFS search - while ( Vec_IntSize(vStack) ) - { - NodeId = Vec_IntPop( vStack ); - if ( NodeId & 1 ) // extrated second time - { - pNode = Sat_SetFromId( p, NodeId ^ 1 ); - pNode->Label = *pnSize; - *pnSize += Sat_SetSize(pNode); - // update fanins - Sat_SetForEachSet( p, pNode, pNext, i ) - if ( pNext ) - pNode->pEnts[i] = pNext->Label; - continue; - } - // extracted first time - // add second time - Vec_IntPush( vStack, NodeId ^ 1 ); - // add its anticedents - pNode = Sat_SetFromId( p, NodeId ); - Sat_SetForEachSet( p, pNode, pNext, i ) - if ( pNext && !pNext->Label ) - { - pNext->Label = 1; - Vec_IntPush( vStack, Sat_SetId(p, pNode) ); // add first time - } - } - return pNode->Label; + Vec_Int_t * vUsed; + satset * pNode; + int hNode; + vUsed = Vec_IntAlloc( 1000 ); + Proof_ForeachNode( p, pNode, hNode ) + Vec_IntPush( vUsed, hNode ); + return vUsed; } /**Function************************************************************* - Synopsis [Recursively visits useful proof nodes.] + Synopsis [Cleans collected resultion nodes belonging to the proof.] Description [] @@ -123,63 +106,55 @@ int Sat_ProofReduceOne( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize, Vec_Int_ SeeAlso [] ***********************************************************************/ -/* -int Sat_ProofReduce_rec( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize ) +void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed ) { - int * pBeg; - assert( Sat_SetCheck(p, pNode) ); - if ( pNode->Label ) - return pNode->Label; - for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ ) - if ( !(*pBeg & 1) ) - *pBeg = Sat_ProofReduce_rec( p, Sat_SetFromId(p, *pBeg), pnSize ); - pNode->Label = *pnSize; - *pnSize += Sat_SetSize(pNode); - return pNode->Label; + satset * pNode; + int hNode; + Proof_ForeachNodeVec( vUsed, vProof, pNode, hNode ) + pNode->Id = 0; } -*/ /**Function************************************************************* - Synopsis [Reduces the proof to contain only roots and their children.] + Synopsis [Recursively visits useful proof nodes.] - Description [The result is updated proof and updated roots.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots ) +void Proof_CollectUsedInt( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack ) { - int i, nSize = 1; - int * pBeg, * pEnd, * pNew; - Vec_Int_t * vStack; - Sat_Set_t * pNode; - // mark used nodes - vStack = Vec_IntAlloc( 1000 ); - Sat_VecForEachSet( vRoots, p, pNode, i ) - vRoots->pArray[i] = Sat_ProofReduceOne( p, pNode, &nSize, vStack ); - Vec_IntFree( vStack ); - // compact proof - pNew = Vec_IntArray(p) + 1; - Sat_PoolForEachSet( p, pNode, i ) + satset * pNext; + int i, hNode; + if ( pNode->Id ) + return; + // start with node + pNode->Id = 1; + Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) << 1 ); + // perform DFS search + while ( Vec_IntSize(vStack) ) { - if ( !pNode->Label ) + hNode = Vec_IntPop( vStack ); + if ( hNode & 1 ) // extrated second time + { + Vec_IntPush( vUsed, hNode >> 1 ); continue; - assert( pNew - Vec_IntArray(p) == pNode->Label ); - pNode->Label = 0; - pBeg = (int *)pNode; - pEnd = pBeg + Sat_SetSize(pNode); - while ( pBeg < pEnd ) - *pNew++ = *pBeg++; + } + // extracted first time + Vec_IntPush( vStack, hNode ^ 1 ); // add second time + // add its anticedents ; + pNode = Proof_NodeRead( p, hNode >> 1 ); + Proof_NodeForeachFanin( p, pNode, pNext, i ) + if ( pNext && !pNext->Id ) + { + pNext->Id = 1; + Vec_IntPush( vStack, Proof_NodeHandle(p, pNext) << 1 ); // add first time + } } - // report the result - printf( "The proof was reduced from %d to %d (by %6.2f %%)\n", - Vec_IntSize(p), nSize, 100.0 * (Vec_IntSize(p) - nSize) / Vec_IntSize(p) ); - assert( pNew - Vec_IntArray(p) == nSize ); - Vec_IntShrink( p, nSize ); -} +} /**Function************************************************************* @@ -192,80 +167,51 @@ void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots ) SeeAlso [] ***********************************************************************/ -void Sat_ProofLabel( Vec_Int_t * p, Sat_Set_t * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack ) +void Proof_CollectUsedRec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed ) { - Sat_Set_t * pNext; - int i, NodeId; - if ( pNode->Label ) + satset * pNext; + int i; + if ( pNode->Id ) return; - // start with node - pNode->Label = 1; - Vec_IntPush( vStack, Sat_SetId(p, pNode) ); - // perform DFS search - while ( Vec_IntSize(vStack) ) - { - NodeId = Vec_IntPop( vStack ); - if ( NodeId & 1 ) // extrated second time - { - Vec_IntPush( vUsed, NodeId ^ 1 ); - continue; - } - // extracted first time - // add second time - Vec_IntPush( vStack, NodeId ^ 1 ); - // add its anticedents - pNode = Sat_SetFromId( p, NodeId ); - Sat_SetForEachSet( p, pNode, pNext, i ) - if ( pNext && !pNext->Label ) - { - pNext->Label = 1; - Vec_IntPush( vStack, Sat_SetId(p, pNode) ); // add first time - } - } + pNode->Id = 1; + Proof_NodeForeachFanin( p, pNode, pNext, i ) + if ( pNext && !pNext->Id ) + Proof_CollectUsedRec( p, pNext, vUsed ); + Vec_IntPush( vUsed, Proof_NodeHandle(p, pNode) ); } /**Function************************************************************* - Synopsis [Computes UNSAT core.] + Synopsis [Recursively visits useful proof nodes.] - Description [The result is the array of root clause indexes.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -Vec_Int_t * Sat_ProofCore( Vec_Int_t * p, int nRoots, int * pBeg, int * pEnd ) +Vec_Int_t * Proof_CollectUsed( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot ) { - unsigned * pSeen; - Vec_Int_t * vCore, * vUsed, * vStack; - Sat_Set_t * pNode; - int i; - // collect visited clauses + Vec_Int_t * vUsed, * vStack; + assert( (hRoot > 0) ^ (vRoots != NULL) ); vUsed = Vec_IntAlloc( 1000 ); vStack = Vec_IntAlloc( 1000 ); - while ( pBeg < pEnd ) - Sat_ProofLabel( p, Sat_SetFromId(p, *pBeg++), vUsed, vStack ); - Vec_IntFree( vStack ); - // find the core - vCore = Vec_IntAlloc( 1000 ); - pSeen = ABC_CALLOC( unsigned, Aig_BitWordNum(nRoots) ); - Sat_VecForEachSet( vUsed, p, pNode, i ) + if ( hRoot ) +// Proof_CollectUsedInt( vProof, Proof_NodeRead(vProof, hRoot), vUsed, vStack ); + Proof_CollectUsedRec( vProof, Proof_NodeRead(vProof, hRoot), vUsed ); + else { - pNode->Label = 0; - for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ ) - if ( (*pBeg & 1) && !Aig_InfoHasBit(pBeg, *pBeg>>1) ) - { - Aig_InfoSetBit( pBeg, *pBeg>>1 ); - Vec_IntPush( vCore, (*pBeg>>1)-1 ); - } + satset * pNode; + int i; + Proof_ForeachNodeVec( vRoots, vProof, pNode, i ) +// Proof_CollectUsedInt( vProof, pNode, vUsed, vStack ); + Proof_CollectUsedRec( vProof, pNode, vUsed ); } - Vec_IntFree( vUsed ); - ABC_FREE( pSeen ); - return vCore; + Vec_IntFree( vStack ); + return vUsed; } - - + /**Function************************************************************* Synopsis [Performs one resultion step.] @@ -277,12 +223,14 @@ Vec_Int_t * Sat_ProofCore( Vec_Int_t * p, int nRoots, int * pBeg, int * pEnd ) SeeAlso [] ***********************************************************************/ -Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) +satset * Proof_ResolveOne( Vec_Int_t * p, satset * c1, satset * c2 ) { + satset * c; int i, k, Id, Var = -1, Count = 0; + // find resolution variable - for ( i = 0; i < c1->nEnts; i++ ) - for ( k = 0; k < c2->nEnts; k++ ) + for ( i = 0; i < (int)c1->nEnts; i++ ) + for ( k = 0; k < (int)c2->nEnts; k++ ) if ( (c1->pEnts[i] ^ c2->pEnts[k]) == 1 ) { Var = (c1->pEnts[i] >> 1); @@ -302,7 +250,7 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) Id = Vec_IntSize( p ); Vec_IntPush( p, 0 ); // placeholder Vec_IntPush( p, 0 ); - for ( i = 0; i < c1->nEnts; i++ ) + for ( i = 0; i < (int)c1->nEnts; i++ ) { if ( (c1->pEnts[i] >> 1) == Var ) continue; @@ -312,7 +260,7 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) if ( k == Vec_IntSize(p) ) Vec_IntPush( p, c1->pEnts[i] ); } - for ( i = 0; i < c2->nEnts; i++ ) + for ( i = 0; i < (int)c2->nEnts; i++ ) { if ( (c2->pEnts[i] >> 1) == Var ) continue; @@ -322,8 +270,9 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) if ( k == Vec_IntSize(p) ) Vec_IntPush( p, c2->pEnts[i] ); } - Vec_IntWriteEntry( p, Id, Vec_IntSize(p) - Id - 2 ); - return Sat_SetFromId( p, Id ); + c = Proof_NodeRead( p, Id ); + c->nEnts = Vec_IntSize(p) - Id - 2; + return c; } /**Function************************************************************* @@ -337,13 +286,15 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 ) SeeAlso [] ***********************************************************************/ -Sat_Set_t * Sat_ProofCheckGetOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt ) +satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt ) { - Sat_Set_t * pAnt; + satset * pAnt; if ( iAnt & 1 ) - return Sat_SetFromId( vClauses, iAnt >> 1 ); - pAnt = Sat_SetFromId( vProof, iAnt ); - return Sat_SetFromId( vResolves, pAnt->Label ); + return Proof_NodeRead( vClauses, iAnt >> 1 ); + assert( iAnt > 0 ); + pAnt = Proof_NodeRead( vProof, iAnt >> 1 ); + assert( pAnt->Id > 0 ); + return Proof_NodeRead( vResolves, pAnt->Id ); } /**Function************************************************************* @@ -357,117 +308,247 @@ Sat_Set_t * Sat_ProofCheckGetOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_ SeeAlso [] ***********************************************************************/ -void Sat_ProofCheck( Vec_Int_t * vClauses, Vec_Int_t * vProof, int iRoot ) +void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) { - Vec_Int_t * vOrigs, * vStack, * vUsed, * vResolves; - Sat_Set_t * pSet, * pSet0, * pSet1; - int i, k; - // collect original clauses - vOrigs = Vec_IntAlloc( 1000 ); - Vec_IntPush( vOrigs, -1 ); - Sat_PoolForEachSet( vClauses, pSet, i ) - Vec_IntPush( vOrigs, Sat_SetId(vClauses, pSet) ); + Vec_Int_t * vUsed, * vResolves; + satset * pSet, * pSet0, * pSet1; + int i, k, Counter = 0; // collect visited clauses - vUsed = Vec_IntAlloc( 1000 ); - vStack = Vec_IntAlloc( 1000 ); - Sat_ProofLabel( vProof, Sat_SetFromId(vProof, iRoot), vUsed, vStack ); - Vec_IntFree( vStack ); + vUsed = Proof_CollectUsed( vProof, NULL, hRoot ); + Proof_CleanCollected( vProof, vUsed ); // perform resolution steps vResolves = Vec_IntAlloc( 1000 ); Vec_IntPush( vResolves, -1 ); - Sat_VecForEachSet( vUsed, vProof, pSet, i ) + Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) { - pSet0 = Sat_ProofCheckGetOne( vOrigs, vProof, vResolves, pSet->pEnts[0] ); - for ( k = 1; k < pSet->nEnts; k++ ) + pSet0 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); + for ( k = 1; k < (int)pSet->nEnts; k++ ) { - pSet1 = Sat_ProofCheckGetOne( vOrigs, vProof, vResolves, pSet->pEnts[k] ); - pSet0 = Sat_ProofResolve( vResolves, pSet0, pSet1 ); + pSet1 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); + pSet0 = Proof_ResolveOne( vResolves, pSet0, pSet1 ); } - pSet->Label = Sat_SetId( vResolves, pSet0 ); + pSet->Id = Proof_NodeHandle( vResolves, pSet0 ); + Counter++; } // clean the proof - Sat_VecForEachSet( vUsed, vProof, pSet, i ) - pSet->Label = 0; + Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) + pSet->Id = 0; // compare the final clause if ( pSet0->nEnts > 0 ) printf( "Cound not derive the empty clause\n" ); Vec_IntFree( vResolves ); Vec_IntFree( vUsed ); - Vec_IntFree( vOrigs ); } + + + /**Function************************************************************* - Synopsis [Creates variable map.] + Synopsis [Recursively visits useful proof nodes.] - Description [1=A, 2=B, neg=global] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -void Sat_ProofVarMapCheck( Vec_Int_t * vClauses, Vec_Int_t * vVarMap ) +int Sat_ProofReduceOne( Vec_Int_t * p, satset * pNode, int * pnSize, Vec_Int_t * vStack ) { - Sat_Set_t * pSet; - int i, k, fSeeA, fSeeB; - // make sure all clauses are either A or B - Sat_PoolForEachSet( vClauses, pSet, i ) + satset * pNext; + int i, NodeId; + if ( pNode->Id ) + return pNode->Id; + // start with node + pNode->Id = 1; + Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) ); + // perform DFS search + while ( Vec_IntSize(vStack) ) { - fSeeA = fSeeB = 0; - for ( k = 0; k < pSet->nEnts; k++ ) + NodeId = Vec_IntPop( vStack ); + if ( NodeId & 1 ) // extrated second time { - fSeeA += (Vec_IntEntry(vVarMap, pSet->pEnts[k]) == 1); - fSeeB += (Vec_IntEntry(vVarMap, pSet->pEnts[k]) == 2); + pNode = Proof_NodeRead( p, NodeId ^ 1 ); + pNode->Id = *pnSize; + *pnSize += Proof_NodeSize(pNode->nEnts); + // update fanins + Proof_NodeForeachFanin( p, pNode, pNext, i ) + if ( pNext ) + pNode->pEnts[i] = pNext->Id; + continue; } - if ( fSeeA && fSeeB ) - printf( "VarMap error!\n" ); + // extracted first time + // add second time + Vec_IntPush( vStack, NodeId ^ 1 ); + // add its anticedents + pNode = Proof_NodeRead( p, NodeId ); + Proof_NodeForeachFanin( p, pNode, pNext, i ) + if ( pNext && !pNext->Id ) + { + pNext->Id = 1; + Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) ); // add first time + } + } + return pNode->Id; +} + +/**Function************************************************************* + + Synopsis [Reduces the proof to contain only roots and their children.] + + Description [The result is updated proof and updated roots.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots ) +{ + int i, nSize = 1; + int * pBeg, * pEnd, * pNew; + Vec_Int_t * vStack; + satset * pNode; + // mark used nodes + vStack = Vec_IntAlloc( 1000 ); + Proof_ForeachNodeVec( vRoots, p, pNode, i ) + vRoots->pArray[i] = Sat_ProofReduceOne( p, pNode, &nSize, vStack ); + Vec_IntFree( vStack ); + // compact proof + pNew = Vec_IntArray(p) + 1; + Proof_ForeachNode( p, pNode, i ) + { + if ( !pNode->Id ) + continue; + assert( pNew - Vec_IntArray(p) == pNode->Id ); + pNode->Id = 0; + pBeg = (int *)pNode; + pEnd = pBeg + Proof_NodeSize(pNode->nEnts); + while ( pBeg < pEnd ) + *pNew++ = *pBeg++; + } + // report the result + printf( "The proof was reduced from %d to %d (by %6.2f %%)\n", + Vec_IntSize(p), nSize, 100.0 * (Vec_IntSize(p) - nSize) / Vec_IntSize(p) ); + assert( pNew - Vec_IntArray(p) == nSize ); + Vec_IntShrink( p, nSize ); +} + +/**Function************************************************************* + + Synopsis [Computes UNSAT core.] + + Description [The result is the array of root clause indexes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, int nRoots, Vec_Int_t * vRoots ) +{ + unsigned * pSeen; + Vec_Int_t * vCore, * vUsed; + satset * pNode; + int i, * pBeg; + // collect visited clauses + vUsed = Proof_CollectUsed( vProof, vRoots, 0 ); + // find the core + vCore = Vec_IntAlloc( 1000 ); + pSeen = ABC_CALLOC( unsigned, Aig_BitWordNum(nRoots) ); + Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) + { + pNode->Id = 0; + for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ ) + if ( (*pBeg & 1) && !Aig_InfoHasBit(pBeg, *pBeg>>1) ) + { + Aig_InfoSetBit( pBeg, *pBeg>>1 ); + Vec_IntPush( vCore, (*pBeg>>1)-1 ); + } } + Vec_IntFree( vUsed ); + ABC_FREE( pSeen ); + return vCore; } /**Function************************************************************* Synopsis [Computes interpolant of the proof.] - Description [Assuming that res vars are recorded, too...] + Description [Aassuming that global vars and A-clauses are marked.] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vProof, int iRoot, Vec_Int_t * vClauses, Vec_Int_t * vVarMap ) +Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot, Vec_Int_t * vGlobVars ) { - Vec_Int_t * vOrigs, * vUsed, * vStack; + Vec_Int_t * vUsed; Aig_Man_t * pAig; - Sat_Set_t * pSet; int i; - Sat_ProofVarMapCheck( vClauses, vVarMap ); - - // collect original clauses - vOrigs = Vec_IntAlloc( 1000 ); - Vec_IntPush( vOrigs, -1 ); - Sat_PoolForEachSet( vClauses, pSet, i ) - Vec_IntPush( vOrigs, Sat_SetId(vClauses, pSet) ); - // collect visited clauses - vUsed = Vec_IntAlloc( 1000 ); - vStack = Vec_IntAlloc( 1000 ); - Sat_ProofLabel( vProof, Sat_SetFromId(vProof, iRoot), vUsed, vStack ); - Vec_IntFree( vStack ); + vUsed = Proof_CollectUsed( vProof, NULL, hRoot ); // start the AIG pAig = Aig_ManStart( 10000 ); pAig->pName = Aig_UtilStrsav( "interpol" ); - for ( i = 0; i < Vec_IntSize(vVarMap); i++ ) - if ( Vec_IntEntry(vVarMap, i) < 0 ) - Aig_ObjCreatePi( pAig ); + for ( i = 0; i < Vec_IntSize(vGlobVars); i++ ) + Aig_ObjCreatePi( pAig ); return pAig; } +/* + Sat_ProofTest( + &s->clauses, // clauses + &s->proof_clas, // proof clauses + &s->proof_vars, // proof variables + NULL, // proof roots + veci_begin(&s->claProofs)[clause_read(s, s->iLearntLast)->Id)], // one root + &s->glob_vars ); // global variables (for interpolation) +*/ + +/**Function************************************************************* + + Synopsis [Computes interpolant of the proof.] + + Description [Aassuming that global vars and A-clauses are marked.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, int hRoot, veci * pGlobVars ) +{ + Vec_Int_t * vClauses = (Vec_Int_t *)pClauses; + Vec_Int_t * vProof = (Vec_Int_t *)pProof; + Vec_Int_t * vVars = (Vec_Int_t *)pVars; + Vec_Int_t * vRoots = (Vec_Int_t *)pRoots; + Vec_Int_t * vGlobVars = (Vec_Int_t *)pGlobVars; + Vec_Int_t * vUsed; +// int i, Entry; + + // collect visited clauses + vUsed = Proof_CollectUsed( vProof, NULL, hRoot ); + Proof_CleanCollected( vProof, vUsed ); +// Vec_IntForEachEntry( vUsed, Entry, i ) +// printf( "%d ", Entry ); +// printf( "\n" ); + + printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) ); + Vec_IntFree( vUsed ); + vUsed = Proof_CollectAll( vProof ); + printf( "Found %d total resolution nodes.\n", Vec_IntSize(vUsed) ); + Vec_IntFree( vUsed ); + + Proof_Check( vClauses, vProof, hRoot ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |