LMCAS
Lamina Computer Algebra System
载入中...
搜索中...
未找到
equivalence_options.cpp
浏览该文件的文档.
2
3#include <utility>
4
5namespace LMCAS {
6namespace equivalence_detail {
7
9 if (options.budget.max_rewrite_steps == 0 ||
10 options.budget.max_rewrite_depth == 0 ||
11 options.budget.max_node_growth_factor == 0) {
14 "equivalence rewrite budget exhausted before normalization",
16 }
17 return Result<void>::success();
18}
19
20bool exact_integer_node(const std::shared_ptr<const SymbolicNode>& node,
21 int expected) {
22 auto number = std::dynamic_pointer_cast<const NumberNode>(node);
23 if (!number) return false;
24 if (std::holds_alternative<BigInt>(number->value())) {
25 return std::get<BigInt>(number->value()) == BigInt(expected);
26 }
27 return std::get<Rational>(number->value()) == Rational(expected);
28}
29
30}
31namespace {
32
39
40}
41
43 if (name == "Core") {
45 }
46 if (name == "Trig-Basic") {
48 }
49 if (name == "ExpLog-Basic") {
51 }
52 return eqv_profile_failure("unsupported equivalence profile: " + name);
53}
54
56 const std::string& name) {
57 auto profile = eqv_profile_from_name(name);
58 if (!profile) {
59 return Result<void>::failure(profile.error());
60 }
61 options.profile = profile.value();
62 return Result<void>::success();
63}
64
66 std::size_t steps,
67 std::size_t depth,
68 std::size_t growth) {
69 EqvOptions candidate = options;
70 candidate.budget.max_rewrite_steps = steps;
71 candidate.budget.max_rewrite_depth = depth;
73 auto valid = equivalence_detail::validate_eqv_options(candidate);
74 if (!valid) {
75 return valid;
76 }
77 options = candidate;
78 return Result<void>::success();
79}
80
81}
static Result failure(CasErrc code, std::string message, std::string operation={})
static Result success(T value)
Result< EqvProfile > eqv_profile_failure(std::string message)
Result< void > validate_eqv_options(const EqvOptions &options)
bool exact_integer_node(const std::shared_ptr< const SymbolicNode > &node, int expected)
std::size_t max_rewrite_depth
同时活动的重写及嵌套 visitor 层数,根为第 1 层。
constexpr const char * kEquivalentProfileOperation
const std::string ComputationContext const SolveOptions & options
std::size_t std::size_t std::size_t growth
std::size_t std::size_t depth
std::size_t max_rewrite_steps
一次证明及 profile 切换共享的重写遍历、候选追加与阶段步数。 形状查询和缓存清空的实际工作计入 ResourceLimits::max_steps。
Result< void > set_eqv_profile(EqvOptions &options, const std::string &name)
std::size_t max_node_growth_factor
候选树及未封装孩子列表的规模上限取 context.max_ast_nodes 与原始两输入节点总数乘此因子的较小值。 每次子树引用分别计数;整个证明及 profile 切换共用原始基数。 乘法饱和为 ...
Result< void > set_eqv_budget(EqvOptions &options, std::size_t steps, std::size_t depth, std::size_t growth)
Result< EqvProfile > eqv_profile_from_name(const std::string &name)
__attribute__((visibility("default"))) Result< EqvProfile > eqv_profile_from_name(const std const std::string & name
constexpr const char * kEquivalentOperation