saigGlaPba.c 18.2 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
/**CFile****************************************************************

  FileName    [saigGlaPba.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Sequential AIG package.]

  Synopsis    [Gate level abstraction.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

***********************************************************************/
20
 
21
#include "saig.h"
22 23
#include "sat/bsat/satSolver.h"
#include "sat/bsat/satStore.h"
24 25 26 27 28 29 30 31 32 33 34 35 36

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Aig_Gla2Man_t_ Aig_Gla2Man_t;
struct Aig_Gla2Man_t_
{
    // user data
    Aig_Man_t *    pAig;
37
    int            nStart;
38 39 40 41 42 43
    int            nFramesMax;
    int            fVerbose;
    // unrolling
    Vec_Int_t *    vObj2Vec;   // maps obj ID into its vec ID
    Vec_Int_t *    vVec2Var;   // maps vec ID into its sat Var (nFrames per vec ID)
    Vec_Int_t *    vVar2Inf;   // maps sat Var into its frame and obj ID
44 45 46 47
    // clause mapping
    Vec_Int_t *    vCla2Obj;   // maps clause into its root object
    Vec_Int_t *    vCla2Fra;   // maps clause into its frame
    Vec_Int_t *    vVec2Use;   // maps vec ID into its used frames (nFrames per vec ID)
48 49 50
    // SAT solver
    sat_solver *   pSat;
    // statistics
51 52 53
    clock_t        timePre;
    clock_t        timeSat;
    clock_t        timeTotal;
54 55 56 57 58 59
};

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

60

61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200
/**Function*************************************************************

  Synopsis    [Adds constant to the solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Aig_Gla2AddConst( sat_solver * pSat, int iVar, int fCompl )
{
    lit Lit = toLitCond( iVar, fCompl );
    if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
        return 0;
    return 1;
}

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

  Synopsis    [Adds buffer to the solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Aig_Gla2AddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
{
    lit Lits[2];

    Lits[0] = toLitCond( iVar0, 0 );
    Lits[1] = toLitCond( iVar1, !fCompl );
    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
        return 0;

    Lits[0] = toLitCond( iVar0, 1 );
    Lits[1] = toLitCond( iVar1, fCompl );
    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
        return 0;

    return 1;
}

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

  Synopsis    [Adds buffer to the solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Aig_Gla2AddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
{
    lit Lits[3];

    Lits[0] = toLitCond( iVar, 1 );
    Lits[1] = toLitCond( iVar0, fCompl0 );
    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
        return 0;

    Lits[0] = toLitCond( iVar, 1 );
    Lits[1] = toLitCond( iVar1, fCompl1 );
    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
        return 0;

    Lits[0] = toLitCond( iVar, 0 );
    Lits[1] = toLitCond( iVar0, !fCompl0 );
    Lits[2] = toLitCond( iVar1, !fCompl1 );
    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
        return 0;

    return 1;
}


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

  Synopsis    [Finds existing SAT variable or creates a new one.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Aig_Gla2FetchVar( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int k )
{
    int i, iVecId, iSatVar;
    assert( k < p->nFramesMax );
    iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
    if ( iVecId == 0 )
    {
        iVecId = Vec_IntSize( p->vVec2Var ) / p->nFramesMax;
        for ( i = 0; i < p->nFramesMax; i++ )
            Vec_IntPush( p->vVec2Var, 0 );
        Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId );
    }
    iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFramesMax + k );
    if ( iSatVar == 0 )
    {
        iSatVar = Vec_IntSize( p->vVar2Inf ) / 2;
        Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) );
        Vec_IntPush( p->vVar2Inf, k );
        Vec_IntWriteEntry( p->vVec2Var, iVecId * p->nFramesMax + k, iSatVar );
    }
    return iSatVar;
}

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

  Synopsis    [Assigns variables to the AIG nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Aig_Gla2AssignVars_rec( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int f )
{
    int nVars = Vec_IntSize(p->vVar2Inf);
    Aig_Gla2FetchVar( p, pObj, f );
    if ( nVars == Vec_IntSize(p->vVar2Inf) )
        return;
    if ( Aig_ObjIsConst1(pObj) )
        return;
    if ( Saig_ObjIsPo( p->pAig, pObj ) )
    {
        Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
        return;
    }
201
    if ( Aig_ObjIsCi( pObj ) )
202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229
    {
        if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 )
            Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
    Aig_Gla2AssignVars_rec( p, Aig_ObjFanin1(pObj), f );
}

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

  Synopsis    [Creates SAT solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
{
    Vec_Int_t * vPoLits;
    Aig_Obj_t * pObj;
    int i, f, ObjId, nVars, RetValue = 1;

    // assign variables
230 231
    for ( f = p->nFramesMax - 1; f >= 0; f-- )
//    for ( f = 0; f < p->nFramesMax; f++ )
232
        Aig_Gla2AssignVars_rec( p, Aig_ManCo(p->pAig, 0), f );
233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254

    // create SAT solver
    p->pSat = sat_solver_new();
    sat_solver_store_alloc( p->pSat ); 
    sat_solver_setnvars( p->pSat, Vec_IntSize(p->vVar2Inf)/2 );

    // add clauses
    nVars = Vec_IntSize( p->vVar2Inf );
    Vec_IntForEachEntryDouble( p->vVar2Inf, ObjId, f, i )
    {
        if ( ObjId == -1 )
            continue;
        pObj = Aig_ManObj( p->pAig, ObjId );
        if ( Aig_ObjIsNode(pObj) )
        {
            RetValue &= Aig_Gla2AddNode( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 
                                                  Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f), 
                                                  Aig_Gla2FetchVar(p, Aig_ObjFanin1(pObj), f), 
                                                  Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
            Vec_IntPush( p->vCla2Obj, ObjId );
            Vec_IntPush( p->vCla2Obj, ObjId );
            Vec_IntPush( p->vCla2Obj, ObjId );
255 256 257 258

            Vec_IntPush( p->vCla2Fra, f );
            Vec_IntPush( p->vCla2Fra, f );
            Vec_IntPush( p->vCla2Fra, f );
259 260 261 262 263 264 265
        }
        else if ( Saig_ObjIsLo(p->pAig, pObj) )
        {
            if ( f == 0 )
            {
                RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 1 );
                Vec_IntPush( p->vCla2Obj, ObjId );
266 267

                Vec_IntPush( p->vCla2Fra, f );
268 269 270 271 272 273 274 275 276
            }
            else
            {
                Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
                RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 
                                                        Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObjLi), f-1), 
                                                        Aig_ObjFaninC0(pObjLi) );
                Vec_IntPush( p->vCla2Obj, ObjId );
                Vec_IntPush( p->vCla2Obj, ObjId );
277 278 279

                Vec_IntPush( p->vCla2Fra, f );
                Vec_IntPush( p->vCla2Fra, f );
280 281 282 283 284 285 286 287 288
            }
        }
        else if ( Saig_ObjIsPo(p->pAig, pObj) )
        {
            RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 
                                                    Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f), 
                                                    Aig_ObjFaninC0(pObj) );
            Vec_IntPush( p->vCla2Obj, ObjId );
            Vec_IntPush( p->vCla2Obj, ObjId );
289 290 291

            Vec_IntPush( p->vCla2Fra, f );
            Vec_IntPush( p->vCla2Fra, f );
292 293 294 295 296
        }
        else if ( Aig_ObjIsConst1(pObj) )
        {
            RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 0 );
            Vec_IntPush( p->vCla2Obj, ObjId );
297 298

            Vec_IntPush( p->vCla2Fra, f );
299 300 301 302 303 304
        }
        else assert( Saig_ObjIsPi(p->pAig, pObj) );
    }

    // add output clause
    vPoLits = Vec_IntAlloc( p->nFramesMax );
305
    for ( f = p->nStart; f < p->nFramesMax; f++ )
306
        Vec_IntPush( vPoLits, 2 * Aig_Gla2FetchVar(p, Aig_ManCo(p->pAig, 0), f) );
307 308 309
    RetValue &= sat_solver_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) );
    Vec_IntFree( vPoLits );
    Vec_IntPush( p->vCla2Obj, 0 );
310 311
    Vec_IntPush( p->vCla2Fra, 0 );
    assert( Vec_IntSize(p->vCla2Fra) == Vec_IntSize(p->vCla2Obj) );
312 313 314

    assert( nVars == Vec_IntSize(p->vVar2Inf) );
    assert( ((Sto_Man_t *)p->pSat->pStore)->nClauses == Vec_IntSize(p->vCla2Obj) );
315
//    Sto_ManDumpClauses( ((Sto_Man_t *)p->pSat->pStore), "temp_sto.cnf" );
316
    sat_solver_store_mark_roots( p->pSat ); 
317 318

    if ( p->fVerbose )
319 320
        printf( "The resulting SAT problem contains %d variables and %d clauses.\n", 
            p->pSat->size, p->pSat->stats.clauses );
321 322 323 324 325 326 327 328 329 330 331 332 333 334
    return RetValue;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
335
Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nStart, int nFramesMax, int fVerbose )
336 337 338 339 340 341 342 343 344 345 346
{
    Aig_Gla2Man_t * p;
    int i;

    p = ABC_CALLOC( Aig_Gla2Man_t, 1 );
    p->pAig       = pAig;

    p->vObj2Vec   = Vec_IntStart( Aig_ManObjNumMax(pAig) );
    p->vVec2Var   = Vec_IntAlloc( 1 << 20 );
    p->vVar2Inf   = Vec_IntAlloc( 1 << 20 );
    p->vCla2Obj   = Vec_IntAlloc( 1 << 20 );
347
    p->vCla2Fra   = Vec_IntAlloc( 1 << 20 );
348 349

    // skip first vector ID
350
    p->nStart     = nStart;
351
    p->nFramesMax = nFramesMax;
352
    p->fVerbose   = fVerbose;
353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378
    for ( i = 0; i < p->nFramesMax; i++ )
        Vec_IntPush( p->vVec2Var, -1 );

    // skip  first SAT variable
    Vec_IntPush( p->vVar2Inf, -1 );
    Vec_IntPush( p->vVar2Inf, -1 );
    return p;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Aig_Gla2ManStop( Aig_Gla2Man_t * p )
{
    Vec_IntFreeP( &p->vObj2Vec );
    Vec_IntFreeP( &p->vVec2Var );
    Vec_IntFreeP( &p->vVar2Inf );
    Vec_IntFreeP( &p->vCla2Obj );
379 380
    Vec_IntFreeP( &p->vCla2Fra );
    Vec_IntFreeP( &p->vVec2Use );
381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403

    if ( p->pSat )
        sat_solver_delete( p->pSat );
    ABC_FREE( p );
}


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

  Synopsis    [Finds the set of clauses involved in the UNSAT core.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose, int * piRetValue )
{
    Vec_Int_t * vCore;
    void * pSatCnf; 
    Intp_Man_t * pManProof;
404 405
    int RetValue;
    clock_t clk = clock();
406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423
    if ( piRetValue )
        *piRetValue = -1;
    // solve the problem
    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( RetValue == l_Undef )
    {
        printf( "Conflict limit is reached.\n" );
        return NULL;
    }
    if ( RetValue == l_True )
    {
        printf( "The BMC problem is SAT.\n" );
        if ( piRetValue )
            *piRetValue = 0;
        return NULL;
    }
    if ( fVerbose )
    {
424
        printf( "SAT solver returned UNSAT after %7d conflicts.      ", (int)pSat->stats.conflicts );
425
        Abc_PrintTime( 1, "Time", clock() - clk );
426 427 428 429
    }
    assert( RetValue == l_False );
    pSatCnf = sat_solver_store_release( pSat ); 
    // derive the UNSAT core
430
    clk = clock();
431 432 433 434 435
    pManProof = Intp_ManAlloc();
    vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0 );
    Intp_ManFree( pManProof );
    if ( fVerbose )
    {
436 437
        printf( "SAT core contains %8d clauses (out of %8d).   ", Vec_IntSize(vCore), sat_solver_nclauses(pSat) );
        Abc_PrintTime( 1, "Time", clock() - clk );
438
    }
439
    Sto_ManFree( (Sto_Man_t *)pSatCnf );
440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457
    return vCore;
}

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

  Synopsis    [Collects abstracted objects.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore )
{
    Vec_Int_t * vResult;
    Aig_Obj_t * pObj;
458 459 460
    int i, ClaId, iVecId;
//    p->vVec2Use = Vec_IntStart( Vec_IntSize(p->vVec2Var) );

461 462 463 464 465
    vResult = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
    Vec_IntWriteEntry( vResult, 0, 1 ); // add const1
    Vec_IntForEachEntry( vCore, ClaId, i )
    {
        pObj = Aig_ManObj( p->pAig, Vec_IntEntry(p->vCla2Obj, ClaId) );
466
        if ( Saig_ObjIsPi(p->pAig, pObj) || Saig_ObjIsPo(p->pAig, pObj) || Aig_ObjIsConst1(pObj) )
467 468 469
            continue;
        assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) );
        Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 );
470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486
/*
        // add flop inputs with multiple fanouts
        if ( Saig_ObjIsLo(p->pAig, pObj) )
        {
            Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
            if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObjLi)) )
//            if ( Aig_ObjRefs( Aig_ObjFanin0(pObjLi) ) > 1 )
                Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObjLi), 1 );
        }
        else
        {
            if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObj)) )
                Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObj), 1 );
            if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin1(pObj)) )
                Vec_IntWriteEntry( vResult, Aig_ObjFaninId1(pObj), 1 );
        }
*/
487 488 489 490 491 492
        if ( p->vVec2Use )
        {
            iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
            Vec_IntWriteEntry( p->vVec2Use, iVecId * p->nFramesMax + Vec_IntEntry(p->vCla2Fra, ClaId), 1 );
        }
    }
493
//    printf( "Number of entries %d\n", Vec_IntCountPositive(vResult) );
494 495 496 497 498 499 500 501 502 503 504 505 506 507

    // count the number of objects in each frame
    if ( p->vVec2Use )
    {
        Vec_Int_t * vCounts = Vec_IntStart( p->nFramesMax );
        int v, f, Entry, nVecIds = Vec_IntSize(p->vVec2Use) / p->nFramesMax;
        for ( f = 0; f < p->nFramesMax; f++ )
        for ( v = 0; v < nVecIds; v++ )
            if ( Vec_IntEntry( p->vVec2Use, v * p->nFramesMax + f ) )
                Vec_IntAddToEntry( vCounts, f, 1 );
        Vec_IntForEachEntry( vCounts, Entry, f )
            printf( "%d ", Entry );
        printf( "\n" );
        Vec_IntFree( vCounts );
508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524
    }
    return vResult;
}

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

  Synopsis    [Performs gate-level localization abstraction.]

  Description [Returns array of objects included in the abstraction. This array
  may contain only const1, flop outputs, and internal nodes, that is, objects
  that should have clauses added to the SAT solver.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
525
Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose )
526 527 528
{
    Aig_Gla2Man_t * p;
    Vec_Int_t * vCore, * vResult;
529 530
    clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0;
    clock_t clk, clk2 = clock();
531 532 533 534 535 536 537 538 539 540 541
    assert( Saig_ManPoNum(pAig) == 1 );

    if ( fVerbose )
    {
        if ( TimeLimit )
            printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit );
        else
            printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax );
    }

    // start the solver
542
    clk = clock();
543
    p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose );
544 545 546 547 548 549
    if ( !Aig_Gla2CreateSatSolver( p ) )
    {
        printf( "Error!  SAT solver became UNSAT.\n" );
        Aig_Gla2ManStop( p );
        return NULL;
    }
550
    sat_solver_set_random( p->pSat, fSkipRand );
551
    p->timePre += clock() - clk;
552 553 554

    // set runtime limit
    if ( TimeLimit )
555
        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
556 557

    // compute UNSAT core
558
    clk = clock();
559 560 561 562 563 564
    vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL );
    if ( vCore == NULL )
    {
        Aig_Gla2ManStop( p );
        return NULL;
    }
565 566
    p->timeSat += clock() - clk;
    p->timeTotal += clock() - clk2;
567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589

    // print stats
    if ( fVerbose )
    {
        ABC_PRTP( "Pre   ", p->timePre,   p->timeTotal );
        ABC_PRTP( "Sat   ", p->timeSat,   p->timeTotal );
        ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
    }

    // prepare return value
    vResult = Aig_Gla2ManCollect( p, vCore );
    Vec_IntFree( vCore );
    Aig_Gla2ManStop( p );
    return vResult;
}

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


ABC_NAMESPACE_IMPL_END