diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-28 22:21:05 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-28 22:21:05 -0700 |
| commit | cc7d3e3747f0e1f397945eaac63120401a49d5c1 (patch) | |
| tree | 1216020a1eb9bc26ae2843c658e5a973c908ae9a /src/base/abci/abcQbf.c | |
| parent | b7cd22786ed2643d3730ec5d8a5f2fbb30393be6 (diff) | |
| download | abc-cc7d3e3747f0e1f397945eaac63120401a49d5c1.tar.gz abc-cc7d3e3747f0e1f397945eaac63120401a49d5c1.tar.bz2 abc-cc7d3e3747f0e1f397945eaac63120401a49d5c1.zip | |
Added dumping QDIMACS files in command 'qbf'.
Diffstat (limited to 'src/base/abci/abcQbf.c')
| -rw-r--r-- | src/base/abci/abcQbf.c | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c index 0731d23f..e64871ff 100644 --- a/src/base/abci/abcQbf.c +++ b/src/base/abci/abcQbf.c @@ -75,39 +75,41 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fDumpCnf, int f // assert( Abc_NtkPiNum(pNtk)-nPars < 32 ); nInputs = Abc_NtkPiNum(pNtk) - nPars; - Abc_ObjXorFaninC( Abc_NtkPo(pNtk,0), 0 ); if ( fDumpCnf ) { + // original problem: \exists p \forall x \exists y. M(p,x,y) + // negated problem: \forall p \exists x \exists y. !M(p,x,y) extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pMan = Abc_NtkToDar( pNtk, 0, 0 ); - Cnf_Dat_t * pCnf = Cnf_DeriveSimple( pMan, 0 ); + Cnf_Dat_t * pCnf = Cnf_Derive( pMan, 0 ); Vec_Int_t * vVarMap, * vForAlls, * vExists; Aig_Obj_t * pObj; + char * pFileName; int i, Entry; // create var map vVarMap = Vec_IntStart( pCnf->nVars ); Aig_ManForEachCi( pMan, pObj, i ) - if ( i >= nPars ) + if ( i < nPars ) Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Aig_ObjId(pObj)], 1 ); // create various maps + vForAlls = Vec_IntAlloc( nPars ); vExists = Vec_IntAlloc( Abc_NtkPiNum(pNtk) - nPars ); - vForAlls = Vec_IntAlloc( pCnf->nVars ); Vec_IntForEachEntry( vVarMap, Entry, i ) if ( Entry ) - Vec_IntPush( vExists, i ); - else Vec_IntPush( vForAlls, i ); + else + Vec_IntPush( vExists, i ); // generate CNF - Cnf_DataWriteIntoFile( pCnf, "test.qdimacs", 0, vForAlls, vExists ); + pFileName = Extra_FileNameGenericAppend( pNtk->pSpec, ".qdimacs" ); + Cnf_DataWriteIntoFile( pCnf, pFileName, 0, vForAlls, vExists ); Aig_ManStop( pMan ); Cnf_DataFree( pCnf ); Vec_IntFree( vForAlls ); Vec_IntFree( vExists ); Vec_IntFree( vVarMap ); - Abc_ObjXorFaninC( Abc_NtkPo(pNtk,0), 0 ); + printf( "The 2QBF formula was written into file \"%s\".\n", pFileName ); return; } - Abc_ObjXorFaninC( Abc_NtkPo(pNtk,0), 0 ); // initialize the synthesized network with 0000-combination vPiValues = Vec_IntStart( Abc_NtkPiNum(pNtk) ); |