Experiments with SAT sweeping.

3 files changed, 79 insertions, 24 deletions

diff --git a/src/proof/cec/cecSat.c b/src/proof/cec/cecSat.c
index 025668d3..fc53d503 100644
--- a/src/proof/cec/cecSat.c
+++ b/src/proof/cec/cecSat.c
@@ -61,6 +61,7 @@ struct Cec2_Man_t_
     Vec_Int_t *      vObjSatPairs;   // nodes
     Vec_Int_t *      vCexTriples;    // nodes
     // statistics
+    int              nPatterns;
     int              nSatSat;
     int              nSatUnsat;
     int              nSatUndec;
@@ -100,7 +101,7 @@ void Cec2_SetDefaultParams( Cec2_Par_t * p )
     p->nItersMax      =      10;    // max number of iterations
     p->nConfLimit     =    1000;    // conflict limit at a node
     p->fIsMiter       =       0;    // this is a miter
-    p->fUseCones      =       0;     // use logic cones
+    p->fUseCones      =       0;    // use logic cones
     p->fVeryVerbose   =       0;    // verbose stats
     p->fVerbose       =       0;    // verbose stats
 }  
@@ -487,18 +488,18 @@ void Cec2_ManSaveCis( Gia_Man_t * p )
         Gia_ManForEachCiId( p, Id, i )
             Vec_WrdPush( p->vSimsPi, Cec2_ObjSim(p, Id)[w] );
 }
-void Cec2_ManSimulate( Gia_Man_t * p, Vec_Int_t * vTriples, Cec2_Man_t * pMan )
+int Cec2_ManSimulate( Gia_Man_t * p, Vec_Int_t * vTriples, Cec2_Man_t * pMan )
 {
     extern void Cec2_ManSimClassRefineOne( Gia_Man_t * p, int iRepr );
     abctime clk = Abc_Clock();
     Gia_Obj_t * pObj; 
-    int i, iRepr, iObj, Entry;
+    int i, iRepr, iObj, Entry, Count = 0;
     //Cec2_ManSaveCis( p );
     Gia_ManForEachAnd( p, pObj, i )
         Cec2_ObjSimAnd( p, i );
     pMan->timeSim += Abc_Clock() - clk;
     if ( p->pReprs == NULL )
-        return;
+        return 0;
     if ( vTriples )
     {
         Vec_IntForEachEntryTriple( vTriples, iRepr, iObj, Entry, i )
@@ -508,13 +509,17 @@ void Cec2_ManSimulate( Gia_Man_t * p, Vec_Int_t * vTriples, Cec2_Man_t * pMan )
             int iPat     = Abc_Lit2Var(Entry);
             int fPhase   = Abc_LitIsCompl(Entry);
             if ( (fPhase ^ Abc_InfoHasBit((unsigned *)pSim0, iPat)) == Abc_InfoHasBit((unsigned *)pSim1, iPat) )
-                printf( "ERROR:  Pattern %d did not disprove pair %d and %d.\n", iPat, iRepr, iObj );
+            {
+                //printf( "ERROR:  Pattern %d did not disprove pair %d and %d.\n", iPat, iRepr, iObj );
+                Count++;
+            }
         }
     }
     clk = Abc_Clock();
     Gia_ManForEachClass0( p, i )
         Cec2_ManSimClassRefineOne( p, i );
     pMan->timeRefine += Abc_Clock() - clk;
+    return Count;
 }
 void Cec2_ManSimAlloc( Gia_Man_t * p, int nWords )
 {
@@ -677,6 +682,7 @@ Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars )
     p->vSatVars     = Vec_IntAlloc( 100 );
     p->vObjSatPairs = Vec_IntAlloc( 100 );
     p->vCexTriples  = Vec_IntAlloc( 100 );
+    p->pSat->opts.conf_limit = pPars->nConfLimit;
     // remember pointer to the solver in the AIG manager
     pAig->pData     = p->pSat;
     return p;
@@ -849,12 +855,13 @@ int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj )
     if ( status == SATOKO_SAT )
     {
         p->nSatSat++;
+        p->nPatterns++;
         p->pAig->iPatsPi = (p->pAig->iPatsPi == 64 * p->pAig->nSimWords - 1) ? 1 : p->pAig->iPatsPi + 1;
         assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
         Vec_IntForEachEntryDouble( p->vObjSatPairs, IdAig, IdSat, i )
             Cec2_ObjSimSetInputBit( p->pAig, IdAig, var_polarity(p->pSat, IdSat) == LIT_TRUE );
-        RetValue = 0;
         p->timeSatSat += Abc_Clock() - clk;
+        RetValue = 0;
     }
     else if ( status == SATOKO_UNSAT )
     {
@@ -862,14 +869,15 @@ int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj )
         pObj->Value = Abc_LitNotCond( pRepr->Value, fCompl );
         Gia_ObjSetProved( p->pAig, iObj );
         p->timeSatUnsat += Abc_Clock() - clk;
+        RetValue = 1;
     }
     else 
     {
         p->nSatUndec++;
         assert( status == SATOKO_UNDEC );
         Gia_ObjSetFailed( p->pAig, iObj );
-        assert( 0 );
         p->timeSatUndec += Abc_Clock() - clk;
+        RetValue = 2;
     }
     if ( p->pPars->fUseCones )
         return RetValue;
@@ -895,6 +903,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
     int i, Iter, fDisproved = 1;
 
     // check if any output trivially fails under all-0 pattern
+    Gia_ManRandomW( 1 );
     Gia_ManSetPhase( p );
     if ( pPars->fIsMiter ) 
     {
@@ -902,7 +911,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
             if ( pObj->fPhase )
             {
                 p->pCexSeq = Cec2_ManDeriveCex( p, i, -1 );
-                return 0;
+                goto finalize;
             }
     }
 
@@ -911,7 +920,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
     Cec2_ManSimulateCis( p );
     Cec2_ManSimulate( p, NULL, pMan );
     if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected
-        return 0;
+        goto finalize;
     Cec2_ManCreateClasses( p, pMan );
     Cec2_ManPrintStats( p, pPars, pMan );
 
@@ -921,7 +930,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
         Cec2_ManSimulateCis( p );
         Cec2_ManSimulate( p, NULL, pMan );
         if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected
-            return 0;
+            goto finalize;
         Cec2_ManPrintStats( p, pPars, pMan );
     }
     // perform sweeping
@@ -929,14 +938,12 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
     for ( Iter = 0; fDisproved && Iter < pPars->nItersMax; Iter++ )
     {
         fDisproved = 0;
+        pMan->nPatterns = 0;
         Cec2_ManSimulateCis( p );
         Vec_IntClear( pMan->vCexTriples );
         Gia_ManForEachAnd( p, pObj, i )
         {
-            pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 || Gia_ObjFanin1(pObj)->fMark1;
-            if ( pObj->fMark1 ) // skip nodes in the TFO of a disproved one
-                continue;
-            if ( ~pObj->Value ) // skip swept nodes
+            if ( ~pObj->Value || Gia_ObjFailed(p, i) ) // skip swept nodes and failed nodes
                 continue;
             if ( !~Gia_ObjFanin0(pObj)->Value || !~Gia_ObjFanin1(pObj)->Value ) // skip fanouts of non-swept nodes
                 continue;
@@ -952,7 +959,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
             }
             assert( Vec_IntSize(&pMan->pNew->vCopies) == Gia_ManObjNum(pMan->pNew) );
             pRepr = Gia_ObjReprObj( p, i );
-            if ( pRepr == NULL || pRepr->fMark1 || !~pRepr->Value )
+            if ( pRepr == NULL || !~pRepr->Value )
                 continue;
             if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
             {
@@ -964,18 +971,13 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
                 continue;
             pObj->Value = ~0;
             Vec_IntPushThree( pMan->vCexTriples, Gia_ObjId(p, pRepr), i, Abc_Var2Lit(p->iPatsPi, pObj->fPhase ^ pRepr->fPhase) );
-            // mark nodes as disproved
             fDisproved = 1;
-            //if ( Iter > 5 )
-                continue;
-            if ( Gia_ObjIsAnd(pRepr) )
-                pRepr->fMark1 = 1;
-            pObj->fMark1 = 1;
         }
         if ( fDisproved )
         {
-            //printf( "The number of pattern = %d.\n", p->iPatsPi );
-            Cec2_ManSimulate( p, pMan->vCexTriples, pMan );
+            int Fails = Cec2_ManSimulate( p, pMan->vCexTriples, pMan );
+            if ( Fails && pPars->fVerbose )
+                printf( "Failed to resimulate %d times with pattern = %d  (total = %d).\n", Fails, pMan->nPatterns, pPars->nSimWords * 64 );
             if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected
                 break;
         }
@@ -993,6 +995,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN
         (*ppNew)->pName = Abc_UtilStrsav( p->pName );
         (*ppNew)->pSpec = Abc_UtilStrsav( p->pSpec );
     }
+finalize:
     Cec2_ManDestroy( pMan );
     //Gia_ManEquivPrintClasses( p, 1, 0 );
     return p->pCexSeq ? 0 : 1;
diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c
index c00723bc..6e5fd221 100644
--- a/src/proof/cec/cecSynth.c
+++ b/src/proof/cec/cecSynth.c
@@ -372,6 +372,58 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Gia_ManTestOnePair_rec( sat_solver * pSat, Gia_Man_t * p, int iObj, Vec_Int_t * vSatVar )
+{
+    Gia_Obj_t * pObj; 
+    int iVar, iVar0, iVar1;
+    if ( Vec_IntEntry(vSatVar, iObj) >= 0 )
+        return Vec_IntEntry(vSatVar, iObj);
+    iVar = sat_solver_addvar(pSat);
+    Vec_IntWriteEntry( vSatVar, iObj, iVar );
+    pObj = Gia_ManObj( p, iObj );
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        iVar0 = Gia_ManTestOnePair_rec( pSat, p, Gia_ObjFaninId0(pObj, iObj), vSatVar );
+        iVar1 = Gia_ManTestOnePair_rec( pSat, p, Gia_ObjFaninId1(pObj, iObj), vSatVar );
+        sat_solver_add_and( pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
+    }
+    return iVar;
+}
+int Gia_ManTestOnePair( Gia_Man_t * p, int iObj1, int iObj2, int fPhase )
+{
+    int Lits[2] = {1}, status;
+    sat_solver * pSat = sat_solver_new();
+    Vec_Int_t * vSatVar = Vec_IntStartFull( Gia_ManObjNum(p) );
+    Vec_IntWriteEntry( vSatVar, 0, sat_solver_addvar(pSat) );
+    sat_solver_addclause( pSat, Lits, Lits + 1 );
+    Gia_ManTestOnePair_rec( pSat, p, iObj1, vSatVar );
+    Gia_ManTestOnePair_rec( pSat, p, iObj2, vSatVar );
+    Lits[0] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj1), 1 );
+    Lits[1] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj2), fPhase );
+    status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 );
+    if ( status == l_False )
+    {
+        Lits[0] = Abc_LitNot( Lits[0] );
+        Lits[1] = Abc_LitNot( Lits[1] );
+        status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 );
+    }
+    Vec_IntFree( vSatVar );
+    sat_solver_delete( pSat );
+    return status;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 368ece2f..a72e39f7 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -639,7 +639,7 @@ char solver_search(solver_t *s)
             /* No conflict */
             unsigned next_lit;
 
-            if (solver_rst(s)) {
+            if (solver_rst(s) || solver_check_limits(s) == 0) {
                 b_queue_clean(s->bq_lbd);
                 solver_cancel_until(s, 0);
                 return SATOKO_UNDEC;