如何使用混合数据类型执行约束求解？

Question

我正在为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），那么b else b1）时，约束x==c被添加到then分支的约束系统中，约束x！=c，依次添加到else分支的约束系统（公式）中。

因此，该分支的新公式是：x==c/\公式（公式的正部分是等式的结合）；

else分支的新公式是：x！=c\/formula（公式的负部分是分离的析取的连词）。

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

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

因此，当存在取代基θ时，约束系统得到满足，对于每个等式v=cθv在语法上与θc相同，同样地，对于每个不等式w！=dThetaw在语法上与Thetad不同。

不幸的是，我对约束编程非常陌生，遇到了一些问题。

>

目前尚不清楚如何处理长型。重写基于int的解算器，使其基于long还是使用浮点解算器？

目前还不清楚如何处理组合整数和浮点数据。正如我意识到的，简单的解决方案是对整数和浮点约束使用浮点解算器。这是真的吗？或者我可以分别解决浮点和整数部分的约束？

拜托，有人能帮我吗？一些指示，提示。。。

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




Answer 1

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

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

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

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