diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2018-06-20 20:09:41 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2018-06-20 20:09:41 -0700 |
| commit | 2dd629a4e5298d3d4fba7d87f51254510a5bb58b (patch) | |
| tree | f03943a9429b85c398ea795181fbcf38743f8e73 /src/proof | |
| parent | 28a1307a61cbc5b3a027f21a3b1ce74c58a52d03 (diff) | |
| download | abc-2dd629a4e5298d3d4fba7d87f51254510a5bb58b.tar.gz abc-2dd629a4e5298d3d4fba7d87f51254510a5bb58b.tar.bz2 abc-2dd629a4e5298d3d4fba7d87f51254510a5bb58b.zip | |
Bug fix in polynomial construction.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/acec/acecPo.c | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/proof/acec/acecPo.c b/src/proof/acec/acecPo.c index 6b992714..91f6d5aa 100644 --- a/src/proof/acec/acecPo.c +++ b/src/proof/acec/acecPo.c @@ -671,7 +671,7 @@ Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Wec_t * vSign, Vec_Int_t * Vec_IntForEachEntryStop( vLevel, Entry, k, Vec_IntSize(vLevel)-1 ) { if ( Entry < 0 ) // input - Vec_IntPush( vTempM[0], Vec_IntEntry(vLeaves, -1-Entry) ); + Vec_IntPushUniqueOrder( vTempM[0], Vec_IntEntry(vLeaves, -1-Entry) ); else // output { assert( OutLit == -1 ); // only one output literal is expected @@ -682,7 +682,7 @@ Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Wec_t * vSign, Vec_Int_t * nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC[0], vTempM[0] ); // mono without out else if ( !Abc_LitIsCompl(OutLit) ) // positive literal { - Vec_IntPush( vTempM[0], Abc_Lit2Var(OutLit) ); + Vec_IntPushUniqueOrder( vTempM[0], Abc_Lit2Var(OutLit) ); nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC[0], vTempM[0] ); // mono with pos out } else // negative literal @@ -691,7 +691,7 @@ Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Wec_t * vSign, Vec_Int_t * nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC[0], vTempM[0] ); // mono without out // second monomial Vec_IntFill( vTempC[0], 1, -Vec_IntEntryLast(vLevel) ); - Vec_IntPush( vTempM[0], Abc_Lit2Var(OutLit) ); + Vec_IntPushUniqueOrder( vTempM[0], Abc_Lit2Var(OutLit) ); nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC[0], vTempM[0] ); // mono with neg out } nBuilds++; |