diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-09-16 14:59:28 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-09-16 14:59:28 -0700 |
commit | 288d64d033516f992b7c07620e43ee6fbbf9e26a (patch) | |
tree | 15947c3418400ce2fb2e2b3c4f7134958cbea3ca /src/map/if | |
parent | e033a62282ef94ddca87a1778d66a4a4270ac1c3 (diff) | |
download | abc-288d64d033516f992b7c07620e43ee6fbbf9e26a.tar.gz abc-288d64d033516f992b7c07620e43ee6fbbf9e26a.tar.bz2 abc-288d64d033516f992b7c07620e43ee6fbbf9e26a.zip |
New choice computation.
Diffstat (limited to 'src/map/if')
-rw-r--r-- | src/map/if/ifTune.c | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c index d21ebad0..400520e6 100644 --- a/src/map/if/ifTune.c +++ b/src/map/if/ifTune.c @@ -394,14 +394,14 @@ void Ift_TtComparisonConstr( word * pTruth, int nVars, int fMore, int fEqual ) { word Cond[4], Equa[4], Temp[4]; word s_TtElems[8][4] = { - ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA), - ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC), - ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0), - ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00), - ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000), - ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000), - ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF), - ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) + { ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA) }, + { ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC) }, + { ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0) }, + { ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00) }, + { ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000) }, + { ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000) }, + { ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF) }, + { ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) } }; int i, nWords = Abc_TtWordNum(2*nVars); assert( nVars > 0 && nVars <= 4 ); @@ -528,7 +528,7 @@ int Ift_NtkAddClauses( Ift_Ntk_t * p, int * pValues, sat_solver * pSat ) int nSatVars = sat_solver_nvars(pSat); for ( i = 0; i < p->nObjs-1; i++ ) p->Nodes[i].Var = nSatVars++; - p->Nodes[p->nObjs-1].Var = -ABC_INFINITY; + p->Nodes[p->nObjs-1].Var = 0xFFFF; sat_solver_setnvars( pSat, nSatVars ); // verify variable values for ( i = 0; i < p->nVars; i++ ) |