Version abc80301

3 files changed, 54 insertions, 0 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index cc64b024..48588eb2 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -297,6 +297,7 @@ extern int                 Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t *
 extern int                 Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots );
 extern void                Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots );
 extern Aig_Man_t *         Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots );
+extern void                Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots );
 /*=== fraImp.c ========================================================*/
 extern Vec_Int_t *         Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
 extern void                Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index 4a3f9b03..222f5bcc 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -420,6 +420,49 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots )
     return pNew;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Assumes one-hot implications in the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+**********************************************************************/
+void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots )
+{
+    Vec_Int_t * vGroup;
+    Aig_Obj_t * pObj1, * pObj2;
+    int k, i, j, Out1, Out2, pLits[2];
+    //
+    // these constrants should be added to different timeframes!
+    // (also note that PIs follow first - then registers)
+    //
+    Vec_PtrForEachEntry( vOnehots, vGroup, k )
+    {
+        Vec_IntForEachEntry( vGroup, Out1, i )
+        Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 )
+        {
+            pObj1 = Aig_ManPi( p->pManFraig, Out1 );
+            pObj2 = Aig_ManPi( p->pManFraig, Out2 );
+            pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 );
+            pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 );
+            // add contraint to solver
+            if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
+            {
+                printf( "Fra_OneHotAddKnownConstraint(): Adding clause makes SAT solver unsat.\n" );
+                sat_solver_delete( p->pSat );
+                p->pSat = NULL;
+                return;
+            }
+        }
+    }
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 0715524e..7e0d080c 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -253,6 +253,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
     int * pMapBack;
     int i, nCountPis, nCountRegs;
     int nClasses, nPartSize, fVerbose;
+    int clk = clock();
 
     // save parameters
     nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
@@ -281,6 +282,9 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
     Vec_PtrForEachEntry( vResult, vPart, i )
     {
         pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
+        // create the projection of 1-hot registers
+        if ( pAig->vOnehots )
+            pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
         // run SSW
         pNew = Fra_FraigInduction( pTemp, pPars );
         nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
@@ -299,6 +303,10 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
     Vec_VecFree( (Vec_Vec_t *)vResult );
     pPars->nPartSize = nPartSize;
     pPars->fVerbose = fVerbose;
+    if ( fVerbose )
+    {
+        PRT( "Total time", clock() - clk );
+    }
     return pNew;
 }
 
@@ -485,6 +493,8 @@ p->timeTrav += clock() - clk2;
         // add one-hotness clauses
         if ( p->pPars->fUse1Hot )
             Fra_OneHotAssume( p, p->vOneHots );
+//        if ( p->pManAig->vOnehots )
+//            Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots );
 
         // report the intermediate results
         if ( pPars->fVerbose )