summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-06-04 12:00:37 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2014-06-04 12:00:37 -0700
commitf2818ddb83cb405724233c62ae577cb9c78096a9 (patch)
tree462123b8d8e4cb89ec58a76582e65f8e0efca17d /src/proof
parent97bd9d8f1b1755422f65b288ee42a1d4ccb8b777 (diff)
downloadabc-f2818ddb83cb405724233c62ae577cb9c78096a9.tar.gz
abc-f2818ddb83cb405724233c62ae577cb9c78096a9.tar.bz2
abc-f2818ddb83cb405724233c62ae577cb9c78096a9.zip
Adding CEC command &splitprove.
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/cec/cecSplit.c15
1 files changed, 11 insertions, 4 deletions
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c
index 7ba3d51e..e04d6224 100644
--- a/src/proof/cec/cecSplit.c
+++ b/src/proof/cec/cecSplit.c
@@ -204,12 +204,14 @@ Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-int Gia_SplitCofVar2( Gia_Man_t * p )
+int Gia_SplitCofVar2( Gia_Man_t * p, int LookAhead )
{
+ abctime clk = Abc_Clock();
Gia_Man_t * pPart;
int * pOrder = Gia_PermuteSpecialOrder( p );
int Cost0, Cost1, CostBest = ABC_INFINITY;
- int i, iBest = -1, LookAhead = 10;
+ int i, iBest = -1;
+ LookAhead = Abc_MinInt( LookAhead, Gia_ManPiNum(p) );
for ( i = 0; i < LookAhead; i++ )
{
pPart = Gia_ManDupCofactor( p, pOrder[i], 0 );
@@ -222,9 +224,14 @@ int Gia_SplitCofVar2( Gia_Man_t * p )
if ( CostBest > Cost0 + Cost1 )
CostBest = Cost0 + Cost1, iBest = pOrder[i];
+
+// printf( "%2d : Var = %4d Refs = %3d %6d %6d -> %6d\n",
+// i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])),
+// Cost0, Cost1, Cost0+Cost1 );
}
ABC_FREE( pOrder );
assert( iBest >= 0 );
+// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return iBest;
}
@@ -359,7 +366,7 @@ void Cec_GiaSplitPrintRefs( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int fVerbose )
+int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, int fVerbose )
{
abctime clk, clkTotal = Abc_Clock();
Gia_Man_t * pPart0, * pPart1, * pLast;
@@ -387,7 +394,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int fVerbose )
pLast = (Gia_Man_t *)Vec_PtrPop( vStack );
// determine cofactoring variable
Depth = Vec_IntSize(pLast->vCofVars);
- iVar = Gia_SplitCofVar2( pLast );
+ iVar = Gia_SplitCofVar2( pLast, LookAhead );
// cofactor
pPart0 = Gia_ManDupCofactor( pLast, iVar, 0 );
// create variable