理论来源与开源库选型
研究总览 · 2026-09-20
选用和排除的成熟算法、离线抽象与可选 OpenModelica 分析后端；采用不等于已接入。
3. 采用哪些理论，以及哪些已经是先例
Section titled “3. 采用哪些理论，以及哪些已经是先例”| 理论/研究 | 本方案采用的机制 | 不从该研究推出什么 |
|---|---|---|
| InverseCSG，2018 | 几何程序视为可搜索语法，结构选择与几何处理分工 | 不证明所有制造设计都可自动合成 |
| Differentiable 3D CAD Programs，2021 | 固定结构中的约束反向编辑与参数优化 | 论文明确不面向跨几何拓扑变化的优化 |
| SKETCH/CEGIS，2006 | 提案—验证—有语义反例—收紧搜索 | 任意内核错误不自动成为逻辑反例 |
| Logic-based Benders | 离散主问题与连续子问题之间传递有推理依据的 cut | 局部求解失败不能形成全局有效 cut |
| DPLL(T) | 借鉴冲突解释必须被理论蕴含的原则 | 不因此另建 SMT 内核或引入第二个规划循环 |
| Inference Duality / Sensitivity，1999 | 在前提保持时复用参数化推理证据 | 对偶缓存本身不是 Aira 的新发明 |
| Verified LP，Jansson 2004 | 数值解提出候选，严格算术与变量界核验结论 | 浮点残差很小不等于精确恒等式 |
| 几何约束分解 | 按约束子系统分解并控制共享变量 | 所有修改都能局部求解 |
| Nominal Adapton | 名称、依赖与从头重算一致性的要求 | 不需要把其 OCaml 运行时引入 Aira |
| Lineage-based CAD Referencing，2023 | 以来源和可查询关系保持设计引用 | 面分裂/合并时自动存在唯一后继 |
| Szalinski，2020 | 从程序结构中恢复更紧凑、可编辑的表示 | 浮点 B-Rep 布尔表达式任意重排都等价 |
| DreamCoder，2021 | 抽象库与搜索策略共同改善的研究框架 | 整套 Python/OCaml/学习运行时必须部署 |
| Stitch，2023 | 基于程序语料的自顶向下抽象搜索与压缩 | 论文压缩性能自动转化成 CAD 任务成功率 |
| babble，2023 | 认识到等式理论可提高抽象鲁棒性 | 未建立 CAD 等价理论时就应做无限制等式饱和 |
这些论文支持构件和组合方式，不构成新系统成功的证明。本研究的突破目标必须落在可以执行、可证正确性条件和可做消融的具体算法上，见 §10。
3.1 开源库的明确选用与排除
Section titled “3.1 开源库的明确选用与排除”“无冗余”落实为每种生产职责只有一个后端，同类候选不全部装入浏览器。包管理缓存中附带某个插件，不等于应该发布或加载它；相同数学问题可以被多个库表达，也不等于这些库在完整诊断、增量更新和几何语义上相互可替代。
| 库及本研究核对身份 | 裁决 | 实际职责、性能依据及代价 |
|---|---|---|
| OCCT V8_0_1，提交 b8f597c… | 保留并维护现有二开 | B-Rep、解析/样条面、拓扑、STEP、历史；当前构件已绑定大部分所需构面设施。几何内核选择与数值求解器选择不能混为一谈 |
| PlaneGCS 1.2.0-aira.1 | 保留唯一草图后端 | 草图约束、DOF、冗余诊断；不以通用 NLP 替换已接线语义。历史 ezpz 对照不支持“所有任务更快”的结论，也不支持再加载第二个草图库 |
| CasADi 3.8.0 + IPOPT 3.14.19 | 保留非线性路径 | 符号 AD 与通用稀疏 NLP；固定图复用、参数与乘子热启动以现有 API 为限。LP 不经该路径 |
| highs@1.15.3（highs-js）/ HiGHS 1.15.1 | 选为唯一生产线性/整数/凸 QP 底座 | 已有数值稀疏模型、持久修改、basis、ray；LP-only 不加载 CasADi。核对发布构件，而不只看 README 的简易文本 solve 示例 |
| CasADi 附带 HiGHS 1.13.1 插件 | 不纳入产品发布 | 研究已证明可用与增量优势；独立部署已有成熟 API，故不为它自研额外绑定，不维护两份 HiGHS |
| Manifold 3.5.1 | 保留声明为网格的职责 | MeshSolid 布尔与 level-set 网格提取；不代替 B-Rep、STEP 或曲面连续性。已有 Field3D 路径优先复用 |
| ml-matrix 6.15.0 | 保留现有局部线性代数 | Jacobian SVD、数值秩与零空间诊断；不是第二套设计优化器，不据局部秩宣布全局唯一 |
| num-rational 0.4.2 + num-bigint 0.4.8 | 复用锁定 Rust 数值设施 | 小型严格证书检查；与浮点求解职责不同。限制位长和预算，不自行实现大整数。显式浮点转换通过已有传递依赖 num-traits 0.2.19 的 ToPrimitive 调用，现声明为直接依赖 |
| Stitch，锁定提交见 §8 | 仅离线研究/开发工具 | 抽象候选生成；不引入浏览器运行时，不以论文压缩速度冒充 Aira 求解提升 |
| OSQP | 不新增生产 QP 后端 | 凸 QP 的分裂算法、缓存分解和参数更新很有价值；本方案已有 HiGHS 同类接受域，尚无 Aira 工作负载证据支持增加第二个 QP 库 |
| qpOASES | 不发布额外插件 | 在线主动集适合相关参数化 QP；不解决一般 MILP/非线性几何。并未证明它慢，只是没有足以抵偿重复职责的实际收益证据 |
| Fatrop；核对 CasADi 3.8.0 接口 | 不新增生产 NLP 后端 | 锁定接口已支持通用 dense NLP，以及利用 OCP 结构的模式；不能说它“只会控制问题”。当前关系图需通用稀疏 NLP，没有证据支持替换现有 IPOPT 或并置另一个后端 |
| Z3 npm 5.2.0 | 不引入 | 精确整数/有理数、逻辑、unsat core 是新增能力；本方案接受域无需第二套 SMT 语义。代价是明确不承诺一般整数不可行证明 |
| cvc5 1.4.0 | 不引入 | SMT、SyGuS 与证明系统扩展了问题范围，但不是当前必要组成。官方已有 WASM，不能用“不支持浏览器”作为排除理由 |
| SCIP 10.1.0 | 不引入 | MIQP/MINLP 与全局搜索能力真实；本研究选择有限结构加局部 NLP，并接受超域 unknown，不声称 HiGHS/IPOPT 完整替代 SCIP |
| egg / babble / DreamCoder 完整栈 | 不引入产品运行时 | 等式饱和或学习框架不能自动提供 CAD 等价律；可展开抽象由 Stitch 与同一编译器承担，避免并置多个学习/执行系统 |
库能力的直接依据：highs-js 持久绑定、OSQP 官方算法与更新能力、qpOASES 原实现、锁定 Fatrop 接口、Z3 官方 JS 说明、cvc5 官方发布、SCIP 官方发布。
算法性能专长应按作者证据理解：OSQP 论文研究凸 QP 的 ADMM 与分解缓存；qpOASES 论文研究参数化 QP 的在线主动集，非凸扩展不等于保证全局最优；Fatrop 论文利用阶段结构与专门线性代数。Fatrop 当前上游又有 dense/graph 路线和浏览器 WASM 演示，因此排除理由不能简写为“只能 OCP”或“没有 WASM”。这里不因功能范围扩大就重复加载所有后端。
当前发布只允许按需加载真正使用的构件。OSQP/Fatrop 的许可证或名称出现在 CasADi 分发包中，不证明当前浏览器存在相应插件、更不证明产品调用过它们。替换裁决生效时同批移除重复入口；本研究不执行依赖增删。
许可身份亦须按实际组件区分：HiGHS/highs-js、Manifold、Stitch 为 MIT；CasADi 为 LGPL-3.0-or-later；IPOPT 为 EPL-2.0；OCCT 为 LGPL-2.1 加其附加例外。PlaneGCS 以维护源码 LICENSE 和具体文件头为准，不能仅凭历史包 metadata 判定。现有 IPOPT 组合还包含 MUMPS 的 CeCILL-C 和 METIS 4.0.3 的自定义条款；同一构建上游保存了作者的商业使用澄清，不能把它误记成现代 METIS 的 Apache-2.0。该记录是选型事实，不将整个链接组合简写成“全部 MIT”。
3.2 最高性能的判据
Section titled “3.2 最高性能的判据”先固定接受域、输出正确性、诊断与资源释放，再比较冷首次任务和热编辑完整 P95，并报告包体、峰值内存及失败/unknown。没有任务分布和这些约束时，不能从库名推出统一冠军。本研究为每个职责选定一个生产后端；未实测竞争项不会被伪装成已经落败的跑分。
端到端成本包括模型编译、加载、数值求解、几何构造、实际检查和提交。决定性能的关键有：消元与稀疏性、保留模型及 basis、先做必要条件排除、经证明的局部失效、减少无效几何调用。证书匹配或抽象展开若比直接求解更贵，应由同一控制器预算停止；不能让“学习”无条件占用交互路径。
8. 程序抽象学习的最终选择
Section titled “8. 程序抽象学习的最终选择”8.1 成熟程序压缩算法采用 Stitch
Section titled “8.1 成熟程序压缩算法采用 Stitch”采用 Stitch 作为本地离线压缩候选生成器，锁定研究提交 350804b7b35807c78bd21c313785ae5152ae2985（2026-09-08）；Cargo 包名 stitch_core，manifest 版本 0.1.0，MIT，不能仅凭版本号认为各提交同一实现。
Stitch 直接从程序语料寻找抽象，Rust 实现避免引入 DreamCoder 的完整多语言学习运行时。论文在其压缩语料上报告相对 DreamCoder 压缩算法显著更低的时间和内存；这只支持候选生成器的选择，不是 Aira 的性能测量。论文 本选择限于成熟程序压缩算法，不意味着 Stitch 已解决关系语义归纳、适用域推导或 AI 能力演化；这些是 §16 的自主研究职责，不能受其现有输入形式限制。
Stitch 当前源码有线程、随机、CLI 等设施，不宣称现成浏览器发行物。部署裁决是离线开发/研究工具，不是浏览器内核依赖。 原生产品只消费审核过的、可展开的 AMIR 抽象定义；普通建模不需要安装 Stitch。所有训练语料留在本地，默认不调用模型服务。
不同时采用 egg/babble。它们擅长给定等价理论上的搜索，但 Aira 当前优先需要可按展开核验的压缩，缺少将任意浮点几何/历史重写为等价程序的依据。该排除针对当前契约，不是对库质量的判断。
8.2 抽象如何进入同一语言
Section titled “8.2 抽象如何进入同一语言”输入语料限于已经通过真实验收、具有稳定类型的程序。去除具体用户身份，保留单位、参数角色、纯数值表达式及构造依赖。Stitch 提出候选；Aira 为候选恢复类型、前提、效果与预算信息。
接受条件不是“程序变短”：
- 卫生展开后得到与原片段一致的规范化操作序列，允许的差别仅限明确的变量重命名。
- 不改变求值次数、顺序、资源所有权、操作身份和引用来源。不能将重复调用误当可共享的纯值。
- 单位、形状类型、错误和前置条件全部保持；抽象不能藏掉新的要求。
- 对新参数仍执行真实几何与要求检查。过去有限实例成功不证明宏的所有参数都有效。
库依赖必须无环，限定展开深度、展开后的操作数和内核调用预算；B/C/D 的语法规模界均按展开后的程序计算。“规范化”只允许列明的卫生变量替换和保持求值结构的变换，不暗含浮点重结合、调用合并或效果重排；变量 α 重命名不包括持久操作 ID 的任意改名。
抽象定义是有版本的语义载荷；提交的实现封存必要定义或完整展开，不能因全局库更新而改变旧 Revision 的含义。只有 expand(compressed, library) 的确定结果进入现有执行器；不增加第二个 DSL 运行时。
8.3 优化什么
Section titled “8.3 优化什么”压缩目标至少惩罚库体积与调用复杂度；是否提升设计能力由独立留出任务上的搜索成本和预算成功率判定。重复参数化板件容易压缩并不等于可设计新的产品族。拒绝只在训练语料上减少 AST 节点就宣称“智能进化”。
22.10 行为分析的具体实现选择：本地 OpenModelica
Section titled “22.10 行为分析的具体实现选择：本地 OpenModelica”新增选型的真实需求是：用户列出的工业系统不仅有静态几何，还需要实际部件连接、连续状态、离散事件与指定工况；源码核查又证实当前若干动态/热流类不能直接承担这些职责。因此选择 OpenModelica 1.27.1＋Modelica Standard Library 4.1.0，作为本机可选、独立安装的方程与状态事件分析后端。它不替换 OCCT 几何或 HiGHS/CasADi 设计求解，也不成为普通 CAD 操作的启动依赖。
官方 Windows 下载页与 1.27.1 发布说明确认正式版本；MSL 4.1.0提供模型库身份。本选择基于功能适用性、可执行工具链和职责收敛，不是未经测量的“全球最快”宣称。本轮未安装或运行该工具，性能、具体生成模型的数值结果和接线尚无本机实测。
集成路线确定为原生 CLI，不引入 OMPython、FMI host 或 OMSimulator。 官方 1.27 命令行文档支持 omc Script.mos；buildModel将模型转为 C 并构建仿真程序。Aira 在现有本地 Node 主机内用非 shell 子进程调用，临时模型/结果通过文件传递，Windows 隐藏后台窗口；不新建 CAD 状态服务。
执行链为：持久工程图与选定工况 → 有类型的模型生成 → loadModel/loadFile/checkModel/buildModel → 仿真程序 → 轨迹/事件/诊断 → 原要求检查与源状态绑定。脚本由已检查的结构生成，不把模型数据拼成宿主命令。保留 getErrorString 及编译/运行状态；进程退出、结果文件完整、数值成功与设计要求通过分别判断。输出优先采用声明变量的 CSV，保留事件前后时刻，不为了省行数删除同一时间的跳变。官方 运行参数提供结果文件和参数覆盖等机制。
| 持久语义 | 具体模型承接 | 必须保留的边界 |
|---|---|---|
| 实例、质量、质心、完整惯性张量与坐标 | MSL MultiBody 的刚体与 frame | 在编译边界处理 mm→m、kg·mm²→kg·m²及惯量参考坐标；不能由外形自动猜材料和动力学假设 |
| 关节、初始位姿、轴及驱动 | MultiBody joints 与明确力/扭矩/运动输入 | 关节种类、自由度、限位和初始化必须有对应方程；不自动保证任意接触 |
| 热端口、热容、热阻与热源 | MSL HeatTransfer 组件及连接方程 | 集中参数热模型，不冒充三维热场网格解 |
| 管段、储容、阀与介质 | MSL Fluid/Media | 明确的一维热流网络，不是完整 CFD |
| 信号、状态与事件 | 方程、离散变量、when 及 MSL Blocks | 同时事件、初值与时间语义明确；有限资源流程需生成容量/占用及转换规则，不能只命名 process |
| 分析输出 | 状态、反力、温度、流量等显式结果 | 反向绑定原 occurrence、工况和要求；源输入变化即过期 |
这些能力范围由 MSL MultiBody与 MSL Fluid的实际定义支持。有限资源/流程语义由 Aira 根据明确规则编译，不再同时引入 SimPy 承担同一模型的另一套权威。任意数量动态对象、最优排程、全三维场及完整制造验证不由这组选型自动完成。
结构不变时可复用生成程序，仅对允许运行时覆盖、未被结构化消去的参数使用 -overrideFile；结构、连接或相关参数变化必须重新编译。缓存绑定编译器、MSL、生成器、结构模型与相关选项，结果还绑定全部数值工况。host 控制墙钟、输出大小、取消与临时资源释放。能力发现明确当前 backend 是否可用；缺后端或求值失败不得落回旧的无条件成功路径。
许可证按组件记录：编译器/环境涉及 AGPL v3 / OSMC-PL 1.8；runtime header另有 BSD New 选项；MSL 许可证为 BSD-3-Clause，不能把整个安装包写成 BSD/MIT。本方案调用用户本机独立安装的未修改工具，不把编译器链接或捆绑到 Aira；进程分离本身不构成法律豁免结论，若分发生成物仍需核对实际链接组件及相应义务。
由此，行为分析的实施有具体的编译目标、执行程序、数据往返和失败语义；其完成仍须经过真实公共链的接线验收。它支撑本次统一内核的工业语义范围，不把整个 CAE 生态扩张为首批实现清单。
语法级转换由Modelica 生成规约统一定义：显式分析绑定、组件/端口、单位与惯量坐标、初始化/事件、完整 .mo/.mos 和输出来源。上表说明库可承接的领域，不等于转换器已覆盖全部组件；只有具有生成规则的子集才能声明可执行。