11

我正在研究Java 6 *1)的源到源转换器。

我需要维护负面信息和正面信息，所以我必须为变压器实施小约束系统。约束系统是一种受限的CNF 公式，可以定义如下：

(v1 == c1 /\ v2 == c2 ... vn == cn) /\ ((w1,1 != d1,1 \/ w1,2 !== d1,2 ... w1,k != d1,k) /\ (w2,1 != d2,1 \/ ...) /\ ... (wm,1 != dm,1 \/ ... \/ wm,k != dm,k))

哪里vi == ci是等式约束（替换，变量赋值），

wj != dj,l是不等式约束，

vi, wj,l是变量，

ci, dj,l是常数（文字）。

常量类型是映射到整数的 Java 原始类型和引用类型。常量也是任意的类似 AST 的结构（代表部分评估的表达式，可能包含（元）变量）。

约束系统的工作原理如下：

当转换器达到条件（例如if(x == c) then b else b1）时，约束x == c被添加到then分支的约束系统中，而约束又被添加到else分支的约束系统（公式）中。x != c

因此，then分支的新公式为：（公式的x == c /\ formula正部分为等式的合取）；

else分支的新公式是：（公式的x != c \/ formula负部分是不等式析取的合取）。

编辑：约束系统的可满足性。

为了使约束系统可满足，必须可以为系统中的变量分配值以使约束得到满足。

因此，如果存在替代Theta则满足约束系统，使得对于每个方程Theta在句法上与Theta相同，同样，对于每个不等式Theta在句法上与Theta不同。 v = c vcw != d wd

不幸的是，我对约束编程很陌生，遇到了问题。

  1. 在这种情况下，我并不完全清楚如何将 AST 常量映射到整数。我应该简单地使用常量数组的索引还是一些哈希函数？

  2. 目前尚不清楚如何处理长类型。重写基于 int 的求解器使其基于 long 或使用浮点求解器？

  3. 也不清楚如何处理组合的整数和浮点数据。我意识到直接的解决方案是使用浮点求解器来处理整数和浮点约束。这是真的吗？或者我可以分别解决约束的浮点和整数部分？

请问，有人可以帮我吗？一些方向，提示...

1)目前，source=8 / target=8方案已被接受。

4

1 回答 1

3

如果您也发布您的最终目标（已解决的约束实际上意味着什么），那就太好了。

但是，在我看来，您想知道给定语句中每个变量的一组可能值。在这种情况下，您将需要一个区间约束求解器

整数和有理区间之间的区别取决于您的用例和您选择的求解器，但通常可以将整数作为浮点数处理（这可能会导致约束的非整数解）。

重要的是要记住，您将无法证明任意 AST 片段的相等性。因此，您要么需要减少所述片段的表达能力（例如，给定顺序的变量上的多项式）或近似相等（例如，引用相同（即相同的上下文、相同的语法、无副作用）的 AST 片段。但是，它最好将 AST 片段转换为未绑定（或悲观绑定）的间隔。

于 2015-08-17T11:31:38.803 回答