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

#include <cstdio>
#include <fstream>
#include <iostream>
#include <iomanip>
#include <map>
#include <algorithm>
#include <array>
#include <regex>
#include <queue>

#ifdef _WIN32
#include <windows.h>
#endif

#include <base/wlc/wlc.h>
#include <sat/cnf/cnf.h>
#include <aig/gia/giaAig.h>
#include "opt/untk/NtkNtk.h"
#include "opt/util/util.h"
#include "UfarMgr.h"

ABC_NAMESPACE_IMPL_START

using namespace std;

namespace UFAR {

static inline unsigned log_level() {
    return LogT::loglevel;
}

static unsigned           s_nOrigCexChecks    = 0;
static unsigned           s_nOrigBitBlasts    = 0;
static unsigned long long s_tOrigBitBlastUsec = 0;
static unsigned long long s_tOrigCexCheckUsec = 0;

void Ufar_ResetOrigCexStats()
{
    s_nOrigCexChecks    = 0;
    s_nOrigBitBlasts    = 0;
    s_tOrigBitBlastUsec = 0;
    s_tOrigCexCheckUsec = 0;
}

void Ufar_GetOrigCexStats( unsigned * pChecks, unsigned * pBitBlasts, unsigned long long * pBitBlastUsec, unsigned long long * pCexCheckUsec )
{
    if ( pChecks )       *pChecks       = s_nOrigCexChecks;
    if ( pBitBlasts )    *pBitBlasts    = s_nOrigBitBlasts;
    if ( pBitBlastUsec ) *pBitBlastUsec = s_tOrigBitBlastUsec;
    if ( pCexCheckUsec ) *pCexCheckUsec = s_tOrigCexCheckUsec;
}

static void split(const string &s, char delim, vector<string>& elems) {
    stringstream ss(s);
    string item;
    elems.clear();
    while (getline(ss, item, delim)) {
        elems.push_back(std::move(item));
    }
}

static void set_state_b(vector<bool>& vec_b_state, const string& str_state) {
    if (vec_b_state.size() != str_state.size()) {
        cerr << "Invalid initial states for B.\n" ;
        return;
    }

    for(size_t i = 0; i < str_state.size(); ++i) {
        char state = str_state[i];
        if (state == '0') {
            vec_b_state[i] = false;
        } else if (state == '1') {
            vec_b_state[i] = true;
        } else if (state != '1') {
            assert(false);
        }
    }
}

static void set_state_p(set<UIF_PAIR>& set_p_state, const string& str_pair) {
    vector<string> tokens;
    split(str_pair, ',', tokens);
    assert(tokens.size() == 5);
    set_p_state.insert(UIF_PAIR(OperatorID(stoi(tokens[0]), stoi(tokens[1])), OperatorID(stoi(tokens[2]), stoi(tokens[3])), tokens[4]=="1"));
}

static void readCexFromVec(Gia_Man_t * pGia, const vector<int>& vec_cex, Abc_Cex_t ** ppCex) {
    int nBits = vec_cex.size();
    int nRegs = Gia_ManRegNum(pGia);
    int nPis  = Gia_ManPiNum(pGia);

    int iFrame = (nBits - nRegs) / nPis - 1;
    assert(nBits == (nRegs + (iFrame + 1)*nPis));

    *ppCex = Abc_CexAlloc(nRegs, nPis, iFrame + 1);
    (*ppCex)->iFrame = iFrame;
    (*ppCex)->iPo = 0;
    for(size_t i = 0; i < vec_cex.size(); ++i) {
        if (vec_cex[i] == 1 || vec_cex[i] == 0) {
            if (vec_cex[i] == 1)
                Abc_InfoSetBit((*ppCex)->pData, i);
        }
    }
}

static Vec_Int_t * collect_boxes(const vector<int>& vec_ids, const vector<bool>& vec_marks, bool fCollectBlack) {
    Vec_Int_t * vec_ops = Vec_IntAlloc(10);
    for(unsigned i = 0; i < vec_ids.size(); i++) {
        int op_id = vec_ids[i];
        bool is_black = vec_marks[i];
        if((is_black && fCollectBlack) || (!is_black && !fCollectBlack))
            Vec_IntPush(vec_ops, op_id);
    }
    return vec_ops;
}

static bool verify_cex_direct(Wlc_Ntk_t * pNtk, Abc_Cex_t * pCex) {
    Gia_Man_t * pGia = BitBlast(pNtk);
    int i;

    Gia_ManConst0(pGia)->Value = 0;
    Gia_Obj_t * pObj, * pObjRi;
    Gia_ManForEachRi( pGia, pObj, i )
        pObj->Value = 0;
    for ( int f = 0; f <= pCex->iFrame; f++ ) {
        for( i = 0; i < Gia_ManPiNum(pGia); i++ ) {
            Gia_ManPi(pGia, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i);
        }
        Gia_ManForEachRiRo( pGia, pObjRi, pObj, i )
            pObj->Value = pObjRi->Value;
        Gia_ManForEachAnd( pGia, pObj, i )
            pObj->Value = Gia_ObjFanin0Copy(pObj) & Gia_ObjFanin1Copy(pObj);
        Gia_ManForEachCo( pGia, pObj, i )
            pObj->Value = Gia_ObjFanin0Copy(pObj);
        Gia_ManForEachPo( pGia, pObj, i ) {
            if (pObj->Value==1) {
                LOG(3) << "CEX is valid.";
                Gia_ManStop(pGia);
                return true;
            }
        }
    }

    LOG(3) << "CEX is invalid.";
    Gia_ManStop(pGia);
    return false;
}

static bool verify_cex_on_original(Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex) {
    timeval t1, t2, tCheck1, tCheck2;
    gettimeofday(&tCheck1, NULL);
    gettimeofday(&t1, NULL);
    Gia_Man_t * pGiaOrig = BitBlast(pOrig);
    gettimeofday(&t2, NULL);
    s_nOrigCexChecks++;
    s_nOrigBitBlasts++;
    s_tOrigBitBlastUsec += elapsed_time_usec(t1, t2);

    unsigned nbits_orig_pis = compute_bit_level_pi_num(pOrig);
    int nbits_ppis = pCex->nPis - Gia_ManPiNum(pGiaOrig);
    LOG(3) << "VerifyCEX: #ppis = " << nbits_ppis;

    int i;

    Gia_ManConst0(pGiaOrig)->Value = 0;
    Gia_Obj_t * pObj, * pObjRi;
    Gia_ManForEachRi( pGiaOrig, pObj, i )
        pObj->Value = 0;
    for ( int f = 0; f <= pCex->iFrame; f++ ) {
        for( i = 0; i < Gia_ManPiNum(pGiaOrig); i++ ) {
            if ( i < nbits_orig_pis ) {
                Gia_ManPi(pGiaOrig, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i);
            } else { // undc PIs
                Gia_ManPi(pGiaOrig, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i + nbits_ppis);
            }
        }
        Gia_ManForEachRiRo( pGiaOrig, pObjRi, pObj, i )
            pObj->Value = pObjRi->Value;
        Gia_ManForEachAnd( pGiaOrig, pObj, i )
            pObj->Value = Gia_ObjFanin0Copy(pObj) & Gia_ObjFanin1Copy(pObj);
        Gia_ManForEachCo( pGiaOrig, pObj, i )
            pObj->Value = Gia_ObjFanin0Copy(pObj);
        Gia_ManForEachPo( pGiaOrig, pObj, i ) {
            if (pObj->Value==1) {
                LOG(3) << "CEX is real.";
                Gia_ManStop(pGiaOrig);
                gettimeofday(&tCheck2, NULL);
                s_tOrigCexCheckUsec += elapsed_time_usec(tCheck1, tCheck2);
                return true;
            }
        }
    }

    Gia_ManStop(pGiaOrig);
    LOG(3) << "CEX is spurious.";
    gettimeofday(&tCheck2, NULL);
    s_tOrigCexCheckUsec += elapsed_time_usec(tCheck1, tCheck2);
    return false;
}

static bool bitstr_not_equal(const string& str1, const string& str2) {
    if (str1.size()!=str2.size()) return true;

    for(unsigned i = 0; i < str1.size(); i++) {
        if (str1[i]=='1' && str2[i]=='0')
            return true;
        if (str1[i]=='0' && str2[i]=='1')
            return true;

        if (str1[i]=='u' && str2[i]=='s')
            return true;
        if (str1[i]=='s' && str2[i]=='u')
            return true;
    }

    return false;
}

static bool bitstr_all_x(const string& str) {
    for(auto& x : str) {
        if(x!='x') return false;
    }
    return true;
}

static void print_blackboxes(const vector<bool>& vec_bb) {
    ostringstream oss;
    for(const auto& x : vec_bb) {
        oss << (x ? "1" : "0");
    }
    LOG(3) << oss.str();
}

static void print_pairs(const set<UifPair>& set_pairs) {
    for(auto& x : set_pairs) {
        LOG(3) << "(" << x.first << ", " << x.second << ")" << (x.fMark ? " [r]" : "");
    }
}

/*
static int super_prove(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, bool fSimp, const string* pFileName = NULL) {
    if(*ppCex) {
        Abc_CexFree(*ppCex);
        *ppCex = NULL;
    }

    Gia_Man_t * pGia = BitBlast(pNtk);

    if (pFileName && !pFileName->empty())
        Gia_AigerWriteSimple(pGia, &((*pFileName + ".aig")[0u]));

    string tmpName = tmpnam(nullptr);
    string tmpFileName = tmpName + ".aig";
    Gia_AigerWrite( pGia, &tmpFileName[0u], 0, 0 );

    //string cmd = "super_prove -r /dev/stderr " + tmpFileName;
    string cmd;
    if (fSimp)
        cmd = "simple " + tmpFileName;
    else
        cmd = "super_prove " + tmpFileName;

    vector<int> vec_cex;
    int result = call_python("run_sp", "verify", cmd.c_str(), vec_cex);
    if(result == 1)
        readCexFromVec(pGia, vec_cex, ppCex);
    remove(tmpFileName.c_str());
    Gia_ManStop(pGia);

    if (result == 0) {
        return 1;
    } else if (result == 1) {
        return 0;
    } else {
        return -1;
    }
}
*/

static void get_operator_pair(Wlc_Ntk_t * p, const UIF_PAIR& uif_pair, array<int, 3>& wires1, array<int, 3>& wires2, const vector<int>& vec_ids, const VecVecInt& vv_op_ffs) {
    const UIF_PAIR& x = uif_pair;
    assert(x.second.timediff == 0);
    wires2[2] = vec_ids[x.second.idx];
    wires2[0] = x.fMark ? Wlc_ObjFaninId1(Wlc_NtkObj(p, vec_ids[x.second.idx])) : Wlc_ObjFaninId0(Wlc_NtkObj(p, vec_ids[x.second.idx]));
    wires2[1] = x.fMark ? Wlc_ObjFaninId0(Wlc_NtkObj(p, vec_ids[x.second.idx])) : Wlc_ObjFaninId1(Wlc_NtkObj(p, vec_ids[x.second.idx]));

    if (x.first.timediff == 0) {
        wires1[2] = vec_ids[x.first.idx];
        wires1[0] = Wlc_ObjFaninId0(Wlc_NtkObj(p, vec_ids[x.first.idx]));
        wires1[1] = Wlc_ObjFaninId1(Wlc_NtkObj(p, vec_ids[x.first.idx]));
    } else {
        int ci_idx = vv_op_ffs[x.first.idx][0 - x.first.timediff - 1];
        wires1[2] = Wlc_ObjId(p, Wlc_NtkCi(p, ci_idx));
        wires1[1] = Wlc_ObjId(p, Wlc_NtkCi(p, ci_idx - 1));
        wires1[0] = Wlc_ObjId(p, Wlc_NtkCi(p, ci_idx - 2));
    }
}

static Gia_Man_t * unroll_with_cex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, int nbits_old_pis, int num_sel_pis, int * p_num_ppis, bool sel_pi_first) {
    Gia_Man_t * pGiaChoice = BitBlast( pChoice );

    int nbits_new_pis = compute_bit_level_pi_num(pChoice);
    int num_ppis = nbits_new_pis - nbits_old_pis - num_sel_pis;
    *p_num_ppis = num_ppis;
    int num_undc_pis = Gia_ManPiNum(pGiaChoice) - nbits_new_pis;
    LOG(3) << "#orig_pis = " << nbits_old_pis << ", #ppis = " << num_ppis << ", #sel_pis = " << num_sel_pis << ", #undc_pis = " << num_undc_pis;
    assert(Gia_ManPiNum(pGiaChoice)==nbits_old_pis+num_ppis+num_sel_pis+num_undc_pis);
    assert(Gia_ManPiNum(pGiaChoice)==pCex->nPis+num_sel_pis);

    Gia_Man_t * pFrames = NULL;

    Gia_Obj_t * pObj, * pObjRi;
    int f, i;
    pFrames = Gia_ManStart( 10000 );
    pFrames->pName = Abc_UtilStrsav( pGiaChoice->pName );
    Gia_ManHashAlloc( pFrames );
    Gia_ManConst0(pGiaChoice)->Value = 0;
    Gia_ManForEachRi( pGiaChoice, pObj, i )
        pObj->Value = 0;

    auto is_sel_pi = [=](int iPi) {
        return (sel_pi_first ? iPi < nbits_old_pis + num_sel_pis : iPi >= nbits_old_pis + num_ppis);
    };

    for ( f = 0; f <= pCex->iFrame; f++ ) {
        for( i = 0; i < Gia_ManPiNum(pGiaChoice); i++ ) {
            if ( i >= nbits_old_pis && i < nbits_old_pis + num_ppis + num_sel_pis ) {
                if(f == 0 || !is_sel_pi(i))
                    Gia_ManPi(pGiaChoice, i)->Value = Gia_ManAppendCi(pFrames);
            } else if (i < nbits_old_pis) {
                Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i);
            } else if (i >= nbits_old_pis + num_ppis + num_sel_pis) {
                Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i - num_sel_pis);
            }
        }
        Gia_ManForEachRiRo( pGiaChoice, pObjRi, pObj, i )
            pObj->Value = pObjRi->Value;
        Gia_ManForEachAnd( pGiaChoice, pObj, i )
            pObj->Value = Gia_ManHashAnd(pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj));
        Gia_ManForEachCo( pGiaChoice, pObj, i )
            pObj->Value = Gia_ObjFanin0Copy(pObj);
        Gia_ManForEachPo( pGiaChoice, pObj, i )
            Gia_ManAppendCo(pFrames, pObj->Value);
    }
    Gia_ManHashStop (pFrames);
    Gia_ManSetRegNum(pFrames, 0);
    Gia_Man_t * pGia;
    pFrames = Gia_ManCleanup(pGia = pFrames);
    Gia_ManStop(pGia);
    Gia_ManStop(pGiaChoice);

    return pFrames;
}

static void compute_core_using_sat(Gia_Man_t * pFrames, vector<unsigned>& vec_cores, int nFrames, int num_sel_pis, int num_other_pis, bool sel_pi_first, VecVecInt* ppi_model = NULL, bool fSatMin = false, int nConfLimit = 0) {
    Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames );
    Cnf_Dat_t * pCnf = Cnf_Derive(pAigFrames, Aig_ManCoNum(pAigFrames));
    sat_solver * pSat = sat_solver_new();
    sat_solver_setnvars(pSat, pCnf->nVars);
    for (unsigned i = 0; i < pCnf->nClauses; i++) {
        if (!sat_solver_addclause(pSat, pCnf->pClauses[i], pCnf->pClauses[i + 1]))
            assert(false);
    }
    {
        Vec_Int_t* vLits = Vec_IntAlloc(100);
        Aig_Obj_t* pObj;
        int i;
        Aig_ManForEachCo( pAigFrames, pObj, i )
        {
            assert(pCnf->pVarNums[pObj->Id] >= 0);
            Vec_IntPush(vLits, toLitCond(pCnf->pVarNums[pObj->Id], 0));
        }
        int ret = sat_solver_addclause(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits));
        if (!ret) {
            LOG(0) << "UNSAT after adding PO clause.";
        }

        Vec_IntFree(vLits);
    }
    {
        Vec_Int_t* vLits = Vec_IntAlloc(100);
        map<int, int> varMap;
        int first_sel_pi = sel_pi_first ? 0 : num_other_pis;
        for (int i = 0; i < num_sel_pis; i++) {
        //for (int i = num_sel_pis - 1; i >= 0; --i) {
            int cur_pi = first_sel_pi + i;
            int var = pCnf->pVarNums[Aig_ManCi(pAigFrames, cur_pi)->Id];
            assert(var >= 0);
            varMap[var] = i;
            Vec_IntPush(vLits, toLitCond(var, 0));
        }
        if(log_level() >= 3) {
            int i, Entry;
            ostringstream oss;
            oss << "#vLits = " << Vec_IntSize(vLits) << "; vLits = ";
            Vec_IntForEachEntry(vLits, Entry, i)
                oss << Entry << " ";
            LOG(3) << oss.str();
        }
        int status = sat_solver_solve(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)(nConfLimit), (ABC_INT64_T)(0), (ABC_INT64_T)(0), (ABC_INT64_T)(0));
        if (status == l_False) {
            LOG(3) << "UNSAT.";
            int nCoreLits, *pCoreLits;
            nCoreLits = sat_solver_final(pSat, &pCoreLits);

            vector<bool> vec_cores_marks (Vec_IntSize(vLits),false);
            for (int i = 0; i < nCoreLits; i++) {
                vec_cores_marks[varMap[lit_var(pCoreLits[i])]] = true;
            }

            // SAT-min
            if (fSatMin && nCoreLits > 1) {
                for (int i = 0; i < vec_cores_marks.size(); i++) {
                    if (!vec_cores_marks[i])
                        Vec_IntWriteEntry(vLits, i, lit_neg(Vec_IntEntry(vLits, i)));
                }

                for (int i = 0; i < vec_cores_marks.size(); i++) {
                    if (!vec_cores_marks[i])
                        continue;

                    Vec_IntWriteEntry(vLits, i, lit_neg(Vec_IntEntry(vLits, i)));
                    int status = sat_solver_solve(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T) (5000), (ABC_INT64_T) (0), (ABC_INT64_T) (0), (ABC_INT64_T) (0));

                    if (status == l_False) {
                        LOG(4) << "Loop[" << i << "] : Drop 1 literal = " << Vec_IntEntry(vLits, i);
                        vec_cores_marks[i] = false;
                    } else {
                        if (status == l_True)
                            LOG(4) << "Loop[" << i << "] : SAT";
                        else
                            LOG(4) << "Loop[" << i << "] : Unknown";
                        Vec_IntWriteEntry(vLits, i, lit_neg(Vec_IntEntry(vLits, i)));
                    }
                }
                LOG(2) << "SAT-MIN : " << nCoreLits << " ==> " << count(vec_cores_marks.begin(), vec_cores_marks.end(), true);
            }

            for (int i = 0; i < vec_cores_marks.size(); i++) {
                if(vec_cores_marks[i])
                    vec_cores.push_back(i);
            }
        } else if (status == l_True) {
            LOG(3) << "SAT.";

            if (ppi_model && sel_pi_first) {
                ppi_model->clear();
                for (int f = 0; f < nFrames; f++) {
                    ppi_model->push_back(vector<int>());
                    for (int i = 0; i < num_other_pis; i++) {
                        int cur_pi = num_sel_pis + f * num_other_pis + i;
                        int var = pCnf->pVarNums[Aig_ManCi(pAigFrames, cur_pi)->Id];
                        ppi_model->back().push_back(sat_solver_var_value(pSat, var));
                    }
                }
            }
        } else {
            LOG(3) << "UNKNOWN.";
        }

        Vec_IntFree(vLits);
    }
    Cnf_ManFree();
    sat_solver_delete(pSat);
    Aig_ManStop(pAigFrames);
}

std::ostream& operator<<(ostream& os, const OperatorID& obj) {
    os << obj.idx << " @ " << obj.timediff;
    return os;
}

class SimUifPairFinder {
    public:
        SimUifPairFinder(Wlc_Ntk_t * pOrig, const vector<int>* p_vec_ids) :
            nWords(1),
            nFrames(1),
            nThreshold(0),
            _pOrigNtk(pOrig),
            _p_vec_op_ids(p_vec_ids)
        {}

        void Simulate() {
            _compute_max_bw();
            _simulate_and_count();
        }
        void ComputeUifPairs() {
            _insert_sim_pairs();
        }
        void SetParams(const string& setting);

        bool HasResults() const {return !_mat_pairwise_matches.empty();}
        int  GetCount(const UIF_PAIR& x) const;
        bool IsGood(const UIF_PAIR& x) const {return (GetCount(x) >= nThreshold);}
        void AddPair(const UIF_PAIR& x);

        const set<UIF_PAIR>* GetSimPairsPtr() { return &_set_sim_pairs; }

        int nWords;
        int nFrames;
        int nThreshold;
    private:
        void _compute_max_bw() { ComputeMaxBW(_pOrigNtk, *_p_vec_op_ids, _max_input_bw, _max_output_bw); }
        void _simulate_and_count();
        void _insert_sim_pairs();
        void _count_matches(Vec_Ptr_t * vRes, int range);
        Vec_Int_t * _collect_sim_nodes(Wlc_Ntk_t * pNtk);

        Wlc_Ntk_t *          _pOrigNtk;
        const vector<int>*   _p_vec_op_ids;

        set<UIF_PAIR>     _set_sim_pairs;

        int               _max_input_bw {-1};
        int               _max_output_bw {-1};

        VecVecInt         _mat_pairwise_matches;
};

void SimUifPairFinder::AddPair(const UIF_PAIR& x) {
    assert(x.first.timediff == 0 && x.second.timediff == 0);
    assert(x.first.idx < x.second.idx);

    if(x.fMark)
        _mat_pairwise_matches[x.second.idx][x.first.idx] += nThreshold;
    else 
        _mat_pairwise_matches[x.first.idx][x.second.idx] += nThreshold;
}
int  SimUifPairFinder::GetCount(const UIF_PAIR& x) const {
    assert(x.first.timediff == 0 && x.second.timediff == 0);
    assert(x.first.idx < x.second.idx);

    return (x.fMark ? _mat_pairwise_matches[x.second.idx][x.first.idx] : _mat_pairwise_matches[x.first.idx][x.second.idx]);
}

void SimUifPairFinder::SetParams(const string& setting) {
    int temp = 0;
    smatch sub_match;

    if(regex_search(setting, sub_match, regex(R"(w:(\d+))")))
        nWords = stoi(sub_match[1].str());

    if(regex_search(setting, sub_match, regex(R"(f:(\d+))")))
        nFrames = stoi(sub_match[1].str());

    if(regex_search(setting, sub_match, regex(R"(t:(\d+))")))
        temp = stoi(sub_match[1].str());

    nThreshold = temp * nWords * nFrames * 64 / 100;
}

Vec_Int_t * SimUifPairFinder::_collect_sim_nodes(Wlc_Ntk_t * pNtk) {
    Vec_Int_t * vNodes = Vec_IntAlloc( _p_vec_op_ids->size() * 2 );
    int i;
    Wlc_Obj_t * pPo;
    int range = Wlc_ObjRange(Wlc_NtkPo(pNtk, 1));
    (void)range;
    Wlc_NtkForEachPo(pNtk, pPo, i) {
       if ((i%3)==0) continue;
       assert(range == Wlc_ObjRange(pPo));
       Vec_IntPush(vNodes, Wlc_ObjId(pNtk, pPo));
    }
    assert(Vec_IntSize(vNodes) == _p_vec_op_ids->size() * 2);

    return vNodes;
}

static unsigned bit_count (word value) {
    unsigned count = 0;
    while (value > 0) {           // until all bits are zero
        if ((value & 1) == 1)     // check lower bit
            count++;
        value >>= 1;              // shift bits, removing lower bit
    }
    return count;
}

static void bit_print (word value) {
    int n_bits = 0;
    while(n_bits < 64) {
        if ((value & 1) == 1)
            cout << "1";
        else
            cout << "0";
        value >>= 1;
        n_bits++;
    }
    cout << endl;
}

void SimUifPairFinder::_count_matches(Vec_Ptr_t * vRes, int range) {
    VecVecInt& mat = _mat_pairwise_matches;
    int num_ops = _p_vec_op_ids->size();
    mat = VecVecInt(num_ops, vector<int>(num_ops, 0));
    array<int, 2> op1, op2;

    for(int i = 0; i < num_ops; i++) {
        for(int j = 0; j < num_ops; j++) {
            if (i == j) continue;

            for(int f = 0; f < nFrames; f++) {
                vector<word> merges(nWords, ~0);

                op1[0] = (i < j) ? (i << 1) : (i << 1) + 1;
                op1[1] = (i < j) ? (i << 1) + 1 : (i << 1);
                op2[0] = (j << 1);
                op2[1] = (j << 1) + 1;

                for (int k = 0; k < range; k++) {
                    for (int w = 0; w < nWords; w++) {
                        word w1, w2;
                        w1 = ((word*) Vec_VecEntryEntry((Vec_Vec_t *) vRes, op1[0], k))[f * nWords + w];
                        w2 = ((word*) Vec_VecEntryEntry((Vec_Vec_t *) vRes, op2[0], k))[f * nWords + w];
                        merges[w] = merges[w] & (~(w1 ^ w2));

                        w1 = ((word*) Vec_VecEntryEntry((Vec_Vec_t *) vRes, op1[1], k))[f * nWords + w];
                        w2 = ((word*) Vec_VecEntryEntry((Vec_Vec_t *) vRes, op2[1], k))[f * nWords + w];
                        merges[w] = merges[w] & (~(w1 ^ w2));
                    }
                }

                for (int w = 0; w < nWords; w++) {
                    mat[i][j] += bit_count(merges[w]);
                }
            }
        }
    }

    /*
    for(int i = 0; i < num_ops; ++i) {
        for(int j = 0; j < num_ops; ++j) {
            if(i == j) continue;
            if(mat[i][j] == 0) continue;
            cout << "[" << i << "][" << j << "] = " << mat[i][j] << endl;
        }
    }
    */
}

void SimUifPairFinder::_simulate_and_count() {
    vector<int> vec_ids = *_p_vec_op_ids;
    Wlc_Ntk_t * pSimNtk = AddAuxPOsForOperators(_pOrigNtk, vec_ids, _max_input_bw, _max_output_bw);
    Vec_Int_t * vNodes = _collect_sim_nodes(pSimNtk);
    Vec_Ptr_t * vRes;
    vRes = Wlc_NtkSimulate( pSimNtk, vNodes, nWords, nFrames );
    // Wlc_NtkSimulatePrint(pSimNtk, vNodes, vRes, nWords, nFrames);
    _count_matches(vRes, Wlc_ObjRange(Wlc_NtkObj(pSimNtk, Vec_IntEntry(vNodes, 0))));

    Wlc_NtkFree(pSimNtk);
    Vec_IntFree(vNodes);
    Wlc_NtkDeleteSim(vRes);
}

void SimUifPairFinder::_insert_sim_pairs() {
    VecVecInt& mat = _mat_pairwise_matches;
    _set_sim_pairs.clear();

    int num_ops = mat.size();

    for(int i = 0; i < num_ops; ++i) {
        for(int j = 0; j < num_ops; ++j) {
            if(i == j) continue;
            if(mat[i][j] < nThreshold) continue;

            if (i < j)
                _set_sim_pairs.insert(UIF_PAIR(OperatorID(i), OperatorID(j), 0));
            else
                _set_sim_pairs.insert(UIF_PAIR(OperatorID(j), OperatorID(i), 1));
        }
    }
}

class CexUifPairFinder {
    public:
        CexUifPairFinder(Wlc_Ntk_t * pOrigNtk, const vector<int>* p_vec_op_ids) :
            _pOrigNtk(pOrigNtk),
            _p_vec_op_ids(p_vec_op_ids)
        {}

        void SetStates(Abc_Cex_t * pCex, const vector<bool>* p_vec_op_marks, const set<UIF_PAIR>* p_set_uif_pairs, set<OperatorID>* p_set_prev_ops, const UfarManager::Params* p_params) {
            _pCex = pCex;
            _p_vec_op_blackbox_marks = p_vec_op_marks;
            _p_set_uif_pairs = p_set_uif_pairs;
            _p_set_prev_ops = p_set_prev_ops;
            _p_params = p_params;
        }
        void FindUifPairs(const VecVecChar& cex_po_values, unsigned nLookBack, set<UIF_PAIR>& set_new_pairs);
        void FindUifPairsBasic(const VecVecChar& cex_po_values, unsigned nLookBack, set<UIF_PAIR>& set_new_pairs);
        void ComputeCoreUifPairs(const set<UIF_PAIR>& set_candidates, set<UIF_PAIR>& set_core, Abc_Cex_t ** ppCex);
        const VecVecStr* GetOutputs() const {return &_outputs;}
    private:
        void _compute_max_bw();
        string _get_bitstr(Wlc_Obj_t * pObj, const VecChar& cur_pos, unsigned& pos, bool isOutput);

        Wlc_Ntk_t * _introduce_choices(const set<UIF_PAIR>& set_candidates, vector<UIF_PAIR>& vec_choice2pair);
        Wlc_Ntk_t * _apply_uif_pairs_with_choices(Wlc_Ntk_t * pNtk, const VecVecInt& vv_op_ffs, vector<int>& vec_ids, const set<UIF_PAIR>& set_candidates, vector<UIF_PAIR>& vec_choice2pair);

        Wlc_Ntk_t *         _pOrigNtk;
        const vector<int>*  _p_vec_op_ids;

        Abc_Cex_t *               _pCex                    {NULL};
        const vector<bool>*       _p_vec_op_blackbox_marks {NULL};
        const set<UIF_PAIR>*      _p_set_uif_pairs         {NULL};
        set<OperatorID>*          _p_set_prev_ops          {NULL};
        const UfarManager::Params* _p_params                {NULL};

        int            _max_input_bw {-1};
        int            _max_output_bw {-1};

        VecVecStr      _outputs;
        VecVecStr      _inputs;
};

void CexUifPairFinder::_compute_max_bw() {
     // compute max bit-width
    ComputeMaxBW(_pOrigNtk, *_p_vec_op_ids, _max_input_bw, _max_output_bw);
    LOG(3) << "maxIn = " << _max_input_bw << "; maxOut = " << _max_output_bw;
}

string CexUifPairFinder::_get_bitstr(Wlc_Obj_t * pObj, const VecChar& cur_pos, unsigned& pos, bool isOutput) {
    int range = Wlc_ObjRange(pObj);
    int max_bw = isOutput ? _max_output_bw : _max_input_bw;
    string bitstr = string(cur_pos.begin() + pos, cur_pos.begin() + pos + range).append(max_bw - range, *(cur_pos.begin() + pos + range - 1));
    pos += range;

    return bitstr;
}

Wlc_Ntk_t * CexUifPairFinder::_apply_uif_pairs_with_choices(Wlc_Ntk_t * pNtk, const VecVecInt& vv_op_ffs, vector<int>& vec_ids, const set<UIF_PAIR>& set_candidates, vector<UIF_PAIR>& vec_choice2pair) {
    array<int, 3> wires1;
    array<int, 3> wires2;

    Wlc_Ntk_t * p = DupNtkAndUpdateIDs(pNtk, vec_ids);
    Vec_Int_t * vUifConstrs = Vec_IntAlloc( 100 );
    Vec_Int_t * vFanins = Vec_IntAlloc( 2 );

    for(auto& x : *_p_set_uif_pairs) {
        get_operator_pair(p, x, wires1, wires2, vec_ids, vv_op_ffs);
        int iObj = AddOneUifImplication(p, wires1, wires2);
        Vec_IntPush(vUifConstrs, iObj);
    }

    for(auto& x : set_candidates) {
        vec_choice2pair.push_back(x);
        get_operator_pair(p, x, wires1, wires2, vec_ids, vv_op_ffs);
        int iObj = AddOneUifImplication(p, wires1, wires2);
        int iSelPi = Wlc_ObjAlloc( p, WLC_OBJ_PI, 0, 0, 0);
        Vec_IntFill(vFanins, 1, iSelPi);
        int iSelPiNeg = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_NOT, 0, 0, 0, vFanins);
        Vec_IntFillTwo(vFanins, 2, iObj, iSelPiNeg);
        int iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins);
        Vec_IntPush(vUifConstrs, iObjNew);
    }

    if (Wlc_NtkFfNum(_pOrigNtk) == 0)
        FoldCombConstraints(p, vUifConstrs);
    else
        FoldSeqConstraints(p, vUifConstrs);

    Wlc_Ntk_t * pNew = DupNtkAndUpdateIDs(p, vec_ids);

    Wlc_NtkFree(p);
    Vec_IntFree(vUifConstrs);
    Vec_IntFree(vFanins);

    return pNew;
}

Wlc_Ntk_t * CexUifPairFinder::_introduce_choices(const set<UIF_PAIR>& set_candidates, vector<UIF_PAIR>& vec_choice2pair) {
    vector<int> vec_ids = *_p_vec_op_ids;
    VecVecInt vv_op_ffs;
    Wlc_Ntk_t * pNew, * pTemp;

    if(!_p_set_prev_ops->empty())
        pNew = IntroducePrevOperators(_pOrigNtk, vec_ids, *_p_set_prev_ops, vv_op_ffs);
    else
        pNew = DupNtkAndUpdateIDs(_pOrigNtk, vec_ids);

    if(_p_params->fGrey) {
        pNew = ApplyGreyConstraints(pTemp = pNew, vec_ids, Wlc_NtkFfNum(_pOrigNtk) > 0);
        Wlc_NtkFree(pTemp);
    }

    pNew = _apply_uif_pairs_with_choices(pTemp = pNew, vv_op_ffs, vec_ids, set_candidates, vec_choice2pair);
    Wlc_NtkFree(pTemp);

    Vec_Int_t * vec_ops = collect_boxes(vec_ids, *_p_vec_op_blackbox_marks, true /*black*/);
    assert(Vec_IntSize(vec_ops) > 0);
    pNew = AbstractNodes(pTemp = pNew, vec_ops);
    Wlc_NtkFree(pTemp);

    return pNew;
}


static Abc_Cex_t * get_new_cex_with_ppi(Abc_Cex_t * pOrigCex, const VecVecInt& ppi_model, int num_orig_pis, int num_ppis, bool one_more_flop) {
    Abc_Cex_t * pCex = Abc_CexAlloc( one_more_flop ? pOrigCex->nRegs + 1 : pOrigCex->nRegs, pOrigCex->nPis, pOrigCex->iFrame + 1);
    pCex->iFrame = pOrigCex->iFrame;
    pCex->iPo = 0;

    for(int f = 0; f < pOrigCex->iFrame + 1; f++) {
        for(int i = 0; i < pOrigCex->nPis; i++) {
            int iOrigBit = pOrigCex->nRegs+pOrigCex->nPis*f + i;
            int iBit = one_more_flop ? iOrigBit + 1 : iOrigBit;
            if ( i >= num_orig_pis && i < num_orig_pis + num_ppis ) {
                if(ppi_model[f][i-num_orig_pis]) {
                    Abc_InfoSetBit(pCex->pData, iBit);
                }
            } else { // i < num_orig_pis || i >= num_orig_pis + num_ppis
                if(Abc_InfoHasBit(pOrigCex->pData, iOrigBit)) {
                    Abc_InfoSetBit(pCex->pData, iBit);
                }
            }
        }
    }

    return pCex;
}

void CexUifPairFinder::ComputeCoreUifPairs(const set<UIF_PAIR>& set_candidates, set<UIF_PAIR>& set_core, Abc_Cex_t ** ppCex) {
    vector<UIF_PAIR> vec_choice2pair;
    Wlc_Ntk_t * pChoice = _introduce_choices(set_candidates, vec_choice2pair);
    assert(set_candidates.size() == vec_choice2pair.size());

    int num_ppis;
    int num_orig_pis = compute_bit_level_pi_num(_pOrigNtk);
    Gia_Man_t * pGiaFrames = unroll_with_cex(pChoice, _pCex, num_orig_pis, vec_choice2pair.size(), &num_ppis, true);

    vector<unsigned> vec_cores;
    VecVecInt ppi_model;
    compute_core_using_sat(pGiaFrames, vec_cores, _pCex->iFrame+1, vec_choice2pair.size(), num_ppis, true, &ppi_model, false, 5000);
    if(ppCex && !ppi_model.empty()) {
        if(*ppCex) Abc_CexFree(*ppCex);
        *ppCex = get_new_cex_with_ppi(_pCex, ppi_model, num_orig_pis, num_ppis, _p_set_uif_pairs->empty() && Wlc_NtkFfNum(_pOrigNtk));
    }
    // Abc_CexPrintStats(_pCex);
    // Abc_CexPrintStats(*ppCex);

    set_core.clear();
    for(auto& x : vec_cores) {
        set_core.insert(vec_choice2pair[x]);
    }

    Gia_ManStop(pGiaFrames);
    Wlc_NtkFree(pChoice);
}

void CexUifPairFinder::FindUifPairsBasic(const VecVecChar& cex_po_values, unsigned nLookBack, set<UIF_PAIR>& set_new_pairs) {
    if ( Wlc_NtkPoNum(_pOrigNtk) != 1 || Wlc_ObjRange(Wlc_NtkPo(_pOrigNtk, 0)) != 1 )
        return;

    _inputs.clear();
    _outputs.clear();

    for (unsigned f = 0; f < cex_po_values.size(); f++) {
        _inputs.push_back(vector<string>());
        _outputs.push_back(vector<string>());

        const vector<char>& cur_po_values = cex_po_values[f];
        unsigned pos = 1;

        for (unsigned i = 0; i < _p_vec_op_ids->size(); i++) {
            int op_id = _p_vec_op_ids->at(i);
            Wlc_Obj_t * pObj = Wlc_NtkObj(_pOrigNtk, op_id);

            Wlc_Obj_t * pObjInput = NULL;

            pObjInput = Wlc_ObjFanin0(_pOrigNtk, pObj);
            _max_input_bw = Wlc_ObjRange(pObjInput);
            string bits_input0 = _get_bitstr(pObjInput, cur_po_values, pos, false);
            bits_input0 += (Wlc_ObjIsSigned(pObjInput) ? 's' : 'u');

            pObjInput = Wlc_ObjFanin1(_pOrigNtk, pObj);
            _max_input_bw = Wlc_ObjRange(pObjInput);
            string bits_input1 = _get_bitstr(pObjInput, cur_po_values, pos, false);
            bits_input1 += (Wlc_ObjIsSigned(pObjInput) ? 's' : 'u');

            _max_output_bw = Wlc_ObjRange(pObj);
            string bits_output = _get_bitstr(pObj, cur_po_values, pos, true);
            bits_output += (Wlc_ObjIsSigned(pObj) ? 's' : 'u');
            _outputs.back().push_back(bits_output);

            vector<string> keys;
            keys.push_back(bits_input0 + ':' + bits_input1);
            keys.push_back(bits_input1 + ':' + bits_input0);
            _inputs.back().push_back(keys[0]);


            for (unsigned reversed = 0; reversed < keys.size(); reversed++) {
                const string& key = keys[reversed];
                for (int g = f; g >= 0 && g >= (int)f - (int)nLookBack; g--) {
                    for (int j = 0; j < _inputs[g].size(); j++) {
                        if (!bitstr_not_equal(key, _inputs[g][j]) && bitstr_not_equal(_outputs[f][i], _outputs[g][j])) {
                            UIF_PAIR pair_int(OperatorID(j, g-f), OperatorID(i), reversed);
                            if (_p_set_uif_pairs->count(pair_int) == 0)
                                set_new_pairs.insert(pair_int);
                            if(g < f)
                                _p_set_prev_ops->insert(OperatorID(j, g-f));
                        }
                    }
                }
            }
            LOG(4) << "[" << f << "][" << i << "] : " << "key = " << keys[0] << " output = " << _outputs[f][i] ;
        }
    }
}

void CexUifPairFinder::FindUifPairs(const VecVecChar& cex_po_values, unsigned nLookBack, set<UIF_PAIR>& set_new_pairs) {
    if ( Wlc_NtkPoNum(_pOrigNtk) != 1 || Wlc_ObjRange(Wlc_NtkPo(_pOrigNtk, 0)) != 1 )
        return;

    _compute_max_bw();

    _inputs.clear();
    _outputs.clear();

    for (unsigned f = 0; f < cex_po_values.size(); f++) {

        _inputs.push_back(vector<string>());
        _outputs.push_back(vector<string>());

        const vector<char>& cur_po_values = cex_po_values[f];
        unsigned pos = 1;

        for (unsigned i = 0; i < _p_vec_op_ids->size(); i++) {
            int op_id = _p_vec_op_ids->at(i);
            Wlc_Obj_t * pObj = Wlc_NtkObj(_pOrigNtk, op_id);

            string bits_input0 = _get_bitstr(Wlc_ObjFanin0(_pOrigNtk, pObj), cur_po_values, pos, false);
            string bits_input1 = _get_bitstr(Wlc_ObjFanin1(_pOrigNtk, pObj), cur_po_values, pos, false);
            assert(bits_input0.size() == bits_input1.size());

            string bits_output = _get_bitstr(pObj, cur_po_values, pos, true);
            _outputs.back().push_back(bits_output);

            vector<string> keys;
            keys.push_back(bits_input0 + ':' + bits_input1);
            keys.push_back(bits_input1 + ':' + bits_input0);
            _inputs.back().push_back(keys[0]);

            for (unsigned reversed = 0; reversed < keys.size(); reversed++) {
                const string& key = keys[reversed];
                for (int g = f; g >= 0 && g >= (int)f - (int)nLookBack; g--) {
                    for (int j = 0; j < _inputs[g].size(); j++) {
                        if (!bitstr_not_equal(key, _inputs[g][j]) && bitstr_not_equal(_outputs[f][i], _outputs[g][j])) {
                            UIF_PAIR pair_int(OperatorID(j, g-f), OperatorID(i), reversed);
                            if (_p_set_uif_pairs->count(pair_int) == 0)
                                set_new_pairs.insert(pair_int);
                            if(g < f)
                                _p_set_prev_ops->insert(OperatorID(j, g-f));
                        }
                    }
                }
            }
            LOG(4) << "[" << f << "][" << i << "] : " << "key = " << keys[0] << " output = " << _outputs[f][i] ;
        }
    }

}

static inline int Ufar_ShouldStop( const UfarManager::Params & p )
{
    return p.pFuncStop && p.pFuncStop( p.RunId );
}

UfarManager::Params::Params() :
                RunId(-1),
                pFuncStop(NULL),
                fCexMin(true),
                fPbaUif(false),
                fLazySim(true),
                fPbaSim(false),
                fPbaCex(false),
                fSatMin(false),
                fCbaWb(false),
                fGrey(false),
                nGrey(0),
                fNorm(true),
                fAllWb(false),
                fCrossOnly(false),
                fSuper_prove(false),
                fSimple(false),
                fSyn(false),
                fPthread(false),
                iOneWb(-1),
                iExp(-1),
                nConstraintLimit(65536),
                nInitAllPairsLimit(0),
                nInitNearMults(0),
                iVerbosity(0),
                nSeqLookBack(0),
                nTimeout(65536)
            {}
UfarManager::UfarManager() : _pOrigNtk(NULL), _pAbsWithAuxPos(NULL), _fCrossReady(false) {}

UfarManager::~UfarManager() {
    if (_pOrigNtk) Wlc_NtkFree(_pOrigNtk);
}

void UfarManager::Initialize(Wlc_Ntk_t * pNtk, const set<unsigned>& types) {
    Ufar_ResetOrigCexStats();
    LogT::loglevel = params.iVerbosity;
    if (_pOrigNtk) Wlc_NtkFree(_pOrigNtk);
    _vec_orig_names.clear();
    _vec_op_ids.clear();
    _vec_op_blackbox_marks.clear();
    _vec_op_side.clear();
    _vec_op_greyness.clear();
    _set_uif_pairs.clear();
    _set_uif_sim_pairs.clear();

    _vec_vec_op_ffs.clear();
    _set_prev_ops.clear();

    profile = Profile();

    _pOrigNtk = Wlc_NtkDupDfsSimple(pNtk);
    if ( _pOrigNtk->pName == NULL )
        _pOrigNtk->pName = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
    if ( _pOrigNtk->pSpec == NULL )
        _pOrigNtk->pSpec = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );

    Wlc_Obj_t * pObj;
    int i;
    _vec_orig_names.resize(Wlc_NtkObjNumMax(pNtk));
    Wlc_NtkForEachObj(pNtk, pObj, i) {
        _vec_orig_names[i] = (Wlc_ObjName(pNtk, i));

        if(types.count(pObj->Type) > 0) {
            _vec_op_ids.push_back(i);
            if(params.nGrey) {
                _vec_op_greyness.push_back(Greyness(pNtk, pObj));
            }
        }
    }

    _vec_op_blackbox_marks.resize(_vec_op_ids.size(), true);
    _vec_op_side.resize(_vec_op_ids.size(), 0);
    _fCrossReady = false;
    if ( params.fAllWb )
        std::fill( _vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false );

    if ( params.fCrossOnly )
    {
        int nObjs = Wlc_NtkObjNumMax(_pOrigNtk);
        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(_pOrigNtk, 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(_pOrigNtk, pObjT);
                    stack.push_back( Wlc_ObjId(_pOrigNtk, pFi) );
                }
                int iFanin, k;
                Wlc_ObjForEachFanin( pObjT, iFanin, k )
                    stack.push_back(iFanin);
            }
        };

        if ( Wlc_NtkPoNum(_pOrigNtk) == 1 )
        {
            Wlc_Obj_t * pPo = Wlc_NtkPo(_pOrigNtk, 0);
            int iMiter = Wlc_ObjFaninId0(pPo);
            if ( iMiter >= 0 && iMiter < nObjs )
            {
                Wlc_Obj_t * pMit = Wlc_NtkObj(_pOrigNtk, iMiter);
                if ( Wlc_ObjFaninNum(pMit) >= 2 )
                {
                    int iL = Wlc_ObjFaninId0(pMit);
                    int iR = Wlc_ObjFaninId1(pMit);
                    mark_cone(iL, vConeL);
                    mark_cone(iR, vConeR);
                    _fCrossReady = true;
                }
            }
        }
        if ( _fCrossReady )
        {
            int nL = 0, nR = 0, nB = 0, nN = 0;
            for ( size_t iOp = 0; iOp < _vec_op_ids.size(); ++iOp )
            {
                int iObj = _vec_op_ids[iOp];
                bool fL = vConeL[iObj] != 0;
                bool fR = vConeR[iObj] != 0;
                char Side = fL ? (fR ? 3 : 1) : (fR ? 2 : 0);
                _vec_op_side[iOp] = Side;
                if ( Side == 1 ) nL++;
                else if ( Side == 2 ) nR++;
                else if ( Side == 3 ) nB++;
                else nN++;
            }
            LOG(1) << "CrossOnly: classified operators L=" << nL << " R=" << nR << " BOTH=" << nB << " NONE=" << nN;
        }
        else
            LOG(1) << "CrossOnly: unable to derive LHS/RHS cones from miter; disabling cross filter.";
    }

    auto seed_pairs_for_indices = [&]( const vector<int>& vOpIdxs )
    {
        auto sig = [&]( int iObj, int iFanin )
        {
            int iFin = (iFanin == 0) ? Wlc_ObjFaninId0(Wlc_NtkObj(_pOrigNtk, iObj)) : Wlc_ObjFaninId1(Wlc_NtkObj(_pOrigNtk, iObj));
            Wlc_Obj_t * pFin = Wlc_NtkObj(_pOrigNtk, iFin);
            return std::make_pair( Wlc_ObjRange(pFin), Wlc_ObjIsSigned(pFin) );
        };
        auto sigOut = [&]( int iObj )
        {
            Wlc_Obj_t * pObj = Wlc_NtkObj(_pOrigNtk, iObj);
            return std::make_pair( Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) );
        };
        for ( size_t i = 0; i < vOpIdxs.size(); ++i )
        for ( size_t j = i + 1; j < vOpIdxs.size(); ++j )
        {
            int idx1  = vOpIdxs[i];
            int idx2  = vOpIdxs[j];
            int iObj1 = _vec_op_ids[idx1];
            int iObj2 = _vec_op_ids[idx2];
            Wlc_Obj_t * pObj1 = Wlc_NtkObj(_pOrigNtk, iObj1);
            Wlc_Obj_t * pObj2 = Wlc_NtkObj(_pOrigNtk, iObj2);
            if ( pObj1->Type != pObj2->Type )
                continue;
            if ( sigOut(iObj1) != sigOut(iObj2) )
                continue;

            bool fDirect = (sig(iObj1, 0) == sig(iObj2, 0)) && (sig(iObj1, 1) == sig(iObj2, 1));
            bool fSwap   = (sig(iObj1, 0) == sig(iObj2, 1)) && (sig(iObj1, 1) == sig(iObj2, 0));
            if ( fDirect ) {
                UIF_PAIR Pair(OperatorID(idx1), OperatorID(idx2), 0);
                if ( _allow_uif_pair(Pair) )
                    _set_uif_pairs.insert( Pair );
            }
            if ( fSwap ) {
                UIF_PAIR Pair(OperatorID(idx1), OperatorID(idx2), 1);
                if ( _allow_uif_pair(Pair) )
                    _set_uif_pairs.insert( Pair );
            }
        }
    };

    if ( params.nInitNearMults > 0 )
    {
        vector<pair<int, int> > vScoreIdx; // (seq distance from outputs, op-index in _vec_op_ids)
        int nObjs = Wlc_NtkObjNumMax(_pOrigNtk);
        vector<int> vDist(nObjs, -1);
        queue<int> q;
        Wlc_Obj_t * pPoT; int iPo;
        Wlc_NtkForEachPo( _pOrigNtk, pPoT, iPo )
        {
            int iRoot = Wlc_ObjFaninId0(pPoT);
            if ( iRoot > 0 && iRoot < nObjs && vDist[iRoot] == -1 )
            {
                vDist[iRoot] = 0;
                q.push(iRoot);
            }
        }
        while ( !q.empty() )
        {
            int iObj = q.front();
            q.pop();
            Wlc_Obj_t * pObjT = Wlc_NtkObj(_pOrigNtk, iObj);
            int dNext = vDist[iObj] + 1;
            if ( pObjT->Type == WLC_OBJ_FO )
            {
                Wlc_Obj_t * pFi = Wlc_ObjFo2Fi(_pOrigNtk, pObjT);
                int iFi = Wlc_ObjId(_pOrigNtk, pFi);
                if ( iFi > 0 && iFi < nObjs && (vDist[iFi] == -1 || dNext < vDist[iFi]) )
                {
                    vDist[iFi] = dNext;
                    q.push(iFi);
                }
            }
            int iFanin, k;
            Wlc_ObjForEachFanin( pObjT, iFanin, k )
            {
                if ( iFanin <= 0 || iFanin >= nObjs )
                    continue;
                if ( vDist[iFanin] == -1 || dNext < vDist[iFanin] )
                {
                    vDist[iFanin] = dNext;
                    q.push(iFanin);
                }
            }
        }

        for ( size_t i = 0; i < _vec_op_ids.size(); ++i )
        {
            int iObj = _vec_op_ids[i];
            if ( Wlc_NtkObj(_pOrigNtk, iObj)->Type != WLC_OBJ_ARI_MULTI )
                continue;
            if ( iObj <= 0 || iObj >= nObjs )
                continue;
            if ( vDist[iObj] < 0 )
                continue;
            vScoreIdx.push_back( { vDist[iObj], (int)i } );
        }
        sort( vScoreIdx.begin(), vScoreIdx.end(),
              []( const pair<int,int>& a, const pair<int,int>& b )
              { return a.first != b.first ? a.first < b.first : a.second < b.second; } );
        vector<int> vSeedOps;
        size_t nTake = Abc_MinInt( (int)vScoreIdx.size(), (int)params.nInitNearMults );
        vSeedOps.reserve( nTake );
        for ( size_t i = 0; i < nTake; ++i )
            vSeedOps.push_back( vScoreIdx[i].second );
        sort( vSeedOps.begin(), vSeedOps.end() );

        size_t nBefore = _set_uif_pairs.size();
        seed_pairs_for_indices( vSeedOps );
        if ( _set_uif_pairs.size() > nBefore ) {
            LOG(1) << "InitNear: pre-seeded " << (_set_uif_pairs.size() - nBefore)
                   << " UIF pairs among " << vSeedOps.size() << " closest multipliers (limit = " << params.nInitNearMults << ")";
        }
    }

    if ( params.nInitAllPairsLimit > 0 && _vec_op_ids.size() <= params.nInitAllPairsLimit )
    {
        vector<int> vAllOps;
        vAllOps.reserve( _vec_op_ids.size() );
        for ( size_t i = 0; i < _vec_op_ids.size(); ++i )
            vAllOps.push_back( (int)i );
        size_t nBefore = _set_uif_pairs.size();
        seed_pairs_for_indices( vAllOps );
        if ( _set_uif_pairs.size() > nBefore ) {
            LOG(1) << "InitAllPairs: pre-seeded " << (_set_uif_pairs.size() - nBefore)
                   << " UIF pairs (ops = " << _vec_op_ids.size() << ", limit = " << params.nInitAllPairsLimit << ")";
        }
    }

    _p_sim_mgr.reset(new SimUifPairFinder(_pOrigNtk, &_vec_op_ids));
    _p_cex_mgr.reset(new CexUifPairFinder(_pOrigNtk, &_vec_op_ids));

    struct timeval now;
    gettimeofday(&now, NULL);
    _timeout.tv_sec = now.tv_sec + params.nTimeout;
    _timeout.tv_nsec = now.tv_usec * 1000;
}

Wlc_Ntk_t * UfarManager::ApplyUifConstraints(Wlc_Ntk_t * pNtk, vector<int>& vec_ids) {
    array<int, 3> wires1;
    array<int, 3> wires2;

    Wlc_Ntk_t * p = DupNtkAndUpdateIDs(pNtk, vec_ids);
    Vec_Int_t * vUifConstrs = Vec_IntAlloc( 100 );

    for(auto& x : _set_uif_pairs) {
        get_operator_pair(p, x, wires1, wires2, vec_ids, _vec_vec_op_ffs);
        int iObj = AddOneUifImplication(p, wires1, wires2);
        Vec_IntPush(vUifConstrs, iObj);
    }

    if (Wlc_NtkFfNum(_pOrigNtk) == 0)
        FoldCombConstraints(p, vUifConstrs);
    else
        FoldSeqConstraints(p, vUifConstrs);

    Wlc_Ntk_t * pNew = DupNtkAndUpdateIDs(p, vec_ids);

    Wlc_NtkFree(p);
    Vec_IntFree(vUifConstrs);

    return pNew;
}

Wlc_Ntk_t * UfarManager::_set_up_constraints(vector<int>& vec_ids) {
    Wlc_Ntk_t * pNew, * pTemp;

    if(!_set_prev_ops.empty())
        pNew = IntroducePrevOperators(_pOrigNtk, vec_ids, _set_prev_ops, _vec_vec_op_ffs);
    else
        pNew = DupNtkAndUpdateIDs(_pOrigNtk, vec_ids);

    if(params.fGrey) {
        pNew = ApplyGreyConstraints(pTemp = pNew, vec_ids, Wlc_NtkFfNum(_pOrigNtk) > 0);
        Wlc_NtkFree(pTemp);
    }

    if(!_set_uif_pairs.empty()) {
        pNew = ApplyUifConstraints(pTemp = pNew, vec_ids);
        Wlc_NtkFree(pTemp);
    }

    if(params.nGrey) {
        pNew = ApplyGreynessConstraints(pTemp = pNew, _vec_op_greyness, vec_ids);
        Wlc_NtkFree(pTemp);
    }

    return pNew;
}


Wlc_Ntk_t * UfarManager::BuildCurrentAbstraction() {
    vector<int> vec_ids = _vec_op_ids;
    Wlc_Ntk_t * pNew, * pTemp;

    pNew = _set_up_constraints(vec_ids);

    pNew = AddAuxPOsForOperators(pTemp = pNew, vec_ids);
    Wlc_NtkFree(pTemp);
    // for(auto x : vec_ids) cout << "ID = " << x << " Type = " << Wlc_NtkObj(pNew, x)->Type << endl;

    if (count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), true) > 0) {
        pNew = _abstract_operators(pTemp = pNew, vec_ids);
        Wlc_NtkFree(pTemp);
    }

    if(_pAbsWithAuxPos) Wlc_NtkFree(_pAbsWithAuxPos);
    _pAbsWithAuxPos = Wlc_NtkDupDfsSimple(pNew);

    pNew = RemoveAuxPOs(pTemp = pNew, Wlc_NtkPoNum(_pOrigNtk));
    Wlc_NtkFree(pTemp);

    // Preserve benchmark identity through abstraction refinements so
    // downstream bit-level engines report a meaningful miter name.
    if ( _pOrigNtk )
    {
        ABC_FREE( pNew->pName );
        ABC_FREE( pNew->pSpec );
        pNew->pName = Abc_UtilStrsav( _pOrigNtk->pName ? _pOrigNtk->pName : _pOrigNtk->pSpec );
        pNew->pSpec = Abc_UtilStrsav( _pOrigNtk->pName ? _pOrigNtk->pName : _pOrigNtk->pSpec );
    }

    // Wlc_WriteVer(pNew, "Abs.v", 0, 0);

    return pNew;
}

void UfarManager::_simulate() {
    timeval t1, t2;
    gettimeofday(&t1, NULL);

    _p_sim_mgr->SetParams(params.simSetting);
    _p_sim_mgr->Simulate();

    gettimeofday(&t2, NULL);
    profile.tUifSim += elapsed_time_usec(t1, t2);
}

void UfarManager::FindUifPairsUsingSim() {
    timeval t1, t2;
    gettimeofday(&t1, NULL);

    _p_sim_mgr->ComputeUifPairs();
    _set_uif_sim_pairs = *_p_sim_mgr->GetSimPairsPtr();

    set<UIF_PAIR> set_new_pairs;
    for(auto& x:_set_uif_sim_pairs) {
        if ( !_allow_uif_pair(x) )
            continue;
        auto res = _set_uif_pairs.insert(x);
        if(res.second)
            set_new_pairs.insert(x);
    }
    if(log_level() >= 3)
        print_pairs(set_new_pairs);

    gettimeofday(&t2, NULL);
    profile.tUifSim += elapsed_time_usec(t1, t2);
}

void UfarManager::FindUifPairsUsingCex(Abc_Cex_t * pCex, Abc_Cex_t ** ppCex) {
    timeval t1, t2;
    gettimeofday(&t1, NULL);

    VecVecChar cex_po_values;
    Gia_Man_t * pGia = BitBlast(_pAbsWithAuxPos);
    CollectPoValuesInCex(pGia, pCex, cex_po_values, params.fCexMin);
    Gia_ManStop(pGia);

    _p_cex_mgr->SetStates(pCex, &_vec_op_blackbox_marks, &_set_uif_pairs, &_set_prev_ops, &params);
    set<UIF_PAIR> set_found_pairs, set_temp;
    if (params.fNorm) {
        _p_cex_mgr->FindUifPairs(cex_po_values, params.nSeqLookBack, set_found_pairs);
    } else {
        _p_cex_mgr->FindUifPairsBasic(cex_po_values, params.nSeqLookBack, set_found_pairs);
    }
    if ( params.fCrossOnly && _fCrossReady )
    {
        for ( auto it = set_found_pairs.begin(); it != set_found_pairs.end(); )
            if ( !_allow_uif_pair(*it) )
                it = set_found_pairs.erase(it);
            else
                ++it;
    }
    if(log_level() >= 3) print_pairs(set_found_pairs);

    if(params.fPbaUif && !set_found_pairs.empty()) {
        _p_cex_mgr->ComputeCoreUifPairs(set_temp = set_found_pairs, set_found_pairs, ppCex);
        if(set_found_pairs.empty()) {
            LOG(2) << "Proof-based refinement failed (SAT)";
            // set_found_pairs = set_temp;
            if(params.fPbaCex) {
                set_found_pairs = set_temp;
            }
            if(params.fPbaSim && _p_sim_mgr->HasResults()) {
                for(auto& x : set_temp) {
                    if(_p_sim_mgr->GetCount(x) > 0)
                        set_found_pairs.insert(x);
                }
                if(set_found_pairs.empty()) {
                    LOG(2) << "No pair found with PBA and SIM";
                }
            }
        }
    }

    if ( params.fCrossOnly && _fCrossReady )
    {
        for ( auto it = set_found_pairs.begin(); it != set_found_pairs.end(); )
            if ( !_allow_uif_pair(*it) )
                it = set_found_pairs.erase(it);
            else
                ++it;
    }
    for(auto& x : set_found_pairs) _set_uif_pairs.insert(x);

    gettimeofday(&t2, NULL);
    profile.tUifRefine += elapsed_time_usec(t1, t2);
}

Wlc_Ntk_t * UfarManager::_introduce_bitwise_choices(vector<IntPair>& vec_choice2idx) {
    vector<int> vec_ids = _vec_op_ids;
    Wlc_Ntk_t * pNew, * pTemp;

    pNew = _set_up_constraints(vec_ids);

    pNew = IntroduceBitwiseChoices(pTemp = pNew, vec_ids, _vec_op_greyness, vec_choice2idx);
    Wlc_NtkFree(pTemp);

    return pNew;
}

Wlc_Ntk_t * UfarManager::_introduce_choices(vector<unsigned>& vec_choice2idx, bool fBlack) {
    vector<int> vec_ids = _vec_op_ids;
    Wlc_Ntk_t * pNew, * pTemp;

    pNew = _set_up_constraints(vec_ids);

    Vec_Int_t * vec_ops = collect_boxes(vec_ids, _vec_op_blackbox_marks, fBlack);
    assert(Vec_IntSize(vec_ops) > 0);
    map<int, int> map_temp;
    for(unsigned i = 0; i < vec_ids.size(); i++)
        map_temp[vec_ids[i]] = i;
    Vec_IntSort(vec_ops, 0);
    for(int i = 0; i < Vec_IntSize(vec_ops); i++)
        vec_choice2idx.push_back(map_temp[Vec_IntEntry(vec_ops, i)]);

    pNew = IntroduceChoices(pTemp = pNew, vec_ops);
    Wlc_NtkFree(pTemp);
    Vec_IntFree(vec_ops);

    return pNew;
}

void UfarManager::_compute_core_choices(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, vector<unsigned>& vec_cores, int num_sel_pis) {
    int num_ppis = -1;
    Gia_Man_t * pGiaFrames = unroll_with_cex(pChoice, pCex, compute_bit_level_pi_num(_pOrigNtk), num_sel_pis, &num_ppis, false);

    compute_core_using_sat(pGiaFrames, vec_cores, pCex->iFrame+1, num_sel_pis, num_ppis, false, NULL, params.fSatMin);

    Gia_ManStop(pGiaFrames);
}

void UfarManager::_perform_cex_based_white_boxing() {
    const VecVecStr* cex_outputs = _p_cex_mgr->GetOutputs();

    unsigned nFrames = cex_outputs->size();
    assert(nFrames);
    unsigned nOperators = (*cex_outputs)[0].size();
    assert(nOperators == _vec_op_ids.size());

    vector<bool> vec_op_refine(nOperators, false);
    for(unsigned i = 0; i < nOperators; i++) {
        for(unsigned f = 0; f < nFrames; f++) {
            if(!bitstr_all_x((*cex_outputs)[f][i])) {
                vec_op_refine[i] = true;
                break;
            }
        }
    }

    if(log_level() >= 2) {
        _oss.str("");
        _oss << "#vWBs = " << count(vec_op_refine.begin(), vec_op_refine.end(), true) << "(" << nOperators << ")" << "; vWBs = ";
        for(unsigned i = 0; i < nOperators; i++) {
            if(vec_op_refine[i])
                _oss << i << " ";
        }
        LOG(2) << _oss.str();
    }

    for(unsigned i = 0; i < nOperators; i++) {
        if(vec_op_refine[i])
            _vec_op_blackbox_marks[i] = false;
    }
}

void UfarManager::_shrink_final_abstraction() {
    vector<unsigned> vec_choice2idx;
    Wlc_Ntk_t * pNtkWithChoices = _introduce_choices(vec_choice2idx, false /*white*/);

    int num_sel_pis = vec_choice2idx.size();
    int num_other_pis = compute_bit_level_pi_num(pNtkWithChoices) - num_sel_pis;

    Gia_Man_t * pMiter = GetInvMiter(pNtkWithChoices, "inv.pla");
    printf("Miter stat: pi = %d, ff = %d, and = %d, po = %d\n", Gia_ManPiNum(pMiter), Gia_ManRegNum(pMiter), Gia_ManAndNum(pMiter), Gia_ManPoNum(pMiter));

    vector<unsigned> vec_core_choices;
    compute_core_using_sat(pMiter, vec_core_choices, 1, num_sel_pis, num_other_pis, false, NULL, params.fSatMin);

    Wlc_NtkFree(pNtkWithChoices);
    Gia_ManStop(pMiter);

    LOG(2) << "Shrink from " << vec_choice2idx.size() << " to " << vec_core_choices.size();
    if(log_level() >= 3) {
        _oss.str("");
        _oss << "remaining white boxes = ";
        for (auto x : vec_core_choices) {
            _oss << x << " ";
        }
        LOG(3) << _oss.str();
    }

    _vec_op_blackbox_marks = vector<bool>(_vec_op_ids.size(), true);
    for (auto x : vec_core_choices)
        _vec_op_blackbox_marks[vec_choice2idx[x]] = false;
}

void UfarManager::_perform_proof_based_grey_boxing(Abc_Cex_t * pCex) {
    vector<IntPair> vec_choice2idx;
    Wlc_Ntk_t * pNtkWithChoices = _introduce_bitwise_choices(vec_choice2idx);

    vector<unsigned> vec_core_choices;
    _compute_core_choices(pNtkWithChoices, pCex, vec_core_choices, vec_choice2idx.size());
    assert(!vec_core_choices.empty());
    Wlc_NtkFree(pNtkWithChoices);

    if(log_level() >= 4) {
        for (auto x : vec_core_choices) {
            LOG(4) << "WBit : operator[" << vec_choice2idx[x].first << "] at " << vec_choice2idx[x].second << "/" << _vec_op_greyness[vec_choice2idx[x].first].Size() ;
        }
    }

    vector<bool> vec_change_marks(_vec_op_greyness.size(), false);
    for (auto x : vec_core_choices) {
        _vec_op_greyness[vec_choice2idx[x].first].Set(vec_choice2idx[x].second, false);
        vec_change_marks[vec_choice2idx[x].first] = true;
    }

    for (size_t i = 0; i < _vec_op_greyness.size(); ++i) {
        Greyness& grey = _vec_op_greyness[i];
        if(vec_change_marks[i])
            grey.UpdateCost();

        if(grey.IsTooWhite(params.nGrey)) {
            LOG(2) << "Grey: SetWhite: [" << i << "] = " << float(grey.CurrentCost())/float(grey.TotalCost()) << " (" << grey.CurrentCost() << " / " << grey.TotalCost() << ") " << grey.to_string();
            grey.SetWhite();
            _vec_op_blackbox_marks[i] = false;
        }
    }
}

void UfarManager::_perform_proof_based_white_boxing(Abc_Cex_t * pCex) {
    vector<unsigned> vec_choice2idx;
    Wlc_Ntk_t * pNtkWithChoices = _introduce_choices(vec_choice2idx, true /*black*/);

    // for(unsigned i = 0; i < vec_choice2idx.size(); i++) cout << "i = " << i << " idx = " << vec_choice2idx[i] << endl;

    vector<unsigned> vec_core_choices;
    _compute_core_choices(pNtkWithChoices, pCex, vec_core_choices, vec_choice2idx.size());
    assert(!vec_core_choices.empty());
    Wlc_NtkFree(pNtkWithChoices);

    if(log_level() >= 2) {
        _oss.str("");
        _oss << "#vCores = " << vec_core_choices.size() << "; vCores = ";
        for (unsigned i = 0; i < vec_core_choices.size(); i++) {
            _oss << vec_choice2idx[vec_core_choices[i]] << " ";
        }
        LOG(2) << _oss.str();
    }

    if (params.iOneWb == -1) {
        for (unsigned i = 0; i < vec_core_choices.size(); i++)
            _vec_op_blackbox_marks[vec_choice2idx[vec_core_choices[i]]] = false;
    } else if (params.iOneWb == 0) {
        unsigned idx = 0;
        for (auto x : vec_core_choices) {
            if (vec_choice2idx[x] > idx)
                idx = vec_choice2idx[x];
        }
        _vec_op_blackbox_marks[idx] = false;
        LOG(2) << "White boxing ID(" << idx << ")";
    }
}

void UfarManager::DetermineGreyness(Abc_Cex_t *pCex) {
    timeval t1, t2;
    gettimeofday(&t1, NULL);

    _perform_proof_based_grey_boxing(pCex);

    gettimeofday(&t2, NULL);
    profile.tGbRefine += elapsed_time_usec(t1, t2);
}

void UfarManager::DetermineWhiteBoxes(Abc_Cex_t * pCex) {
    timeval t1, t2;
    gettimeofday(&t1, NULL);

    if(params.fCbaWb) {
        _perform_cex_based_white_boxing();
    } else {
        _perform_proof_based_white_boxing(pCex);
    }

    gettimeofday(&t2, NULL);
    profile.tWbRefine += elapsed_time_usec(t1, t2);
}

int UfarManager::VerifyCurrentAbstraction(Abc_Cex_t ** ppCex) {
    timeval t1, t2;
    gettimeofday(&t1, NULL);
    if ( Ufar_ShouldStop(params) )
        return -1;

    Wlc_Ntk_t * pCurrent = BuildCurrentAbstraction();
    if ( Ufar_ShouldStop(params) ) {
        Wlc_NtkFree(pCurrent);
        return -1;
    }
    if(!params.fileAbs.empty())
        Wlc_WriteVer(pCurrent, &((params.fileAbs + "_abs.v")[0u]), 0, 0);

    int ret = -1;
    /*
    if(params.fSuper_prove || params.fSimple) {
        ret = super_prove(pCurrent, ppCex, params.fSimple, &params.fileName);
    } else {
        if ( params.fPthread ) {
            ret = verify_model(pCurrent, ppCex, &params.fileName, &params.parSetting, params.fSyn, &_timeout);
        } else {
            ret = bit_level_solve(pCurrent, ppCex, &params.fileName, &params.parSetting, params.fSyn);
        }
    }
    */
    ret = verify_model(pCurrent, ppCex, &params.fileName, &params.parSetting, params.fSyn, &_timeout, params.pFuncStop, params.RunId, &params.solverSetting, (int)params.nTimeout);
    Wlc_NtkFree(pCurrent);

    gettimeofday(&t2, NULL);
    profile.tBLSolver += elapsed_time_usec(t1, t2);

    return ret;
}

int UfarManager::PerformUIFProve(const timeval& timer) {
    struct Mem {
            Mem() : pCex(NULL), pCex2(NULL) {}
            ~Mem() {
                if (pCex)  Abc_CexFree(pCex);
                if (pCex2) Abc_CexFree(pCex2);
            }
            Abc_Cex_t * pCex;
            Abc_Cex_t * pCex2;
    };

    Mem mem;
    char buffer [256];
    int ret;
    unsigned n_iter_wb = 0;
    unsigned n_iter_uif = 0;
    timeval curTime;
    float elapsedTime;

    auto dump_grey_stat = [&]() {
        if(!params.nGrey || log_level()<2 ) return;
        float stat = 0;
        for(size_t i = 0; i < _vec_op_greyness.size(); ++i) {
            if (_vec_op_greyness[i].IsGrey()) {
                unsigned current_cost = _vec_op_greyness[i].CurrentCost();
                unsigned total_cost = _vec_op_greyness[i].TotalCost();
                float cur_stat = float(current_cost) / float(total_cost);
                stat += cur_stat;
                LOG(2) << "Grey: [" << i << "] = " << setprecision(2) << cur_stat << "\t (" << current_cost << " / "
                       << total_cost << ") \t" << _vec_op_greyness[i].to_string();
            }
        }
        LOG(1) << "Grey: [Total] = " << setprecision(4) << stat << " (" << _vec_op_greyness.size() << ")";
    };
    auto print_stat = [&]() {
        unsigned nWhiteBoxes = count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false);
        if (profile.nMaxUifPairs < _set_uif_pairs.size())
            profile.nMaxUifPairs = _set_uif_pairs.size();
        if (profile.nMaxWhiteBoxes < nWhiteBoxes)
            profile.nMaxWhiteBoxes = nWhiteBoxes;
        gettimeofday(&curTime, NULL);
        elapsedTime = elapsed_time_usec(timer, curTime)/1000000.0;
        snprintf(buffer, sizeof(buffer), "Iteration[%2u][%3u]: %4u White boxes\t%4lu UIF constraints (time = %.4f)", n_iter_wb, n_iter_uif, nWhiteBoxes, _set_uif_pairs.size(), elapsedTime);
        LOG(1) << buffer << _get_profile_uf_wb();
        dump_grey_stat();
        if(!params.fileStatesOut.empty()) _dump_states(params.fileStatesOut);
    };

    if ( Ufar_ShouldStop(params) )
        return -1;
    if (!params.fileStatesIn.empty()) {
        _read_states(params.fileStatesIn);
        if (params.iExp != -1) _massage_state_b();
        print_stat();
    }

    if (!params.fLazySim && !params.simSetting.empty()) {
        if ( Ufar_ShouldStop(params) )
            return -1;
        unsigned origSize = _set_uif_pairs.size();
        LOG(1) << "Try using simulation to find UIF pairs";
        _simulate();
        FindUifPairsUsingSim();
        params.simSetting.clear();
        if (origSize == _set_uif_pairs.size()) {
            LOG(1) << "No new UIF pair is found using simulation";
        } else {
            ++n_iter_uif;
            print_stat();
        }
    }

    while(true) {
        while(true) {
            if ( Ufar_ShouldStop(params) )
                return -1;
            if (params.fPbaCex && mem.pCex2) {
                if(mem.pCex) Abc_CexFree(mem.pCex);
                mem.pCex = mem.pCex2;
                mem.pCex2 = NULL;
                Wlc_Ntk_t * pCurrent = BuildCurrentAbstraction();
                Wlc_NtkFree(pCurrent);
                ret = 0;
            } else {
                profile.nVerifyCalls++;
                ret = VerifyCurrentAbstraction(&mem.pCex);
            }

            if (ret ==  0) { // SAT
                profile.nSatCalls++;
                if ( Ufar_ShouldStop(params) )
                    return -1;
                // GetOperatorsInCex(mem.pCex);
                timeval tCheck1, tCheck2;
                gettimeofday(&tCheck1, NULL);
                bool fRealCex = verify_cex_on_original(_pOrigNtk, mem.pCex);
                gettimeofday(&tCheck2, NULL);
                profile.tCexCheckOrig += elapsed_time_usec(tCheck1, tCheck2);
                if (fRealCex) {
                    profile.nRealCex++;
                    PrintWordCEX(_pOrigNtk, mem.pCex, &_vec_orig_names);
                    return 0;
                }
                profile.nSpuriousCex++;
                unsigned n_before = _set_uif_pairs.size();
                set<UIF_PAIR> set_before = _set_uif_pairs;

                FindUifPairsUsingCex(mem.pCex, &mem.pCex2);
                if ( Ufar_ShouldStop(params) )
                    return -1;

                if (n_before == _set_uif_pairs.size()) {
                    LOG(1) << "No new UIF pair is found in CEX";

                    if(!params.simSetting.empty()) {
                        if ( Ufar_ShouldStop(params) )
                            return -1;
                        LOG(1) << "Try using simulation to find UIF pairs";
                        _simulate();
                        FindUifPairsUsingSim();
                        params.simSetting.clear();
                        if (n_before == _set_uif_pairs.size()) {
                            LOG(1) << "No new UIF pair is found using simulation";
                        }
                    }

                    if (params.nGrey) {
                        if ( Ufar_ShouldStop(params) )
                            return -1;
                        DetermineGreyness(mem.pCex);
                    }

                    if (n_before == _set_uif_pairs.size() && !params.nGrey) {
                        break; // entering white-boxing refinement
                    }
                }

                if (_set_uif_pairs.size() > n_before)
                    profile.nUifPairsAdded += (_set_uif_pairs.size() - n_before);
                if (_set_uif_pairs.size() > n_before) {
                    for (const auto& x : _set_uif_pairs) {
                        if (set_before.find(x) == set_before.end() && _is_mul_mul_pair(x))
                            profile.nUifMulMulPairsAdded++;
                    }
                }
                ++n_iter_uif;
                profile.nIterUif++;
                print_stat();

                if(_set_uif_pairs.size() > params.nConstraintLimit)
                    return -1;
            } else if (ret == 1) { // UNSAT
                profile.nUnsatCalls++;
                //_shrink_final_abstraction();
                //print_stat();
                return 1;

            } else {
                profile.nUnknownCalls++;
                return -1;

            }
        }

        if ( Ufar_ShouldStop(params) )
            return -1;
        unsigned nWhiteBoxesBefore = count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false);
        DetermineWhiteBoxes(mem.pCex);
        unsigned nWhiteBoxesAfter  = count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false);
        if (nWhiteBoxesAfter > nWhiteBoxesBefore)
            profile.nWbAdded += (nWhiteBoxesAfter - nWhiteBoxesBefore);

        ++n_iter_wb;
        profile.nIterWb++;
        print_stat();
    }
    return -1;
}

void UfarManager::_massage_state_b() {
    for(const auto& x : _set_uif_pairs ) {
        bool first_black = _vec_op_blackbox_marks[x.first.idx];
        bool second_black = _vec_op_blackbox_marks[x.second.idx];
        if (!first_black && !second_black) {
            int to_black_idx = (params.iExp == 0 ? x.second.idx : x.first.idx);
            _vec_op_blackbox_marks[to_black_idx] = true;
            LOG(2) << "Blackbox (" << to_black_idx << ") for UF (" << x.first.idx << ", " << x.second.idx << ")";
        }
    }
}


bool UfarManager::_is_mul_mul_pair(const UIF_PAIR& x) const {
    if (!_pOrigNtk)
        return false;
    if (x.first.idx >= _vec_op_ids.size() || x.second.idx >= _vec_op_ids.size())
        return false;
    int obj1 = _vec_op_ids[x.first.idx];
    int obj2 = _vec_op_ids[x.second.idx];
    Wlc_Obj_t * pObj1 = Wlc_NtkObj(_pOrigNtk, obj1);
    Wlc_Obj_t * pObj2 = Wlc_NtkObj(_pOrigNtk, obj2);
    return pObj1 && pObj2 && pObj1->Type == WLC_OBJ_ARI_MULTI && pObj2->Type == WLC_OBJ_ARI_MULTI;
}

bool UfarManager::_allow_uif_pair(const UIF_PAIR& x) const {
    if ( !params.fCrossOnly || !_fCrossReady )
        return true;
    if ( x.first.idx < 0 || x.second.idx < 0 )
        return false;
    if ( x.first.idx >= (int)_vec_op_side.size() || x.second.idx >= (int)_vec_op_side.size() )
        return false;
    char s1 = _vec_op_side[x.first.idx];
    char s2 = _vec_op_side[x.second.idx];
    return (s1 == 1 && s2 == 2) || (s1 == 2 && s2 == 1);
}


string UfarManager::_get_profile_uf_wb() {
    if (log_level() <= 4) return "";
    unsigned num_full_white = 0;
    unsigned num_full_black = 0;
    unsigned num_grey = 0;
    for(const auto& x : _set_uif_pairs ) {
        bool first_black = _vec_op_blackbox_marks[x.first.idx];
        bool second_black = _vec_op_blackbox_marks[x.second.idx];
        if(first_black && second_black) {
            ++num_full_black;
        } else if (!first_black && !second_black) {
            ++num_full_white;
            LOG(3) << "ww : (" << x.first.idx << ", " << x.second.idx << ")";
        } else {
            ++num_grey;
        }
    }
    ostringstream oss;
    oss << "; ww = " << num_full_white << "; bb = " << num_full_black << "; gr = " << num_grey <<";";
    return oss.str();
}

void UfarManager::GetOperatorsInCex(Abc_Cex_t *pCex, VecVecStr* pRes) {
    VecVecChar cex_po_values;

    Gia_Man_t * pGia = BitBlast(_pAbsWithAuxPos);
    CollectPoValuesInCex(pGia, pCex, cex_po_values, params.fCexMin);
    Gia_ManStop(pGia);

    unsigned pos;
    for(unsigned f = 0; f < cex_po_values.size(); f++) {
        if (pRes) pRes->push_back(VecStr());
        vector<char>& cur_po_vals = cex_po_values[f];
        pos = 1;
        for(unsigned i = 1; i < Wlc_NtkPoNum(_pAbsWithAuxPos); i++) {
            int range = Wlc_ObjRange(Wlc_NtkPo(_pAbsWithAuxPos, i));
            string bit_str = string(cur_po_vals.begin() + pos, cur_po_vals.begin() + pos + range);
            if (!pRes) {
                cout << "PO[" << i << "]@" << f << " = " << string(bit_str.rbegin(), bit_str.rend()) << endl;
            } else {
                pRes->back().push_back(bit_str);
            }
            pos += range;
        }
    }

}

void UfarManager::DumpParams() const {
    unsigned n_setw = 15;
    cout << "Parameters : " << endl;
    cout << "     " << setw(n_setw) << left << "cexmin" << " : " << (params.fCexMin ? "yes" : "no") << endl;
    cout << "     " << setw(n_setw) << left << "allwb" << " : " << (params.fAllWb ? "yes" : "no") << endl;
    cout << "     " << setw(n_setw) << left << "crossonly" << " : " << (params.fCrossOnly ? "yes" : "no") << endl;
    cout << "     " << setw(n_setw) << left << "initnear" << " : " << params.nInitNearMults << endl;
    cout << "     " << setw(n_setw) << left << "iLogLevel" << " : " << params.iVerbosity << endl;
}

void UfarManager::DumpMgrInfo() const {
    cout << "Operators : " << endl;
    for(unsigned i = 0; i < _vec_op_ids.size(); i++, printf("\n")) {
        cout << "OP_ID = " << i << " : ";
        cout << _vec_orig_names[_vec_op_ids[i]] << " = ";
        cout << _vec_orig_names[Wlc_ObjFaninId0(Wlc_NtkObj(_pOrigNtk, _vec_op_ids[i]))] << " * ";
        cout << _vec_orig_names[Wlc_ObjFaninId1(Wlc_NtkObj(_pOrigNtk, _vec_op_ids[i]))] ;
        cout << (_vec_op_blackbox_marks[i] ? " (black)" : "") ;
    }
}


void UfarManager::_dump_states(const std::string& file) {
    fstream fs;
    fs.open((file + "_s").c_str(), fstream::out);

    if(!fs.is_open()) {
        cerr << "Cannot open the file for dumping states.\n";
        return;
    }

    fs << "B\n";
    for (int i = 0; i < _vec_op_blackbox_marks.size(); ++i) {
        fs << (_vec_op_blackbox_marks[i] == true ? "1" : "0");
    }
    fs << "\nP\n";
    for (const auto& x : _set_uif_pairs) {
        fs << x.first.idx << "," << x.first.timediff << ",";
        fs << x.second.idx << "," << x.second.timediff << ",";
        fs << (x.fMark == true ? "1" : "0") << "\n";
    }

    fs.close();
}

void UfarManager::_read_states(const std::string &file) {
    fstream fs;
    fs.open(file.c_str(), fstream::in);

    if(!fs.is_open()) {
        cerr << "Cannot open the file for reading states.\n";
        return;
    }

    string line;
    getline(fs, line);
    assert(line == "B");
    getline(fs, line);
    set_state_b(_vec_op_blackbox_marks, line);
    getline(fs, line);
    assert(line == "P");
    while(getline(fs, line)) {
        set_state_p(_set_uif_pairs, line);
    }

    if(log_level() >= 3) print_blackboxes(_vec_op_blackbox_marks);
    if(log_level() >= 3) print_pairs(_set_uif_pairs);

    fs.close();
}

 Wlc_Ntk_t * UfarManager::_abstract_operators(Wlc_Ntk_t * pNtk, const vector<int>& vec_ids) const {
    Vec_Int_t * vec_ops = collect_boxes(vec_ids, _vec_op_blackbox_marks, true /*black*/);
    assert(Vec_IntSize(vec_ops) > 0);

    Wlc_Ntk_t * pNew = NULL;
    pNew = AbstractNodes(pNtk, vec_ops);

    Vec_IntFree(vec_ops);

    return pNew;
}

}

ABC_NAMESPACE_IMPL_END
