Searched refs:pCnfFrames (Results 1 – 5 of 5) sorted by relevance
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/int/ |
| H A D | intM114.c | 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()
86 Cnf_DataLift( pCnfAig, -pCnfFrames->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()
162 Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] ); 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()
[all …]
|
| H A D | intM114p.c | 51 Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, in Inter_ManDeriveSatSolverM114p() argument
68 Cnf_DataLift( pCnfAig, pCnfFrames->nVars ); in Inter_ManDeriveSatSolverM114p()
69 Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars ); in Inter_ManDeriveSatSolverM114p()
74 for ( i = 0; i < pCnfFrames->nVars; i++ ) in Inter_ManDeriveSatSolverM114p()
120 Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 ); in Inter_ManDeriveSatSolverM114p()
125 Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 ); in Inter_ManDeriveSatSolverM114p()
132 for ( i = 0; i < pCnfFrames->nClauses; i++ ) in Inter_ManDeriveSatSolverM114p()
135 if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) ) in Inter_ManDeriveSatSolverM114p()
142 Cnf_DataLift( pCnfAig, -pCnfFrames->nVars ); in Inter_ManDeriveSatSolverM114p()
143 Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars ); in Inter_ManDeriveSatSolverM114p()
[all …]
|
| H A D | intMan.c | 85 if ( p->pCnfFrames ) in Inter_ManClean()
86 Cnf_DataFree( p->pCnfFrames ); in Inter_ManClean()
|
| H A D | intInt.h | 61 Cnf_Dat_t * pCnfFrames; // CNF for the timeframes member
|
| H A D | intCore.c | 163 p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) ); in Inter_ManPerformInterpolation()
166 p->pCnfFrames = Cnf_DeriveSimple( p->pFrames, 0 ); in Inter_ManPerformInterpolation()
|