Function can_prove_imply

src/opr/impl/cond.cpp:15–49

return whether ``lhs -> rhs`` can be proved

//! return whether ``lhs -> rhs`` can be proved
bool can_prove_imply(cg::ExecutionMask* lhs, cg::ExecutionMask* rhs) {
    // this function is neither sound nor complete (and it can never be due
    // to the NP-completeness of SAT); here we only handle the most common
    // cases

    if (rhs == lhs->parent()) {
        // nested cond exec oprs
        return true;
    }

    using Mode = CondExecPredLogical::Mode;
    auto is_pred_logical = [](cg::OperatorNodeBase* opr, Mode mode) {
        auto as_p = opr->try_cast_final<CondExecPredLogical>();
        return as_p && as_p->param().mode == mode;
    };

    auto opr = rhs->owner()->owner_opr();

    if (is_pred_logical(opr, Mode::AND) && opr->input().size() == 1) {
        // cross-cn copy of predicate
        opr = opr->input(0)->owner_opr();
    }

    if (is_pred_logical(opr, Mode::OR)) {
        // in the grad of SUM_COND_OUT CondExecMerge
        auto lvar = lhs->owner();
        for (auto i : opr->input()) {
            if (lvar == i) {
                return true;
            }
        }
        return false;
    }
    return false;
}

VarNode* proxy_var_from_mask(cg::ExecutionMask* mask) {
    auto var = mask->owner();