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

ABC: System for Sequential Synthesis and Verification

http://www.eecs.berkeley.edu/~alanmi/abc/

Copyright (c) The Regents of the University of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or
royalty fees, to use, copy, modify, and distribute this software and its
documentation for any purpose, provided that the above copyright notice and
the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF
THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING,
BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS,
AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE,
SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.

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

/**CFile****************************************************************

  FileName    [main.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [The main package.]

  Synopsis    [Here everything starts.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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


#include "base/abc/abc.h"
#include "mainInt.h"
#include "base/wlc/wlc.h"

ABC_NAMESPACE_IMPL_START


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

static int TypeCheck( Abc_Frame_t * pAbc, const char * s);

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


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

  Synopsis    [The main() procedure.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_RealMain( int argc, char * argv[] )
{
    Abc_Frame_t * pAbc;
    Vec_Str_t* sCommandUsr = Vec_StrAlloc(1000);
    char sCommandTmp[ABC_MAX_STR], sReadCmd[1000], sWriteCmd[1000];
    const char * sOutFile, * sInFile;
    char * sCommand;
    int  fStatus = 0;
    int c, fInitSource, fInitRead, fFinalWrite;

    enum {
        INTERACTIVE, // interactive mode
        BATCH, // batch mode, run a command and quit
        BATCH_THEN_INTERACTIVE, // run a command, then back to interactive mode
        BATCH_QUIET, // as in batch mode, but don't echo the command
        BATCH_QUIET_THEN_INTERACTIVE, // as in batch then interactive mode, but don't echo the command
        BATCH_SMT // special batch mode, which expends SMTLIB problem via stdin
    } fBatch;

    // added to detect memory leaks
    // watch for {,,msvcrtd.dll}*__p__crtBreakAlloc()
    // (http://support.microsoft.com/kb/151585)
#if defined(_DEBUG) && defined(_MSC_VER)
    _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
#endif

    // get global frame (singleton pattern)
    // will be initialized on first call
    pAbc = Abc_FrameGetGlobalFrame();
    pAbc->sBinary = argv[0];

    // default options
    fBatch      = INTERACTIVE;
    fInitSource = 1;
    fInitRead   = 0;
    fFinalWrite = 0;
    sInFile = sOutFile = NULL;
    sprintf( sReadCmd,  "read"  );
    sprintf( sWriteCmd, "write" );

    Extra_UtilGetoptReset();
    while ((c = Extra_UtilGetopt(argc, argv, "c:q:C:Q:S:hf:F:o:st:T:xb")) != EOF) {
        switch(c) {
            case 'c':
                if( Vec_StrSize(sCommandUsr) > 0 )
                {
                    Vec_StrAppend(sCommandUsr, " ; ");
                }
                Vec_StrAppend(sCommandUsr, globalUtilOptarg );
                fBatch = BATCH;
                break;

            case 'q':
                if( Vec_StrSize(sCommandUsr) > 0 )
                {
                    Vec_StrAppend(sCommandUsr, " ; ");
                }
                Vec_StrAppend(sCommandUsr, globalUtilOptarg );
                fBatch = BATCH_QUIET;
                break;

            case 'Q':
                if( Vec_StrSize(sCommandUsr) > 0 )
                {
                    Vec_StrAppend(sCommandUsr, " ; ");
                }
                Vec_StrAppend(sCommandUsr, globalUtilOptarg );
                fBatch = BATCH_QUIET_THEN_INTERACTIVE;
                break;

            case 'C':
                if( Vec_StrSize(sCommandUsr) > 0 )
                {
                    Vec_StrAppend(sCommandUsr, " ; ");
                }
                Vec_StrAppend(sCommandUsr, globalUtilOptarg );
                fBatch = BATCH_THEN_INTERACTIVE;
                break;

            case 'S':
                if( Vec_StrSize(sCommandUsr) > 0 )
                {
                    Vec_StrAppend(sCommandUsr, " ; ");
                }
                Vec_StrAppend(sCommandUsr, globalUtilOptarg );
                fBatch = BATCH_SMT;
                break;

            case 'f':
                if( Vec_StrSize(sCommandUsr) > 0 )
                {
                    Vec_StrAppend(sCommandUsr, " ; ");
                }
                Vec_StrPrintF(sCommandUsr, "source %s", globalUtilOptarg );
                fBatch = BATCH;
                break;

            case 'F':
                if( Vec_StrSize(sCommandUsr) > 0 )
                {
                    Vec_StrAppend(sCommandUsr, " ; ");
                }
                Vec_StrPrintF(sCommandUsr, "source -x %s", globalUtilOptarg );
                fBatch = BATCH;
                break;

            case 'h':
                goto usage;
                break;

            case 'o':
                sOutFile = globalUtilOptarg;
                fFinalWrite = 1;
                break;

            case 's':
                fInitSource = 0;
                break;

            case 't':
                if ( TypeCheck( pAbc, globalUtilOptarg ) )
                {
                    if ( (!strcmp(globalUtilOptarg, "none")) == 0 )
                    {
                        fInitRead = 1;
                        sprintf( sReadCmd, "read_%s", globalUtilOptarg );
                    }
                }
                else {
                    goto usage;
                }
                fBatch = BATCH;
                break;

            case 'T':
                if ( TypeCheck( pAbc, globalUtilOptarg ) )
                {
                    if ( (!strcmp(globalUtilOptarg, "none")) == 0)
                    {
                        fFinalWrite = 1;
                        sprintf( sWriteCmd, "write_%s", globalUtilOptarg);
                    }
                }
                else {
                    goto usage;
                }
                fBatch = BATCH;
                break;

            case 'x':
                fFinalWrite = 0;
                fInitRead   = 0;
                fBatch = BATCH;
                break;

            case 'b':
                Abc_FrameSetBridgeMode();
                break;

            default:
                goto usage;
        }
    }

    Vec_StrPush(sCommandUsr, '\0');

    if ( fBatch == BATCH_SMT )
    {
        Wlc_StdinProcessSmt( pAbc, Vec_StrArray(sCommandUsr) );
        Abc_Stop();
        return 0;
    }

    if ( Abc_FrameIsBridgeMode() )
    {
        extern Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit );
        pAbc->pGia = Gia_ManFromBridge( stdin, NULL );
    }
    else if ( fBatch!=INTERACTIVE && fBatch!=BATCH_QUIET && fBatch!=BATCH_QUIET_THEN_INTERACTIVE && Vec_StrSize(sCommandUsr)>0 )
        Abc_Print( 1, "ABC command line: \"%s\".\n\n", Vec_StrArray(sCommandUsr) );

    if ( fBatch!=INTERACTIVE )
    {
        pAbc->fBatchMode = 1;

        if (argc - globalUtilOptind == 0)
        {
            sInFile = NULL;
        }
        else if (argc - globalUtilOptind == 1)
        {
            fInitRead = 1;
            sInFile = argv[globalUtilOptind];
        }
        else
        {
            Abc_UtilsPrintUsage( pAbc, argv[0] );
        }

        // source the resource file
        if ( fInitSource )
        {
            Abc_UtilsSource( pAbc );
        }

        fStatus = 0;
        if ( fInitRead && sInFile )
        {
            sprintf( sCommandTmp, "%s %s", sReadCmd, sInFile );
            fStatus = Cmd_CommandExecute( pAbc, sCommandTmp );
        }

        if ( fStatus == 0 )
        {
            /* cmd line contains `source <file>' */
            fStatus = Cmd_CommandExecute( pAbc, Vec_StrArray(sCommandUsr) );
            if ( (fStatus == 0 || fStatus == -1) && fFinalWrite && sOutFile )
            {
                sprintf( sCommandTmp, "%s %s", sWriteCmd, sOutFile );
                fStatus = Cmd_CommandExecute( pAbc, sCommandTmp );
            }
        }

        if (fBatch == BATCH_THEN_INTERACTIVE || fBatch == BATCH_QUIET_THEN_INTERACTIVE){
            fBatch = INTERACTIVE;
            pAbc->fBatchMode = 0;
        }
    }

    Vec_StrFreeP(&sCommandUsr);

    if ( fBatch==INTERACTIVE )
    {
        // start interactive mode

        // print the hello line
        Abc_UtilsPrintHello( pAbc );
        // print history of the recent commands
        Cmd_HistoryPrint( pAbc, 10 );

        // source the resource file
        if ( fInitSource )
        {
            Abc_UtilsSource( pAbc );
        }

        // execute commands given by the user
        while ( !feof(stdin) )
        {
            // print command line prompt and
            // get the command from the user
            sCommand = Abc_UtilsGetUsersInput( pAbc );

            // execute the user's command
            fStatus = Cmd_CommandExecute( pAbc, sCommand );

            // stop if the user quitted or an error occurred
            if ( fStatus == -1 || fStatus == -2 )
                break;
        }
    }

    // if the memory should be freed, quit packages
//    if ( fStatus < 0 ) 
    {
        Abc_Stop();
    }
    return 0;

usage:
    Abc_UtilsPrintHello( pAbc );
    Abc_UtilsPrintUsage( pAbc, argv[0] );
    return 1;
}

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

  Synopsis    [Returns 1 if s is a file type recognized, else returns 0.]

  Description [Returns 1 if s is a file type recognized by ABC, else returns 0. 
  Recognized types are "blif", "bench", "pla", and "none".]

  SideEffects []

******************************************************************************/
static int TypeCheck( Abc_Frame_t * pAbc, const char * s )
{
    if (strcmp(s, "blif") == 0)
        return 1;
    else if (strcmp(s, "bench") == 0)
        return 1;
    else if (strcmp(s, "pla") == 0)
        return 1;
    else if (strcmp(s, "none") == 0)
        return 1;
    else {
        fprintf( pAbc->Err, "unknown type %s\n", s );
        return 0;
    }
}


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


ABC_NAMESPACE_IMPL_END