/*
 * UifCmd.cpp
 *
 *  Created on: Aug 25, 2015
 *      Author: Yen-Sheng Ho
 */

#ifdef _WIN32
#include <windows.h>
#else
#include <sys/time.h>
#endif

#include <iostream>
#include <iomanip>
#include <climits>
#include <regex>
#include <cstdlib>
#include <cstdio>

#include "base/wlc/wlc.h"
#include "aig/gia/giaAig.h"
#include "opt/ufar/UfarCmd.h"
#include "opt/ufar/UfarMgr.h"
#include "opt/untk/NtkNtk.h"
#include "opt/util/util.h"

ABC_NAMESPACE_IMPL_START

using namespace std;

static UFAR::UfarManager ufar_manager;

static int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAnalyzeCex( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCreateAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCreateMiter( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv );

static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc )                       { return (Wlc_Ntk_t *)pAbc->pAbcWlc;                      }
static inline void        Wlc_AbcFreeNtk( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc));  }
static inline void        Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )  { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk;             }

static string Ufar_GetStatusName( Wlc_Ntk_t * pNtk )
{
    if ( pNtk == NULL || Wlc_NtkPoNum(pNtk) == 0 )
        return "result";
    if ( Wlc_NtkPoNum(pNtk) == 1 )
        return Wlc_ObjName( pNtk, Wlc_ObjId(pNtk, Wlc_NtkPo(pNtk, 0)) );

    string Name0 = Wlc_ObjName( pNtk, Wlc_ObjId(pNtk, Wlc_NtkPo(pNtk, 0)) );
    string Name1 = Wlc_ObjName( pNtk, Wlc_ObjId(pNtk, Wlc_NtkPo(pNtk, 1)) );
    return Name0 + "_xor_" + Name1;
}

static void Ufar_DumpStatusLog( const string & FileName, int RetValue, const string & StatusName )
{
    FILE * pFile;
    if ( FileName.empty() || FileName == "none" )
        return;
    pFile = fopen( FileName.c_str(), "wb" );
    if ( pFile == NULL )
    {
        cout << "Cannot open file \"" << FileName << "\" for writing." << endl;
        return;
    }
    if ( RetValue == 1 )
        fprintf( pFile, "STATUS: UNSAT " );
    else if ( RetValue == 0 )
        fprintf( pFile, "STATUS: SAT " );
    else
        fprintf( pFile, "STATUS: ABORTED " );
    fprintf( pFile, "%s\n", StatusName.c_str() );
    fclose( pFile );
}


void Ufar_Init(Abc_Frame_t *pAbc)
{
    //Cmd_CommandAdd( pAbc, "Word level Prove", "%%test",           Abc_CommandTest,              0 );
    //Cmd_CommandAdd( pAbc, "Word level Prove", "%%cex",            Abc_CommandAnalyzeCex,        0 );
    //Cmd_CommandAdd( pAbc, "Word level Prove", "%%abs",            Abc_CommandCreateAbstraction, 0 );
    Cmd_CommandAdd( pAbc, "Word level", "%ufar",          Abc_CommandProveUsingUif,     0 );
    //Cmd_CommandAdd( pAbc, "Word level Prove", "%%miter",          Abc_CommandCreateMiter,     0 );
}

int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId )
{
    UFAR::UfarManager manager;
    timeval t1;
    set<unsigned> set_op_types;
    Wlc_Ntk_t * pUse = pNtk;
    int RetValue = -1;
    if ( pNtk == NULL )
        return -1;
    if ( Wlc_NtkPoNum(pUse) == 2 )
    {
        pUse = UFAR::CreateMiter( pUse, 0 );
        if ( pUse == NULL )
            return -1;
    }
    else if ( Wlc_NtkPoNum(pUse) != 1 )
        return -1;
    set_op_types.insert( WLC_OBJ_ARI_MULTI );
    if ( !UFAR::HasOperator( pUse, set_op_types ) )
    {
        if ( pUse != pNtk )
            Wlc_NtkFree( pUse );
        return -1;
    }
    manager.params = UFAR::UfarManager::Params();
    manager.params.RunId = RunId;
    manager.params.pFuncStop = pFuncStop;
    if ( nTimeOut > 0 )
        manager.params.nTimeout = nTimeOut;
    manager.params.iVerbosity = fVerbose ? 1 : 0;
    gettimeofday( &t1, NULL );
    manager.Initialize( pUse, set_op_types );
    RetValue = manager.PerformUIFProve( t1 );
    if ( pUse != pNtk )
        Wlc_NtkFree( pUse );
    return RetValue;
}

static int Abc_CommandCreateMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
{
    Wlc_Ntk_t * pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0);
    Wlc_AbcUpdateNtk(pAbc, pNew);
    return 0;
}

static int Abc_CommandCreateAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
{
    Wlc_Ntk_t * pNew = ufar_manager.BuildCurrentAbstraction();
    Wlc_AbcUpdateNtk(pAbc, pNew);
    return 0;
}

static int Abc_CommandAnalyzeCex( Abc_Frame_t * pAbc, int argc, char ** argv )
{
    if ( pAbc->pCex == NULL )
        {
        cout << "There is no CEX.\n";
        return 0;
    }

    // ufar_manager.GetOperatorsInCex(pAbc->pCex);
    ufar_manager.FindUifPairsUsingCex(pAbc->pCex);

    return 0;
}

static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv )
{
    if (Wlc_AbcGetNtk(pAbc) == NULL) {
        cout << "There is no current design.\n";
        return 0;
    }
    // Make each %ufar invocation stateless: always start from factory defaults.
    ufar_manager.params = UFAR::UfarManager::Params();

    OptMgr opt_mgr(argv[0]);
    opt_mgr.AddOpt("--norm", ufar_manager.params.fNorm ? "yes" : "no", "", "toggle using data type normalization");
    opt_mgr.AddOpt("--adder", "no", "", "toggle including adders");
    opt_mgr.AddOpt("--cexmin", ufar_manager.params.fCexMin ? "yes" : "no", "", "toggle using CEX minimization");
    opt_mgr.AddOpt("--sim", "none", "str", "use simulation and specify its setting");
    opt_mgr.AddOpt("-v", to_string(ufar_manager.params.iVerbosity), "num", "specify verbosity level");
    opt_mgr.AddOpt("--seq", to_string(ufar_manager.params.nSeqLookBack), "num", "specify the number of look-back frames (0 = no sequential UIF)");
    opt_mgr.AddOpt("--profile", "no", "", "dump time distribution");
    opt_mgr.AddOpt("--pba_uif", ufar_manager.params.fPbaUif ? "yes" : "no", "", "toggle using proof-based refinement for UIF pairs");
    opt_mgr.AddOpt("--lazysim", ufar_manager.params.fLazySim ? "yes" : "no", "", "toggle applying UIF pairs based on simulation");
    opt_mgr.AddOpt("--pbasim", ufar_manager.params.fPbaSim ? "yes" : "no", "", "toggle combining pba and sim");
    opt_mgr.AddOpt("--pbacex", ufar_manager.params.fPbaCex ? "yes" : "no", "", "toggle combining pba and cex");
    opt_mgr.AddOpt("--satmin", ufar_manager.params.fSatMin ? "yes" : "no", "", "toggle using sat-min in pba");
    opt_mgr.AddOpt("--cbawb", ufar_manager.params.fCbaWb ? "yes" : "no", "", "toggle using cex-based refinement for white boxing");
    opt_mgr.AddOpt("--grey", ufar_manager.params.fGrey ? "yes" : "no", "", "toggle using grey-box constraints");
    opt_mgr.AddOpt("--grey2", to_string(ufar_manager.params.nGrey), "float", "specify the greyness threshold");
    opt_mgr.AddOpt("--allwb", ufar_manager.params.fAllWb ? "yes" : "no", "", "start with all operators white-boxed (no initial abstraction)");
    opt_mgr.AddOpt("--crossonly", ufar_manager.params.fCrossOnly ? "yes" : "no", "", "allow UIF pairs only across LHS/RHS cones of the miter");
    opt_mgr.AddOpt("--crossstats", "no", "", "print multiplier counts in LHS/RHS/shared cones and exit");
    opt_mgr.AddOpt("--dump", "none", "str", "specify file name");
    opt_mgr.AddOpt("--dump-log", "none", "str", "write status log");
    opt_mgr.AddOpt("--dump-first-aig", "none", "str", "dump first internal bit-blasted AIG and exit");
    opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name");
    opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers");
    opt_mgr.AddOpt("--solver", "none", "str", "external solver command line");
    opt_mgr.AddOpt("--dump_states", "none", "str", "specify the name for the states file");
    opt_mgr.AddOpt("--read_states", "none", "str", "specify the name for the states file");
    opt_mgr.AddOpt("--sp", ufar_manager.params.fSuper_prove ? "yes" : "no", "", "toggle using super_prove");
    opt_mgr.AddOpt("--simp", ufar_manager.params.fSimple ? "yes" : "no", "", "toggle using simple (prove)");
    opt_mgr.AddOpt("--syn", ufar_manager.params.fSyn ? "yes" : "no", "", "toggle using simple synthesis");
    opt_mgr.AddOpt("--pth", ufar_manager.params.fPthread ? "yes" : "no", "", "toggle using pthreads");
    opt_mgr.AddOpt("--onewb", to_string(ufar_manager.params.iOneWb), "int", "specify the mode for one-white-boxing");
    opt_mgr.AddOpt("--initallpairs", to_string(ufar_manager.params.nInitAllPairsLimit), "num", "pre-seed all compatible UIF pairs when #ops <= this limit (0=off)");
    opt_mgr.AddOpt("--initnear", to_string(ufar_manager.params.nInitNearMults), "num", "pre-seed UIF pairs among up to this many multipliers closest to output");
    opt_mgr.AddOpt("--timeout", to_string(ufar_manager.params.nTimeout), "num", "specify the timeout (sec)");
    opt_mgr.AddOpt("--exp", to_string(ufar_manager.params.iExp), "int", "specify the exp mode");
    opt_mgr.AddOpt("--miter", "yes", "", "toggle mitering the problem");
    opt_mgr.AddOpt("--under", "-1", "num", "try under-approximation with the given size");
    if(!opt_mgr.Parse(argc, argv)) {
        opt_mgr.PrintUsage();
        cout << "\n       This command was developed by Yen-Sheng Ho at UC Berkeley in 2015.\n";
        cout << "       https://people.eecs.berkeley.edu/~alanmi/publications/2016/fmcad16_uif.pdf \n"; 
        return 0;
    }

    if(opt_mgr["--norm"])
        ufar_manager.params.fNorm ^= 1;
    if(opt_mgr["--cexmin"])
        ufar_manager.params.fCexMin ^= 1;
    if(opt_mgr["--pba_uif"])
        ufar_manager.params.fPbaUif ^= 1;
    if(opt_mgr["--pbasim"])
        ufar_manager.params.fPbaSim ^= 1;
    if(opt_mgr["--pbacex"])
        ufar_manager.params.fPbaCex ^= 1;
    if(opt_mgr["--satmin"])
        ufar_manager.params.fSatMin ^= 1;
    if(opt_mgr["--cbawb"])
        ufar_manager.params.fCbaWb ^= 1;
    if(opt_mgr["--grey"])
        ufar_manager.params.fGrey ^= 1;
    if(opt_mgr["--allwb"])
        ufar_manager.params.fAllWb ^= 1;
    if(opt_mgr["--crossonly"])
        ufar_manager.params.fCrossOnly ^= 1;
    if(opt_mgr["--grey2"])
        ufar_manager.params.nGrey = stof(opt_mgr.GetOptVal("--grey2"));
    if(opt_mgr["--sp"])
        ufar_manager.params.fSuper_prove ^= 1;
    if(opt_mgr["--simp"])
        ufar_manager.params.fSimple ^= 1;
    if(opt_mgr["--syn"])
        ufar_manager.params.fSyn ^= 1;
    if(opt_mgr["--pth"])
        ufar_manager.params.fPthread ^= 1;
    if(opt_mgr["--onewb"])
        ufar_manager.params.iOneWb = stoi(opt_mgr.GetOptVal("--onewb"));
    if(opt_mgr["--initallpairs"])
        ufar_manager.params.nInitAllPairsLimit = stoi(opt_mgr.GetOptVal("--initallpairs"));
    if(opt_mgr["--initnear"])
        ufar_manager.params.nInitNearMults = stoi(opt_mgr.GetOptVal("--initnear"));
    if(opt_mgr["--exp"])
        ufar_manager.params.iExp = stoi(opt_mgr.GetOptVal("--exp"));
    if(opt_mgr["--par"])
        ufar_manager.params.parSetting = opt_mgr.GetOptVal("--par");
    if(opt_mgr["--solver"])
        ufar_manager.params.solverSetting = opt_mgr.GetOptVal("--solver");
    if(opt_mgr["--sim"])
        ufar_manager.params.simSetting = opt_mgr.GetOptVal("--sim");
    if(opt_mgr["--dump_states"]) {
        smatch sub_match;
        string option = opt_mgr.GetOptVal("--dump_states");
        if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
            ufar_manager.params.fileStatesOut = sub_match[1].str();
        else
            ufar_manager.params.fileStatesOut = opt_mgr.GetOptVal("--dump_states");
    }
    if(opt_mgr["--read_states"])
        ufar_manager.params.fileStatesIn = opt_mgr.GetOptVal("--read_states");
    if(opt_mgr["--lazysim"])
        ufar_manager.params.fLazySim ^= 1;
    if(opt_mgr["-v"])
        ufar_manager.params.iVerbosity = stoi(opt_mgr.GetOptVal("-v"));
    if(opt_mgr["--timeout"])
        ufar_manager.params.nTimeout = stoi(opt_mgr.GetOptVal("--timeout"));
    if(opt_mgr["--seq"])
        ufar_manager.params.nSeqLookBack = stoi(opt_mgr.GetOptVal("--seq"));
    if(opt_mgr["--dump-abs"]) {
        smatch sub_match;
        string option = opt_mgr.GetOptVal("--dump-abs");
        if(regex_search(option, sub_match, regex(R"(/?(\w+)\.v$)")))
            ufar_manager.params.fileAbs = sub_match[1].str();
        else
            ufar_manager.params.fileAbs = opt_mgr.GetOptVal("--dump-abs");
    }
    if(opt_mgr["--dump"]) {
        smatch sub_match;
        string option = opt_mgr.GetOptVal("--dump");
        if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
            ufar_manager.params.fileName = sub_match[1].str();
        else
            ufar_manager.params.fileName = opt_mgr.GetOptVal("--dump");
    }
    string firstAigDumpFile = "";
    if ( opt_mgr["--dump-first-aig"] )
        firstAigDumpFile = opt_mgr.GetOptVal("--dump-first-aig");

    // ufar_manager.DumpParams();
    LogT::prefix = "UIF_PROVE";
    string dumpLogFile = opt_mgr["--dump-log"] ? opt_mgr.GetOptVal("--dump-log") : "";
    string statusName = Ufar_GetStatusName( Wlc_AbcGetNtk(pAbc) );

    set<unsigned> set_op_types;
    set_op_types.insert(WLC_OBJ_ARI_MULTI);
    if (opt_mgr["--adder"])
        set_op_types.insert(WLC_OBJ_ARI_ADD);
    if (!UFAR::HasOperator(Wlc_AbcGetNtk(pAbc), set_op_types)) {
        cout << "There is no operator for UIF.\n";
        return 0;
    }

    Wlc_Ntk_t * pNew = NULL;
    timeval t1, t2;
    gettimeofday(&t1, NULL);

    if (!opt_mgr["--miter"]) {
        if (Wlc_NtkPoNum(Wlc_AbcGetNtk(pAbc)) != 2) {
            cout << "The current design doesn't have dual outputs.\n";
            return 0;
        }
        pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0);
        Wlc_AbcUpdateNtk(pAbc, pNew);
    }

    if (ufar_manager.params.fNorm) {
        pNew = UFAR::NormalizeDataTypes(Wlc_AbcGetNtk(pAbc), set_op_types, true);
        Wlc_AbcUpdateNtk(pAbc, pNew);
    }

    if ( opt_mgr["--crossstats"] )
    {
        Wlc_Ntk_t * pCur = Wlc_AbcGetNtk(pAbc);
        if ( Wlc_NtkPoNum(pCur) != 2 )
        {
            cout << "CrossStats requires dual outputs before mitering.\n";
            return 0;
        }
        int nObjs = Wlc_NtkObjNumMax(pCur);
        vector<char> vConeL(nObjs, 0), vConeR(nObjs, 0);
        auto mark_cone = [&]( int iStart, vector<char>& vMark )
        {
            if ( iStart < 0 || iStart >= nObjs )
                return;
            vector<int> stack(1, iStart);
            while ( !stack.empty() )
            {
                int iObj = stack.back();
                stack.pop_back();
                if ( iObj < 0 || iObj >= nObjs || vMark[iObj] )
                    continue;
                vMark[iObj] = 1;
                Wlc_Obj_t * pObjT = Wlc_NtkObj(pCur, iObj);
                // Sequential traversal: from flop output (FO) continue to corresponding flop input (FI).
                if ( pObjT->Type == WLC_OBJ_FO )
                {
                    Wlc_Obj_t * pFi = Wlc_ObjFo2Fi(pCur, pObjT);
                    stack.push_back( Wlc_ObjId(pCur, pFi) );
                }
                int iFanin, k;
                Wlc_ObjForEachFanin( pObjT, iFanin, k )
                    stack.push_back(iFanin);
            }
        };
        int iRootL = Wlc_ObjFaninId0( Wlc_NtkPo(pCur, 0) );
        int iRootR = Wlc_ObjFaninId0( Wlc_NtkPo(pCur, 1) );
        mark_cone(iRootL, vConeL);
        mark_cone(iRootR, vConeR);

        int nL = 0, nR = 0, nB = 0, nN = 0;
        Wlc_Obj_t * pObjT; int iObj;
        Wlc_NtkForEachObj( pCur, pObjT, iObj )
        {
            if ( pObjT->Type != WLC_OBJ_ARI_MULTI )
                continue;
            bool fL = vConeL[iObj] != 0;
            bool fR = vConeR[iObj] != 0;
            if ( fL && fR ) nB++;
            else if ( fL )  nL++;
            else if ( fR )  nR++;
            else            nN++;
        }
        cout << "UIF_PROVE : CrossStats: L=" << nL
             << " R=" << nR
             << " BOTH=" << nB
             << " NONE=" << nN
             << " TOTAL=" << (nL + nR + nB + nN) << endl;
        //fflush(stdout);
        //exit(1);
        return 0;
    }

    if (opt_mgr["--under"]) {
        pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), stoi(opt_mgr.GetOptVal("--under")));
        Wlc_AbcUpdateNtk(pAbc, pNew);
        pNew = UFAR::MakeUnderApprox2(Wlc_AbcGetNtk(pAbc), set_op_types, stoi(opt_mgr.GetOptVal("--under")));
        Wlc_AbcUpdateNtk(pAbc, pNew);
        Wlc_WriteVer(Wlc_AbcGetNtk(pAbc), "UND.v", 0, 0);
    }

    Gia_Man_t * pGia = UFAR::BitBlast(Wlc_AbcGetNtk(pAbc));
    Gia_ManPrintStats( pGia, NULL );
    if ( !firstAigDumpFile.empty() && firstAigDumpFile != "none" )
    {
        Gia_AigerWriteSimple( pGia, (char *)firstAigDumpFile.c_str() );
        Gia_ManStop( pGia );
        return 0;
    }
    Gia_ManStop( pGia );

    ufar_manager.Initialize(Wlc_AbcGetNtk(pAbc), set_op_types);

    int ret = ufar_manager.PerformUIFProve(t1);
    if (ret == 1) {
        LOG(0) << "Proved by UIF (UNSAT).";
    } else if (ret == 0) {
        LOG(0) << "Falsified by UIF (SAT).";
    } else {
        LOG(0) << "Undecided by UIF.";
    }
    Ufar_DumpStatusLog( dumpLogFile, ret, statusName );

    gettimeofday(&t2, NULL);
    unsigned tTotal = elapsed_time_usec(t1, t2);
    if(opt_mgr["--profile"]) {
        unsigned nCexChecks = 0, nBitBlasts = 0;
        unsigned long long tBitBlastUsec = 0, tCexCheckUsec = 0;
        UFAR::Ufar_GetOrigCexStats(&nCexChecks, &nBitBlasts, &tBitBlastUsec, &tCexCheckUsec);
        LOG(0) << "OrigCexStats: checks = " << nCexChecks
               << ", bitblasts = " << nBitBlasts
               << ", blast_time = " << fixed << setprecision(4) << ((double)tBitBlastUsec / 1000000.0)
               << " sec [" << (tTotal ? (100.0 * (double)tBitBlastUsec / (double)tTotal) : 0.0) << "%]"
               << ", cex_check_time = " << ((double)tCexCheckUsec / 1000000.0)
               << " sec [" << (tTotal ? (100.0 * (double)tCexCheckUsec / (double)tTotal) : 0.0) << "%]";
        auto log_profile = [&](const string& str, abctime t) {
          LOG(0) << str << " time = " << fixed << setprecision(4) << setw(8) << (double)t/1000000 << " sec [" << setw(7) << (double)t/tTotal*100 << "%]";
        };
        auto pct = [&](unsigned n, unsigned d) {
            return d ? 100.0 * (double)n / (double)d : 0.0;
        };
        log_profile("BLSolver  ", ufar_manager.profile.tBLSolver);
        log_profile("UifRefine ", ufar_manager.profile.tUifRefine);
        log_profile("WbRefine  ", ufar_manager.profile.tWbRefine);
        log_profile("UifSim    ", ufar_manager.profile.tUifSim);
        log_profile("GbRefine  ", ufar_manager.profile.tGbRefine);
        log_profile("CexCheck  ", ufar_manager.profile.tCexCheckOrig);
        {
            unsigned long long tKnown = (unsigned long long)ufar_manager.profile.tBLSolver
                                      + (unsigned long long)ufar_manager.profile.tUifRefine
                                      + (unsigned long long)ufar_manager.profile.tWbRefine
                                      + (unsigned long long)ufar_manager.profile.tUifSim
                                      + (unsigned long long)ufar_manager.profile.tGbRefine
                                      + (unsigned long long)ufar_manager.profile.tCexCheckOrig;
            unsigned long long tUnaccounted = (tTotal > tKnown) ? (tTotal - tKnown) : 0;
            LOG(0) << "Unaccounted time = " << fixed << setprecision(4) << setw(8)
                   << ((double)tUnaccounted / 1000000.0) << " sec [" << setw(7)
                   << (tTotal ? (double)tUnaccounted * 100.0 / (double)tTotal : 0.0) << "%]";
        }
        LOG(0) << "UFAR calls: verify = " << ufar_manager.profile.nVerifyCalls
               << " (sat = " << ufar_manager.profile.nSatCalls
               << ", unsat = " << ufar_manager.profile.nUnsatCalls
               << ", undec = " << ufar_manager.profile.nUnknownCalls << ")";
        LOG(0) << "UFAR cex  : real = " << ufar_manager.profile.nRealCex
               << ", spurious = " << ufar_manager.profile.nSpuriousCex
               << " [" << fixed << setprecision(1)
               << pct(ufar_manager.profile.nSpuriousCex, ufar_manager.profile.nSatCalls)
               << "% spurious among SAT-abstraction]";
        LOG(0) << "UFAR ref  : iters_uif = " << ufar_manager.profile.nIterUif
               << ", iters_wb = " << ufar_manager.profile.nIterWb
               << ", pairs_added = " << ufar_manager.profile.nUifPairsAdded
               << ", mul_mul_pairs_added = " << ufar_manager.profile.nUifMulMulPairsAdded
               << ", wb_added = " << ufar_manager.profile.nWbAdded;
        LOG(0) << "UFAR size : max_pairs = " << ufar_manager.profile.nMaxUifPairs
               << ", max_white_boxes = " << ufar_manager.profile.nMaxWhiteBoxes;
        if ( ufar_manager.profile.nVerifyCalls ) {
            LOG(0) << "UFAR avg  : blsolve_call = "
                   << fixed << setprecision(4)
                   << (double)ufar_manager.profile.tBLSolver / 1000000.0 / (double)ufar_manager.profile.nVerifyCalls
                   << " sec/call";
        }
    }

    LOG(0) << "Time = " << setprecision(5) << ((double) (tTotal) / 1000000) << " sec";

    return 0;
}

static int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
    LogT::prefix = "TEST::";
    OptMgr opt_mgr(argv[0]);
    opt_mgr.AddOpt("--ntk", "none", "str", "specify the file name (*.aig) for the input network");
    opt_mgr.AddOpt("--adder", "no", "", "toggle including adders");
    if(!opt_mgr.Parse(argc, argv)) {
        opt_mgr.PrintUsage();
        return 0;
    }
    set<unsigned> set_op_types;
    set_op_types.insert(WLC_OBJ_ARI_MULTI);
    if(opt_mgr["--adder"]) {
        set_op_types.insert(WLC_OBJ_ARI_ADD);
    }
    Wlc_Ntk_t * pNew = UFAR::AddConstFlops(Wlc_AbcGetNtk(pAbc), set_op_types);
    Wlc_AbcUpdateNtk(pAbc, pNew);
    return 0;

#if 0
    opt_mgr.AddOpt("--ntk", "none", "str", "specify the file name (*.aig) for the input network");
    opt_mgr.AddOpt("--inv", "none", "str", "specify the file name (*.pla) for the invariant");
    if(!opt_mgr.Parse(argc, argv)) {
        opt_mgr.PrintUsage();
        return 0;
    }

    string nameNtk = opt_mgr.GetOptVal("--ntk");
    string nameInv = opt_mgr.GetOptVal("--inv");
    UFAR::TestInvariant(nameNtk, nameInv);
#endif
#if 0
    set<unsigned> set_op_types;
    set_op_types.insert(WLC_OBJ_ARI_MULTI);

    OptMgr opt_mgr(argv[0]);
    opt_mgr.AddOpt("--cube", "no", "", "toggle using cubes for interpolants");
    if(!opt_mgr.Parse(argc, argv)) {
        opt_mgr.PrintUsage();
        return 0;
    }

    UFAR::TestITP(Wlc_AbcGetNtk(pAbc), set_op_types, opt_mgr["--cube"]);
#endif
#if 0
     if (  Wlc_AbcGetNtk(pAbc) == NULL ) {
         cout << "There is no current design.\n";
         return 0;
     }

     if (Wlc_NtkPoNum(Wlc_AbcGetNtk(pAbc)) != 2) {
         cout << "The current design doesn't have dual outputs.\n";
         return 0;
     }

     set<unsigned> set_op_types;
     set_op_types.insert(WLC_OBJ_ARI_MULTI);
     if (!UFAR::HasOperator(Wlc_AbcGetNtk(pAbc), set_op_types)) {
         cout << "There is no operator for UIF.\n";
         return 0;
     }

     Wlc_Ntk_t * pNew = NULL;

     pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0);
     Wlc_AbcUpdateNtk(pAbc, pNew);

     pNew = UFAR::NormalizeDataTypes(Wlc_AbcGetNtk(pAbc), set_op_types, true);
     Wlc_AbcUpdateNtk(pAbc, pNew);

     ufar_manager.Initialize(Wlc_AbcGetNtk(pAbc), set_op_types);
     ufar_manager.DumpMgrInfo();

     pNew = ufar_manager.BuildCurrentAbstraction();
     Wlc_AbcUpdateNtk(pAbc, pNew);


    return 0;
#endif
}

ABC_NAMESPACE_IMPL_END
