summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-07-04 00:11:47 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-07-04 00:11:47 -0700
commit7fd65344929ef70f36be9f9b73529c084f8b7a50 (patch)
treefc8955e3817d18cee265643e432749a89ff07da3 /src/sat
parent500c76d213b829a7729d717a09704d6197a37e1b (diff)
downloadabc-7fd65344929ef70f36be9f9b73529c084f8b7a50.tar.gz
abc-7fd65344929ef70f36be9f9b73529c084f8b7a50.tar.bz2
abc-7fd65344929ef70f36be9f9b73529c084f8b7a50.zip
Performance improvement in &gla.
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/cnf/cnf.h1
-rw-r--r--src/sat/cnf/cnfCore.c1
-rw-r--r--src/sat/cnf/cnfMan.c1
3 files changed, 3 insertions, 0 deletions
diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h
index 0b6fc8c2..54aaf5ca 100644
--- a/src/sat/cnf/cnf.h
+++ b/src/sat/cnf/cnf.h
@@ -64,6 +64,7 @@ struct Cnf_Dat_t_
int * pVarNums; // the number of CNF variable for each node ID (-1 if unused)
int * pObj2Clause; // the mapping of objects into clauses
int * pObj2Count; // the mapping of objects into clause number
+ Vec_Int_t * vMapping; // mapping of internal nodes
};
// the cut used to represent node in the AIG
diff --git a/src/sat/cnf/cnfCore.c b/src/sat/cnf/cnfCore.c
index eb46e704..d1dd8561 100644
--- a/src/sat/cnf/cnfCore.c
+++ b/src/sat/cnf/cnfCore.c
@@ -180,6 +180,7 @@ clk = clock();
Cnf_ManTransferCuts( p );
vMapped = Cnf_ManScanMapping( p, 1, 1 );
pCnf = Cnf_ManWriteCnfOther( p, vMapped );
+ pCnf->vMapping = Cnf_ManWriteCnfMapping( p, vMapped );
Vec_PtrFree( vMapped );
Aig_MmFixedStop( pMemCuts, 0 );
p->timeSave = clock() - clk;
diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c
index a4081f86..c3099d1e 100644
--- a/src/sat/cnf/cnfMan.c
+++ b/src/sat/cnf/cnfMan.c
@@ -181,6 +181,7 @@ void Cnf_DataFree( Cnf_Dat_t * p )
{
if ( p == NULL )
return;
+ Vec_IntFreeP( &p->vMapping );
ABC_FREE( p->pObj2Clause );
ABC_FREE( p->pObj2Count );
ABC_FREE( p->pClauses[0] );