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

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) then b else b1)时,约束x == c被添加到当时分支的约束系统,并且约束又被添加到else分支的约束系统(公式)中.x != c

所以,新的配方,然后分支为:x == c /\ formula(式正部分是的结合等式);

else分支的新公式是:( 公式的x != c \/ formula负部分是不等式的分离的结合).

编辑:约束系统的可满足性.

为了使约束系统可满足,必须能够为系统中的变量赋值,以满足约束.

该约束系统因此当且仅当满足存在substituition 西塔,使得对于每个方程v = c 西塔v将语法上等同于西塔c,并且同样地,对于每个disequation w != d 西塔w将从语法不同西塔d.

不幸的是,我对限制编程很新,我遇到了问题.

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

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

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

拜托,有人能帮帮我吗？一些方向,提示......

¹⁾目前,source=8 / target=8计划被接受.

Answer 1

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

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

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

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