Home
last modified time | relevance | path

Searched refs:pCubeMin (Results 1 – 2 of 2) sorted by relevance

/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/pdr/
H A DpdrCore.c98 Pdr_Set_t * pCubeMin; in Pdr_ManReduceClause() local
135 return pCubeMin; in Pdr_ManReduceClause()
707 if ( pCubeMin == NULL ) in Pdr_ManGeneralize()
714 if ( pCubeMin->nLits > 1 ) in Pdr_ManGeneralize()
721 *ppCubeMin = pCubeMin; in Pdr_ManGeneralize()
769 Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; in Pdr_ManGeneralize()
816 pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i ); in Pdr_ManGeneralize()
847 Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; in Pdr_ManGeneralize()
859 pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i ); in Pdr_ManGeneralize()
877 *ppCubeMin = pCubeMin; in Pdr_ManGeneralize()
[all …]
H A DpdrIncr.c72 Pdr_Set_t * pCubeMin; in IPdr_ManPushClausesK() local
73 pCubeMin = Pdr_ManReduceClause( p, k, pCubeK ); in IPdr_ManPushClausesK()
74 if ( pCubeMin != NULL ) in IPdr_ManPushClausesK()
78 pCubeK = pCubeMin; in IPdr_ManPushClausesK()