LMCAS
Lamina Computer Algebra System
载入中...
搜索中...
未找到
LMCAS::anonymous_namespace{residual_verification.cpp} 命名空间参考

类

class  FormalResidual
 在原公共定义域上证明形式有理恒等式。 将不透明标量子式视为不定元,保留其点值可能为零的情况; 交叉相乘免去因式分解及符号系数 GCD。 更多...
class  ResidualBranch
struct  ResidualProfiles
class  ResidualRecursionScope

类型定义

using RootReplacementResult

函数

Result< void > check_residual_coefficient (const Rational &value, ComputationContext &context, const std::string &operation)
ResidualCheckResult classify_residual (const ExprPtr &expression, detail::RewriteBudget &budget, const std::string &operation)
void collect_function_profile (const FunctionNode &function, ResidualProfiles &profiles)
void collect_residual_profile_children (const std::vector< detail::SymbolicNodePtr > &children, ResidualProfiles &profiles)
void collect_residual_profiles (const detail::SymbolicNodePtr &node, ResidualProfiles &profiles)
Result< bool > has_zero_root_remainder (Polynomial< Rational > remainder, const Polynomial< Rational > &defining, ComputationContext &context, const std::string &operation)
bool is_decided (const ResidualCheck &result)
ResidualCheckResult prove_exact_root_residual (const ExprPtr &expression, detail::RewriteBudget &budget, const std::string &operation)
ResidualCheckResult prove_normalized_residual (const ExprPtr &residual, detail::RewriteBudget &budget, const EqvOptions &options, const std::string &operation)
std::optional< ResidualCheckResult > prove_piecewise_residual (const ExprPtr &residual, detail::RewriteBudget &budget, const EqvOptions &options)
ResidualCheckResult prove_with_profiles (const ExprPtr &current, ComputationContext &context, const EqvOptions &options)
RootReplacementResult replace_exact_root (const detail::SymbolicNodePtr &node, const detail::ExactRootId *&identity, detail::RewriteBudget &budget, const std::string &operation)
RootReplacementResult replace_root_operands (const detail::SymbolicNodePtr &node, const std::vector< detail::SymbolicNodePtr > &operands, bool sum, const detail::ExactRootId *&identity, detail::RewriteBudget &budget, const std::string &operation)
RootReplacementResult replace_root_power (const detail::SymbolicNodePtr &node, const PowerNode &power, const detail::ExactRootId *&identity, detail::RewriteBudget &budget, const std::string &operation)
const PiecewiseNode * residual_piecewise (const detail::SymbolicNodePtr &node, detail::RewriteBudget &budget)

类说明

◆ LMCAS::anonymous_namespace{residual_verification.cpp}::ResidualProfiles

struct LMCAS::anonymous_namespace{residual_verification.cpp}::ResidualProfiles

在文件 residual_verification.cpp 第 849 行定义.

LMCAS::anonymous_namespace{residual_verification.cpp}::ResidualProfiles 的协作图:
类成员
bool exp_log = false
bool trig = false

类型定义说明

◆ RootReplacementResult

using LMCAS::anonymous_namespace{residual_verification.cpp}::RootReplacementResult

函数说明

◆ check_residual_coefficient()

Result< void > LMCAS::anonymous_namespace{residual_verification.cpp}::check_residual_coefficient ( const Rational & value,
ComputationContext & context,
const std::string & operation )

在文件 residual_verification.cpp 第 737 行定义.

739 {
740 return context.require_integer_bits(std::max(
741 value.get_numerator().bit_length(),
742 value.get_denominator().bit_length()), operation);
743}
const std::vector< Polynomial< BigInt > > const BigInt ComputationContext & context
const std::string const ExprPtr & value

引用了 check_residual_coefficient(), LMCAS::context , 以及 LMCAS::value.

被这些函数引用 check_residual_coefficient() , 以及 has_zero_root_remainder().

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

◆ classify_residual()

ResidualCheckResult LMCAS::anonymous_namespace{residual_verification.cpp}::classify_residual ( const ExprPtr & expression,
detail::RewriteBudget & budget,
const std::string & operation )

在文件 residual_verification.cpp 第 809 行定义.

812 {
813 auto& context = budget.context();
814 auto root_proof = prove_exact_root_residual(expression, budget, operation);
815 if (!root_proof ||
816 std::holds_alternative<ProvedZeroResidual>(root_proof.value())) {
817 return root_proof;
818 }
819 auto proof = detail::classify_exact_zero(
820 expression, context, operation);
821 if (!proof) { return ResidualCheckResult::failure(proof.error()); }
822 if (proof.value() == detail::ZeroProof::Zero) {
823 return ResidualCheckResult::success(ProvedZeroResidual{
824 ExactNormalizationProof{expression}});
825 }
826 const auto variables = free_variables(detail::node(expression), &budget);
827 if (variables.size() == 1) {
828 auto polynomial = recognize_rational_polynomial(
829 *expression, *variables.begin(), context);
830 if (!polynomial) {
831 return ResidualCheckResult::failure(polynomial.error());
832 }
833 if (polynomial.value() && !polynomial.value()->is_zero()) {
835 ProvedNonIdentityResidual{expression});
836 }
837 }
838 if (proof.value() == detail::ZeroProof::NonZero) {
840 ProvedNonIdentityResidual{expression});
841 }
842 return ResidualCheckResult::success(UnprovedResidual{expression});
843}
static Result failure(CasErrc code, std::string message, std::string operation={})
static Result success(ResidualCheck value)
ComputationContext & context() const noexcept
ResidualCheckResult prove_exact_root_residual(const ExprPtr &expression, detail::RewriteBudget &budget, const std::string &operation)
Result< ZeroProof > classify_exact_zero(const ExprPtr &expression, ComputationContext &context, const std::string &operation)
const SymbolicNodePtr & node(const ::LMCAS::SymbolicExpr &expression) noexcept
std::set< std::string > free_variables(const detail::SymbolicNodePtr &expression, detail::RewriteBudget *budget)
Result< OptionalRationalPolynomial > recognize_rational_polynomial(const SymbolicExpr &expression, const std::string &variable, ComputationContext &context)

引用了 LMCAS::detail::classify_exact_zero(), classify_residual(), LMCAS::context, LMCAS::detail::RewriteBudget::context(), LMCAS::Result< ResidualCheck >::failure(), LMCAS::free_variables(), LMCAS::detail::node(), LMCAS::detail::NonZero, prove_exact_root_residual(), LMCAS::recognize_rational_polynomial(), LMCAS::Result< ResidualCheck >::success() , 以及 LMCAS::detail::Zero.

被这些函数引用 classify_residual() , 以及 prove_normalized_residual().

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

◆ collect_function_profile()

void LMCAS::anonymous_namespace{residual_verification.cpp}::collect_function_profile ( const FunctionNode & function,
ResidualProfiles & profiles )

在文件 residual_verification.cpp 第 865 行定义.

引用了 collect_function_profile(), collect_residual_profile_children(), LMCAS::FunctionNode::Cos, LMCAS::FunctionNode::Exp, LMCAS::anonymous_namespace{residual_verification.cpp}::ResidualProfiles::exp_log, LMCAS::function(), LMCAS::FunctionNode::Ln, LMCAS::FunctionNode::Sin , 以及 LMCAS::anonymous_namespace{residual_verification.cpp}::ResidualProfiles::trig.

被这些函数引用 collect_function_profile() , 以及 collect_residual_profiles().

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

◆ collect_residual_profile_children()

void LMCAS::anonymous_namespace{residual_verification.cpp}::collect_residual_profile_children ( const std::vector< detail::SymbolicNodePtr > & children,
ResidualProfiles & profiles )

在文件 residual_verification.cpp 第 857 行定义.

859 {
860 for (const auto& child : children) {
861 collect_residual_profiles(child, profiles);
862 }
863}
void collect_residual_profiles(const detail::SymbolicNodePtr &node, ResidualProfiles &profiles)

引用了 collect_residual_profile_children() , 以及 collect_residual_profiles().

被这些函数引用 collect_function_profile(), collect_residual_profile_children() , 以及 collect_residual_profiles().

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

◆ collect_residual_profiles()

void LMCAS::anonymous_namespace{residual_verification.cpp}::collect_residual_profiles ( const detail::SymbolicNodePtr & node,
ResidualProfiles & profiles )

在文件 residual_verification.cpp 第 876 行定义.

877 {
878 if (!node || (profiles.trig && profiles.exp_log)) {
879 return;
880 }
881 if (const auto function =
882 std::dynamic_pointer_cast<const FunctionNode>(node)) {
884 return;
885 }
886 if (const auto add = std::dynamic_pointer_cast<const AddNode>(node)) {
887 collect_residual_profile_children(add->operands(), profiles);
888 return;
889 }
890 if (const auto multiply =
891 std::dynamic_pointer_cast<const MultiplyNode>(node)) {
892 collect_residual_profile_children(multiply->operands(), profiles);
893 return;
894 }
895 if (const auto power = std::dynamic_pointer_cast<const PowerNode>(node)) {
896 collect_residual_profiles(power->base(), profiles);
897 collect_residual_profiles(power->exponent(), profiles);
898 return;
899 }
900 if (const auto complex =
901 std::dynamic_pointer_cast<const ComplexNode>(node)) {
902 collect_residual_profiles(complex->real(), profiles);
903 collect_residual_profiles(complex->imag(), profiles);
904 }
905}
void collect_function_profile(const FunctionNode &function, ResidualProfiles &profiles)
ExprResult add(const ExprPtr &lhs, const ExprPtr &rhs, ComputationContext &context)
ExprResult complex(ExprPtr real, ExprPtr imag)

引用了 LMCAS::add(), collect_function_profile(), collect_residual_profile_children(), collect_residual_profiles(), LMCAS::complex(), LMCAS::anonymous_namespace{residual_verification.cpp}::ResidualProfiles::exp_log, LMCAS::function() , 以及 LMCAS::anonymous_namespace{residual_verification.cpp}::ResidualProfiles::trig.

被这些函数引用 collect_residual_profile_children(), collect_residual_profiles() , 以及 prove_with_profiles().

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

◆ has_zero_root_remainder()

Result< bool > LMCAS::anonymous_namespace{residual_verification.cpp}::has_zero_root_remainder ( Polynomial< Rational > remainder,
const Polynomial< Rational > & defining,
ComputationContext & context,
const std::string & operation )

在文件 residual_verification.cpp 第 745 行定义.

749 {
750 auto terms = context.require_expansion_terms(
751 std::max(remainder.coeffs.size(), defining.coeffs.size()), operation);
752 if (!terms) return Result<bool>::failure(terms.error());
753 for (const auto& coefficient : remainder.coeffs) {
754 auto checked = check_residual_coefficient(coefficient, context, operation);
755 if (!checked) return Result<bool>::failure(checked.error());
756 }
757 for (const auto& coefficient : defining.coeffs) {
758 auto checked = check_residual_coefficient(coefficient, context, operation);
759 if (!checked) return Result<bool>::failure(checked.error());
760 }
761 while (remainder.degree() >= defining.degree()) {
762 const auto offset = remainder.coeffs.size() - defining.coeffs.size();
763 const auto& factor = remainder.coeffs.back();
764 for (std::size_t index = 0; index + 1 < defining.coeffs.size(); ++index) {
765 auto step = context.consume_steps(1, operation);
766 if (!step) return Result<bool>::failure(step.error());
767 auto product = factor * defining.coeffs[index];
768 auto checked = check_residual_coefficient(product, context, operation);
769 if (!checked) return Result<bool>::failure(checked.error());
770 auto& coefficient = remainder.coeffs[offset + index];
771 coefficient = coefficient - product;
772 checked = check_residual_coefficient(coefficient, context, operation);
773 if (!checked) return Result<bool>::failure(checked.error());
774 }
775 remainder.coeffs.pop_back();
776 remainder.trim();
777 }
778 return Result<bool>::success(remainder.is_zero());
779}
bool is_zero() const
判断是否为零多项式
std::vector< CoeffType > coeffs
系数数组,coeffs[i] 为 x^i 的系数
int degree() const
获取多项式的次数
void trim()
去除高次零系数
Result< void > check_residual_coefficient(const Rational &value, ComputationContext &context, const std::string &operation)

引用了 check_residual_coefficient(), LMCAS::Polynomial< CoeffType >::coeffs, LMCAS::context, LMCAS::Polynomial< CoeffType >::degree(), LMCAS::Result< T >::failure(), has_zero_root_remainder(), LMCAS::Polynomial< CoeffType >::is_zero(), LMCAS::Result< T >::success() , 以及 LMCAS::Polynomial< CoeffType >::trim().

被这些函数引用 has_zero_root_remainder() , 以及 prove_exact_root_residual().

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

◆ is_decided()

bool LMCAS::anonymous_namespace{residual_verification.cpp}::is_decided ( const ResidualCheck & result)

在文件 residual_verification.cpp 第 845 行定义.

845 {
846 return !std::holds_alternative<UnprovedResidual>(result);
847}

引用了 is_decided().

被这些函数引用 is_decided() , 以及 prove_normalized_residual().

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

◆ prove_exact_root_residual()

ResidualCheckResult LMCAS::anonymous_namespace{residual_verification.cpp}::prove_exact_root_residual ( const ExprPtr & expression,
detail::RewriteBudget & budget,
const std::string & operation )

在文件 residual_verification.cpp 第 781 行定义.

783 {
784 auto& context = budget.context();
785 const detail::ExactRootId* identity = nullptr;
786 auto replaced = replace_exact_root(
787 detail::node(expression), identity, budget, operation);
788 if (!replaced) return ResidualCheckResult::failure(replaced.error());
789 if (!replaced.value() || !identity) {
791 }
792 auto polynomial = recognize_rational_polynomial(
793 *detail::make_expression_ptr(*replaced.value()),
794 "_residual_root", context);
795 if (!polynomial) return ResidualCheckResult::failure(polynomial.error());
796 if (polynomial.value()) {
797 auto zero = has_zero_root_remainder(
798 std::move(*polynomial.value()), identity->polynomial, context, operation);
799 if (!zero) return ResidualCheckResult::failure(zero.error());
800 if (zero.value()) {
801 return ResidualCheckResult::success(ProvedZeroResidual{
802 ExactResidualProof{expression}});
803 }
804 }
805 return ResidualCheckResult::success(UnprovedResidual{expression});
806}
RootReplacementResult replace_exact_root(const detail::SymbolicNodePtr &node, const detail::ExactRootId *&identity, detail::RewriteBudget &budget, const std::string &operation)
Result< bool > has_zero_root_remainder(Polynomial< Rational > remainder, const Polynomial< Rational > &defining, ComputationContext &context, const std::string &operation)
std::shared_ptr<::LMCAS::SymbolicExpr > make_expression_ptr(SymbolicNodePtr root)
Polynomial< Rational > polynomial

引用了 LMCAS::context, LMCAS::detail::RewriteBudget::context(), LMCAS::Result< ResidualCheck >::failure(), has_zero_root_remainder(), LMCAS::detail::make_expression_ptr(), LMCAS::detail::node(), LMCAS::detail::ExactRootId::polynomial, prove_exact_root_residual(), LMCAS::recognize_rational_polynomial(), replace_exact_root() , 以及 LMCAS::Result< ResidualCheck >::success().

被这些函数引用 classify_residual() , 以及 prove_exact_root_residual().

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

◆ prove_normalized_residual()

ResidualCheckResult LMCAS::anonymous_namespace{residual_verification.cpp}::prove_normalized_residual ( const ExprPtr & residual,
detail::RewriteBudget & budget,
const EqvOptions & options,
const std::string & operation )

通分证明受计算预算约束,替代符号系数的 Euclid 及因子搜索。 支持绑定整数名同时出现在参数分母中的解族。

在文件 residual_verification.cpp 第 937 行定义.

938 {
939 auto& context = budget.context();
940 std::optional<detail::AssumptionFacts> assumed;
941 if (context.assumptions()) { assumed.emplace(*context.assumptions()); }
942 const auto& facts = assumed
943 ? static_cast<const FactsQuery&>(*assumed) : detail::no_facts();
944 auto current = detail::make_expression_ptr(
945 detail::normalize_node(detail::node(residual), budget, facts));
946 auto first = classify_residual(current, budget, operation);
947 if (!first || is_decided(first.value())) { return first; }
949 detail::expand_node(detail::node(current), budget, facts));
950 auto expanded = classify_residual(current, budget, operation);
951 if (!expanded || is_decided(expanded.value())) { return expanded; }
952 /**
953 * @brief 通分证明受计算预算约束,替代符号系数的 Euclid 及因子搜索。
954 * 支持绑定整数名同时出现在参数分母中的解族。
955 */
956 auto formal = FormalResidual(budget).prove(detail::node(current));
957 if (!formal) { return ResidualCheckResult::failure(formal.error()); }
958 if (formal.value()) {
959 return ResidualCheckResult::success(ProvedZeroResidual{ExactResidualProof{current}});
960 }
961 return prove_with_profiles(current, context, options);
962}
ResidualCheckResult prove_with_profiles(const ExprPtr &current, ComputationContext &context, const EqvOptions &options)
ResidualCheckResult classify_residual(const ExprPtr &expression, detail::RewriteBudget &budget, const std::string &operation)
SymbolicNodePtr expand_node(const SymbolicNodePtr &node, RewriteBudget &budget, const FactsQuery &facts, Domain domain)
const FactsQuery & no_facts() noexcept
SymbolicNodePtr normalize_node(const SymbolicNodePtr &node, RewriteBudget &budget, const FactsQuery &facts, Domain domain)
const std::string ComputationContext const SolveOptions & options

引用了 classify_residual(), LMCAS::context, LMCAS::detail::RewriteBudget::context(), LMCAS::detail::expand_node(), LMCAS::Result< ResidualCheck >::failure(), is_decided(), LMCAS::detail::make_expression_ptr(), LMCAS::detail::no_facts(), LMCAS::detail::node(), LMCAS::detail::normalize_node(), LMCAS::options, LMCAS::anonymous_namespace{residual_verification.cpp}::FormalResidual::prove(), prove_normalized_residual(), prove_with_profiles() , 以及 LMCAS::Result< ResidualCheck >::success().

被这些函数引用 prove_normalized_residual().

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

◆ prove_piecewise_residual()

std::optional< ResidualCheckResult > LMCAS::anonymous_namespace{residual_verification.cpp}::prove_piecewise_residual ( const ExprPtr & residual,
detail::RewriteBudget & budget,
const EqvOptions & options )

在文件 residual_verification.cpp 第 1009 行定义.

1011 {
1012 const auto* piecewise = residual_piecewise(detail::node(residual), budget);
1013 if (!piecewise) { return std::nullopt; }
1014 auto& context = budget.context();
1015 auto entered = context.enter_recursion("residual.piecewise");
1016 if (!entered) { return ResidualCheckResult::failure(entered.error()); }
1017 ResidualRecursionScope scope(context);
1018 const auto count = piecewise->branches().size() +
1019 static_cast<std::size_t>(piecewise->default_expr() != nullptr);
1020 for (std::size_t index = 0; index < count; ++index) {
1021 ResidualBranch select(*piecewise, index, budget);
1022 auto branch = select.rewrite(detail::node(residual));
1023 budget.measure(branch);
1025 if (!proof) { return proof; }
1026 if (!std::holds_alternative<ProvedZeroResidual>(proof.value())) {
1027 return ResidualCheckResult::success(UnprovedResidual{residual});
1028 }
1029 }
1031 ProvedZeroResidual{ExactResidualProof{residual}});
1032}
std::size_t measure(const std::shared_ptr< const SymbolicNode > &node)
const PiecewiseNode * residual_piecewise(const detail::SymbolicNodePtr &node, detail::RewriteBudget &budget)
ResidualCheckResult check_zero_residual(const ExprPtr &residual, ComputationContext &context, const LMCAS::EqvOptions &options)

引用了 LMCAS::check_zero_residual(), LMCAS::context, LMCAS::detail::RewriteBudget::context(), LMCAS::Result< ResidualCheck >::failure(), LMCAS::detail::make_expression_ptr(), LMCAS::detail::RewriteBudget::measure(), LMCAS::detail::node(), LMCAS::options, prove_piecewise_residual(), residual_piecewise(), LMCAS::detail::SymbolicRewriter::rewrite() , 以及 LMCAS::Result< ResidualCheck >::success().

被这些函数引用 prove_piecewise_residual().

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

◆ prove_with_profiles()

ResidualCheckResult LMCAS::anonymous_namespace{residual_verification.cpp}::prove_with_profiles ( const ExprPtr & current,
ComputationContext & context,
const EqvOptions & options )

在文件 residual_verification.cpp 第 907 行定义.

909 {
910 ResidualProfiles required;
911 collect_residual_profiles(detail::node(current), required);
912 const auto zero = SymbolicExpr::number(0);
913 for (const auto profile : {
915 if ((profile == EqvProfile::TrigBasic && !required.trig) ||
916 (profile == EqvProfile::ExpLogBasic && !required.exp_log)) {
917 continue;
918 }
919 auto profile_options = options;
920 profile_options.profile = profile;
921 auto equivalent = detail::equivalent_impl(*current, *zero, context, profile_options);
922 if (!equivalent) {
925 continue;
926 }
928 }
929 if (equivalent.value()) {
930 return ResidualCheckResult::success(ProvedZeroResidual{
931 ExactResidualProof{current}});
932 }
933 }
934 return ResidualCheckResult::success(UnprovedResidual{current});
935}
CasError & error()
Result< bool > equivalent_impl(const SymbolicExpr &lhs, const SymbolicExpr &rhs, ComputationContext &context, const EqvOptions &options)
Result< bool > equivalent(const SymbolicExpr &lhs, const SymbolicExpr &rhs, ComputationContext &context, const EqvOptions &options)

引用了 LMCAS::CasError::code, collect_residual_profiles(), LMCAS::context, LMCAS::Core, LMCAS::equivalent(), LMCAS::detail::equivalent_impl(), LMCAS::Result< T >::error(), LMCAS::anonymous_namespace{residual_verification.cpp}::ResidualProfiles::exp_log, LMCAS::ExpLogBasic, LMCAS::Result< ResidualCheck >::failure(), LMCAS::Inconclusive, LMCAS::detail::node(), LMCAS::options, prove_with_profiles(), LMCAS::Result< ResidualCheck >::success(), LMCAS::anonymous_namespace{residual_verification.cpp}::ResidualProfiles::trig, LMCAS::TrigBasic, LMCAS::UnsupportedExpression , 以及 LMCAS::Result< T >::value().

被这些函数引用 prove_normalized_residual() , 以及 prove_with_profiles().

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

◆ replace_exact_root()

RootReplacementResult LMCAS::anonymous_namespace{residual_verification.cpp}::replace_exact_root ( const detail::SymbolicNodePtr & node,
const detail::ExactRootId *& identity,
detail::RewriteBudget & budget,
const std::string & operation )

在文件 residual_verification.cpp 第 704 行定义.

708 {
709 auto& context = budget.context();
710 auto entered = context.enter_recursion(operation);
711 if (!entered) { return RootReplacementResult::failure(entered.error()); }
712 ResidualRecursionScope scope(context);
713 if (const auto* root = dynamic_cast<const RootOfNode*>(node.get())) {
714 if (identity && identity->compare(root->exact_id()) != 0) {
715 return RootReplacementResult::success(std::nullopt);
716 }
717 identity = &root->exact_id();
718 budget.require_nodes(1);
720 SymbolicFactory::create_variable("_residual_root"));
721 }
722 if (dynamic_cast<const NumberNode*>(node.get())) {
724 }
725 const auto* sum = dynamic_cast<const AddNode*>(node.get());
726 const auto* product = dynamic_cast<const MultiplyNode*>(node.get());
727 if (sum || product) {
728 const auto& operands = sum ? sum->operands() : product->operands();
729 return replace_root_operands(node, operands, sum != nullptr, identity, budget, operation);
730 }
731 if (const auto* power = dynamic_cast<const PowerNode*>(node.get())) {
732 return replace_root_power(node, *power, identity, budget, operation);
733 }
734 return RootReplacementResult::success(std::nullopt);
735}
static std::shared_ptr< const SymbolicNode > create_variable(const std::string &name)
void require_nodes(std::size_t nodes) const
RootReplacementResult replace_root_power(const detail::SymbolicNodePtr &node, const PowerNode &power, const detail::ExactRootId *&identity, detail::RewriteBudget &budget, const std::string &operation)
RootReplacementResult replace_root_operands(const detail::SymbolicNodePtr &node, const std::vector< detail::SymbolicNodePtr > &operands, bool sum, const detail::ExactRootId *&identity, detail::RewriteBudget &budget, const std::string &operation)
int compare(const ExactRootId &other) const

引用了 LMCAS::detail::ExactRootId::compare(), LMCAS::context, LMCAS::detail::RewriteBudget::context(), LMCAS::SymbolicFactory::create_variable(), LMCAS::Result< std::optional< detail::SymbolicNodePtr > >::failure(), replace_exact_root(), replace_root_operands(), replace_root_power(), LMCAS::detail::RewriteBudget::require_nodes() , 以及 LMCAS::Result< std::optional< detail::SymbolicNodePtr > >::success().

被这些函数引用 prove_exact_root_residual(), replace_exact_root(), replace_root_operands() , 以及 replace_root_power().

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

◆ replace_root_operands()

RootReplacementResult LMCAS::anonymous_namespace{residual_verification.cpp}::replace_root_operands ( const detail::SymbolicNodePtr & node,
const std::vector< detail::SymbolicNodePtr > & operands,
bool sum,
const detail::ExactRootId *& identity,
detail::RewriteBudget & budget,
const std::string & operation )

在文件 residual_verification.cpp 第 665 行定义.

667 {
668 bool changed = false;
669 std::vector<detail::SymbolicNodePtr> replaced;
670 std::size_t nodes = 1;
671 for (auto operand = operands.begin(); operand != operands.end(); ++operand) {
672 auto child = replace_exact_root(*operand, identity, budget, operation);
673 if (!child || !child.value()) { return child; }
674 nodes = budget.append_size(nodes, budget.measure(*child.value()));
675 if (!changed && *child.value() != *operand) {
676 replaced.reserve(operands.size());
677 replaced.insert(replaced.end(), operands.begin(), operand);
678 changed = true;
679 }
680 if (changed) { replaced.push_back(std::move(*child.value())); }
681 }
682 if (!changed) { return RootReplacementResult::success(node); }
684 ? SymbolicFactory::create_add(std::move(replaced), &budget)
685 : SymbolicFactory::create_multiply(std::move(replaced), &budget));
686}
static std::shared_ptr< const SymbolicNode > create_add(std::vector< std::shared_ptr< const SymbolicNode > > ops, detail::RewriteBudget *budget=nullptr)
创建加法节点,自动扁平化嵌套加法并消除零项.
static std::shared_ptr< const SymbolicNode > create_multiply(std::vector< std::shared_ptr< const SymbolicNode > > ops, detail::RewriteBudget *budget=nullptr)
创建乘法节点,自动扁平化嵌套乘法并消除单位元.
std::size_t append_size(std::size_t current, std::size_t child)

引用了 LMCAS::detail::RewriteBudget::append_size(), LMCAS::SymbolicFactory::create_add(), LMCAS::SymbolicFactory::create_multiply(), LMCAS::detail::RewriteBudget::measure(), replace_exact_root(), replace_root_operands() , 以及 LMCAS::Result< std::optional< detail::SymbolicNodePtr > >::success().

被这些函数引用 replace_exact_root() , 以及 replace_root_operands().

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

◆ replace_root_power()

RootReplacementResult LMCAS::anonymous_namespace{residual_verification.cpp}::replace_root_power ( const detail::SymbolicNodePtr & node,
const PowerNode & power,
const detail::ExactRootId *& identity,
detail::RewriteBudget & budget,
const std::string & operation )

在文件 residual_verification.cpp 第 688 行定义.

690 {
691 auto base = replace_exact_root(power.base(), identity, budget, operation);
692 if (!base || !base.value()) { return base; }
693 auto exponent = replace_exact_root(power.exponent(), identity, budget, operation);
694 if (!exponent || !exponent.value()) { return exponent; }
695 if (*base.value() == power.base() && *exponent.value() == power.exponent()) {
697 }
699 budget.measure(*exponent.value()));
701 SymbolicFactory::create_power(*base.value(), *exponent.value()));
702}
const std::shared_ptr< const SymbolicNode > & exponent() const noexcept
const std::shared_ptr< const SymbolicNode > & base() const noexcept
static std::shared_ptr< const SymbolicNode > create_power(std::shared_ptr< const SymbolicNode > base, std::shared_ptr< const SymbolicNode > exponent)
创建幂运算节点,自动处理指数为 0/1 及底数为 0/1 的情况.
const ExprPtr & exponent

引用了 LMCAS::detail::RewriteBudget::append_size(), LMCAS::PowerNode::base(), LMCAS::SymbolicFactory::create_power(), LMCAS::exponent, LMCAS::PowerNode::exponent(), LMCAS::detail::RewriteBudget::measure(), replace_exact_root(), replace_root_power() , 以及 LMCAS::Result< std::optional< detail::SymbolicNodePtr > >::success().

被这些函数引用 replace_exact_root() , 以及 replace_root_power().

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

◆ residual_piecewise()

const PiecewiseNode * LMCAS::anonymous_namespace{residual_verification.cpp}::residual_piecewise ( const detail::SymbolicNodePtr & node,
detail::RewriteBudget & budget )

在文件 residual_verification.cpp 第 964 行定义.

965 {
966 detail::RewriteScope scope(&budget);
967 if (const auto* piecewise = dynamic_cast<const PiecewiseNode*>(node.get())) {
968 return piecewise;
969 }
970 const auto* add = dynamic_cast<const AddNode*>(node.get());
971 const auto* mul = dynamic_cast<const MultiplyNode*>(node.get());
972 if (add || mul) {
973 for (const auto& child : add ? add->operands() : mul->operands()) {
974 if (auto piecewise = residual_piecewise(child, budget)) { return piecewise; }
975 }
976 }
977 if (const auto* power = dynamic_cast<const PowerNode*>(node.get())) {
978 return residual_piecewise(power->base(), budget);
979 }
980 return nullptr;
981}
加法节点,表示多个操作数的求和。
乘法节点,表示多个操作数的乘积。
分段函数节点,表示条件分支表达式.
ExprResult mul(const ExprPtr &lhs, const ExprPtr &rhs, ComputationContext &context)

引用了 LMCAS::add(), LMCAS::mul() , 以及 residual_piecewise().

被这些函数引用 prove_piecewise_residual() , 以及 residual_piecewise().

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