summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2016-09-05 23:54:44 +0300
committerAlan Mishchenko <alanmi@berkeley.edu>2016-09-05 23:54:44 +0300
commitca93730781ac2a6559e16a6203786073b1cbd514 (patch)
treef245b86fa6036b28dcf8045e2e5a8c36c18890c6
parent198fe99416cdc4cb8ec131f190024bb1d5608efa (diff)
downloadabc-ca93730781ac2a6559e16a6203786073b1cbd514.tar.gz
abc-ca93730781ac2a6559e16a6203786073b1cbd514.tar.bz2
abc-ca93730781ac2a6559e16a6203786073b1cbd514.zip
Experimental code for polynomial construction.
-rw-r--r--src/base/exor/exor.c2
-rw-r--r--src/proof/acec/acecCo.c2
-rw-r--r--src/proof/acec/acecPo.c1
3 files changed, 3 insertions, 2 deletions
diff --git a/src/base/exor/exor.c b/src/base/exor/exor.c
index 052362e5..2310de5f 100644
--- a/src/base/exor/exor.c
+++ b/src/base/exor/exor.c
@@ -78,6 +78,7 @@ extern int s_fDecreaseLiterals;
SeeAlso []
***********************************************************************/
+/*
static int QCost[16][16] =
{
{ 1}, // 0
@@ -90,6 +91,7 @@ static int QCost[16][16] =
{ 56, 56, 56, 56, 58, 60, 62, 64}, // 7
{ 0 }
};
+*/
int GetQCost( int nVars, int nNegs )
{
int Extra;
diff --git a/src/proof/acec/acecCo.c b/src/proof/acec/acecCo.c
index a82bd1e2..14eecc9c 100644
--- a/src/proof/acec/acecCo.c
+++ b/src/proof/acec/acecCo.c
@@ -93,7 +93,7 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t *
Vec_Int_t * vRoots = Vec_IntAlloc( 5 * Gia_ManCoNum(pGia) );
Vec_Int_t * vLeaves = Vec_IntAlloc( 2 * Gia_ManCiNum(pGia) );
Vec_Wec_t * vMap = Vec_WecStart( Gia_ManObjNum(pGia) );
- int i, k, Index, Driver, Entry1, Entry2;
+ int i, k, Index, Driver, Entry1, Entry2 = -1;
// nodes driven by adders into adder indexes
for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ )
{
diff --git a/src/proof/acec/acecPo.c b/src/proof/acec/acecPo.c
index 96e40405..1e77ab20 100644
--- a/src/proof/acec/acecPo.c
+++ b/src/proof/acec/acecPo.c
@@ -339,7 +339,6 @@ Vec_Wec_t * Gia_PolynBuildNew2( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int
// complement leave nodes
Vec_IntForEachEntry( vLeaves, iObj, i )
{
- Gia_Obj_t * pObj = Gia_ManObj( pGia, iObj );
int iLits[2] = { Abc_Var2Lit(iObj, 0), Abc_Var2Lit(iObj, 1) };
// add inverter
Vec_Int_t * vArray = Vec_WecEntry( vLit2Mono, iLits[1] );