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

函数
Result< bool >	apply_profile (const SymbolicExpr &lhs, const SymbolicExpr &rhs, ComputationContext &context, const EqvOptions &options, detail::RewriteBudget &budget)
Result< bool >	equivalent_with_budget (const SymbolicExpr &lhs, const SymbolicExpr &rhs, ComputationContext &context, const EqvOptions &options, detail::RewriteBudget *budget)
Result< std::pair< ExprPtr, ExprPtr > >	prepare_operands (const SymbolicExpr &lhs, const SymbolicExpr &rhs, ComputationContext &context, detail::RewriteBudget &budget)
Result< bool >	prove_checked_operands (const SymbolicExpr &lhs, const SymbolicExpr &rhs, ComputationContext &context, const EqvOptions &options, detail::RewriteBudget &budget)
Result< bool >	prove_operands (const SymbolicExpr &lhs, const SymbolicExpr &rhs, ComputationContext &context, const EqvOptions &options, detail::RewriteBudget &budget)

函数说明

apply_profile()

Result< bool > LMCAS::anonymous_namespace{equivalence_engine.cpp}::apply_profile	(	const SymbolicExpr &	lhs,
		const SymbolicExpr &	rhs,
		ComputationContext &	context,
		const EqvOptions &	options,
		detail::RewriteBudget &	budget )

在文件 equivalence_engine.cpp 第 66 行定义.

                                                                                   {
    if (options.profile != EqvProfile::TrigBasic &&
        options.profile != EqvProfile::ExpLogBasic) {
        return prove_operands(lhs, rhs, context, options, budget);
    }
    const bool trig = options.profile == EqvProfile::TrigBasic;
    budget.consume();
    ExprPtr rewritten_lhs;
    ExprPtr rewritten_rhs;
    if (trig) {
        rewritten_lhs = equivalence_detail::rewrite_trig_basic_identity(detail::node(lhs), budget);
        rewritten_rhs = equivalence_detail::rewrite_trig_basic_identity(detail::node(rhs), budget);
    } else {
        rewritten_lhs = equivalence_detail::rewrite_exp_log_basic_identity(
            detail::node(lhs), context.assumptions().get(), budget);
        rewritten_rhs = equivalence_detail::rewrite_exp_log_basic_identity(
            detail::node(rhs), context.assumptions().get(), budget);
    }
    rewritten_lhs = equivalence_detail::normalize_equivalence(rewritten_lhs, budget);
    rewritten_rhs = equivalence_detail::normalize_equivalence(rewritten_rhs, budget);
    EqvOptions core_options = options;
    core_options.profile = EqvProfile::Core;
    return equivalent_with_budget(*rewritten_lhs, *rewritten_rhs, context, core_options, &budget);
}

引用了 apply_profile(), LMCAS::detail::RewriteBudget::consume(), LMCAS::context, LMCAS::Core, equivalent_with_budget(), LMCAS::ExpLogBasic, LMCAS::detail::node(), LMCAS::equivalence_detail::normalize_equivalence(), LMCAS::options, LMCAS::EqvOptions::profile, prove_operands(), LMCAS::equivalence_detail::rewrite_exp_log_basic_identity(), LMCAS::equivalence_detail::rewrite_trig_basic_identity(), LMCAS::rhs , 以及 LMCAS::TrigBasic.

被这些函数引用 apply_profile() , 以及 prove_checked_operands().

函数调用图:

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

equivalent_with_budget()

Result< bool > LMCAS::anonymous_namespace{equivalence_engine.cpp}::equivalent_with_budget	(	const SymbolicExpr &	lhs,
		const SymbolicExpr &	rhs,
		ComputationContext &	context,
		const EqvOptions &	options,
		detail::RewriteBudget *	budget )

在文件 equivalence_engine.cpp 第 149 行定义.

                                                                 {
    try {
        auto valid = equivalence_detail::validate_eqv_options(options);
        if (!valid) { return Result<bool>::failure(valid.error()); }
        auto step = context.consume_steps(1, kEquivalentOperation);
        if (!step) { return Result<bool>::failure(step.error()); }
        if (budget) {
            return prove_checked_operands(lhs, rhs, context, options, *budget);
        }
        const auto input_nodes = detail::RewriteBudget::input_nodes(
            detail::node(lhs), detail::node(rhs), context,
            options.budget.max_rewrite_depth, kEquivalentOperation);
        const auto maximum = std::numeric_limits<std::size_t>::max();
        const auto factor = options.budget.max_node_growth_factor;
        const auto growth_nodes = input_nodes > maximum / factor
            ? maximum : input_nodes * factor;
        const auto max_nodes = std::min(context.limits().max_ast_nodes, growth_nodes);
        detail::RewriteBudget initial_budget(
            context, options.budget.max_rewrite_steps,
            options.budget.max_rewrite_depth, max_nodes, kEquivalentOperation);
        return prove_checked_operands(lhs, rhs, context, options, initial_budget);
    } catch (const CasError& error) {
        return Result<bool>::failure(error);
    } catch (const std::length_error& error) {
        return Result<bool>::failure(CasErrc::ResourceLimit, error.what(),
                                     kEquivalentOperation);
    } catch (const std::bad_alloc&) {
        return Result<bool>::failure(CasErrc::ResourceLimit,
                                     "equivalence check allocation failed",
                                     kEquivalentOperation);
    } catch (const std::exception& error) {
        return Result<bool>::failure(CasErrc::InternalInvariant, error.what(),
                                     kEquivalentOperation);
    }
}

引用了 LMCAS::context, equivalent_with_budget(), LMCAS::Result< T >::failure(), LMCAS::detail::RewriteBudget::input_nodes(), LMCAS::InternalInvariant, LMCAS::kEquivalentOperation, LMCAS::detail::node(), LMCAS::options, prove_checked_operands(), LMCAS::ResourceLimit, LMCAS::rhs , 以及 LMCAS::equivalence_detail::validate_eqv_options().

被这些函数引用 apply_profile() , 以及 equivalent_with_budget().

函数调用图:

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

prepare_operands()

Result< std::pair< ExprPtr, ExprPtr > > LMCAS::anonymous_namespace{equivalence_engine.cpp}::prepare_operands	(	const SymbolicExpr &	lhs,
		const SymbolicExpr &	rhs,
		ComputationContext &	context,
		detail::RewriteBudget &	budget )

在文件 equivalence_engine.cpp 第 46 行定义.

                                                              {
    using OperandsResult = Result<std::pair<ExprPtr, ExprPtr>>;
    auto left = std::make_shared<SymbolicExpr>(lhs);
    auto right = std::make_shared<SymbolicExpr>(rhs);
    if (auto quantity = std::dynamic_pointer_cast<const QuantityNode>(detail::node(lhs))) {
        normalization_check_arithmetic<MultiplyNode>(&budget, 1, quantity->value());
        auto stripped = strip_unit(left, UnitStripMode::BaseValue, context);
        if (!stripped) { return OperandsResult::failure(stripped.error()); }
        left = stripped.value();
    }
    if (auto quantity = std::dynamic_pointer_cast<const QuantityNode>(detail::node(rhs))) {
        normalization_check_arithmetic<MultiplyNode>(&budget, 1, quantity->value());
        auto stripped = strip_unit(right, UnitStripMode::BaseValue, context);
        if (!stripped) { return OperandsResult::failure(stripped.error()); }
        right = stripped.value();
    }
    return OperandsResult::success({std::move(left), std::move(right)});
}

引用了 LMCAS::BaseValue, LMCAS::context, LMCAS::detail::node(), LMCAS::normalization_check_arithmetic(), prepare_operands(), LMCAS::rhs, LMCAS::right , 以及 LMCAS::strip_unit().

被这些函数引用 prepare_operands() , 以及 prove_operands().

函数调用图:

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

prove_checked_operands()

Result< bool > LMCAS::anonymous_namespace{equivalence_engine.cpp}::prove_checked_operands	(	const SymbolicExpr &	lhs,
		const SymbolicExpr &	rhs,
		ComputationContext &	context,
		const EqvOptions &	options,
		detail::RewriteBudget &	budget )

在文件 equivalence_engine.cpp 第 129 行定义.

                                 {
    budget.consume();
    budget.measure(detail::node(lhs));
    budget.measure(detail::node(rhs));
    if (structurally_equal(lhs, rhs)) { return true; }
    auto lhs_dimension = dimension_of(lhs);
    if (!lhs_dimension) { return Result<bool>::failure(lhs_dimension.error()); }
    auto rhs_dimension = dimension_of(rhs);
    if (!rhs_dimension) { return Result<bool>::failure(rhs_dimension.error()); }
    if (lhs_dimension.value() != rhs_dimension.value()) {
        return Result<bool>::success(false);
    }
    return options.profile == EqvProfile::Core
        ? prove_operands(lhs, rhs, context, options, budget)
        : apply_profile(lhs, rhs, context, options, budget);
}

引用了 apply_profile(), LMCAS::detail::RewriteBudget::consume(), LMCAS::context, LMCAS::Core, LMCAS::dimension_of(), LMCAS::Result< T >::failure(), LMCAS::detail::RewriteBudget::measure(), LMCAS::detail::node(), LMCAS::options, prove_checked_operands(), prove_operands(), LMCAS::rhs, LMCAS::structurally_equal() , 以及 LMCAS::Result< T >::success().

被这些函数引用 equivalent_with_budget() , 以及 prove_checked_operands().

函数调用图:

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

prove_operands()

Result< bool > LMCAS::anonymous_namespace{equivalence_engine.cpp}::prove_operands	(	const SymbolicExpr &	lhs,
		const SymbolicExpr &	rhs,
		ComputationContext &	context,
		const EqvOptions &	options,
		detail::RewriteBudget &	budget )

在文件 equivalence_engine.cpp 第 93 行定义.

                                                                                    {
    budget.consume();
    auto operands = prepare_operands(lhs, rhs, context, budget);
    if (!operands) { return Result<bool>::failure(operands.error()); }
    auto left = equivalence_detail::canonicalize_complex_product(
        *operands.value().first, budget);
    auto right = equivalence_detail::canonicalize_complex_product(
        *operands.value().second, budget);
    if (structurally_equal(*left, *right)) {
        return Result<bool>::success(true);
    }
    normalization_check_arithmetic<MultiplyNode>(&budget, 1, detail::node(right));
    auto negative = SymbolicExpr::multiply(SymbolicExpr::number(-1), right);
    normalization_check_arithmetic<AddNode>(&budget, 0, detail::node(left), detail::node(negative));
    auto difference = SymbolicExpr::add(left, negative);
    if (!difference) {
        return Result<bool>::failure(CasErrc::InternalInvariant,
                                     "equivalence difference construction failed",
                                     kEquivalentOperation);
    }
    difference = equivalence_detail::normalize_equivalence(difference, budget);
    const auto value = detail::exact_rational_value(detail::node(difference));
    if (value && value->is_zero()) {
        return Result<bool>::success(true);
    }
    auto polynomial = equivalence_detail::prove_rational_polynomial_equivalence(
        difference, context, options, budget);
    if (!polynomial) { return Result<bool>::failure(polynomial.error()); }
    if (polynomial.value()) { return Result<bool>::success(*polynomial.value()); }
    return Result<bool>::failure(CasErrc::Inconclusive,
                                 "equivalence proof is inconclusive",
                                 kEquivalentOperation);
}

引用了 LMCAS::equivalence_detail::canonicalize_complex_product(), LMCAS::detail::RewriteBudget::consume(), LMCAS::context, LMCAS::detail::exact_rational_value(), LMCAS::Result< T >::failure(), LMCAS::Inconclusive, LMCAS::InternalInvariant, LMCAS::kEquivalentOperation, LMCAS::detail::node(), LMCAS::normalization_check_arithmetic(), LMCAS::equivalence_detail::normalize_equivalence(), LMCAS::options, prepare_operands(), prove_operands(), LMCAS::equivalence_detail::prove_rational_polynomial_equivalence(), LMCAS::rhs, LMCAS::right, LMCAS::structurally_equal(), LMCAS::Result< T >::success() , 以及 LMCAS::value.

被这些函数引用 apply_profile(), prove_checked_operands() , 以及 prove_operands().

函数调用图:

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