The weakly relational domain of Octagons offers a decent compromise between precision and efficiency for numerical properties. Here, we are concerned with the construction of non-numerical relational domains. We provide a general construction of weakly relational domains, which we exemplify with an extension of constant propagation by disjunctions. Since for the resulting domain of 2-disjunctive formulas, satisfiability is NP-complete, we provide a general construction for a further, more abstract weakly relational domain where the abstract operations of restriction and least upper bound can be efficiently implemented. In the second step, we consider a relational domain that tracks conjunctions of inequalities between variables, and between variables and constants for arbitrary partial orders of values. Examples are sub(multi)sets, as well as prefix, substring or scattered substring orderings on strings. When the partial order is a lattice, we provide precise polynomial algorithms for satisfiability, restriction, and the best abstraction of disjunction. Complementary to the constructions for lattices, we find that, in general, satisfiability of conjunctions is NP-complete. We therefore again provide polynomial abstract versions of restriction, conjunction, and join. By using our generic constructions, these domains are extended to weakly relational domains that additionally track disjunctions. For all our domains, we indicate how abstract transformers for assignments and guards can be constructed.

翻译：八边形域作为弱关系域，在数值属性的精度与效率之间提供了良好折衷。本文关注非数值关系域的构建。我们给出了弱关系域的一般构造方法，并以析取常量传播的扩展为例加以说明。由于所得2析取公式域的可满足性问题是NP完全的，我们进一步给出了一种更抽象的弱关系域的一般构造，其中约束和上确界抽象操作可高效实现。第二步，我们考虑一种追踪变量间不等式合取（以及变量与任意值偏序中常量间的不等式）的关系域。示例包括子（多）集、字符串上的前缀序、子串序及散落子串序。当该偏序为格时，我们为可满足性、约束以及析取的最佳抽象提供了精确的多项式时间算法。与格的构造互补，我们发现一般情况下合取的可满足性是NP完全的。因此我们再次提供了约束、合取与并的多项式抽象版本。通过使用我们的通用构造，这些域被扩展为额外追踪析取的弱关系域。针对所有域，我们说明了如何为赋值与守卫构造抽象变换器。