diff options
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/aig/aigRepar.c | 397 | ||||
| -rw-r--r-- | src/aig/aig/module.make | 1 |
2 files changed, 398 insertions, 0 deletions
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 \ |