diff options
Diffstat (limited to 'src/opt/res/resSat.c')
| -rw-r--r-- | src/opt/res/resSat.c | 163 |
1 files changed, 149 insertions, 14 deletions
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c index f9558c97..dd0e7a23 100644 --- a/src/opt/res/resSat.c +++ b/src/opt/res/resSat.c @@ -128,25 +128,27 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ) Synopsis [Loads AIG into the SAT solver for constrained simulation.] - Description [The array of fanins contains exactly two entries: the - care set and the functions.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ) +void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, int fOnSet ) { sat_solver * pSat; + Vec_Ptr_t * vFanins; Vec_Ptr_t * vNodes; Abc_Obj_t * pObj; int i, nNodes; - // make sure fanins contain POs of the AIG - pObj = Vec_PtrEntry( vFanins, 0 ); - assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) ); - assert( Vec_PtrSize(vFanins) == 2 ); + // start the array + vFanins = Vec_PtrAlloc( 2 ); + pObj = Abc_NtkPo( pAig, 0 ); + Vec_PtrPush( vFanins, pObj ); + pObj = Abc_NtkPo( pAig, 1 ); + Vec_PtrPush( vFanins, pObj ); // collect reachable nodes vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize ); @@ -171,21 +173,154 @@ void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ) Res_SatAddAnd( pSat, (int)pObj->pCopy, (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); Vec_PtrFree( vNodes ); - // add clauses for POs - Vec_PtrForEachEntry( vFanins, pObj, i ) - Res_SatAddEqual( pSat, (int)pObj->pCopy, - (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); + // add clauses for the first PO + pObj = Abc_NtkPo( pAig, 0 ); + Res_SatAddEqual( pSat, (int)pObj->pCopy, + (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); + // add clauses for the second PO + pObj = Abc_NtkPo( pAig, 1 ); + Res_SatAddEqual( pSat, (int)pObj->pCopy, + (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); // add trivial clauses - pObj = Vec_PtrEntry(vFanins, 0); + pObj = Abc_NtkPo( pAig, 0 ); Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set - pObj = Vec_PtrEntry(vFanins, 1); - Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set + + pObj = Abc_NtkPo( pAig, 1 ); + Res_SatAddConst1( pSat, (int)pObj->pCopy, !fOnSet ); // on-set + + Vec_PtrFree( vFanins ); return pSat; } /**Function************************************************************* + Synopsis [Loads AIG into the SAT solver for constrained simulation.] + + Description [Returns 1 if the required number of patterns are found. + Returns 0 if the solver ran out of time or proved a constant. + In the latter, case one of the flags, fConst0 or fConst1, are set to 1.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet ) +{ + Vec_Int_t * vLits; + Vec_Ptr_t * vPats; + sat_solver * pSat; + int RetValue, i, k, value, status, Lit, Var, iPat; + int clk = clock(); + +//printf( "Looking for %s: ", fOnSet? "onset " : "offset" ); + + // decide what problem should be solved + Lit = toLitCond( (int)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet ); + if ( fOnSet ) + { + iPat = p->nPats1; + vPats = p->vPats1; + } + else + { + iPat = p->nPats0; + vPats = p->vPats0; + } + assert( iPat < nPatsLimit ); + + // derive the SAT solver + pSat = Res_SatSimulateConstr( p->pAig, fOnSet ); + pSat->fSkipSimplify = 1; + status = sat_solver_simplify( pSat ); + if ( status == 0 ) + { + if ( iPat == 0 ) + { +// if ( fOnSet ) +// p->fConst0 = 1; +// else +// p->fConst1 = 1; + RetValue = 0; + } + goto finish; + } + + // enumerate through the SAT assignments + RetValue = 1; + vLits = Vec_IntAlloc( 32 ); + for ( k = iPat; k < nPatsLimit; k++ ) + { + // solve with the assumption +// status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); + status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); + if ( status == l_False ) + { +//printf( "Const %d\n", !fOnSet ); + if ( k == 0 ) + { + if ( fOnSet ) + p->fConst0 = 1; + else + p->fConst1 = 1; + RetValue = 0; + } + break; + } + else if ( status == l_True ) + { + // save the pattern + Vec_IntClear( vLits ); + for ( i = 0; i < p->nTruePis; i++ ) + { + Var = (int)Abc_NtkPi(p->pAig,i)->pCopy; + value = (int)(pSat->model.ptr[Var] == l_True); + if ( value ) + Abc_InfoSetBit( Vec_PtrEntry(vPats, i), k ); + Lit = toLitCond( Var, value ); + Vec_IntPush( vLits, Lit ); +// printf( "%d", value ); + } +// printf( "\n" ); + + status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); + if ( status == 0 ) + { + k++; + RetValue = 1; + break; + } + } + else + { +//printf( "Undecided\n" ); + if ( k == 0 ) + RetValue = 0; + else + RetValue = 1; + break; + } + } + Vec_IntFree( vLits ); +//printf( "Found %d patterns\n", k - iPat ); + + // set the new number of patterns + if ( fOnSet ) + p->nPats1 = k; + else + p->nPats0 = k; + +finish: + + sat_solver_delete( pSat ); +p->timeSat += clock() - clk; + return RetValue; +} + + +/**Function************************************************************* + Synopsis [Asserts equality of the variable to a constant.] Description [] |