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;
}
};