summaryrefslogtreecommitdiffstats
path: root/src/aig/saig
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-06-24 18:45:42 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-06-24 18:45:42 -0700
commit7629fd6aea2ff9cf27c16b235da7d90bec0f3e7e (patch)
treec1c899e41b24c4cf239e8ed5b3dbb7727376fc93 /src/aig/saig
parent2f64033b3767ffdb16d8a530d813e39ee53b6e73 (diff)
downloadabc-7629fd6aea2ff9cf27c16b235da7d90bec0f3e7e.tar.gz
abc-7629fd6aea2ff9cf27c16b235da7d90bec0f3e7e.tar.bz2
abc-7629fd6aea2ff9cf27c16b235da7d90bec0f3e7e.zip
Added min-cut-based refinement of gate-level abstraction (command &gla_refine).
Diffstat (limited to 'src/aig/saig')
-rw-r--r--src/aig/saig/saigAbsCba.c2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 7863069f..55a429e1 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -761,11 +761,13 @@ if ( fVerbose )
printf( "Care " );
Abc_CexPrintStats( pCare );
}
+/*
// verify the reduced counter-example using ternary simulation
if ( !Saig_ManCexVerifyUsingTernary( pAig, pCex, pCare ) )
printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification has failed!!!\n" );
else if ( fVerbose )
printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification is successful.\n" );
+*/
Aig_ManCleanMarkAB( pAig );
return pCare;
}