New SAT-based optimization package.

src/opt/sbd/sbdWin.c

@@ -46,46 +46,62 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
+sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
 {
     Gia_Obj_t * pObj;
-    int i, iObj, Fan0, Fan1, Node, fCompl0, fCompl1, RetValue;
+    int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue;
+    int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo);
     int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
+    //Vec_IntPrint( vWinObjs );
+    //Vec_IntPrint( vTfo );
+    //Vec_IntPrint( vRoots );
     // create SAT solver
     if ( pSat == NULL )
         pSat = sat_solver_new();
     else
         sat_solver_restart( pSat );
     sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + 32 );
+    // create constant 0 clause
+    sat_solver_addclause( pSat, &iLit, &iLit + 1 );
     // add clauses for all nodes
-    Vec_IntForEachEntry( vWinObjs, iObj, i )
+    Vec_IntForEachEntryStart( vWinObjs, iObj, i, 1 )
     {
         pObj = Gia_ManObj( p, iObj );
         if ( Gia_ObjIsCi(pObj) )
             continue;
         assert( Gia_ObjIsAnd(pObj) );
+        assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
         Node = Vec_IntEntry( vObj2Var, iObj );
-        Fan0 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId0(pObj, iObj) );
-        Fan1 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId1(pObj, iObj) );
-        fCompl0 = Gia_ObjFaninC0(pObj);
-        fCompl1 = Gia_ObjFaninC1(pObj);
+        Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+        Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
+        Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
+        Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
+        Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
+        Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
+        fCompl0 = Gia_ObjFaninC0(pObj) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
+        fCompl1 = Gia_ObjFaninC1(pObj) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
         if ( Gia_ObjIsXor(pObj) )
             sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
         else
             sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 );
     }
     // add second clauses for the TFO
-    Vec_IntForEachEntryStart( vWinObjs, iObj, i, Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo) )
+    Vec_IntForEachEntryStart( vWinObjs, iObj, i, TfoStart )
     {
         pObj = Gia_ManObj( p, iObj );
         assert( Gia_ObjIsAnd(pObj) );
+        assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
         Node = Vec_IntEntry( vObj2Var, iObj ) + Vec_IntSize(vTfo);
-        Fan0 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId0(pObj, iObj) );
-        Fan1 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId1(pObj, iObj) );
-        Fan0 = Fan0 <= PivotVar ? Fan0 : Fan0 + Vec_IntSize(vTfo);
-        Fan1 = Fan1 <= PivotVar ? Fan1 : Fan1 + Vec_IntSize(vTfo);
-        fCompl0 = Gia_ObjFaninC0(pObj) ^ (Fan0 == PivotVar);
-        fCompl1 = Gia_ObjFaninC1(pObj) ^ (Fan1 == PivotVar);
+        Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+        Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
+        Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
+        Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
+        Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
+        Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
+        Fan0 = Fan0 < TfoStart ? Fan0 : Fan0 + Vec_IntSize(vTfo);
+        Fan1 = Fan1 < TfoStart ? Fan1 : Fan1 + Vec_IntSize(vTfo);
+        fCompl0 = Gia_ObjFaninC0(pObj) ^ (Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
+        fCompl1 = Gia_ObjFaninC1(pObj) ^ (Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
         if ( Gia_ObjIsXor(pObj) )
             sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
         else
@@ -98,8 +114,9 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, int Pivot, Vec_
         Vec_Int_t * vFaninVars = Vec_IntAlloc( Vec_IntSize(vRoots) );
         Vec_IntForEachEntry( vRoots, iObj, i )
         {
-            Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) );
+            assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
             Node = Vec_IntEntry( vObj2Var, iObj );
+            Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) );
             sat_solver_add_xor( pSat, Node, Node + Vec_IntSize(vTfo), nVars++, 0 );
         }
         // make OR clause for the last nRoots variables
@@ -190,6 +207,50 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
     return SBD_SAT_SAT;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns a bunch of positive/negative random care minterms.]
+
+  Description [Returns 0/1 if the functions is const 0/1.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void sat_solver_random_polarity(sat_solver* s)
+{
+    int i, k;
+    for ( i = 0; i < s->size; i += 64 )
+    {
+        word Polar = Gia_ManRandomW(0);
+        for ( k = 0; k < 64 && (i << 6) + k < s->size; k++ )
+            s->polarity[(i << 6) + k] = Abc_TtGetBit(&Polar, k);
+    }
+}
+int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds )
+{
+    int nBTLimit = 0;
+    int i, Ind; 
+    assert( Vec_IntSize(vInds) == nCareMints[0] + nCareMints[1] );
+    Vec_IntForEachEntry( vInds, Ind, i )
+    {
+        int fOffSet = (int)(i < nCareMints[0]);
+        int status, k, iLit = Abc_Var2Lit( PivotVar, fOffSet );
+        sat_solver_random_polarity( pSat );
+        status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            return -2;
+        if ( status == l_False )
+            return fOffSet;
+        for ( k = 0; k <= PivotVar; k++ )
+            if ( Abc_TtGetBit(pVarSims[k], Ind) != sat_solver_var_value(pSat, k) )
+                Abc_TtXorBit(pVarSims[k], Ind);
+    }
+    return -1;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////