Untitled
unknown
c_cpp
3 years ago
7.2 kB
333
Indexable
Never
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; } };