cecSatG2.c 59 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
/**CFile****************************************************************

  FileName    [cecSatG2.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Combinational equivalence checking.]

  Synopsis    [Detection of structural isomorphism.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: cecSatG2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "aig/gia/gia.h"
#include "misc/util/utilTruth.h"
#include "cec.h"

25 26 27 28 29 30
#define USE_GLUCOSE2

#ifdef USE_GLUCOSE2

#include "sat/glucose2/AbcGlucose2.h"

31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
#define sat_solver                         bmcg2_sat_solver
#define sat_solver_start                   bmcg2_sat_solver_start
#define sat_solver_stop                    bmcg2_sat_solver_stop
#define sat_solver_addclause               bmcg2_sat_solver_addclause
#define sat_solver_addvar                  bmcg2_sat_solver_addvar
#define sat_solver_read_cex_varvalue       bmcg2_sat_solver_read_cex_varvalue
#define sat_solver_reset                   bmcg2_sat_solver_reset
#define sat_solver_set_conflict_budget     bmcg2_sat_solver_set_conflict_budget
#define sat_solver_conflictnum             bmcg2_sat_solver_conflictnum
#define sat_solver_solve                   bmcg2_sat_solver_solve
#define sat_solver_read_cex_varvalue       bmcg2_sat_solver_read_cex_varvalue
#define sat_solver_read_cex                bmcg2_sat_solver_read_cex
#define sat_solver_jftr                    bmcg2_sat_solver_jftr
#define sat_solver_set_jftr                bmcg2_sat_solver_set_jftr
#define sat_solver_set_var_fanin_lit       bmcg2_sat_solver_set_var_fanin_lit
#define sat_solver_start_new_round         bmcg2_sat_solver_start_new_round
#define sat_solver_mark_cone               bmcg2_sat_solver_mark_cone
48 49 50 51 52

#else

#include "sat/glucose/AbcGlucose.h"

53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
#define sat_solver                         bmcg_sat_solver
#define sat_solver_start                   bmcg_sat_solver_start
#define sat_solver_stop                    bmcg_sat_solver_stop
#define sat_solver_addclause               bmcg_sat_solver_addclause
#define sat_solver_addvar                  bmcg_sat_solver_addvar
#define sat_solver_read_cex_varvalue       bmcg_sat_solver_read_cex_varvalue
#define sat_solver_reset                   bmcg_sat_solver_reset
#define sat_solver_set_conflict_budget     bmcg_sat_solver_set_conflict_budget
#define sat_solver_conflictnum             bmcg_sat_solver_conflictnum
#define sat_solver_solve                   bmcg_sat_solver_solve
#define sat_solver_read_cex_varvalue       bmcg_sat_solver_read_cex_varvalue
#define sat_solver_read_cex                bmcg_sat_solver_read_cex
#define sat_solver_jftr                    bmcg_sat_solver_jftr
#define sat_solver_set_jftr                bmcg_sat_solver_set_jftr
#define sat_solver_set_var_fanin_lit       bmcg_sat_solver_set_var_fanin_lit
#define sat_solver_start_new_round         bmcg_sat_solver_start_new_round
#define sat_solver_mark_cone               bmcg_sat_solver_mark_cone
70 71 72

#endif

73 74
ABC_NAMESPACE_IMPL_START

75

76 77 78 79 80 81 82 83
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

// SAT solving manager
typedef struct Cec4_Man_t_ Cec4_Man_t;
struct Cec4_Man_t_
{
84
    Cec_ParFra_t *   pPars;          // parameters
85 86 87
    Gia_Man_t *      pAig;           // user's AIG
    Gia_Man_t *      pNew;           // internal AIG
    // SAT solving
88
    sat_solver *     pSat;           // SAT solver
89 90 91 92 93
    Vec_Ptr_t *      vFrontier;      // CNF construction
    Vec_Ptr_t *      vFanins;        // CNF construction
    Vec_Int_t *      vCexMin;        // minimized CEX
    Vec_Int_t *      vClassUpdates;  // updated equiv classes
    Vec_Int_t *      vCexStamps;     // time stamps
94 95 96
    Vec_Int_t *      vCands;
    Vec_Int_t *      vVisit;
    Vec_Int_t *      vPat;
97 98 99
    Vec_Bit_t *      vFails;
    int              iPosRead;       // candidate reading position
    int              iPosWrite;      // candidate writing position
100
    int              iLastConst;     // last const node proved
101 102 103 104 105 106
    // refinement
    Vec_Int_t *      vRefClasses;
    Vec_Int_t *      vRefNodes;
    Vec_Int_t *      vRefBins;
    int *            pTable;
    int              nTableSize;
107
    // statistics
108 109 110
    int              nItersSim;
    int              nItersSat;
    int              nAndNodes;
111 112 113 114 115 116 117 118
    int              nPatterns;
    int              nSatSat;
    int              nSatUnsat;
    int              nSatUndec;
    int              nCallsSince;
    int              nSimulates;
    int              nRecycles;
    int              nConflicts[2][3];
119 120
    abctime          timeCnf;
    abctime          timeGenPats;
121 122 123 124 125 126 127 128 129 130 131 132 133
    abctime          timeSatSat0;
    abctime          timeSatUnsat0;
    abctime          timeSatSat;
    abctime          timeSatUnsat;
    abctime          timeSatUndec;
    abctime          timeSim;
    abctime          timeRefine;
    abctime          timeResimGlo;
    abctime          timeResimLoc;
    abctime          timeStart;
};

static inline int    Cec4_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj )             { return Gia_ObjCopy2Array(p, Gia_ObjId(p, pObj));                                                     }
134
static inline int    Cec4_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec4_ObjSatId(p, pObj) == -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), Num); Vec_IntPush(&p->vSuppVars, Gia_ObjId(p, pObj)); if ( Gia_ObjIsCi(pObj) ) Vec_IntPushTwo(&p->vCopiesTwo, Gia_ObjId(p, pObj), Num); assert(Vec_IntSize(&p->vVarMap) == Num); Vec_IntPush(&p->vVarMap, Gia_ObjId(p, pObj)); return Num;  }
135 136 137 138 139 140
static inline void   Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj )        { assert(Cec4_ObjSatId(p, pObj) != -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), -1);               }

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

141

142 143 144 145 146 147 148 149 150 151 152
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
153
Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
154
{
155
    Cec4_Man_t * p = ABC_CALLOC( Cec4_Man_t, 1 );
156
    memset( p, 0, sizeof(Cec4_Man_t) );
157 158 159
    p->timeStart     = Abc_Clock();
    p->pPars         = pPars;
    p->pAig          = pAig;
160 161
    p->pSat          = sat_solver_start();  
    sat_solver_set_jftr( p->pSat, pPars->jType );
162 163 164 165 166
    p->vFrontier     = Vec_PtrAlloc( 1000 );
    p->vFanins       = Vec_PtrAlloc( 100 );
    p->vCexMin       = Vec_IntAlloc( 100 );
    p->vClassUpdates = Vec_IntAlloc( 100 );
    p->vCexStamps    = Vec_IntStart( Gia_ManObjNum(pAig) );
167
    p->vCands        = Vec_IntAlloc( 100 );
168 169
    p->vVisit        = Vec_IntAlloc( 100 );
    p->vPat          = Vec_IntAlloc( 100 );
170
    p->vFails        = Vec_BitStart( Gia_ManObjNum(pAig) );
171
    //pAig->pData     = p->pSat; // point AIG manager to the solver
172 173 174 175 176 177 178 179
    return p;
}
void Cec4_ManDestroy( Cec4_Man_t * p )
{
    if ( p->pPars->fVerbose ) 
    {
        abctime timeTotal = Abc_Clock() - p->timeStart;
        abctime timeSat   = p->timeSatSat0 + p->timeSatSat + p->timeSatUnsat0 + p->timeSatUnsat + p->timeSatUndec;
180
        abctime timeOther = timeTotal - timeSat - p->timeSim - p->timeRefine - p->timeResimLoc - p->timeGenPats;// - p->timeResimGlo;
181 182 183 184 185 186
        ABC_PRTP( "SAT solving  ", timeSat,          timeTotal );
        ABC_PRTP( "  sat(easy)  ", p->timeSatSat0,   timeTotal );
        ABC_PRTP( "  sat        ", p->timeSatSat,    timeTotal );
        ABC_PRTP( "  unsat(easy)", p->timeSatUnsat0, timeTotal );
        ABC_PRTP( "  unsat      ", p->timeSatUnsat,  timeTotal );
        ABC_PRTP( "  fail       ", p->timeSatUndec,  timeTotal );
187 188
        ABC_PRTP( "Generate CNF ", p->timeCnf,       timeTotal );
        ABC_PRTP( "Generate pats", p->timeGenPats,   timeTotal );
189 190 191 192 193 194 195 196 197
        ABC_PRTP( "Simulation   ", p->timeSim,       timeTotal );
        ABC_PRTP( "Refinement   ", p->timeRefine,    timeTotal );
        ABC_PRTP( "Resim global ", p->timeResimGlo,  timeTotal );
        ABC_PRTP( "Resim local  ", p->timeResimLoc,  timeTotal );
        ABC_PRTP( "Other        ", timeOther,        timeTotal );
        ABC_PRTP( "TOTAL        ", timeTotal,        timeTotal );
        fflush( stdout );
    }
    Vec_WrdFreeP( &p->pAig->vSims );
198
    Vec_WrdFreeP( &p->pAig->vSimsPi );
199
    Gia_ManCleanMark01( p->pAig );
200
    sat_solver_stop( p->pSat );
201 202 203 204 205 206
    Gia_ManStopP( &p->pNew );
    Vec_PtrFreeP( &p->vFrontier );
    Vec_PtrFreeP( &p->vFanins );
    Vec_IntFreeP( &p->vCexMin );
    Vec_IntFreeP( &p->vClassUpdates );
    Vec_IntFreeP( &p->vCexStamps );
207 208 209
    Vec_IntFreeP( &p->vCands );
    Vec_IntFreeP( &p->vVisit );
    Vec_IntFreeP( &p->vPat );
210
    Vec_BitFreeP( &p->vFails );
211 212 213 214
    Vec_IntFreeP( &p->vRefClasses );
    Vec_IntFreeP( &p->vRefNodes );
    Vec_IntFreeP( &p->vRefBins );
    ABC_FREE( p->pTable );
215 216
    ABC_FREE( p );
}
217 218 219 220 221 222 223 224 225 226 227 228 229 230 231
Gia_Man_t * Cec4_ManStartNew( Gia_Man_t * pAig )
{
    Gia_Obj_t * pObj; int i;
    Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(pAig) );
    pNew->pName = Abc_UtilStrsav( pAig->pName );
    pNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
    Gia_ManFillValue( pAig );
    Gia_ManConst0(pAig)->Value = 0;
    Gia_ManForEachCi( pAig, pObj, i )
        pObj->Value = Gia_ManAppendCi( pNew );
    Gia_ManHashAlloc( pNew );
    Vec_IntFill( &pNew->vCopies2, Gia_ManObjNum(pAig), -1 );
    Gia_ManSetRegNum( pNew, Gia_ManRegNum(pAig) );
    return pNew;
}
232 233 234 235 236 237 238 239 240 241 242 243

/**Function*************************************************************

  Synopsis    [Adds clauses to the solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
244
void Cec4_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, sat_solver * pSat )
245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279
{
    int fPolarFlip = 0;
    Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
    int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;

    assert( !Gia_IsComplement( pNode ) );
    assert( pNode->fMark0 );
    // get nodes (I = if, T = then, E = else)
    pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
    // get the variable numbers
    VarF = Cec4_ObjSatId(p, pNode);
    VarI = Cec4_ObjSatId(p, pNodeI);
    VarT = Cec4_ObjSatId(p, Gia_Regular(pNodeT));
    VarE = Cec4_ObjSatId(p, Gia_Regular(pNodeE));
    // get the complementation flags
    fCompT = Gia_IsComplement(pNodeT);
    fCompE = Gia_IsComplement(pNodeE);

    // f = ITE(i, t, e)

    // i' + t' + f
    // i' + t  + f'
    // i  + e' + f
    // i  + e  + f'

    // create four clauses
    pLits[0] = Abc_Var2Lit(VarI, 1);
    pLits[1] = Abc_Var2Lit(VarT, 1^fCompT);
    pLits[2] = Abc_Var2Lit(VarF, 0);
    if ( fPolarFlip )
    {
        if ( pNodeI->fPhase )               pLits[0] = Abc_LitNot( pLits[0] );
        if ( Gia_Regular(pNodeT)->fPhase )  pLits[1] = Abc_LitNot( pLits[1] );
        if ( pNode->fPhase )                pLits[2] = Abc_LitNot( pLits[2] );
    }
280
    RetValue = sat_solver_addclause( pSat, pLits, 3 );
281 282 283 284 285 286 287 288 289 290
    assert( RetValue );
    pLits[0] = Abc_Var2Lit(VarI, 1);
    pLits[1] = Abc_Var2Lit(VarT, 0^fCompT);
    pLits[2] = Abc_Var2Lit(VarF, 1);
    if ( fPolarFlip )
    {
        if ( pNodeI->fPhase )               pLits[0] = Abc_LitNot( pLits[0] );
        if ( Gia_Regular(pNodeT)->fPhase )  pLits[1] = Abc_LitNot( pLits[1] );
        if ( pNode->fPhase )                pLits[2] = Abc_LitNot( pLits[2] );
    }
291
    RetValue = sat_solver_addclause( pSat, pLits, 3 );
292 293 294 295 296 297 298 299 300 301
    assert( RetValue );
    pLits[0] = Abc_Var2Lit(VarI, 0);
    pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
    pLits[2] = Abc_Var2Lit(VarF, 0);
    if ( fPolarFlip )
    {
        if ( pNodeI->fPhase )               pLits[0] = Abc_LitNot( pLits[0] );
        if ( Gia_Regular(pNodeE)->fPhase )  pLits[1] = Abc_LitNot( pLits[1] );
        if ( pNode->fPhase )                pLits[2] = Abc_LitNot( pLits[2] );
    }
302
    RetValue = sat_solver_addclause( pSat, pLits, 3 );
303 304 305 306 307 308 309 310 311 312
    assert( RetValue );
    pLits[0] = Abc_Var2Lit(VarI, 0);
    pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
    pLits[2] = Abc_Var2Lit(VarF, 1);
    if ( fPolarFlip )
    {
        if ( pNodeI->fPhase )               pLits[0] = Abc_LitNot( pLits[0] );
        if ( Gia_Regular(pNodeE)->fPhase )  pLits[1] = Abc_LitNot( pLits[1] );
        if ( pNode->fPhase )                pLits[2] = Abc_LitNot( pLits[2] );
    }
313
    RetValue = sat_solver_addclause( pSat, pLits, 3 );
314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337
    assert( RetValue );

    // two additional clauses
    // t' & e' -> f'
    // t  & e  -> f 

    // t  + e   + f'
    // t' + e'  + f 

    if ( VarT == VarE )
    {
//        assert( fCompT == !fCompE );
        return;
    }

    pLits[0] = Abc_Var2Lit(VarT, 0^fCompT);
    pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
    pLits[2] = Abc_Var2Lit(VarF, 1);
    if ( fPolarFlip )
    {
        if ( Gia_Regular(pNodeT)->fPhase )  pLits[0] = Abc_LitNot( pLits[0] );
        if ( Gia_Regular(pNodeE)->fPhase )  pLits[1] = Abc_LitNot( pLits[1] );
        if ( pNode->fPhase )                pLits[2] = Abc_LitNot( pLits[2] );
    }
338
    RetValue = sat_solver_addclause( pSat, pLits, 3 );
339 340 341 342 343 344 345 346 347 348
    assert( RetValue );
    pLits[0] = Abc_Var2Lit(VarT, 1^fCompT);
    pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
    pLits[2] = Abc_Var2Lit(VarF, 0);
    if ( fPolarFlip )
    {
        if ( Gia_Regular(pNodeT)->fPhase )  pLits[0] = Abc_LitNot( pLits[0] );
        if ( Gia_Regular(pNodeE)->fPhase )  pLits[1] = Abc_LitNot( pLits[1] );
        if ( pNode->fPhase )                pLits[2] = Abc_LitNot( pLits[2] );
    }
349
    RetValue = sat_solver_addclause( pSat, pLits, 3 );
350 351
    assert( RetValue );
}
352
void Cec4_AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, sat_solver * pSat )
353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372
{
    int fPolarFlip = 0;
    Gia_Obj_t * pFanin;
    int * pLits, nLits, RetValue, i;
    assert( !Gia_IsComplement(pNode) );
    assert( Gia_ObjIsAnd( pNode ) );
    // create storage for literals
    nLits = Vec_PtrSize(vSuper) + 1;
    pLits = ABC_ALLOC( int, nLits );
    // suppose AND-gate is A & B = C
    // add !A => !C   or   A + !C
    Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
    {
        pLits[0] = Abc_Var2Lit(Cec4_ObjSatId(p, Gia_Regular(pFanin)), Gia_IsComplement(pFanin));
        pLits[1] = Abc_Var2Lit(Cec4_ObjSatId(p, pNode), 1);
        if ( fPolarFlip )
        {
            if ( Gia_Regular(pFanin)->fPhase )  pLits[0] = Abc_LitNot( pLits[0] );
            if ( pNode->fPhase )                pLits[1] = Abc_LitNot( pLits[1] );
        }
373
        RetValue = sat_solver_addclause( pSat, pLits, 2 );
374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389
        assert( RetValue );
    }
    // add A & B => C   or   !A + !B + C
    Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
    {
        pLits[i] = Abc_Var2Lit(Cec4_ObjSatId(p, Gia_Regular(pFanin)), !Gia_IsComplement(pFanin));
        if ( fPolarFlip )
        {
            if ( Gia_Regular(pFanin)->fPhase )  pLits[i] = Abc_LitNot( pLits[i] );
        }
    }
    pLits[nLits-1] = Abc_Var2Lit(Cec4_ObjSatId(p, pNode), 0);
    if ( fPolarFlip )
    {
        if ( pNode->fPhase )  pLits[nLits-1] = Abc_LitNot( pLits[nLits-1] );
    }
390
    RetValue = sat_solver_addclause( pSat, pLits, nLits );
391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426
    assert( RetValue );
    ABC_FREE( pLits );
}

/**Function*************************************************************

  Synopsis    [Adds clauses and returns CNF variable of the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec4_CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
{
    // if the new node is complemented or a PI, another gate begins
    if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) || 
         (!fFirst && Gia_ObjValue(pObj) > 1) || 
         (fUseMuxes && pObj->fMark0) )
    {
        Vec_PtrPushUnique( vSuper, pObj );
        return;
    }
    // go through the branches
    Cec4_CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
    Cec4_CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
}
void Cec4_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
{
    assert( !Gia_IsComplement(pObj) );
    assert( !Gia_ObjIsCi(pObj) );
    Vec_PtrClear( vSuper );
    Cec4_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
}
427
void Cec4_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, sat_solver * pSat )
428 429 430 431 432 433
{
    assert( !Gia_IsComplement(pObj) );
    assert( !Gia_ObjIsConst0(pObj) );
    if ( Cec4_ObjSatId(p, pObj) >= 0 )
        return;
    assert( Cec4_ObjSatId(p, pObj) == -1 );
434
    Cec4_ObjSetSatId( p, pObj, sat_solver_addvar(pSat) );
435 436 437 438 439 440 441 442 443 444 445 446 447 448 449
    if ( Gia_ObjIsAnd(pObj) )
        Vec_PtrPush( vFrontier, pObj );
}
int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj )
{ 
    int fUseAnd2  = 1; // enable simple CNF
    int fUseMuxes = 1; // enable MUXes when using complex CNF
    Gia_Obj_t * pNode, * pFanin;
    Gia_Obj_t * pObj = Gia_ManObj(p->pNew, iObj);
    int i, k;
    // quit if CNF is ready
    if ( Cec4_ObjSatId(p->pNew,pObj) >= 0 )
        return Cec4_ObjSatId(p->pNew,pObj);
    assert( iObj > 0 );
    if ( Gia_ObjIsCi(pObj) )
450
        return Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
451 452 453 454 455
    assert( Gia_ObjIsAnd(pObj) );
    if ( fUseAnd2 )
    {
        Cec4_ObjGetCnfVar( p, Gia_ObjFaninId0(pObj, iObj) );
        Cec4_ObjGetCnfVar( p, Gia_ObjFaninId1(pObj, iObj) );
456
        Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
457 458 459 460 461 462 463 464 465 466 467 468
        if( sat_solver_jftr( p->pSat ) < 2 )
        {
            Vec_PtrClear( p->vFanins );
            Vec_PtrPush( p->vFanins, Gia_ObjChild0(pObj) );
            Vec_PtrPush( p->vFanins, Gia_ObjChild1(pObj) );
            Cec4_AddClausesSuper( p->pNew, pObj, p->vFanins, p->pSat );
        }
        if( 0 < sat_solver_jftr( p->pSat ) )
            sat_solver_set_var_fanin_lit( p->pSat\
                , Cec4_ObjSatId( p->pNew, pObj )\
                , Abc_Var2Lit( Cec4_ObjSatId( p->pNew, Gia_ObjFanin0(pObj) ), Gia_ObjFaninC0(pObj) )\
                , Abc_Var2Lit( Cec4_ObjSatId( p->pNew, Gia_ObjFanin1(pObj) ), Gia_ObjFaninC1(pObj) ) );
469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504
        return Cec4_ObjSatId( p->pNew, pObj );
    }
    // start the frontier
    Vec_PtrClear( p->vFrontier );
    Cec4_ObjAddToFrontier( p->pNew, pObj, p->vFrontier, p->pSat );
    // explore nodes in the frontier
    Vec_PtrForEachEntry( Gia_Obj_t *, p->vFrontier, pNode, i )
    {
        // create the supergate
        assert( Cec4_ObjSatId(p->pNew,pNode) >= 0 );
        if ( fUseMuxes && pNode->fMark0 )
        {
            Vec_PtrClear( p->vFanins );
            Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) );
            Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) );
            Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
                Cec4_ObjAddToFrontier( p->pNew, Gia_Regular(pFanin), p->vFrontier, p->pSat );
            Cec4_AddClausesMux( p->pNew, pNode, p->pSat );
        }
        else
        {
            Cec4_CollectSuper( pNode, fUseMuxes, p->vFanins );
            Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
                Cec4_ObjAddToFrontier( p->pNew, Gia_Regular(pFanin), p->vFrontier, p->pSat );
            Cec4_AddClausesSuper( p->pNew, pNode, p->vFanins, p->pSat );
        }
        assert( Vec_PtrSize(p->vFanins) > 1 );
    }
    return Cec4_ObjSatId(p->pNew,pObj);
}


/**Function*************************************************************

505
  Synopsis    [Refinement of equivalence classes.]
506 507 508 509 510 511 512 513 514 515 516 517

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline word * Cec4_ObjSim( Gia_Man_t * p, int iObj )
{
    return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj );
}
518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678
static inline int Cec4_ObjSimEqual( Gia_Man_t * p, int iObj0, int iObj1 )
{
    int w;
    word * pSim0 = Cec4_ObjSim( p, iObj0 );
    word * pSim1 = Cec4_ObjSim( p, iObj1 );
    if ( (pSim0[0] & 1) == (pSim1[0] & 1) )
    {
        for ( w = 0; w < p->nSimWords; w++ )
            if ( pSim0[w] != pSim1[w] )
                return 0;
        return 1;
    }
    else
    {
        for ( w = 0; w < p->nSimWords; w++ )
            if ( pSim0[w] != ~pSim1[w] )
                return 0;
        return 1;
    }
}
int Cec4_ManSimHashKey( word * pSim, int nSims, int nTableSize )
{
    static int s_Primes[16] = { 
        1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 
        4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
    unsigned uHash = 0, * pSimU = (unsigned *)pSim;
    int i, nSimsU = 2 * nSims;
    if ( pSimU[0] & 1 )
        for ( i = 0; i < nSimsU; i++ )
            uHash ^= ~pSimU[i] * s_Primes[i & 0xf];
    else
        for ( i = 0; i < nSimsU; i++ )
            uHash ^= pSimU[i] * s_Primes[i & 0xf];
    return (int)(uHash % nTableSize);

}
void Cec4_RefineOneClassIter( Gia_Man_t * p, int iRepr )
{
    int iObj, iPrev = iRepr, iPrev2, iRepr2;
    assert( Gia_ObjRepr(p, iRepr) == GIA_VOID );
    assert( Gia_ObjNext(p, iRepr) > 0 );
    Gia_ClassForEachObj1( p, iRepr, iRepr2 )
        if ( Cec4_ObjSimEqual(p, iRepr, iRepr2) )
            iPrev = iRepr2;
        else
            break;
    if ( iRepr2 <= 0 ) // no refinement
        return;
    // relink remaining nodes of the class
    // nodes that are equal to iRepr, remain in the class of iRepr
    // nodes that are not equal to iRepr, move to the class of iRepr2
    Gia_ObjSetRepr( p, iRepr2, GIA_VOID );
    iPrev2 = iRepr2;
    for ( iObj = Gia_ObjNext(p, iRepr2); iObj > 0; iObj = Gia_ObjNext(p, iObj) )
    {
        if ( Cec4_ObjSimEqual(p, iRepr, iObj) ) // remains with iRepr
        {
            Gia_ObjSetNext( p, iPrev, iObj );
            iPrev = iObj;
        }
        else // moves to iRepr2
        {
            Gia_ObjSetRepr( p, iObj, iRepr2 );
            Gia_ObjSetNext( p, iPrev2, iObj );
            iPrev2 = iObj;
        }
    }
    Gia_ObjSetNext( p, iPrev, -1 );
    Gia_ObjSetNext( p, iPrev2, -1 );
    // refine incrementally
    if ( Gia_ObjNext(p, iRepr2) > 0 )
        Cec4_RefineOneClassIter( p, iRepr2 );
}
void Cec4_RefineOneClass( Gia_Man_t * p, Cec4_Man_t * pMan, Vec_Int_t * vNodes )
{
    int k, iObj, Bin;
    Vec_IntClear( pMan->vRefBins );
    Vec_IntForEachEntryReverse( vNodes, iObj, k )
    {
        int Key = Cec4_ManSimHashKey( Cec4_ObjSim(p, iObj), p->nSimWords, pMan->nTableSize );
        assert( Key >= 0 && Key < pMan->nTableSize );
        if ( pMan->pTable[Key] == -1 )
            Vec_IntPush( pMan->vRefBins, Key );
        p->pNexts[iObj] = pMan->pTable[Key];
        pMan->pTable[Key] = iObj;
    }
    Vec_IntForEachEntry( pMan->vRefBins, Bin, k )
    {
        int iRepr = pMan->pTable[Bin];
        pMan->pTable[Bin] = -1;
        assert( p->pReprs[iRepr].iRepr == GIA_VOID );
        assert( p->pNexts[iRepr] != 0 );
        if ( p->pNexts[iRepr] == -1 )
            continue;
        for ( iObj = p->pNexts[iRepr]; iObj > 0; iObj = p->pNexts[iObj] )
            p->pReprs[iObj].iRepr = iRepr;
        Cec4_RefineOneClassIter( p, iRepr );
    }
    Vec_IntClear( pMan->vRefBins );
}
void Cec4_RefineClasses( Gia_Man_t * p, Cec4_Man_t * pMan, Vec_Int_t * vClasses )
{
    if ( Vec_IntSize(pMan->vRefClasses) == 0 )
        return;
    if ( Vec_IntSize(pMan->vRefNodes) > 0 )
        Cec4_RefineOneClass( p, pMan, pMan->vRefNodes );
    else
    {
        int i, k, iObj, iRepr;
        Vec_IntForEachEntry( pMan->vRefClasses, iRepr, i )
        {
            assert( p->pReprs[iRepr].fColorA );
            p->pReprs[iRepr].fColorA = 0;
            Vec_IntClear( pMan->vRefNodes );
            Vec_IntPush( pMan->vRefNodes, iRepr );
            Gia_ClassForEachObj1( p, iRepr, k )
                Vec_IntPush( pMan->vRefNodes, k );
            Vec_IntForEachEntry( pMan->vRefNodes, iObj, k )
            {
                p->pReprs[iObj].iRepr = GIA_VOID;
                p->pNexts[iObj] = -1;
            }
            Cec4_RefineOneClass( p, pMan, pMan->vRefNodes );
        }
    }
    Vec_IntClear( pMan->vRefClasses );
    Vec_IntClear( pMan->vRefNodes );
}
void Cec4_RefineInit( Gia_Man_t * p, Cec4_Man_t * pMan )
{
    Gia_Obj_t * pObj; int i;
    ABC_FREE( p->pReprs );
    ABC_FREE( p->pNexts );
    p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
    p->pNexts = ABC_FALLOC( int, Gia_ManObjNum(p) );
    pMan->nTableSize  = Abc_PrimeCudd( Gia_ManObjNum(p) );
    pMan->pTable      = ABC_FALLOC( int, pMan->nTableSize );
    pMan->vRefNodes   = Vec_IntAlloc( Gia_ManObjNum(p) );
    Gia_ManForEachObj( p, pObj, i )
    {
        p->pReprs[i].iRepr = GIA_VOID;
        if ( !Gia_ObjIsCo(pObj) )
            Vec_IntPush( pMan->vRefNodes, i );
    }
    pMan->vRefBins    = Vec_IntAlloc( Gia_ManObjNum(p)/2 );
    pMan->vRefClasses = Vec_IntAlloc( Gia_ManObjNum(p)/2 );
    Vec_IntPush( pMan->vRefClasses, 0 );
}


/**Function*************************************************************

  Synopsis    [Internal simulation APIs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
679 680 681 682 683 684
static inline void Cec4_ObjSimSetInputBit( Gia_Man_t * p, int iObj, int Bit )
{
    word * pSim = Cec4_ObjSim( p, iObj );
    if ( Abc_InfoHasBit( (unsigned*)pSim, p->iPatsPi ) != Bit )
        Abc_InfoXorBit( (unsigned*)pSim, p->iPatsPi );
}
685 686 687 688 689
static inline int Cec4_ObjSimGetInputBit( Gia_Man_t * p, int iObj )
{
    word * pSim = Cec4_ObjSim( p, iObj );
    return Abc_InfoHasBit( (unsigned*)pSim, p->iPatsPi );
}
690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786
static inline void Cec4_ObjSimRo( Gia_Man_t * p, int iObj )
{
    int w;
    word * pSimRo = Cec4_ObjSim( p, iObj );
    word * pSimRi = Cec4_ObjSim( p, Gia_ObjRoToRiId(p, iObj) );
    for ( w = 0; w < p->nSimWords; w++ )
        pSimRo[w] = pSimRi[w];
}
static inline void Cec4_ObjSimCo( Gia_Man_t * p, int iObj )
{
    int w;
    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
    word * pSimCo  = Cec4_ObjSim( p, iObj );
    word * pSimDri = Cec4_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) );
    if ( Gia_ObjFaninC0(pObj) )
        for ( w = 0; w < p->nSimWords; w++ )
            pSimCo[w] = ~pSimDri[w];
    else
        for ( w = 0; w < p->nSimWords; w++ )
            pSimCo[w] =  pSimDri[w];
}
static inline void Cec4_ObjSimAnd( Gia_Man_t * p, int iObj )
{
    int w;
    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
    word * pSim  = Cec4_ObjSim( p, iObj );
    word * pSim0 = Cec4_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) );
    word * pSim1 = Cec4_ObjSim( p, Gia_ObjFaninId1(pObj, iObj) );
    if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
        for ( w = 0; w < p->nSimWords; w++ )
            pSim[w] = ~pSim0[w] & ~pSim1[w];
    else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
        for ( w = 0; w < p->nSimWords; w++ )
            pSim[w] = ~pSim0[w] & pSim1[w];
    else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
        for ( w = 0; w < p->nSimWords; w++ )
            pSim[w] = pSim0[w] & ~pSim1[w];
    else
        for ( w = 0; w < p->nSimWords; w++ )
            pSim[w] = pSim0[w] & pSim1[w];
}
static inline void Cec4_ObjSimCi( Gia_Man_t * p, int iObj )
{
    int w;
    word * pSim = Cec4_ObjSim( p, iObj );
    for ( w = 0; w < p->nSimWords; w++ )
        pSim[w] = Gia_ManRandomW( 0 );
    pSim[0] <<= 1;
}
static inline void Cec4_ObjClearSimCi( Gia_Man_t * p, int iObj )
{
    int w;
    word * pSim = Cec4_ObjSim( p, iObj );
    for ( w = 0; w < p->nSimWords; w++ )
        pSim[w] = 0;
}
void Cec4_ManSimulateCis( Gia_Man_t * p )
{
    int i, Id;
    Gia_ManForEachCiId( p, Id, i )
        Cec4_ObjSimCi( p, Id );
    p->iPatsPi = 0;
}
void Cec4_ManClearCis( Gia_Man_t * p )
{
    int i, Id;
    Gia_ManForEachCiId( p, Id, i )
        Cec4_ObjClearSimCi( p, Id );
    p->iPatsPi = 0;
}
Abc_Cex_t * Cec4_ManDeriveCex( Gia_Man_t * p, int iOut, int iPat )
{
    Abc_Cex_t * pCex;
    int i, Id;
    pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p), 1 );
    pCex->iPo = iOut;
    if ( iPat == -1 )
        return pCex;
    Gia_ManForEachCiId( p, Id, i )
        if ( Abc_InfoHasBit((unsigned *)Cec4_ObjSim(p, Id), iPat) )
            Abc_InfoSetBit( pCex->pData, i );
    return pCex;
}
int Cec4_ManSimulateCos( Gia_Man_t * p )
{
    int i, Id;
    // check outputs and generate CEX if they fail
    Gia_ManForEachCoId( p, Id, i )
    {
        Cec4_ObjSimCo( p, Id );
        if ( Cec4_ObjSimEqual(p, Id, 0) )
            continue;
        p->pCexSeq = Cec4_ManDeriveCex( p, i, Abc_TtFindFirstBit2(Cec4_ObjSim(p, Id), p->nSimWords) );
        return 0;
    }
    return 1;
}
787
void Cec4_ManSimulate( Gia_Man_t * p, Cec4_Man_t * pMan )
788 789 790 791
{
    abctime clk = Abc_Clock();
    Gia_Obj_t * pObj; int i;
    pMan->nSimulates++;
792 793 794 795
    if ( pMan->pTable == NULL )
        Cec4_RefineInit( p, pMan );
    else
        assert( Vec_IntSize(pMan->vRefClasses) == 0 );
796
    Gia_ManForEachAnd( p, pObj, i )
797 798
    {
        int iRepr = Gia_ObjRepr( p, i );
799
        Cec4_ObjSimAnd( p, i );
800 801 802 803 804
        if ( iRepr == GIA_VOID || p->pReprs[iRepr].fColorA || Cec4_ObjSimEqual(p, iRepr, i) )
            continue;
        p->pReprs[iRepr].fColorA = 1;
        Vec_IntPush( pMan->vRefClasses, iRepr );
    }
805 806
    pMan->timeSim += Abc_Clock() - clk;
    clk = Abc_Clock();
807
    Cec4_RefineClasses( p, pMan, pMan->vRefClasses );
808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826
    pMan->timeRefine += Abc_Clock() - clk;
}
void Cec4_ManSimulate_rec( Gia_Man_t * p, Cec4_Man_t * pMan, int iObj )
{
    Gia_Obj_t * pObj; 
    if ( !iObj || Vec_IntEntry(pMan->vCexStamps, iObj) == p->iPatsPi )
        return;
    Vec_IntWriteEntry( pMan->vCexStamps, iObj, p->iPatsPi );
    pObj = Gia_ManObj(p, iObj);
    if ( Gia_ObjIsCi(pObj) )
        return;
    assert( Gia_ObjIsAnd(pObj) );
    Cec4_ManSimulate_rec( p, pMan, Gia_ObjFaninId0(pObj, iObj) );
    Cec4_ManSimulate_rec( p, pMan, Gia_ObjFaninId1(pObj, iObj) );
    Cec4_ObjSimAnd( p, iObj );
}
void Cec4_ManSimAlloc( Gia_Man_t * p, int nWords )
{
    Vec_WrdFreeP( &p->vSims );
827 828 829
    Vec_WrdFreeP( &p->vSimsPi );
    p->vSims     = Vec_WrdStart( Gia_ManObjNum(p) * nWords );
    p->vSimsPi   = Vec_WrdStart( (Gia_ManCiNum(p) + 1) * nWords );
830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868
    p->nSimWords = nWords;
}


/**Function*************************************************************

  Synopsis    [Creating initial equivalence classes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec4_ManPrintTfiConeStats( Gia_Man_t * p )
{
    Vec_Int_t * vRoots  = Vec_IntAlloc( 100 );
    Vec_Int_t * vNodes  = Vec_IntAlloc( 100 );
    Vec_Int_t * vLeaves = Vec_IntAlloc( 100 );
    int i, k;
    Gia_ManForEachClass0( p, i )
    {
        Vec_IntClear( vRoots );
        if ( i % 100 != 0 )
            continue;
        Vec_IntPush( vRoots, i );
        Gia_ClassForEachObj1( p, i, k )
            Vec_IntPush( vRoots, k );
        Gia_ManCollectTfi( p, vRoots, vNodes );
        printf( "Class %6d : ", i );
        printf( "Roots = %6d  ", Vec_IntSize(vRoots) );
        printf( "Nodes = %6d  ", Vec_IntSize(vNodes) );
        printf( "\n" );
    }
    Vec_IntFree( vRoots );
    Vec_IntFree( vNodes );
    Vec_IntFree( vLeaves );
}
869
void Cec4_ManPrintStats( Gia_Man_t * p, Cec_ParFra_t * pPars, Cec4_Man_t * pMan, int fSim )
870
{
871 872 873
    static abctime clk = 0;
    abctime clkThis = 0;
    int i, nLits, Counter = 0, Counter0 = 0, CounterX = 0;
874 875
    if ( !pPars->fVerbose )
        return;
876 877 878 879
    if ( pMan->nItersSim + pMan->nItersSat )
        clkThis = Abc_Clock() - clk;
    clk = Abc_Clock();
    for ( i = 0; i < Gia_ManObjNum(p); i++ )
880
    {
881 882 883 884 885 886
        if ( Gia_ObjIsHead(p, i) )
            Counter++;
        else if ( Gia_ObjIsConst(p, i) )
            Counter0++;
        else if ( Gia_ObjIsNone(p, i) )
            CounterX++;
887
    }
888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904
    nLits = Gia_ManObjNum(p) - Counter - CounterX;
    if ( fSim )
    {
        printf( "Sim %4d : ",     pMan->nItersSim++ + pMan->nItersSat );
        printf( "%6.2f %%  ", 100.0*nLits/Gia_ManCandNum(p) );
    }
    else
    {
        printf( "SAT %4d : ",     pMan->nItersSim + pMan->nItersSat++ );
        printf( "%6.2f %%  ", 100.0*pMan->nAndNodes/Gia_ManAndNum(p) );
    }
    printf( "P =%7d  ",   pMan ? pMan->nSatUnsat : 0 );
    printf( "D =%7d  ",   pMan ? pMan->nSatSat   : 0 );
    printf( "F =%8d  ",   pMan ? pMan->nSatUndec : 0 );
    //printf( "Last =%6d  ", pMan ? pMan->iLastConst : 0 );
    Abc_Print( 1, "cst =%9d  cls =%8d  lit =%9d   ",  Counter0, Counter, nLits );
    Abc_PrintTime( 1, "Time", clkThis );
905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936
}
void Cec4_ManPrintClasses2( Gia_Man_t * p )
{
    int i, k;
    Gia_ManForEachClass0( p, i )
    {
        printf( "Class %d : ", i );
        Gia_ClassForEachObj1( p, i, k )
            printf( "%d ", k );
        printf( "\n" );
    }
}
void Cec4_ManPrintClasses( Gia_Man_t * p )
{
    int k, Count = 0;
    Gia_ClassForEachObj1( p, 0, k )
        Count++;
    printf( "Const0 class has %d entries.\n", Count );
}


/**Function*************************************************************

  Synopsis    [Verify counter-example.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
937
int Cec4_ManVerify_rec( Gia_Man_t * p, int iObj, sat_solver * pSat )
938 939 940 941 942 943 944 945
{
    int Value0, Value1;
    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
    if ( iObj == 0 ) return 0;
    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
        return pObj->fMark1;
    Gia_ObjSetTravIdCurrentId(p, iObj);
    if ( Gia_ObjIsCi(pObj) )
946
        return pObj->fMark1 = sat_solver_read_cex_varvalue(pSat, Cec4_ObjSatId(p, pObj));
947 948 949 950 951
    assert( Gia_ObjIsAnd(pObj) );
    Value0 = Cec4_ManVerify_rec( p, Gia_ObjFaninId0(pObj, iObj), pSat ) ^ Gia_ObjFaninC0(pObj);
    Value1 = Cec4_ManVerify_rec( p, Gia_ObjFaninId1(pObj, iObj), pSat ) ^ Gia_ObjFaninC1(pObj);
    return pObj->fMark1 = Value0 & Value1;
}
952
void Cec4_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, sat_solver * pSat )
953 954 955 956 957 958 959 960 961 962 963 964
{
    int Value0, Value1;
    Gia_ManIncrementTravId( p );
    Value0 = Cec4_ManVerify_rec( p, iObj0, pSat );
    Value1 = Cec4_ManVerify_rec( p, iObj1, pSat );
    if ( (Value0 ^ Value1) == fPhase )
        printf( "CEX verification FAILED for obj %d and obj %d.\n", iObj0, iObj1 );
//    else
//        printf( "CEX verification succeeded for obj %d and obj %d.\n", iObj0, iObj1 );;
}


965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002
/**Function*************************************************************

  Synopsis    [Verify counter-example.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec4_ManCexVerify_rec( Gia_Man_t * p, int iObj )
{
    int Value0, Value1;
    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
    if ( iObj == 0 ) return 0;
    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
        return pObj->fMark1;
    Gia_ObjSetTravIdCurrentId(p, iObj);
    if ( Gia_ObjIsCi(pObj) )
        return pObj->fMark1 = Cec4_ObjSimGetInputBit(p, iObj);
    assert( Gia_ObjIsAnd(pObj) );
    Value0 = Cec4_ManCexVerify_rec( p, Gia_ObjFaninId0(pObj, iObj) ) ^ Gia_ObjFaninC0(pObj);
    Value1 = Cec4_ManCexVerify_rec( p, Gia_ObjFaninId1(pObj, iObj) ) ^ Gia_ObjFaninC1(pObj);
    return pObj->fMark1 = Value0 & Value1;
}
void Cec4_ManCexVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase )
{
    int Value0, Value1;
    Gia_ManIncrementTravId( p );
    Value0 = Cec4_ManCexVerify_rec( p, iObj0 );
    Value1 = Cec4_ManCexVerify_rec( p, iObj1 );
    if ( (Value0 ^ Value1) == fPhase )
        printf( "CEX verification FAILED for obj %d and obj %d.\n", iObj0, iObj1 );
//    else
//        printf( "CEX verification succeeded for obj %d and obj %d.\n", iObj0, iObj1 );;
}

1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049
/**Function*************************************************************

  Synopsis    [Packs simulation patterns into array of simulation info.]

  Description []
               
  SideEffects []

  SeeAlso     []

*************************************`**********************************/
int Cec4_ManPackAddPatternTry( Gia_Man_t * p, int iBit, Vec_Int_t * vLits )
{
    int i, Lit;
    assert( p->iPatsPi > 0 && p->iPatsPi < 64 * p->nSimWords );
    Vec_IntForEachEntry( vLits, Lit, i )
    {
        word * pInfo = Vec_WrdEntryP( p->vSims,   p->nSimWords * Abc_Lit2Var(Lit) );
        word * pPres = Vec_WrdEntryP( p->vSimsPi, p->nSimWords * Abc_Lit2Var(Lit) );
        if ( Abc_InfoHasBit( (unsigned *)pPres, iBit ) && 
             Abc_InfoHasBit( (unsigned *)pInfo, iBit ) != Abc_LitIsCompl(Lit) )
             return 0;
    }
    Vec_IntForEachEntry( vLits, Lit, i )
    {
        word * pInfo = Vec_WrdEntryP( p->vSims,   p->nSimWords * Abc_Lit2Var(Lit) );
        word * pPres = Vec_WrdEntryP( p->vSimsPi, p->nSimWords * Abc_Lit2Var(Lit) );
        Abc_InfoSetBit( (unsigned *)pPres, iBit );
        if ( Abc_InfoHasBit( (unsigned *)pInfo, iBit ) != Abc_LitIsCompl(Lit) )
             Abc_InfoXorBit( (unsigned *)pInfo, iBit );
    }
    return 1;
}
int Cec4_ManPackAddPattern( Gia_Man_t * p, Vec_Int_t * vLits )
{
    int k;
    for ( k = 1; k < 64 * p->nSimWords; k++ )
    {
        if ( ++p->iPatsPi == 64 * p->nSimWords )
            p->iPatsPi = 1;
        if ( Cec4_ManPackAddPatternTry( p, p->iPatsPi, vLits ) )
            break;
    }
    //assert( k < 64 * p->nSimWords );
    return k;
}

1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068
/**Function*************************************************************

  Synopsis    [Generates counter-examples to refine the candidate equivalences.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cec4_ObjFan0HasValue( Gia_Obj_t * pObj, int v )
{
    return (v ^ Gia_ObjFaninC0(pObj)) ? Gia_ObjFanin0(pObj)->fMark1 : Gia_ObjFanin0(pObj)->fMark0;
}
static inline int Cec4_ObjFan1HasValue( Gia_Obj_t * pObj, int v )
{
    return (v ^ Gia_ObjFaninC1(pObj)) ? Gia_ObjFanin1(pObj)->fMark1 : Gia_ObjFanin1(pObj)->fMark0;
}
1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083
static inline int Cec4_ObjObjIsImpliedValue( Gia_Obj_t * pObj, int v )
{
    assert( !pObj->fMark0 && !pObj->fMark1 ); // not visited
    if ( v ) 
    return Cec4_ObjFan0HasValue(pObj, 1) && Cec4_ObjFan1HasValue(pObj, 1);
    return Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0);
}
static inline int Cec4_ObjFan0IsImpliedValue( Gia_Obj_t * pObj, int v )
{
    return Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) && Cec4_ObjObjIsImpliedValue( Gia_ObjFanin0(pObj), v ^ Gia_ObjFaninC0(pObj) );
}
static inline int Cec4_ObjFan1IsImpliedValue( Gia_Obj_t * pObj, int v )
{
    return Gia_ObjIsAnd(Gia_ObjFanin1(pObj)) && Cec4_ObjObjIsImpliedValue( Gia_ObjFanin1(pObj), v ^ Gia_ObjFaninC1(pObj) );
}
1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126
int Cec4_ManGeneratePatterns_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int Value, Vec_Int_t * vPat, Vec_Int_t * vVisit )
{
    Gia_Obj_t * pFan0, * pFan1;
    assert( !pObj->fMark0 && !pObj->fMark1 ); // not visited
    if ( Value ) pObj->fMark1 = 1; else pObj->fMark0 = 1;
    Vec_IntPush( vVisit, Gia_ObjId(p, pObj) );
    if ( Gia_ObjIsCi(pObj) )
    {
        Vec_IntPush( vPat, Abc_Var2Lit(Gia_ObjId(p, pObj), Value) );
        return 1;
    }
    assert( Gia_ObjIsAnd(pObj) );
    pFan0 = Gia_ObjFanin0(pObj);
    pFan1 = Gia_ObjFanin1(pObj);
    if ( Value )
    {
        if ( Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0) )
            return 0;
        if ( !Cec4_ObjFan0HasValue(pObj, 1) && !Cec4_ManGeneratePatterns_rec(p, pFan0, !Gia_ObjFaninC0(pObj), vPat, vVisit) )
            return 0;
        if ( !Cec4_ObjFan1HasValue(pObj, 1) && !Cec4_ManGeneratePatterns_rec(p, pFan1, !Gia_ObjFaninC1(pObj), vPat, vVisit) )
            return 0;
        assert( Cec4_ObjFan0HasValue(pObj, 1) && Cec4_ObjFan1HasValue(pObj, 1) );
        return 1;
    }
    else
    {
        if ( Cec4_ObjFan0HasValue(pObj, 1) && Cec4_ObjFan1HasValue(pObj, 1) )
            return 0;
        if ( Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0) )
            return 1;
        if ( Cec4_ObjFan0HasValue(pObj, 1) )
        {
            if ( !Cec4_ManGeneratePatterns_rec(p, pFan1, Gia_ObjFaninC1(pObj), vPat, vVisit) )
                return 0;
        }
        else if ( Cec4_ObjFan1HasValue(pObj, 1) )
        {
            if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, Gia_ObjFaninC0(pObj), vPat, vVisit) )
                return 0;
        }
        else
        {
1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156
            if ( Cec4_ObjFan0IsImpliedValue( pObj, 0 ) )
            {
                if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, Gia_ObjFaninC0(pObj), vPat, vVisit) )
                    return 0;
            }
            else if ( Cec4_ObjFan1IsImpliedValue( pObj, 0 ) )
            {
                if ( !Cec4_ManGeneratePatterns_rec(p, pFan1, Gia_ObjFaninC1(pObj), vPat, vVisit) )
                    return 0;
            }
            else if ( Cec4_ObjFan0IsImpliedValue( pObj, 1 ) )
            {
                if ( !Cec4_ManGeneratePatterns_rec(p, pFan1, Gia_ObjFaninC1(pObj), vPat, vVisit) )
                    return 0;
            }
            else if ( Cec4_ObjFan1IsImpliedValue( pObj, 1 ) )
            {
                if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, Gia_ObjFaninC0(pObj), vPat, vVisit) )
                    return 0;
            }
            else if ( Abc_Random(0) & 1 )
            {
                if ( !Cec4_ManGeneratePatterns_rec(p, pFan1, Gia_ObjFaninC1(pObj), vPat, vVisit) )
                    return 0;
            }
            else
            {
                if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, Gia_ObjFaninC0(pObj), vPat, vVisit) )
                    return 0;
            }
1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177
        }
        assert( Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0) );
        return 1;
    }
}
int Cec4_ManGeneratePatternOne( Gia_Man_t * p, int iRepr, int iReprVal, int iCand, int iCandVal, Vec_Int_t * vPat, Vec_Int_t * vVisit )
{
    int Res, k;
    Gia_Obj_t * pObj;
    assert( iCand > 0 );
    if ( !iRepr && iReprVal )
        return 0;
    Vec_IntClear( vPat );
    Vec_IntClear( vVisit );
    //Gia_ManForEachObj( p, pObj, k )
    //    assert( !pObj->fMark0 && !pObj->fMark1 );
    Res = (!iRepr || Cec4_ManGeneratePatterns_rec(p, Gia_ManObj(p, iRepr), iReprVal, vPat, vVisit)) && Cec4_ManGeneratePatterns_rec(p, Gia_ManObj(p, iCand), iCandVal, vPat, vVisit);
    Gia_ManForEachObjVec( vVisit, p, pObj, k )
        pObj->fMark0 = pObj->fMark1 = 0;
    return Res;
}
1178
void Cec4_ManCandIterStart( Cec4_Man_t * p )
1179
{
1180 1181 1182 1183 1184 1185 1186 1187 1188
    int i, * pArray;
    assert( p->iPosWrite == 0 );
    assert( p->iPosRead == 0 );
    assert( Vec_IntSize(p->vCands) == 0 );
    for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ )
        if ( Gia_ObjRepr(p->pAig, i) != GIA_VOID )
            Vec_IntPush( p->vCands, i );
    pArray = Vec_IntArray( p->vCands );
    for ( i = 0; i < Vec_IntSize(p->vCands); i++ )
1189
    {
1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201
        int iNew = Abc_Random(0) % Vec_IntSize(p->vCands);
        ABC_SWAP( int, pArray[i], pArray[iNew] );
    }
}
int Cec4_ManCandIterNext( Cec4_Man_t * p )
{
    while ( Vec_IntSize(p->vCands) > 0 )
    {
        int fStop, iCand = Vec_IntEntry( p->vCands, p->iPosRead );
        if ( fStop = (Gia_ObjRepr(p->pAig, iCand) != GIA_VOID) )
            Vec_IntWriteEntry( p->vCands, p->iPosWrite++, iCand );
        if ( ++p->iPosRead == Vec_IntSize(p->vCands) )
1202
        {
1203 1204 1205
            Vec_IntShrink( p->vCands, p->iPosWrite );
            p->iPosWrite = 0;
            p->iPosRead = 0;
1206
        }
1207 1208
        if ( fStop )
            return iCand;
1209
    }
1210 1211 1212 1213 1214 1215
    return 0;
}
int Cec4_ManGeneratePatterns( Cec4_Man_t * p )
{
    abctime clk = Abc_Clock();
    int i, iCand, nPats = 64 * p->pAig->nSimWords, Count = 0, Packs = 0;
1216 1217 1218
    p->pAig->iPatsPi = 0;
    Vec_WrdFill( p->pAig->vSimsPi, Vec_WrdSize(p->pAig->vSimsPi), 0 );
    for ( i = 0; i < 100 * nPats; i++ )
1219
        if ( (iCand = Cec4_ManCandIterNext(p)) )
1220
        {
1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237
            int iRepr    = Gia_ObjRepr( p->pAig, iCand );
            int iCandVal = Gia_ManObj(p->pAig, iCand)->fPhase;
            int iReprVal = Gia_ManObj(p->pAig, iRepr)->fPhase;
            int Res = Cec4_ManGeneratePatternOne( p->pAig, iRepr,  iReprVal, iCand, !iCandVal, p->vPat, p->vVisit );
            if ( !Res )
                Res = Cec4_ManGeneratePatternOne( p->pAig, iRepr, !iReprVal, iCand,  iCandVal, p->vPat, p->vVisit );
            if ( Res )
            {
                int Ret = Cec4_ManPackAddPattern( p->pAig, p->vPat );
                Packs += Ret;
                if ( Ret == 64 * p->pAig->nSimWords )
                    break;
                if ( ++Count == 4 * 64 * p->pAig->nSimWords )
                    break;
                //Cec4_ManCexVerify( p->pAig, iRepr, iCand, iReprVal ^ iCandVal );
                //Gia_ManCleanMark01( p->pAig );
            }
1238
        }
1239 1240 1241
    p->nSatSat += Count;
    //printf( "%3d : %6.2f %% : Generated %d CEXs after trying %d pairs. Ave tries = %.2f. Ave packs = %.2f\n", p->nItersSim++, 100.0*Vec_IntSize(p->vCands)/Gia_ManAndNum(p->pAig),
    //    Count, 100 * nPats, (float)p->pPars->nGenIters * nPats / Abc_MaxInt(1, Count), (float)Packs / Abc_MaxInt(1, Count) );
1242
    p->timeGenPats += Abc_Clock() - clk;
1243
    return Count >= 100 * nPats / 1000 / 2;
1244 1245
}

1246

1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261
/**Function*************************************************************

  Synopsis    [Internal simulation APIs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec4_ManSatSolverRecycle( Cec4_Man_t * p )
{
    Gia_Obj_t * pObj;
    int i;
1262
    //printf( "Solver size = %d.\n", sat_solver_varnum(p->pSat) );
1263 1264
    p->nRecycles++;
    p->nCallsSince = 0;
1265
    sat_solver_reset( p->pSat );
1266 1267 1268
    // clean mapping of AigIds into SatIds
    Gia_ManForEachObjVec( &p->pNew->vSuppVars, p->pNew, pObj, i )
        Cec4_ObjCleanSatId( p->pNew, pObj );
1269 1270 1271
    Vec_IntClear( &p->pNew->vSuppVars  );  // AigIds for which SatId is defined
    Vec_IntClear( &p->pNew->vCopiesTwo );  // pairs (CiAigId, SatId)
    Vec_IntClear( &p->pNew->vVarMap    );  // mapping of SatId into AigId
1272 1273 1274
}
int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose )
{
1275
    abctime clk;
1276 1277
    int nBTLimit = Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1) ? p->pPars->nBTLimit/10 : p->pPars->nBTLimit;
    int nConfEnd, nConfBeg, status, iVar0, iVar1, Lits[2];
1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289
    int UnsatConflicts[3] = {0};
    if ( iObj1 <  iObj0 ) 
         iObj1 ^= iObj0, iObj0 ^= iObj1, iObj1 ^= iObj0;
    assert( iObj0 < iObj1 );    
    *pfEasy = 0;
    // check if SAT solver needs recycling
    p->nCallsSince++; 
    if ( p->nCallsSince > p->pPars->nCallsRecycle && 
         Vec_IntSize(&p->pNew->vSuppVars) > p->pPars->nSatVarMax && p->pPars->nSatVarMax )
        Cec4_ManSatSolverRecycle( p );
    // add more logic to the solver
    if ( !iObj0 && Cec4_ObjSatId(p->pNew, Gia_ManConst0(p->pNew)) == -1 )
1290
        Cec4_ObjSetSatId( p->pNew, Gia_ManConst0(p->pNew), sat_solver_addvar(p->pSat) );
1291
    clk = Abc_Clock();
1292 1293
    iVar0 = Cec4_ObjGetCnfVar( p, iObj0 );
    iVar1 = Cec4_ObjGetCnfVar( p, iObj1 );
1294 1295 1296 1297 1298 1299
    if( sat_solver_jftr( p->pSat ) )
    {
        sat_solver_start_new_round( p->pSat );
        sat_solver_mark_cone( p->pSat, Cec4_ObjSatId(p->pNew, Gia_ManObj(p->pNew, iObj0)) );
        sat_solver_mark_cone( p->pSat, Cec4_ObjSatId(p->pNew, Gia_ManObj(p->pNew, iObj1)) );
    }
1300
    p->timeCnf += Abc_Clock() - clk;
1301 1302 1303
    // perform solving
    Lits[0] = Abc_Var2Lit(iVar0, 1);
    Lits[1] = Abc_Var2Lit(iVar1, fPhase);
1304
    sat_solver_set_conflict_budget( p->pSat, nBTLimit );
1305 1306 1307
    nConfBeg = sat_solver_conflictnum( p->pSat );
    status = sat_solver_solve( p->pSat, Lits, 2 );
    nConfEnd = sat_solver_conflictnum( p->pSat );
1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333
    assert( nConfEnd >= nConfBeg );
    if ( fVerbose )
    {
        if ( status == GLUCOSE_SAT ) 
        {
            p->nConflicts[0][0] += nConfEnd == nConfBeg;
            p->nConflicts[0][1] += nConfEnd -  nConfBeg;
            p->nConflicts[0][2]  = Abc_MaxInt(p->nConflicts[0][2], nConfEnd - nConfBeg);
            *pfEasy = nConfEnd == nConfBeg;
        }
        else if ( status == GLUCOSE_UNSAT ) 
        {
            if ( iObj0 > 0 )
            {
                UnsatConflicts[0] = nConfEnd == nConfBeg;
                UnsatConflicts[1] = nConfEnd -  nConfBeg;
                UnsatConflicts[2] = Abc_MaxInt(p->nConflicts[1][2], nConfEnd - nConfBeg);
            }
            else
            {
                p->nConflicts[1][0] += nConfEnd == nConfBeg;
                p->nConflicts[1][1] += nConfEnd -  nConfBeg;
                p->nConflicts[1][2]  = Abc_MaxInt(p->nConflicts[1][2], nConfEnd - nConfBeg);
                *pfEasy = nConfEnd == nConfBeg;
            }
        }
1334 1335
        else 
            return status;
1336 1337 1338 1339 1340
    }
    if ( status == GLUCOSE_UNSAT && iObj0 > 0 )
    {
        Lits[0] = Abc_Var2Lit(iVar0, 0);
        Lits[1] = Abc_Var2Lit(iVar1, !fPhase);
1341
        sat_solver_set_conflict_budget( p->pSat, nBTLimit );
1342 1343 1344
        nConfBeg = sat_solver_conflictnum( p->pSat );
        status = sat_solver_solve( p->pSat, Lits, 2 );
        nConfEnd = sat_solver_conflictnum( p->pSat );
1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372
        assert( nConfEnd >= nConfBeg );
        if ( fVerbose )
        {
            if ( status == GLUCOSE_SAT ) 
            {
                p->nConflicts[0][0] += nConfEnd == nConfBeg;
                p->nConflicts[0][1] += nConfEnd -  nConfBeg;
                p->nConflicts[0][2]  = Abc_MaxInt(p->nConflicts[0][2], nConfEnd - nConfBeg);
                *pfEasy = nConfEnd == nConfBeg;
            }
            else if ( status == GLUCOSE_UNSAT ) 
            {
                UnsatConflicts[0]  &= nConfEnd == nConfBeg;
                UnsatConflicts[1]  += nConfEnd -  nConfBeg;
                UnsatConflicts[2]   = Abc_MaxInt(p->nConflicts[1][2], nConfEnd - nConfBeg);

                p->nConflicts[1][0] += UnsatConflicts[0];
                p->nConflicts[1][1] += UnsatConflicts[1];
                p->nConflicts[1][2]  = Abc_MaxInt(p->nConflicts[1][2], UnsatConflicts[2]);
                *pfEasy = UnsatConflicts[0];
            }
        }
    }
    return status;
}
int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
{
    abctime clk = Abc_Clock();
1373
    int i, iLit, IdAig, IdSat, status, fEasy, RetValue = 1;
1374 1375 1376 1377 1378 1379
    Gia_Obj_t * pObj = Gia_ManObj( p->pAig, iObj );
    Gia_Obj_t * pRepr = Gia_ManObj( p->pAig, iRepr );
    int fCompl = Abc_LitIsCompl(pObj->Value) ^ Abc_LitIsCompl(pRepr->Value) ^ pObj->fPhase ^ pRepr->fPhase;
    status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose );
    if ( status == GLUCOSE_SAT )
    {
1380
        int * pCex;
1381 1382 1383 1384 1385
        //printf( "Disproved: %d == %d.\n", Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value) );
        p->nSatSat++;
        p->nPatterns++;
        p->pAig->iPatsPi++;
        assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
1386 1387
        //Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
        //    Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) );
Alan Mishchenko's avatar
Alan Mishchenko committed
1388
        pCex = NULL;//sat_solver_read_cex( p->pSat );
1389 1390 1391 1392 1393 1394 1395 1396
        Vec_IntClear( p->vPat );
        if ( pCex == NULL )
        {
            Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
                Vec_IntPush( p->vPat, Abc_Var2Lit(IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat)) );
        }
        else
        {
1397
            int * pMap = Vec_IntArray(&p->pNew->vVarMap);
1398
            for ( i = 0; i < pCex[0]; )
1399
                Vec_IntPush( p->vPat, Abc_Lit2LitV(pMap, Abc_LitNot(pCex[++i])) );
1400 1401 1402
        }
        Vec_IntForEachEntry( p->vPat, iLit, i )
            Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) );
1403 1404 1405 1406 1407 1408
        if ( fEasy )
            p->timeSatSat0 += Abc_Clock() - clk;
        else
            p->timeSatSat += Abc_Clock() - clk;
        RetValue = 0;
        // this is not needed, but we keep it here anyway, because it takes very little time
1409
        //Cec4_ManVerify( p->pNew, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, p->pSat );
1410 1411 1412 1413
        // resimulated once in a while
        if ( p->pAig->iPatsPi == 64 * p->pAig->nSimWords - 1 )
        {
            abctime clk2 = Abc_Clock();
1414
            Cec4_ManSimulate( p->pAig, p );
1415
            //if ( p->nSatSat && p->nSatSat % 100 == 0 )
1416
                Cec4_ManPrintStats( p->pAig, p->pPars, p, 0 );
1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440
            Vec_IntFill( p->vCexStamps, Gia_ManObjNum(p->pAig), 0 );
            p->pAig->iPatsPi = 0;
            p->timeResimGlo += Abc_Clock() - clk2;
        }
    }
    else if ( status == GLUCOSE_UNSAT )
    {
        //printf( "Proved: %d == %d.\n", Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value) );
        p->nSatUnsat++;
        pObj->Value = Abc_LitNotCond( pRepr->Value, fCompl );
        Gia_ObjSetProved( p->pAig, iObj );
        if ( iRepr == 0 )
            p->iLastConst = iObj;
        if ( fEasy )
            p->timeSatUnsat0 += Abc_Clock() - clk;
        else
            p->timeSatUnsat += Abc_Clock() - clk;
        RetValue = 1;
    }
    else 
    {
        p->nSatUndec++;
        assert( status == GLUCOSE_UNDEC );
        Gia_ObjSetFailed( p->pAig, iObj );
1441 1442 1443
        Vec_BitWriteEntry( p->vFails, iObj, 1 );
        //if ( iRepr )
        //Vec_BitWriteEntry( p->vFails, iRepr, 1 );
1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480
        p->timeSatUndec += Abc_Clock() - clk;
        RetValue = 2;
    }
    return RetValue;
}
Gia_Obj_t * Cec4_ManFindRepr( Gia_Man_t * p, Cec4_Man_t * pMan, int iObj )
{
    abctime clk = Abc_Clock();
    int iMem, iRepr;
    assert( Gia_ObjHasRepr(p, iObj) );
    assert( !Gia_ObjProved(p, iObj) );
    iRepr = Gia_ObjRepr(p, iObj);
    assert( iRepr != iObj );
    assert( !Gia_ObjProved(p, iRepr) );
    Cec4_ManSimulate_rec( p, pMan, iObj );
    Cec4_ManSimulate_rec( p, pMan, iRepr );
    if ( Cec4_ObjSimEqual(p, iObj, iRepr) )
    {
        pMan->timeResimLoc += Abc_Clock() - clk;
        return Gia_ManObj(p, iRepr);
    }
    Gia_ClassForEachObj1( p, iRepr, iMem )
    {
        if ( iObj == iMem )
            break;
        if ( Gia_ObjProved(p, iMem) )
            continue;
        Cec4_ManSimulate_rec( p, pMan, iMem );
        if ( Cec4_ObjSimEqual(p, iObj, iMem) )
        {
            pMan->timeResimLoc += Abc_Clock() - clk;
            return Gia_ManObj(p, iMem);
        }
    }
    pMan->timeResimLoc += Abc_Clock() - clk;
    return NULL;
}
1481
int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew )
1482 1483
{
    Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars ); 
1484 1485
    Gia_Obj_t * pObj, * pRepr; 
    int i, fSimulate = 1;
1486
    if ( pPars->fVerbose )
Alan Mishchenko's avatar
Alan Mishchenko committed
1487 1488
        printf( "Solver type = %d. Simulate %d words in %d rounds. SAT with %d confs. Recycle after %d SAT calls.\n", 
            pPars->jType, pPars->nWords, pPars->nRounds, pPars->nBTLimit, pPars->nCallsRecycle );
1489

1490 1491 1492 1493
    // this is currently needed to have a correct mapping
    Gia_ManForEachCi( p, pObj, i )
        assert( Gia_ObjId(p, pObj) == i+1 );

1494
    // check if any output trivially fails under all-0 pattern
1495
    Gia_ManRandom( 1 );
1496
    Gia_ManSetPhase( p );
1497
    //Gia_ManStaticFanoutStart( p );
1498
    if ( pPars->fCheckMiter ) 
1499 1500 1501 1502 1503 1504 1505 1506 1507 1508
    {
        Gia_ManForEachCo( p, pObj, i )
            if ( pObj->fPhase )
            {
                p->pCexSeq = Cec4_ManDeriveCex( p, i, -1 );
                goto finalize;
            }
    }

    // simulate one round and create classes
1509
    Cec4_ManSimAlloc( p, pPars->nWords );
1510
    Cec4_ManSimulateCis( p );
1511
    Cec4_ManSimulate( p, pMan );
1512
    if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected
1513 1514
        goto finalize;
    if ( pPars->fVerbose )
1515
        Cec4_ManPrintStats( p, pPars, pMan, 1 );
1516

1517
    // perform simulation
1518
    for ( i = 0; i < pPars->nRounds; i++ )
1519 1520
    {
        Cec4_ManSimulateCis( p );
1521
        Cec4_ManSimulate( p, pMan );
1522
        if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected
1523
            goto finalize;
Alan Mishchenko's avatar
Alan Mishchenko committed
1524
        if ( i && i % (pPars->nRounds / 5) == 0 && pPars->fVerbose )
1525 1526 1527 1528
            Cec4_ManPrintStats( p, pPars, pMan, 1 );
    }

    // perform additional simulation
1529
    Cec4_ManCandIterStart( pMan );
1530 1531 1532 1533 1534 1535 1536
    for ( i = 0; fSimulate && i < pPars->nGenIters; i++ )
    {
        Cec4_ManSimulateCis( p );
        fSimulate = Cec4_ManGeneratePatterns( pMan );
        Cec4_ManSimulate( p, pMan );
        if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected
            goto finalize;
Alan Mishchenko's avatar
Alan Mishchenko committed
1537
        if ( i && i % 5 == 0 && pPars->fVerbose )
1538
            Cec4_ManPrintStats( p, pPars, pMan, 1 );
1539
    }
Alan Mishchenko's avatar
Alan Mishchenko committed
1540 1541
    if ( i && i % 5 && pPars->fVerbose )
        Cec4_ManPrintStats( p, pPars, pMan, 1 );
1542

1543
    p->iPatsPi = 0;
1544
    pMan->nSatSat = 0;
1545
    pMan->pNew = Cec4_ManStartNew( p );
1546 1547
    Gia_ManForEachAnd( p, pObj, i )
    {
1548
        Gia_Obj_t * pObjNew; 
1549
        pMan->nAndNodes++;
1550
        pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
1551
        pObjNew = Gia_ManObj( pMan->pNew, Abc_Lit2Var(pObj->Value) );
1552
        if ( Gia_ObjIsAnd(pObjNew) )
1553 1554 1555
        if ( Vec_BitEntry(pMan->vFails, Gia_ObjFaninId0(pObjNew, Abc_Lit2Var(pObj->Value))) || 
             Vec_BitEntry(pMan->vFails, Gia_ObjFaninId1(pObjNew, Abc_Lit2Var(pObj->Value))) )
            Vec_BitWriteEntry( pMan->vFails, Abc_Lit2Var(pObjNew->Value), 1 );
1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581
        //if ( Gia_ObjIsAnd(pObjNew) )
        //    Gia_ObjSetAndLevel( pMan->pNew, pObjNew );
        // select representative based on candidate equivalence classes
        pRepr = Gia_ObjReprObj( p, i );
        if ( pRepr == NULL )
            continue;
        if ( 1 ) // select representative based on recent counter-examples
        {
            pRepr = Cec4_ManFindRepr( p, pMan, i );
            if ( pRepr == NULL )
                continue;
        }
        if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
        {
            assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
            Gia_ObjSetProved( p, i );
            if ( Gia_ObjId(p, pRepr) == 0 )
                pMan->iLastConst = i;
            continue;
        }
        if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) )
            pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
    }
    if ( p->iPatsPi > 0 )
    {
        abctime clk2 = Abc_Clock();
1582
        Cec4_ManSimulate( p, pMan );
1583 1584 1585 1586 1587
        Vec_IntFill( pMan->vCexStamps, Gia_ManObjNum(p), 0 );
        p->iPatsPi = 0;
        pMan->timeResimGlo += Abc_Clock() - clk2;
    }
    if ( pPars->fVerbose )
1588
        Cec4_ManPrintStats( p, pPars, pMan, 0 );
1589 1590 1591 1592 1593 1594 1595 1596 1597 1598 1599 1600 1601 1602 1603
    if ( ppNew )
    {
        Gia_ManForEachCo( p, pObj, i )
            pObj->Value = Gia_ManAppendCo( pMan->pNew, Gia_ObjFanin0Copy(pObj) );
        *ppNew = Gia_ManCleanup( pMan->pNew );
    }
finalize:
    if ( pPars->fVerbose )
        printf( "Performed %d SAT calls:  P = %d (0=%d a=%.2f m=%d)  D = %d (0=%d a=%.2f m=%d)  F = %d   Sim = %d  Recyc = %d\n", 
            pMan->nSatUnsat + pMan->nSatSat + pMan->nSatUndec, 
            pMan->nSatUnsat, pMan->nConflicts[1][0], (float)pMan->nConflicts[1][1]/Abc_MaxInt(1, pMan->nSatUnsat-pMan->nConflicts[1][0]), pMan->nConflicts[1][2],
            pMan->nSatSat,   pMan->nConflicts[0][0], (float)pMan->nConflicts[0][1]/Abc_MaxInt(1, pMan->nSatSat  -pMan->nConflicts[0][0]), pMan->nConflicts[0][2],  
            pMan->nSatUndec,  
            pMan->nSimulates, pMan->nRecycles );
    Cec4_ManDestroy( pMan );
1604
    //Gia_ManStaticFanoutStop( p );
1605 1606 1607
    //Gia_ManEquivPrintClasses( p, 1, 0 );
    return p->pCexSeq ? 0 : 1;
}
1608
Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
1609 1610 1611 1612 1613 1614 1615 1616 1617 1618 1619 1620 1621
{
    Gia_Man_t * pNew = NULL;
    Cec4_ManPerformSweeping( p, pPars, &pNew );
    return pNew;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END