Commit c20f1dcc by Alan Mishchenko

Another way of dumping QBF problem into a file (bug fix).

parent 6e6c728b
...@@ -499,8 +499,8 @@ void Gia_QbfDumpFileInv( Gia_Man_t * pGia, int nPars ) ...@@ -499,8 +499,8 @@ void Gia_QbfDumpFileInv( Gia_Man_t * pGia, int nPars )
Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Gia_ManCiIdToId(pGia, i)], i < nPars ? 1 : 2 ); Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Gia_ManCiIdToId(pGia, i)], i < nPars ? 1 : 2 );
// create various maps // create various maps
vExists1 = Vec_IntAlloc( nPars ); vExists1 = Vec_IntAlloc( nPars );
vForAlls = Vec_IntAlloc( nPars ); vForAlls = Vec_IntAlloc( Gia_ManCiNum(pGia) - nPars );
vExists2 = Vec_IntAlloc( Gia_ManCiNum(pGia) - 2*nPars ); vExists2 = Vec_IntAlloc( pCnf->nVars - Gia_ManCiNum(pGia) );
Vec_IntForEachEntry( vVarMap, Entry, i ) Vec_IntForEachEntry( vVarMap, Entry, i )
if ( Entry == 1 ) if ( Entry == 1 )
Vec_IntPush( vExists1, i ); Vec_IntPush( vExists1, i );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment