49     Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames,   in Inter_ManDeriveSatSolver()  argument
70     Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );  in Inter_ManDeriveSatSolver()
71     Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );  in Inter_ManDeriveSatSolver()
76     sat_solver_setnvars( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );  in Inter_ManDeriveSatSolver()
86             Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );  in Inter_ManDeriveSatSolver()
87             Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );  in Inter_ManDeriveSatSolver()
142             assert( pCnfFrames->pVarNums[pObj->Id] >= 0 );  in Inter_ManDeriveSatSolver()
143             Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );  in Inter_ManDeriveSatSolver()
146             Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );  in Inter_ManDeriveSatSolver()
150             Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );  in Inter_ManDeriveSatSolver()
162             Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );  in Inter_ManDeriveSatSolver()
165             Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );  in Inter_ManDeriveSatSolver()
169             Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );  in Inter_ManDeriveSatSolver()
177     for ( i = 0; i < pCnfFrames->nClauses; i++ )  in Inter_ManDeriveSatSolver()
179         if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )  in Inter_ManDeriveSatSolver()
187     Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );  in Inter_ManDeriveSatSolver()
188     Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );  in Inter_ManDeriveSatSolver()
216 …ver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB, fUs…  in Inter_ManPerformOneStep()