LMCAS::anonymous_namespace{assumption_conditionals.cpp} 命名空间参考

函数
Tribool	evaluate_symbol_sign (const AssumptionContext &ctx, const std::string &name, RelationOp op)
Tribool	evaluate_zero_comparison (const AssumptionContext &ctx, const RelationalNode &relation)

函数说明

evaluate_symbol_sign()

Tribool LMCAS::anonymous_namespace{assumption_conditionals.cpp}::evaluate_symbol_sign	(	const AssumptionContext &	ctx,
		const std::string &	name,
		RelationOp	op )

在文件 assumption_conditionals.cpp 第 11 行定义.

                                                                  {
    struct SignRule {
        RelationOp op;
        std::initializer_list<Sign> true_signs;
        std::initializer_list<Sign> false_signs;
    };
    const SignRule rules[] = {
        {RelationOp::GT, {Sign::Positive},
         {Sign::Negative, Sign::NonPositive, Sign::Zero}},
        {RelationOp::GEQ, {Sign::NonNegative, Sign::Positive, Sign::Zero},
         {Sign::Negative}},
        {RelationOp::LT, {Sign::Negative},
         {Sign::Positive, Sign::NonNegative, Sign::Zero}},
        {RelationOp::LEQ, {Sign::NonPositive, Sign::Negative, Sign::Zero},
         {Sign::Positive}},
        {RelationOp::NEQ, {Sign::NonZero, Sign::Positive, Sign::Negative},
         {Sign::Zero}},
        {RelationOp::EQ, {Sign::Zero},
         {Sign::Positive, Sign::Negative, Sign::NonZero}}
    };
    for (const auto& rule : rules) {
        if (rule.op != op) continue;
        for (Sign sign : rule.true_signs) {
            if (ctx.has_sign(name, sign)) return Tribool::True;
        }
        for (Sign sign : rule.false_signs) {
            if (ctx.has_sign(name, sign)) return Tribool::False;
        }
        break;
    }
    return Tribool::Unknown;
}

引用了 LMCAS::EQ, evaluate_symbol_sign(), LMCAS::False, LMCAS::GEQ, LMCAS::GT, LMCAS::LEQ, LMCAS::LT, LMCAS::name, LMCAS::Negative, LMCAS::NEQ, LMCAS::NonNegative, LMCAS::NonPositive, LMCAS::NonZero, LMCAS::op, LMCAS::Positive, LMCAS::True, LMCAS::Unknown , 以及 LMCAS::Zero.

被这些函数引用 evaluate_symbol_sign() , 以及 evaluate_zero_comparison().

函数调用图:

这是这个函数的调用关系图:

evaluate_zero_comparison()

Tribool LMCAS::anonymous_namespace{assumption_conditionals.cpp}::evaluate_zero_comparison	(	const AssumptionContext &	ctx,
		const RelationalNode &	relation )

在文件 assumption_conditionals.cpp 第 45 行定义.

                                                                {
    const auto lhs_var = std::dynamic_pointer_cast<const VariableNode>(relation.left());
    const auto rhs_num = std::dynamic_pointer_cast<const NumberNode>(relation.right());
    if (lhs_var && !lhs_var->is_constant() && rhs_num && rhs_num->is_zero()) {
        return evaluate_symbol_sign(ctx, lhs_var->name(), relation.op());
    }
    const auto lhs_num = std::dynamic_pointer_cast<const NumberNode>(relation.left());
    const auto rhs_var = std::dynamic_pointer_cast<const VariableNode>(relation.right());
    if (lhs_num && lhs_num->is_zero() && rhs_var && !rhs_var->is_constant()) {
        return evaluate_symbol_sign(
            ctx, rhs_var->name(), detail::reversed_relation(relation.op()));
    }
    return Tribool::Unknown;
}

引用了 evaluate_symbol_sign(), evaluate_zero_comparison(), LMCAS::relation(), LMCAS::detail::reversed_relation() , 以及 LMCAS::Unknown.

被这些函数引用 evaluate_zero_comparison().

函数调用图:

这是这个函数的调用关系图: