summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2018-06-20 20:09:41 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2018-06-20 20:09:41 -0700
commit2dd629a4e5298d3d4fba7d87f51254510a5bb58b (patch)
treef03943a9429b85c398ea795181fbcf38743f8e73 /src/proof
parent28a1307a61cbc5b3a027f21a3b1ce74c58a52d03 (diff)
downloadabc-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.c6
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++;