summaryrefslogtreecommitdiffstats
path: root/src/proof/dch/dchSimSat.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/dch/dchSimSat.c')
-rw-r--r--src/proof/dch/dchSimSat.c258
1 files changed, 258 insertions, 0 deletions
diff --git a/src/proof/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c
new file mode 100644
index 00000000..808e754a
--- /dev/null
+++ b/src/proof/dch/dchSimSat.c
@@ -0,0 +1,258 @@
+/**CFile****************************************************************
+
+ FileName [dchSimSat.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Choice computation for tech-mapping.]
+
+ Synopsis [Performs resimulation using counter-examples.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 29, 2008.]
+
+ Revision [$Id: dchSimSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Collects internal nodes in the reverse DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pFanout, * pRepr;
+ int iFanout = -1, i;
+ assert( !Aig_IsComplement(pObj) );
+ if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
+ // traverse the fanouts
+ Aig_ObjForEachFanout( p->pAigTotal, pObj, pFanout, iFanout, i )
+ Dch_ManCollectTfoCands_rec( p, pFanout );
+ // check if the given node has a representative
+ pRepr = Aig_ObjRepr( p->pAigTotal, pObj );
+ if ( pRepr == NULL )
+ return;
+ // pRepr is the constant 1 node
+ if ( pRepr == Aig_ManConst1(p->pAigTotal) )
+ {
+ Vec_PtrPush( p->vSimRoots, pObj );
+ return;
+ }
+ // pRepr is the representative of an equivalence class
+ if ( pRepr->fMarkA )
+ return;
+ pRepr->fMarkA = 1;
+ Vec_PtrPush( p->vSimClasses, pRepr );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collect equivalence classes and const1 cands in the TFO.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Vec_PtrClear( p->vSimRoots );
+ Vec_PtrClear( p->vSimClasses );
+ Aig_ManIncrementTravId( p->pAigTotal );
+ Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
+ Dch_ManCollectTfoCands_rec( p, pObj1 );
+ Dch_ManCollectTfoCands_rec( p, pObj2 );
+ Vec_PtrSort( p->vSimRoots, (int (*)(void))Aig_ObjCompareIdIncrease );
+ Vec_PtrSort( p->vSimClasses, (int (*)(void))Aig_ObjCompareIdIncrease );
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pObj, i )
+ pObj->fMarkA = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resimulates the cone of influence of the solved nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
+{
+ if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ Aig_Obj_t * pObjFraig;
+ int nVarNum;
+ pObjFraig = Dch_ObjFraig( pObj );
+ assert( !Aig_IsComplement(pObjFraig) );
+ nVarNum = Dch_ObjSatNum( p, pObjFraig );
+ // get the value from the SAT solver
+ // (account for the fact that some vars may be minimized away)
+ pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
+// pObj->fMarkB = !nVarNum? Aig_ManRandom(0) & 1 : sat_solver_var_value( p->pSat, nVarNum );
+ return;
+ }
+ Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
+ Dch_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj) );
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+ & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+ // count the cone size
+ if ( Dch_ObjSatNum( p, Aig_Regular(Dch_ObjFraig(pObj)) ) > 0 )
+ p->nConeThis++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resimulates the cone of influence of the other nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
+{
+ if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ // set random value
+ pObj->fMarkB = Aig_ManRandom(0) & 1;
+ return;
+ }
+ Dch_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
+ Dch_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
+ pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+ & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Handle the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+ Aig_Obj_t * pRoot, ** ppClass;
+ int i, k, nSize, RetValue1, RetValue2, clk = clock();
+ // get the equivalence classes
+ Dch_ManCollectTfoCands( p, pObj, pRepr );
+ // resimulate the cone of influence of the solved nodes
+ p->nConeThis = 0;
+ Aig_ManIncrementTravId( p->pAigTotal );
+ Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
+ Dch_ManResimulateSolved_rec( p, pObj );
+ Dch_ManResimulateSolved_rec( p, pRepr );
+ p->nConeMax = Abc_MaxInt( p->nConeMax, p->nConeThis );
+ // resimulate the cone of influence of the other nodes
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
+ Dch_ManResimulateOther_rec( p, pRoot );
+ // refine these nodes
+ RetValue1 = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
+ // resimulate the cone of influence of the cand classes
+ RetValue2 = 0;
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pRoot, i )
+ {
+ ppClass = Dch_ClassesReadClass( p->ppClasses, pRoot, &nSize );
+ for ( k = 0; k < nSize; k++ )
+ Dch_ManResimulateOther_rec( p, ppClass[k] );
+ // refine this class
+ RetValue2 += Dch_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
+ }
+ // make sure refinement happened
+ if ( Aig_ObjIsConst1(pRepr) )
+ assert( RetValue1 );
+ else
+ assert( RetValue2 );
+p->timeSimSat += clock() - clk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Handle the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+ Aig_Obj_t * pRoot;
+ int i, RetValue, clk = clock();
+ // get the equivalence class
+ if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
+ Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots );
+ else
+ Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vSimRoots );
+ // resimulate the cone of influence of the solved nodes
+ p->nConeThis = 0;
+ Aig_ManIncrementTravId( p->pAigTotal );
+ Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
+ Dch_ManResimulateSolved_rec( p, pObj );
+ Dch_ManResimulateSolved_rec( p, pRepr );
+ p->nConeMax = Abc_MaxInt( p->nConeMax, p->nConeThis );
+ // resimulate the cone of influence of the other nodes
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
+ Dch_ManResimulateOther_rec( p, pRoot );
+ // refine this class
+ if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
+ RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
+ else
+ RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 );
+ assert( RetValue );
+p->timeSimSat += clock() - clk;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 19:04:34 +0000