From 9ebcd9eca983890738bc76f84f4e276a9cb693d7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 4 Jul 2012 14:53:07 -0700 Subject: Various changes to enable sensitization-based refinement in &gla. --- src/proof/fra/fraClaus.c | 4 ++-- src/proof/pdr/pdrCnf.c | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'src/proof') diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c index 571cc510..f651b0ad 100644 --- a/src/proof/fra/fraClaus.c +++ b/src/proof/fra/fraClaus.c @@ -637,7 +637,7 @@ ABC_PRT( "Lat-cla", clock() - clk ); // generate cuts for all nodes, assign cost, and find best cuts clk = clock(); - pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 1 ); + pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 ); // pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 ); if ( p->fVerbose ) { @@ -771,7 +771,7 @@ if ( p->fVerbose ) // generate cuts for all nodes, assign cost, and find best cuts clk = clock(); -// pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 1 ); +// pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 ); pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose ); if ( p->fVerbose ) { diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c index 2b039c01..66bea130 100644 --- a/src/proof/pdr/pdrCnf.c +++ b/src/proof/pdr/pdrCnf.c @@ -300,7 +300,7 @@ static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p, assert( pSat ); if ( p->pCnf2 == NULL ) { - p->pCnf2 = Cnf_DeriveOther( p->pAig ); + p->pCnf2 = Cnf_DeriveOther( p->pAig, 0 ); p->pvId2Vars = ABC_CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAig) ); p->vVar2Ids = Vec_PtrAlloc( 256 ); } -- cgit v1.2.3