summaryrefslogtreecommitdiffstats
path: root/src/proof/cec/cecPat.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/cec/cecPat.c')
-rw-r--r--src/proof/cec/cecPat.c28
1 files changed, 18 insertions, 10 deletions
diff --git a/src/proof/cec/cecPat.c b/src/proof/cec/cecPat.c
index c175eaa7..91a0c941 100644
--- a/src/proof/cec/cecPat.c
+++ b/src/proof/cec/cecPat.c
@@ -360,20 +360,21 @@ void Cec_ManPatSavePattern( Cec_ManPat_t * pMan, Cec_ManSat_t * p, Gia_Obj_t *
{
Vec_Int_t * vPat;
int nPatLits;
- abctime clk, clkTotal = Abc_Clock();
+ abctime clkTotal = Abc_Clock();
+// abctime clk;
assert( Gia_ObjIsCo(pObj) );
pMan->nPats++;
pMan->nPatsAll++;
// compute values in the cone of influence
-clk = Abc_Clock();
+//clk = Abc_Clock();
Gia_ManIncrementTravId( p->pAig );
nPatLits = Cec_ManPatComputePattern_rec( p, p->pAig, Gia_ObjFanin0(pObj) );
assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 1 );
pMan->nPatLits += nPatLits;
pMan->nPatLitsAll += nPatLits;
-pMan->timeFind += Abc_Clock() - clk;
+//pMan->timeFind += Abc_Clock() - clk;
// compute sensitizing path
-clk = Abc_Clock();
+//clk = Abc_Clock();
Vec_IntClear( pMan->vPattern1 );
Gia_ManIncrementTravId( p->pAig );
Cec_ManPatComputePattern1_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern1 );
@@ -385,19 +386,26 @@ clk = Abc_Clock();
vPat = Vec_IntSize(pMan->vPattern1) < Vec_IntSize(pMan->vPattern2) ? pMan->vPattern1 : pMan->vPattern2;
pMan->nPatLitsMin += Vec_IntSize(vPat);
pMan->nPatLitsMinAll += Vec_IntSize(vPat);
-pMan->timeShrink += Abc_Clock() - clk;
+//pMan->timeShrink += Abc_Clock() - clk;
// verify pattern using ternary simulation
-clk = Abc_Clock();
- Cec_ManPatVerifyPattern( p->pAig, pObj, vPat );
-pMan->timeVerify += Abc_Clock() - clk;
+//clk = Abc_Clock();
+// Cec_ManPatVerifyPattern( p->pAig, pObj, vPat );
+//pMan->timeVerify += Abc_Clock() - clk;
// sort pattern
-clk = Abc_Clock();
+//clk = Abc_Clock();
Vec_IntSort( vPat, 0 );
-pMan->timeSort += Abc_Clock() - clk;
+//pMan->timeSort += Abc_Clock() - clk;
// save pattern
Cec_ManPatStore( pMan, vPat );
pMan->timeTotal += Abc_Clock() - clkTotal;
}
+void Cec_ManPatSavePatternCSat( Cec_ManPat_t * pMan, Vec_Int_t * vPat )
+{
+ // sort pattern
+ Vec_IntSort( vPat, 0 );
+ // save pattern
+ Cec_ManPatStore( pMan, vPat );
+}
/**Function*************************************************************