diff options
-rw-r--r-- | abclib.dsp | 4 | ||||
-rw-r--r-- | src/aig/aig/aigRepar.c | 397 | ||||
-rw-r--r-- | src/aig/aig/module.make | 1 | ||||
-rw-r--r-- | src/base/abci/abc.c | 5 | ||||
-rw-r--r-- | src/sat/bsat/satProof.c | 209 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 8 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.h | 5 |
7 files changed, 478 insertions, 151 deletions
@@ -3227,6 +3227,10 @@ 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/aigRepar.c b/src/aig/aig/aigRepar.c new file mode 100644 index 00000000..d10471d7 --- /dev/null +++ b/src/aig/aig/aigRepar.c @@ -0,0 +1,397 @@ +/**CFile**************************************************************** + + FileName [aigRepar.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Interpolation-based reparametrization.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigRepar.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" +#include "cnf.h" +#include "satSolver2.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Adds buffer to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Aig_ManInterAddBuffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark ) +{ + lit Lits[2]; + int Cid; + assert( iVarA >= 0 && iVarB >= 0 ); + + Lits[0] = toLitCond( iVarA, 0 ); + Lits[1] = toLitCond( iVarB, !fCompl ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + + Lits[0] = toLitCond( iVarA, 1 ); + Lits[1] = toLitCond( iVarB, fCompl ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); +} + +/**Function************************************************************* + + Synopsis [Adds constraints for the two-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Aig_ManInterAddXor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark ) +{ + lit Lits[3]; + int Cid; + assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 ); + + Lits[0] = toLitCond( iVarA, !fCompl ); + Lits[1] = toLitCond( iVarB, 1 ); + Lits[2] = toLitCond( iVarC, 1 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + + Lits[0] = toLitCond( iVarA, !fCompl ); + Lits[1] = toLitCond( iVarB, 0 ); + Lits[2] = toLitCond( iVarC, 0 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + + Lits[0] = toLitCond( iVarA, fCompl ); + Lits[1] = toLitCond( iVarB, 1 ); + Lits[2] = toLitCond( iVarC, 0 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + + Lits[0] = toLitCond( iVarA, fCompl ); + Lits[1] = toLitCond( iVarB, 0 ); + Lits[2] = toLitCond( iVarC, 1 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose ) +{ + sat_solver2 * pSat; + Aig_Man_t * pInter; + Vec_Int_t * vVars; + Cnf_Dat_t * pCnf; + Aig_Obj_t * pObj; + int Lit, Cid, Var, status, i; + int clk = clock(); + assert( Aig_ManRegNum(pMan) == 0 ); + assert( Aig_ManPoNum(pMan) == 1 ); + + // derive CNFs + pCnf = Cnf_Derive( pMan, 1 ); + + // start the solver + pSat = sat_solver2_new(); + sat_solver2_setnvars( pSat, 2*pCnf->nVars+1 ); + // set A-variables (all used except PI/PO) + Aig_ManForEachObj( pMan, pObj, i ) + { + if ( pCnf->pVarNums[pObj->Id] < 0 ) + continue; + if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsPo(pObj) ) + var_set_partA( pSat, pCnf->pVarNums[pObj->Id], 1 ); + } + + // add clauses of A + for ( i = 0; i < pCnf->nClauses; i++ ) + { + Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ); + clause_set_partA( pSat, Cid, 1 ); + } + + // add clauses of B + Cnf_DataLift( pCnf, pCnf->nVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) + sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ); + Cnf_DataLift( pCnf, -pCnf->nVars ); + + // add PI equality clauses + vVars = Vec_IntAlloc( Aig_ManPoNum(pMan)+1 ); + Aig_ManForEachPi( pMan, pObj, i ) + { + if ( Aig_ObjRefs(pObj) == 0 ) + continue; + Var = pCnf->pVarNums[pObj->Id]; + Aig_ManInterAddBuffer( pSat, Var, pCnf->nVars + Var, 0, 0 ); + Vec_IntPush( vVars, Var ); + } + + // add an XOR clause in the end + Var = pCnf->pVarNums[Aig_ManPo(pMan,0)->Id]; + Aig_ManInterAddXor( pSat, Var, pCnf->nVars + Var, 2*pCnf->nVars, 0, 0 ); + Vec_IntPush( vVars, Var ); + + // solve the problem + Lit = toLitCond( 2*pCnf->nVars, 0 ); + status = sat_solver2_solve( pSat, &Lit, &Lit + 1, 0, 0, 0, 0 ); + assert( status == l_False ); + Sat_Solver2PrintStats( stdout, pSat ); + + // derive interpolant + pInter = Sat_ProofInterpolant( pSat, vVars ); + Aig_ManPrintStats( pInter ); + Aig_ManDumpBlif( pInter, "int.blif", NULL, NULL ); + + // clean up + Aig_ManStop( pInter ); + Vec_IntFree( vVars ); + Cnf_DataFree( pCnf ); + sat_solver2_delete( pSat ); + ABC_PRT( "Total interpolation time", clock() - clk ); +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG while mapping PIs into the given array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManAppend( Aig_Man_t * pBase, Aig_Man_t * pNew ) +{ + Aig_Obj_t * pObj; + int i; + assert( Aig_ManPoNum(pNew) == 1 ); + assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(pBase) ); + // create the PIs + Aig_ManCleanData( pNew ); + Aig_ManConst1(pNew)->pData = Aig_ManConst1(pBase); + Aig_ManForEachPi( pNew, pObj, i ) + pObj->pData = Aig_IthVar(pBase, i); + // duplicate internal nodes + Aig_ManForEachNode( pNew, pObj, i ) + pObj->pData = Aig_And( pBase, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // add one PO to base + pObj = Aig_ManPo( pNew, 0 ); + Aig_ObjCreatePo( pBase, Aig_ObjChild0Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose ) +{ + Aig_Man_t * pAigTemp, * pInter, * pBase = NULL; + sat_solver2 * pSat; + Vec_Int_t * vVars; + Cnf_Dat_t * pCnf, * pCnfInter; + Aig_Obj_t * pObj; + int nOuts = Aig_ManPoNum(pMan); + int ShiftP[2], ShiftCnf[2], ShiftOr[2], ShiftAssume; + int Cid, Lit, status, i, k, c; + int clk = clock(); + assert( Aig_ManRegNum(pMan) == 0 ); + + // derive CNFs + pCnf = Cnf_Derive( pMan, nOuts ); + + // start the solver + pSat = sat_solver2_new(); + sat_solver2_setnvars( pSat, 4*pCnf->nVars + 6*nOuts ); + // vars: pGlobal + (p0 + A1 + A2 + or0) + (p1 + B1 + B2 + or1) + pAssume; + ShiftP[0] = nOuts; + ShiftP[1] = 2*pCnf->nVars + 3*nOuts; + ShiftCnf[0] = ShiftP[0] + nOuts; + ShiftCnf[1] = ShiftP[1] + nOuts; + ShiftOr[0] = ShiftCnf[0] + 2*pCnf->nVars; + ShiftOr[1] = ShiftCnf[1] + 2*pCnf->nVars; + ShiftAssume = ShiftOr[1] + nOuts; + assert( ShiftAssume + nOuts == pSat->size ); + + // mark variables of A + for ( i = ShiftCnf[0]; i < ShiftP[1]; i++ ) + var_set_partA( pSat, i, 1 ); + + // add clauses of A, then B + vVars = Vec_IntAlloc( 2*nOuts ); + for ( k = 0; k < 2; k++ ) + { + // copy A1 + Cnf_DataLift( pCnf, ShiftCnf[k] ); + for ( i = 0; i < pCnf->nClauses; i++ ) + { + Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ); + clause_set_partA( pSat, Cid, k==0 ); + } + // add equality p[k] == A1/B1 + Aig_ManForEachPo( pMan, pObj, i ) + Aig_ManInterAddBuffer( pSat, ShiftP[k] + i, pCnf->pVarNums[pObj->Id], k==1, k==0 ); + // copy A2 + Cnf_DataLift( pCnf, pCnf->nVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) + { + Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ); + clause_set_partA( pSat, Cid, k==0 ); + } + // add comparator (!p[k] ^ A2/B2) == or[k] + Vec_IntClear( vVars ); + Aig_ManForEachPo( pMan, pObj, i ) + { + Aig_ManInterAddXor( pSat, ShiftP[k] + i, pCnf->pVarNums[pObj->Id], ShiftOr[k] + i, k==1, k==0 ); + Vec_IntPush( vVars, toLitCond(ShiftOr[k] + i, 1) ); + } + Cid = sat_solver2_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars) ); + clause_set_partA( pSat, Cid, k==0 ); + // return to normal + Cnf_DataLift( pCnf, -ShiftCnf[k]-pCnf->nVars ); + } + // add clauses to constrain p[0] and p[1] + for ( k = 0; k < nOuts; k++ ) + Aig_ManInterAddXor( pSat, ShiftP[0] + k, ShiftP[1] + k, ShiftAssume + k, 0, 0 ); + + // start the interpolant + pBase = Aig_ManStart( 1000 ); + pBase->pName = Aig_UtilStrsav( "repar" ); + for ( k = 0; k < 2*nOuts; k++ ) + Aig_IthVar(pBase, i); + + // start global variables (pGlobal and p[0]) + Vec_IntClear( vVars ); + for ( k = 0; k < 2*nOuts; k++ ) + Vec_IntPush( vVars, k ); + + // perform iterative solving + // vars: pGlobal + (p0 + A1 + A2 + or0) + (p1 + B1 + B2 + or1) + pAssume; + for ( k = 0; k < nOuts; k++ ) + { + // swap k-th variables + int Temp = Vec_IntEntry( vVars, k ); + Vec_IntWriteEntry( vVars, k, Vec_IntEntry(vVars, nOuts+k) ); + Vec_IntWriteEntry( vVars, nOuts+k, Temp ); + + // solve incrementally + Lit = toLitCond( ShiftAssume + k, 1 ); // XOR output is 0 ==> p1 == p2 + status = sat_solver2_solve( pSat, &Lit, &Lit + 1, 0, 0, 0, 0 ); + assert( status == l_False ); + Sat_Solver2PrintStats( stdout, pSat ); + + // derive interpolant + pInter = Sat_ProofInterpolant( pSat, vVars ); + Aig_ManPrintStats( pInter ); + // make sure interpolant does not depend on useless vars + Aig_ManForEachPi( pInter, pObj, i ) + assert( i <= k || Aig_ObjRefs(pObj) == 0 ); + + // simplify + pInter = Dar_ManRwsat( pAigTemp = pInter, 1, 0 ); + Aig_ManStop( pAigTemp ); + + // add interpolant to the solver + pCnfInter = Cnf_Derive( pInter, 1 ); + Cnf_DataLift( pCnfInter, pSat->size ); + sat_solver2_setnvars( pSat, pSat->size + 2*pCnfInter->nVars ); + for ( i = 0; i < pCnfInter->nVars; i++ ) + var_set_partA( pSat, pSat->size-2*pCnfInter->nVars + i, 1 ); + for ( c = 0; c < 2; c++ ) + { + if ( c == 1 ) + Cnf_DataLift( pCnfInter, pCnfInter->nVars ); + // add to A + for ( i = 0; i < pCnfInter->nClauses; i++ ) + { + Cid = sat_solver2_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ); + clause_set_partA( pSat, Cid, c==0 ); + } + // connect to the inputs + Aig_ManForEachPi( pInter, pObj, i ) + if ( i <= k ) + Aig_ManInterAddBuffer( pSat, i, pCnf->pVarNums[pObj->Id], 0, c==0 ); + // connect to the outputs + pObj = Aig_ManPo(pInter, 0); + Aig_ManInterAddBuffer( pSat, ShiftP[c] + k, pCnf->pVarNums[pObj->Id], 0, c==0 ); + if ( c == 1 ) + Cnf_DataLift( pCnfInter, -pCnfInter->nVars ); + } + Cnf_DataFree( pCnfInter ); + + // accumulate + Aig_ManAppend( pBase, pInter ); + Aig_ManStop( pInter ); + + // update global variables + Temp = Vec_IntEntry( vVars, k ); + Vec_IntWriteEntry( vVars, k, Vec_IntEntry(vVars, nOuts+k) ); + Vec_IntWriteEntry( vVars, nOuts+k, Temp ); + } + + Vec_IntFree( vVars ); + Cnf_DataFree( pCnf ); + sat_solver2_delete( pSat ); + ABC_PRT( "Reparameterization time", clock() - clk ); + return pBase; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make index c291433f..aaf5bf6d 100644 --- a/src/aig/aig/module.make +++ b/src/aig/aig/module.make @@ -17,6 +17,7 @@ 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/base/abci/abc.c b/src/base/abci/abc.c index 9042d1ed..862288fd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8891,12 +8891,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) */ { - extern void Abs_VfaManTest( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose ); +// extern void Abs_VfaManTest( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose ); + extern void Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose ); extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); if ( pNtk ) { Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); - Abs_VfaManTest( pAig, 32, 1000000, 1 ); + Aig_ManInterRepar( pAig, 1 ); Aig_ManStop( pAig ); } } diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 337fe3ca..ded11f1e 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -133,10 +133,10 @@ static inline satset* Proof_ResolveRead (Rec_Int_t* p, cla h ) { return (sats // iterating through fanins of a proof node #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] >> 2)), 1); i++ ) -#define Proof_NodeForeachLeaf( pLeaves, pNode, pLeaf, i ) \ - for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : NULL), 1); i++ ) -#define Proof_NodeForeachFaninLeaf( p, pLeaves, pNode, pFanin, i ) \ - for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, 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_NodeRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ ) +#define Proof_NodeForeachFaninLeaf( p, pClauses, pNode, pFanin, i ) \ + for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ ) //////////////////////////////////////////////////////////////////////// @@ -420,135 +420,6 @@ void Sat_ProofReduce( sat_solver2 * s ) -#if 0 - -/**Function************************************************************* - - Synopsis [Performs one resultion step.] - - Description [Returns ID of the resolvent if success, and -1 if failure.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -satset * Sat_ProofCheckResolveOne( Vec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp ) -{ - satset * c; - int i, k, hNode, Var = -1, Count = 0; - // find resolution variable - 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); - Count++; - } - if ( Count == 0 ) - { - printf( "Cannot find resolution variable\n" ); - return NULL; - } - if ( Count > 1 ) - { - printf( "Found more than 1 resolution variables\n" ); - return NULL; - } - // perform resolution - Vec_IntClear( vTemp ); - for ( i = 0; i < (int)c1->nEnts; i++ ) - if ( (c1->pEnts[i] >> 1) != Var ) - Vec_IntPush( vTemp, c1->pEnts[i] ); - for ( i = 0; i < (int)c2->nEnts; i++ ) - if ( (c2->pEnts[i] >> 1) != Var ) - Vec_IntPushUnique( vTemp, c2->pEnts[i] ); - // move to the new one - hNode = Vec_IntSize( p ); - Vec_IntPush( p, 0 ); // placeholder - Vec_IntPush( p, 0 ); - Vec_IntForEachEntry( vTemp, Var, i ) - Vec_IntPush( p, Var ); - c = Proof_NodeRead( p, hNode ); - c->nEnts = Vec_IntSize(vTemp); - return c; -} - -/**Function************************************************************* - - Synopsis [Checks the proof for consitency.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt ) -{ - satset * pAnt; - if ( iAnt & 1 ) - return Proof_NodeRead( vClauses, iAnt >> 2 ); - assert( iAnt > 0 ); - pAnt = Proof_NodeRead( vProof, iAnt >> 2 ); - assert( pAnt->Id > 0 ); - return Proof_NodeRead( vResolves, pAnt->Id ); -} - -/**Function************************************************************* - - Synopsis [Checks the proof for consitency.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_ProofCheck( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) -{ - Vec_Int_t * vUsed, * vResolves, * vTemp; - satset * pSet, * pSet0, * pSet1; - int i, k, Counter = 0, clk = clock(); - // collect visited clauses - vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); - Proof_CleanCollected( vProof, vUsed ); - // perform resolution steps - vTemp = Vec_IntAlloc( 1000 ); - vResolves = Vec_IntAlloc( 1000 ); - Vec_IntPush( vResolves, -1 ); - Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) - { - pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); - for ( k = 1; k < (int)pSet->nEnts; k++ ) - { - pSet1 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); - pSet0 = Sat_ProofCheckResolveOne( vResolves, pSet0, pSet1, vTemp ); - } - pSet->Id = Proof_NodeHandle( vResolves, pSet0 ); -//printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) ); -//satset_print( pSet0 ); - Counter++; - } - Vec_IntFree( vTemp ); - // clean the proof - Proof_CleanCollected( vProof, vUsed ); - // compare the final clause - printf( "Used %6.2f Mb for resolvents.\n", 4.0 * Vec_IntSize(vResolves) / (1<<20) ); - if ( pSet0->nEnts > 0 ) - printf( "Cound not derive the empty clause. " ); - else - printf( "Proof verification successful. " ); - Abc_PrintTime( 1, "Time", clock() - clk ); - // cleanup - Vec_IntFree( vResolves ); - Vec_IntFree( vUsed ); -} - -#endif - /**Function************************************************************* Synopsis [Performs one resultion step.] @@ -669,7 +540,7 @@ void Sat_ProofCheck( sat_solver2 * s ) // compare the final clause printf( "Used %6.2f Mb for resolvents.\n", 4.0 * Rec_IntSize(vResolves) / (1<<20) ); if ( pSet0->nEnts > 0 ) - printf( "Cound not derive the empty clause. " ); + printf( "Derived clause with %d lits instead of the empty clause. ", pSet0->nEnts ); else printf( "Proof verification successful. " ); Abc_PrintTime( 1, "Time", clock() - clk ); @@ -689,7 +560,7 @@ void Sat_ProofCheck( sat_solver2 * s ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed ) +Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed, int fUseIds ) { Vec_Int_t * vCore; satset * pNode, * pFanin; @@ -709,11 +580,59 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_ Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) { pNode->mark = 0; - Vec_IntWriteEntry( vCore, i, pNode->Id - 1 ); + if ( fUseIds ) + Vec_IntWriteEntry( vCore, i, pNode->Id - 1 ); } return vCore; } +/**Function************************************************************* + + Synopsis [Verifies that variables are labeled correctly.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_ProofInterpolantCheckVars( sat_solver2 * s, Vec_Int_t * vGloVars ) +{ + satset* c; + Vec_Int_t * vVarMap; + int i, k, Entry, * pMask; + int Counts[5] = {0}; + // map variables into their type (A, B, or AB) + vVarMap = Vec_IntStart( s->size ); + sat_solver_foreach_clause( s, c, i ) + for ( k = 0; k < (int)c->nEnts; k++ ) + *Vec_IntEntryP(vVarMap, lit_var(c->pEnts[k])) |= 2 - c->partA; + // analyze variables + Vec_IntForEachEntry( vGloVars, Entry, i ) + { + pMask = Vec_IntEntryP(vVarMap, Entry); + assert( *pMask >= 0 && *pMask <= 3 ); + Counts[(*pMask & 3)]++; + *pMask = 0; + } + // count the number of global variables not listed + Vec_IntForEachEntry( vVarMap, Entry, i ) + if ( Entry == 3 ) + Counts[4]++; + Vec_IntFree( vVarMap ); + // report + if ( Counts[0] ) + printf( "Warning: %6d variables listed as global do not appear in clauses (this is normal)\n", Counts[0] ); + if ( Counts[1] ) + printf( "Warning: %6d variables listed as global appear only in A-clauses (this is a BUG)\n", Counts[1] ); + if ( Counts[2] ) + printf( "Warning: %6d variables listed as global appear only in B-clauses (this is a BUG)\n", Counts[2] ); + if ( Counts[3] ) + printf( "Warning: %6d (out of %d) variables listed as global appear in both A- and B-clauses (this is normal)\n", Counts[3], Vec_IntSize(vGloVars) ); + if ( Counts[4] ) + printf( "Warning: %6d variables not listed as global appear in both A- and B-clauses (this is a BUG)\n", Counts[4] ); +} /**Function************************************************************* @@ -737,15 +656,17 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) satset * pNode, * pFanin; Aig_Man_t * pAig; Aig_Obj_t * pObj; - int i, k, iVar, Entry; + int i, k, iVar, Lit, Entry; + + Sat_ProofInterpolantCheckVars( s, vGlobVars ); // collect visited nodes vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); // collect core clauses (cleans vUsed and vCore) - vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed ); + vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 ); // map variables into their global numbers - vVarMap = Vec_IntStartFull( Vec_IntFindMax(vGlobVars) + 1 ); + vVarMap = Vec_IntStartFull( s->size ); Vec_IntForEachEntry( vGlobVars, Entry, i ) Vec_IntWriteEntry( vVarMap, Entry, i ); @@ -762,9 +683,9 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) if ( pNode->partA ) { pObj = Aig_ManConst0( pAig ); - satset_foreach_var( pNode, iVar, k, 0 ) - if ( iVar < Vec_IntSize(vVarMap) && Vec_IntEntry(vVarMap, iVar) >= 0 ) - pObj = Aig_Or( pAig, pObj, Aig_IthVar(pAig, iVar) ); + satset_foreach_lit( pNode, Lit, k, 0 ) + if ( (iVar = Vec_IntEntry(vVarMap, lit_var(Lit))) >= 0 ) + pObj = Aig_Or( pAig, pObj, Aig_NotCond(Aig_IthVar(pAig, iVar), lit_sign(Lit)) ); } else pObj = Aig_ManConst1( pAig ); @@ -777,9 +698,11 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) // copy the numbers out and derive interpol for resolvents Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) { +// satset_print( pNode ); assert( pNode->nEnts > 1 ); Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k ) { + assert( pFanin->Id < 2*Aig_ManObjNumMax(pAig) ); if ( k == 0 ) pObj = Aig_ObjFromLit( pAig, pFanin->Id ); else if ( pNode->pEnts[k] & 2 ) // variable of A @@ -828,7 +751,7 @@ void * Sat_ProofCore( sat_solver2 * s ) // collect visited clauses vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); // collect core clauses - vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed ); + vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 1 ); Vec_IntFree( vUsed ); return vCore; } diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index e2bea751..5eb65132 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -144,11 +144,9 @@ static inline void solver2_clear_marks(sat_solver2* s) { static inline satset* clause_read (sat_solver2* s, cla h) { return (h & 1) ? satset_read(&s->learnts, h>>1) : satset_read(&s->clauses, h>>1); } static inline cla clause_handle (sat_solver2* s, satset* c) { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1; } static inline int clause_check (sat_solver2* s, satset* c) { return c->learnt ? satset_check(&s->learnts, c) : satset_check(&s->clauses, c); } -static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | 1; } +static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | (partA<<1) | 1; } static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 1) ? (h >> 1) < s->hLearntPivot : (h >> 1) < s->hClausePivot; } - - //static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1; } //static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; } //static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause_read(s, s->reasons[v] >> 1) : NULL; } @@ -163,9 +161,6 @@ int clause_is_partA (sat_solver2* s, int h) { return clause void clause_set_partA(sat_solver2* s, int h, int partA) { clause_read(s, h)->partA = partA; } int clause_id(sat_solver2* s, int h) { return clause_read(s, h)->Id; } -#define sat_solver_foreach_clause( s, c, h ) satset_foreach_entry( &s->clauses, c, h, 1 ) -#define sat_solver_foreach_learnt( s, c, h ) satset_foreach_entry( &s->learnts, c, h, 1 ) - //================================================================================================= // Simple helpers: @@ -1452,6 +1447,7 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) if ( !solver2_enqueue(s,begin[0],0) ) assert( 0 ); } +//satset_print( clause_read(s, Cid) ); return Cid; } diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 83dbb6cb..e5b85a43 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -184,6 +184,11 @@ static inline void satset_print (satset * c) { for ( i = 0; (i < veci_size(pVec)) && ((c) = satset_read(p, veci_begin(pVec)[i])); i++ ) #define satset_foreach_var( p, var, i, start ) \ for ( i = start; (i < (int)(p)->nEnts) && ((var) = lit_var((p)->pEnts[i])); i++ ) +#define satset_foreach_lit( p, lit, i, start ) \ + for ( i = start; (i < (int)(p)->nEnts) && ((lit) = (p)->pEnts[i]); i++ ) + +#define sat_solver_foreach_clause( s, c, h ) satset_foreach_entry( &s->clauses, c, h, 1 ) +#define sat_solver_foreach_learnt( s, c, h ) satset_foreach_entry( &s->learnts, c, h, 1 ) //================================================================================================= // Public APIs: |