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

类
struct	QuadraticSigns

函数
JordanDecompositionResult	certified_jordan (const ExprPtr &A, JordanDecomposition value, ComputationContext &context)
JordanDecompositionResult	diagonalization_checked (const ExprPtr &A, ComputationContext &context)
bool	is_defective_upper_pair (const std::vector< std::vector< Rational > > &matrix)
bool	jordan_dimensions_match (const MatrixNode &a, const MatrixNode &p, const MatrixNode &j)
std::optional< int >	quadratic_eigenvalue_sign (const ExprPtr &eigenvalue, const detail::AssumptionFacts &facts, ComputationContext &context)
std::optional< int >	symbolic_quadratic_sign (const ExprPtr &value, const detail::AssumptionFacts &facts, ComputationContext &context)
Result< void >	verify_jordan_decomposition (const ExprPtr &A, const JordanDecomposition &value, ComputationContext &context)
Result< void >	verify_jordan_identity (const ExprPtr &A, const JordanDecomposition &value, const MatrixNode &matrix, ComputationContext &context, const std::string &operation)

函数说明

certified_jordan()

JordanDecompositionResult LMCAS::anonymous_namespace{matrix_decomposition_eigen.cpp}::certified_jordan	(	const ExprPtr &	A,
		JordanDecomposition	value,
		ComputationContext &	context )

在文件 matrix_decomposition_eigen.cpp 第 70 行定义.

                                                            {
    auto proof = verify_jordan_decomposition(A, value, context);
    if (!proof) return JordanDecompositionResult::failure(proof.error());
    return JordanDecompositionResult::success(std::move(value));
}

引用了 certified_jordan(), LMCAS::context, LMCAS::Result< JordanDecomposition >::failure(), LMCAS::Result< JordanDecomposition >::success(), LMCAS::value , 以及 verify_jordan_decomposition().

被这些函数引用 certified_jordan() , 以及 diagonalization_checked().

函数调用图:

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

diagonalization_checked()

JordanDecompositionResult LMCAS::anonymous_namespace{matrix_decomposition_eigen.cpp}::diagonalization_checked	(	const ExprPtr &	A,
		ComputationContext &	context )

在文件 matrix_decomposition_eigen.cpp 第 77 行定义.

                                 {
    auto matrix = validate_decomposition_matrix(A, true, context, "matrix.diagonalize");
    if (!matrix) { return JordanDecompositionResult::failure(matrix.error()); }
    if (auto diagonal = exact_diagonal_entries(matrix.value(), context)) {
        return certified_jordan(A, {rectangular_diagonal_expr(matrix.value()->rows(),
            matrix.value()->cols(), *diagonal), identity_matrix_expr(matrix.value()->rows())}, context);
    }
    auto spaces = detail::matrix_eigenspaces_checked(A, context);
    if (!spaces) { return JordanDecompositionResult::failure(spaces.error()); }
    const auto n = matrix.value()->rows();
    std::size_t count = 0;
    for (const auto& space : spaces.value()) { count += space.second.size(); }
    if (count != n) {
        return JordanDecompositionResult::failure(CasErrc::Inconclusive,
            "ordinary eigenspaces do not span the matrix", "matrix.diagonalize");
    }
    std::vector<std::vector<ExprPtr>> p(n, std::vector<ExprPtr>(n));
    std::vector<std::vector<ExprPtr>> j(n,
        std::vector<ExprPtr>(n, SymbolicExpr::number(0)));
    std::size_t column = 0;
    for (const auto& space : spaces.value()) {
        for (const auto& vector : space.second) {
            if (vector.size() != n) {
                return JordanDecompositionResult::failure(CasErrc::InternalInvariant,
                    "eigenspace vector has invalid dimensions", "matrix.diagonalize");
            }
            for (std::size_t row = 0; row < n; ++row) { p[row][column] = vector[row]; }
            j[column][column] = space.first;
            ++column;
        }
    }
    return certified_jordan(A,
        {SymbolicExpr::matrix(j), SymbolicExpr::matrix(p)}, context);
}

引用了 certified_jordan(), LMCAS::context, diagonalization_checked(), LMCAS::detail::matrix_decomposition::exact_diagonal_entries(), LMCAS::Result< JordanDecomposition >::failure(), LMCAS::detail::matrix_decomposition::identity_matrix_expr(), LMCAS::Inconclusive, LMCAS::InternalInvariant, LMCAS::detail::matrix_eigenspaces_checked(), LMCAS::detail::matrix_decomposition::rectangular_diagonal_expr() , 以及 LMCAS::detail::matrix_decomposition::validate_decomposition_matrix().

被这些函数引用 diagonalization_checked().

函数调用图:

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

is_defective_upper_pair()

bool LMCAS::anonymous_namespace{matrix_decomposition_eigen.cpp}::is_defective_upper_pair

(

const std::vector< std::vector< Rational > > &

matrix

)

在文件 matrix_decomposition_eigen.cpp 第 157 行定义.

                                                                           {
    return matrix.size() == 2 && matrix[0].size() == 2 &&
        matrix[0][0] == matrix[1][1] && matrix[1][0] == Rational(0) &&
        matrix[0][1] != Rational(0);
}

引用了 is_defective_upper_pair().

被这些函数引用 is_defective_upper_pair().

函数调用图:

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

jordan_dimensions_match()

bool LMCAS::anonymous_namespace{matrix_decomposition_eigen.cpp}::jordan_dimensions_match	(	const MatrixNode &	a,
		const MatrixNode &	p,
		const MatrixNode &	j )

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

                         {
    return a.rows() == a.cols() && p.rows() == a.rows() && p.cols() == a.cols() &&
        j.rows() == a.rows() && j.cols() == a.cols();
}

引用了 LMCAS::a, LMCAS::MatrixNode::cols(), jordan_dimensions_match() , 以及 LMCAS::MatrixNode::rows().

被这些函数引用 jordan_dimensions_match() , 以及 verify_jordan_decomposition().

函数调用图:

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

quadratic_eigenvalue_sign()

std::optional< int > LMCAS::anonymous_namespace{matrix_decomposition_eigen.cpp}::quadratic_eigenvalue_sign	(	const ExprPtr &	eigenvalue,
		const detail::AssumptionFacts &	facts,
		ComputationContext &	context )

在文件 matrix_decomposition_eigen.cpp 第 146 行定义.

                                                                     {
    detail::RewriteBudget transform_budget(context, (context).limits().max_recursion_depth,
                                            (context).limits().max_ast_nodes, "transform");
    auto value = detail::make_expression_ptr(detail::normalize_node(detail::node(eigenvalue), transform_budget));
    if (auto rational = exact_rational_expr(value, context)) {
        return *rational > Rational(0) ? 1 : (*rational < Rational(0) ? -1 : 0);
    }
    return symbolic_quadratic_sign(value, facts, context);
}

引用了 LMCAS::context, LMCAS::detail::matrix_decomposition::exact_rational_expr(), LMCAS::detail::make_expression_ptr(), LMCAS::detail::node(), LMCAS::detail::normalize_node(), quadratic_eigenvalue_sign(), LMCAS::rational(), symbolic_quadratic_sign() , 以及 LMCAS::value.

被这些函数引用 quadratic_eigenvalue_sign().

函数调用图:

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

symbolic_quadratic_sign()

std::optional< int > LMCAS::anonymous_namespace{matrix_decomposition_eigen.cpp}::symbolic_quadratic_sign	(	const ExprPtr &	value,
		const detail::AssumptionFacts &	facts,
		ComputationContext &	context )

在文件 matrix_decomposition_eigen.cpp 第 130 行定义.

                                                                     {
    auto real = detail::query_real_value(detail::node(value), facts, context);
    if (!real || real.value() != Tribool::True) { return std::nullopt; }
    auto zero = detail::classify_exact_zero(value, context, "matrix.quadratic_sign");
    if (!zero) { return std::nullopt; }
    if (zero.value() == detail::ZeroProof::Zero) { return 0; }
    auto positive = detail::query_positive_value(detail::node(value), facts, context);
    if (!positive) { return std::nullopt; }
    if (positive.value() == Tribool::True) { return 1; }
    auto negative_value = SymbolicExpr::multiply(SymbolicExpr::number(-1), value);
    auto negative = detail::query_positive_value(detail::node(negative_value), facts, context);
    if (!negative || negative.value() != Tribool::True) { return std::nullopt; }
    return -1;
}

引用了 LMCAS::detail::classify_exact_zero(), LMCAS::context, LMCAS::detail::node(), LMCAS::detail::query_positive_value(), LMCAS::detail::query_real_value(), LMCAS::real(), symbolic_quadratic_sign(), LMCAS::True, LMCAS::Result< T >::value(), LMCAS::value , 以及 LMCAS::detail::Zero.

被这些函数引用 quadratic_eigenvalue_sign() , 以及 symbolic_quadratic_sign().

函数调用图:

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

verify_jordan_decomposition()

Result< void > LMCAS::anonymous_namespace{matrix_decomposition_eigen.cpp}::verify_jordan_decomposition	(	const ExprPtr &	A,
		const JordanDecomposition &	value,
		ComputationContext &	context )

在文件 matrix_decomposition_eigen.cpp 第 51 行定义.

                                                                   {
    const std::string operation = "jordan_form.verify";
    auto a = std::dynamic_pointer_cast<const MatrixNode>(detail::node(A));
    auto p = std::dynamic_pointer_cast<const MatrixNode>(detail::node(value.P));
    auto j = std::dynamic_pointer_cast<const MatrixNode>(detail::node(value.J));
    if (!a || !p || !j || !jordan_dimensions_match(*a, *p, *j)) {
        return Result<void>::failure(CasErrc::InternalInvariant,
            "Jordan certificate has invalid dimensions", operation);
    }
    auto rank = matrix_rank_checked(value.P, context);
    if (!rank) { return Result<void>::failure(rank.error()); }
    if (rank.value() != a->rows()) {
        return Result<void>::failure(CasErrc::InternalInvariant,
            "Jordan change of basis is singular", operation);
    }
    return verify_jordan_identity(A, value, *a, context, operation);
}

引用了 LMCAS::a, LMCAS::context, LMCAS::Result< T >::failure(), LMCAS::InternalInvariant, jordan_dimensions_match(), LMCAS::matrix_rank_checked(), LMCAS::detail::node(), LMCAS::value, verify_jordan_decomposition() , 以及 verify_jordan_identity().

被这些函数引用 certified_jordan() , 以及 verify_jordan_decomposition().

函数调用图:

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

verify_jordan_identity()

Result< void > LMCAS::anonymous_namespace{matrix_decomposition_eigen.cpp}::verify_jordan_identity	(	const ExprPtr &	A,
		const JordanDecomposition &	value,
		const MatrixNode &	matrix,
		ComputationContext &	context,
		const std::string &	operation )

在文件 matrix_decomposition_eigen.cpp 第 13 行定义.

                                                             {
    auto ap = matrix_multiply_checked(A, value.P, context);
    if (!ap) { return Result<void>::failure(ap.error()); }
    auto pj = matrix_multiply_checked(value.P, value.J, context);
    if (!pj) { return Result<void>::failure(pj.error()); }
    auto left = std::dynamic_pointer_cast<const MatrixNode>(detail::node(ap.value()));
    auto right = std::dynamic_pointer_cast<const MatrixNode>(detail::node(pj.value()));
    if (!left || !right) {
        return Result<void>::failure(CasErrc::InternalInvariant,
            "Jordan matrix product did not produce a matrix", operation);
    }
    for (std::size_t row = 0; row < matrix.rows(); ++row) {
        for (std::size_t col = 0; col < matrix.cols(); ++col) {
            auto difference = SymbolicExpr::add(detail::make_expression_ptr(left->get(row, col)),
                SymbolicExpr::multiply(SymbolicExpr::number(-1),
                    detail::make_expression_ptr(right->get(row, col))));
            auto proof = detail::classify_exact_zero(difference, context, operation);
            if (!proof) { return Result<void>::failure(proof.error()); }
            if (proof.value() != detail::ZeroProof::Zero) {
                return Result<void>::failure(proof.value() == detail::ZeroProof::Unknown
                    ? CasErrc::Inconclusive : CasErrc::InternalInvariant,
                    "Jordan intertwining identity is not proved at (" +
                        std::to_string(row) + "," + std::to_string(col) +
                        "): " + difference->to_string(), operation);
            }
        }
    }
    return Result<void>::success();
}

引用了 LMCAS::detail::classify_exact_zero(), LMCAS::MatrixNode::cols(), LMCAS::context, LMCAS::Result< T >::failure(), LMCAS::Inconclusive, LMCAS::InternalInvariant, LMCAS::detail::make_expression_ptr(), LMCAS::matrix_multiply_checked(), LMCAS::detail::node(), LMCAS::right, LMCAS::MatrixNode::rows(), LMCAS::Result< T >::success(), LMCAS::detail::Unknown, LMCAS::value, verify_jordan_identity() , 以及 LMCAS::detail::Zero.

被这些函数引用 verify_jordan_decomposition() , 以及 verify_jordan_identity().

函数调用图:

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