核心概念
本文提出了一種基於 MaxSMT 的新型 GUI 佈局模型 SMT-Layout,該模型可以僅用一個規範來適應各種屏幕尺寸,並支援與真實世界 GUI 佈局的實時交互。
本文介紹了一種基於 MaxSMT 的新型 GUI 佈局模型 SMT-Layout,旨在解決現有佈局模型在適應不同屏幕尺寸和實現實時交互方面的局限性。
現有佈局模型的局限性
傳統佈局模型(如網格和群組)和基於線性約束的佈局模型需要針對不同的屏幕尺寸維護多個規範,耗時且容易導致維護困難。
ORCLayout 雖然可以僅用一個規範適應多種屏幕尺寸,但它無法處理真實世界的佈局設計,並且不支援實時響應。
SMT-Layout 的優勢
僅需一個規範即可適應各種屏幕尺寸。
支援與真實世界 GUI 佈局的實時交互。
為了支援佈局的實時交互,即使在計算資源有限的終端設備上,SMT-Layout 將工作流程分為兩個階段:開發端和終端。
開發端
建模模組: 為設計人員提供建模應用程序接口 (API) 和預設佈局容器,以指定佈局並將規範轉換為 MaxSMT 公式。
預處理模組: 利用開發端豐富的計算資源,提出了兩種新穎的預處理方法:基於區間的軟約束硬化和獨立小部件提取,以簡化公式並提前提取有用信息,從而提高求解效率。
預覽模組: 評估佈局是否符合預期,並將潛在問題通知設計人員。
終端
求解模組: 將簡化的公式和提取的信息部署到終端。根據當前屏幕尺寸,利用 SMT 求解器的推理和增量求解能力,採用兩級求解策略來求解約束。
顯示模組: 將解決方案轉換為佈局以進行顯示。