diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/aig/aigInter.c | 12 | ||||
-rw-r--r-- | src/aig/kit/cloud.c | 60 | ||||
-rw-r--r-- | src/aig/kit/cloud.h | 18 |
3 files changed, 49 insertions, 41 deletions
diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c index c939a38c..c5d0b39f 100644 --- a/src/aig/aig/aigInter.c +++ b/src/aig/aig/aigInter.c @@ -162,7 +162,17 @@ clk = clock(); pRes = Inta_ManInterpolate( pManInter, pSatCnf, vVarsAB, fVerbose ); Inta_ManFree( pManInter ); timeInt += clock() - clk; - +/* + // test UNSAT core computation + { + Intp_Man_t * pManProof; + Vec_Int_t * vCore; + pManProof = Intp_ManAlloc(); + vCore = Intp_ManUnsatCore( pManProof, pSatCnf, 0 ); + Intp_ManFree( pManProof ); + Vec_IntFree( vCore ); + } +*/ Vec_IntFree( vVarsAB ); Sto_ManFree( pSatCnf ); return pRes; diff --git a/src/aig/kit/cloud.c b/src/aig/kit/cloud.c index 6e6691f0..f5c91fe7 100644 --- a/src/aig/kit/cloud.c +++ b/src/aig/kit/cloud.c @@ -105,8 +105,8 @@ clk2 = clock(); dd->nSignCur = 1; dd->tUnique[0].s = dd->nSignCur; dd->tUnique[0].v = CLOUD_CONST_INDEX; - dd->tUnique[0].e = CLOUD_VOID; - dd->tUnique[0].t = CLOUD_VOID; + dd->tUnique[0].e = NULL; + dd->tUnique[0].t = NULL; dd->one = dd->tUnique; dd->zero = Cloud_Not(dd->one); dd->nNodesCur = 1; @@ -256,7 +256,7 @@ CloudNode * Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudN if ( Cloud_IsComplement(t) ) { pRes = cloudMakeNode( dd, v, Cloud_Not(t), Cloud_Not(e) ); - if ( pRes != CLOUD_VOID ) + if ( pRes != NULL ) pRes = Cloud_Not(pRes); } else @@ -314,7 +314,7 @@ CloudNode * cloudMakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNo printf( "Cloud needs restart!\n" ); // fflush( stdout ); // exit(1); - return CLOUD_VOID; + return NULL; } // create the node entryUnique->s = dd->nSignCur; @@ -367,7 +367,7 @@ CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g ) cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashCudd2(f, g, dd->shiftCache[CLOUD_OPER_AND]); // cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashBuddy2(f, g, dd->shiftCache[CLOUD_OPER_AND]); r = cloudCacheLookup2( cacheEntry, dd->nSignCur, f, g ); - if ( r != CLOUD_VOID ) + if ( r != NULL ) { dd->nCacheHits++; return r; @@ -419,16 +419,16 @@ CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g ) else t = cloudBddAnd( dd, gv, fv ); - if ( t == CLOUD_VOID ) - return CLOUD_VOID; + if ( t == NULL ) + return NULL; if ( fnv <= gnv ) e = cloudBddAnd( dd, fnv, gnv ); else e = cloudBddAnd( dd, gnv, fnv ); - if ( e == CLOUD_VOID ) - return CLOUD_VOID; + if ( e == NULL ) + return NULL; if ( t == e ) r = t; @@ -437,15 +437,15 @@ CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g ) if ( Cloud_IsComplement(t) ) { r = cloudMakeNode( dd, var, Cloud_Not(t), Cloud_Not(e) ); - if ( r == CLOUD_VOID ) - return CLOUD_VOID; + if ( r == NULL ) + return NULL; r = Cloud_Not(r); } else { r = cloudMakeNode( dd, var, t, e ); - if ( r == CLOUD_VOID ) - return CLOUD_VOID; + if ( r == NULL ) + return NULL; } } cloudCacheInsert2( cacheEntry, dd->nSignCur, f, g, r ); @@ -484,8 +484,8 @@ static inline CloudNode * cloudBddAnd_gate( CloudManager * dd, CloudNode * f, Cl ******************************************************************************/ CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g ) { - if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID ) - return CLOUD_VOID; + if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL ) + return NULL; CLOUD_ASSERT(f); CLOUD_ASSERT(g); if ( dd->tCaches[CLOUD_OPER_AND] == NULL ) @@ -507,14 +507,14 @@ CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g ) CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g ) { CloudNode * res; - if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID ) - return CLOUD_VOID; + if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL ) + return NULL; CLOUD_ASSERT(f); CLOUD_ASSERT(g); if ( dd->tCaches[CLOUD_OPER_AND] == NULL ) cloudCacheAllocate( dd, CLOUD_OPER_AND ); res = cloudBddAnd_gate( dd, Cloud_Not(f), Cloud_Not(g) ); - res = Cloud_NotCond( res, res != CLOUD_VOID ); + res = Cloud_NotCond( res, res != NULL ); return res; } @@ -532,18 +532,18 @@ CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g ) CloudNode * Cloud_bddXor( CloudManager * dd, CloudNode * f, CloudNode * g ) { CloudNode * t0, * t1, * r; - if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID ) - return CLOUD_VOID; + if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL ) + return NULL; CLOUD_ASSERT(f); CLOUD_ASSERT(g); if ( dd->tCaches[CLOUD_OPER_AND] == NULL ) cloudCacheAllocate( dd, CLOUD_OPER_AND ); t0 = cloudBddAnd_gate( dd, f, Cloud_Not(g) ); - if ( t0 == CLOUD_VOID ) - return CLOUD_VOID; + if ( t0 == NULL ) + return NULL; t1 = cloudBddAnd_gate( dd, Cloud_Not(f), g ); - if ( t1 == CLOUD_VOID ) - return CLOUD_VOID; + if ( t1 == NULL ) + return NULL; r = Cloud_bddOr( dd, t0, t1 ); return r; } @@ -631,7 +631,7 @@ CloudNode * Cloud_Support( CloudManager * dd, CloudNode * n ) if ( support[i] == 1 ) { res = Cloud_bddAnd( dd, res, dd->vars[i] ); - if ( res == CLOUD_VOID ) + if ( res == NULL ) break; } FREE( support ); @@ -831,8 +831,8 @@ CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * bFunc ) // try to find the cube with the negative literal res = Cloud_GetOneCube( dd, bFunc0 ); - if ( res == CLOUD_VOID ) - return CLOUD_VOID; + if ( res == NULL ) + return NULL; if ( res != dd->zero ) { @@ -842,8 +842,8 @@ CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * bFunc ) { // try to find the cube with the positive literal res = Cloud_GetOneCube( dd, bFunc1 ); - if ( res == CLOUD_VOID ) - return CLOUD_VOID; + if ( res == NULL ) + return NULL; assert( res != dd->zero ); res = Cloud_bddAnd( dd, res, dd->vars[Cloud_V(bFunc)] ); } @@ -873,7 +873,7 @@ void Cloud_bddPrint( CloudManager * dd, CloudNode * Func ) while ( 1 ) { Cube = Cloud_GetOneCube( dd, Func ); - if ( Cube == CLOUD_VOID || Cube == dd->zero ) + if ( Cube == NULL || Cube == dd->zero ) break; if ( fFirst ) fFirst = 0; else printf( " + " ); diff --git a/src/aig/kit/cloud.h b/src/aig/kit/cloud.h index ac9d45f4..fa7f2fce 100644 --- a/src/aig/kit/cloud.h +++ b/src/aig/kit/cloud.h @@ -27,6 +27,7 @@ extern "C" { #include <stdlib.h> #include <assert.h> #include <time.h> +#include "port_type.h" #ifdef _WIN32 #define inline __inline // compatible with MS VS 6.0 @@ -162,9 +163,6 @@ struct cloudCacheEntry3 // the three-argument cache // parameters #define CLOUD_NODE_BITS 23 -#define CLOUD_ONE ((unsigned)0x00000001) -#define CLOUD_NOT_ONE ((unsigned)0xfffffffe) -#define CLOUD_VOID ((unsigned)0x00000000) #define CLOUD_CONST_INDEX ((unsigned)0x0fffffff) #define CLOUD_MARK_ON ((unsigned)0x10000000) @@ -182,10 +180,10 @@ struct cloudCacheEntry3 // the three-argument cache #define cloudHashCudd3(f,g,h,s) (((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2 + (unsigned)(h)) * DD_P3) >> (s)) // node complementation (using node) -#define Cloud_Regular(p) ((CloudNode*)(((unsigned)(p)) & CLOUD_NOT_ONE)) // get the regular node (w/o bubble) -#define Cloud_Not(p) ((CloudNode*)(((unsigned)(p)) ^ CLOUD_ONE)) // complement the node -#define Cloud_NotCond(p,c) (((int)(c))? Cloud_Not(p):(p)) // complement the node conditionally -#define Cloud_IsComplement(p) ((int)(((unsigned)(p)) & CLOUD_ONE)) // check if complemented +#define Cloud_Regular(p) ((CloudNode*)(((PORT_PTRUINT_T)(p)) & ~01)) // get the regular node (w/o bubble) +#define Cloud_Not(p) ((CloudNode*)(((PORT_PTRUINT_T)(p)) ^ 01)) // complement the node +#define Cloud_NotCond(p,c) ((CloudNode*)(((PORT_PTRUINT_T)(p)) ^ (c))) // complement the node conditionally +#define Cloud_IsComplement(p) ((int)(((PORT_PTRUINT_T)(p)) & 01)) // check if complemented // checking constants (using node) #define Cloud_IsConstant(p) (((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX) #define cloudIsConstant(p) (((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX) @@ -204,9 +202,9 @@ struct cloudCacheEntry3 // the three-argument cache #define cloudNodeIsMarked(p) ((int)((p)->v & CLOUD_MARK_ON)) // cache lookups and inserts (using node) -#define cloudCacheLookup1(p,sign,f) (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (CLOUD_VOID)) -#define cloudCacheLookup2(p,sign,f,g) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (CLOUD_VOID)) -#define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (CLOUD_VOID)) +#define cloudCacheLookup1(p,sign,f) (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (0)) +#define cloudCacheLookup2(p,sign,f,g) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (0)) +#define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (0)) // cache inserts #define cloudCacheInsert1(p,sign,f,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->r = (r))) #define cloudCacheInsert2(p,sign,f,g,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->r = (r))) |