Untitled

class UnderApproxState{
    public:
        obj_map<expr, ptr_vector<expr>> eq_combination;
        obj_map<expr, int> non_fresh_vars;
        expr_ref_vector equalities;
        expr_ref_vector disequalities;
        bool reassertEQ = false;
        bool reassertDisEQ = false;
        int eqLevel = -1;
        int diseqLevel = -1;
        expr_ref_vector asserting_constraints;
        rational str_int_bound;

        UnderApproxState(ast_manager &m) noexcept: equalities(m), disequalities(m), asserting_constraints(m){
            eq_combination.reset();
        }

        UnderApproxState(ast_manager &m, int _eqLevel, int _diseqLevel,
                         obj_map<expr, ptr_vector<expr>> const& _eq_combination,
                         obj_map<expr, int> const& _non_fresh_vars,
                        expr_ref_vector const& _equalities,
                        expr_ref_vector const& _disequalities,
                        rational _str_int_bound)noexcept:
                        eq_combination(_eq_combination),
                        non_fresh_vars(_non_fresh_vars),
                        equalities(m),
                        disequalities(m),
                        eqLevel(_eqLevel),
                        diseqLevel(_diseqLevel),
                        asserting_constraints(m),
                        str_int_bound(_str_int_bound) {
            asserting_constraints.reset();
            equalities.reset();
            equalities.append(_equalities);
            disequalities.reset();
            disequalities.append(_disequalities);
            reassertEQ = true;
            reassertDisEQ = true;
        }

        ~UnderApproxState() noexcept {}

        // Move constructor.
        UnderApproxState(UnderApproxState&& other, ast_manager &m) noexcept
            : eq_combination(), non_fresh_vars(), equalities(m), disequalities(m), reassertEQ(false), reassertDisEQ(false), eqLevel(-1), diseqLevel(-1), asserting_constraints(m), str_int_bound(0)
        {
            std::cout << "In MemoryBlock(MemoryBlock&&). length = "
                        << ". Moving resource." << std::endl;

            // Copy the data pointer and its length from the
            // source object.
            // eq_combination = std::move(other.eq_combination);
            // non_fresh_vars = std::move(other.non_fresh_vars);
            // equalities = std::move(other.equalities);
            // disequalities = std::move(other.disequalities);
            // reassertEQ = std::move(other.reassertEQ);
            // reassertDisEQ = std::move(other.reassertDisEQ);
            // eqLevel = std::move(other.eqLevel);
            // diseqLevel = std::move(other.diseqLevel);
            // asserting_constraints = std::move(other.asserting_constraints);
            // str_int_bound = std::move(other.str_int_bound);

            // Release the data pointer from the source object so that
            // the destructor does not free the memory multiple times.
            // other.eq_combination = obj_map<expr, ptr_vector<expr>>();
            // other.non_fresh_vars = obj_map<expr, int>();
            // other.equalities = expr_ref_vector(m);
            // other.disequalities = expr_ref_vector(m);
            // other.reassertEQ = false;
            // other.reassertDisEQ = false;
            // other.eqLevel = -1;
            // other.diseqLevel = -1;
            // other.asserting_constraints = expr_ref_vector(m);
            // other.str_int_bound(0);
        }

        UnderApproxState clone(ast_manager &m)noexcept{
            UnderApproxState tmp(m, eqLevel, diseqLevel, eq_combination, non_fresh_vars, equalities, disequalities, str_int_bound);
            tmp.add_asserting_constraints(asserting_constraints);
            reassertEQ = true;
            reassertDisEQ = true;
            return tmp;
        }

        void reset_eq()noexcept{
            STRACE("str", tout << __LINE__ <<  " *** " << __FUNCTION__ <<  ": eqLevel = " << eqLevel << "; diseqLevel = " << diseqLevel << std::endl;);
            eqLevel = -1;
            reassertEQ = false;
        }

        void reset_diseq()noexcept{
            STRACE("str", tout << __LINE__ <<  " *** " << __FUNCTION__ <<  ": eqLevel = " << eqLevel << "; diseqLevel = " << diseqLevel << std::endl;);
            diseqLevel = -1;
            reassertDisEQ = false;
        }

        UnderApproxState&  operator=(const UnderApproxState& other) noexcept {
            eqLevel = other.eqLevel;
            diseqLevel = other.diseqLevel;
            eq_combination = other.eq_combination;
            non_fresh_vars = other.non_fresh_vars;
            equalities.reset();
            equalities.append(other.equalities);
            disequalities.reset();
            disequalities.append(other.disequalities);
            asserting_constraints.reset();
            reassertEQ = true;
            reassertDisEQ = true;
            for (unsigned i = 0; i < other.asserting_constraints.size(); ++i)
                asserting_constraints.push_back(other.asserting_constraints[i]);

            STRACE("str", tout << __LINE__ <<  " *** " << __FUNCTION__ << ":  eq_combination: " << other.eq_combination.size() << " --> " << eq_combination.size() << std::endl;);
            return *this;
        }

        void add_asserting_constraints(expr_ref_vector _assertingConstraints)noexcept{
            // 這邊用 append 不是更快嗎？
            for (unsigned i = 0; i < _assertingConstraints.size(); ++i)
                asserting_constraints.push_back(_assertingConstraints.get(i));
        }

        void add_asserting_constraints(expr_ref assertingConstraint)noexcept{
            asserting_constraints.push_back(assertingConstraint);
        }

        bool operator==(const UnderApproxState state)noexcept{
            obj_map<expr, ptr_vector<expr>> _eq_combination = state.eq_combination;
            if (_eq_combination.size() != eq_combination.size()) {
                STRACE("str", tout << __LINE__ <<  " *** " << __FUNCTION__ << ": " << _eq_combination.size() << " vs " << eq_combination.size() <<  std::endl;);
                return false;
            }

            for (const auto& v : non_fresh_vars)
                if (!state.non_fresh_vars.contains(v.m_key)) {
                    return false;
                }

            for (const auto& n : eq_combination) {
                if (_eq_combination.contains(n.m_key)) {
                    return false;
                }
                ptr_vector<expr> tmp = _eq_combination[n.m_key];
                for (const auto &e : n.get_value()) {

                    if (!tmp.contains(e)) {
                        return false;
                    }
                    else {
                        // it is ok if some elements missing because if its size = 0
                    }
                }
            }
            STRACE("str", tout << __LINE__ <<  " *** " << __FUNCTION__ << ": Equal. " << std::endl;);
            return true;
        }
    };