私は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)に達すると、制約がthen分岐の制約システムx == cに追加され、次に制約がelse分岐の制約システム(式) に追加されます。x != c
したがって、then分岐の新しい式は次のとおりです。x == c /\ formula(式の正の部分は等号の結合です);
else分岐の新しい式は次のとおりですx != c \/ formula(式の負の部分は、不等式の選言の結合です)。
編集：制約システムの充足可能性。
制約システムが充足可能であるためには、制約が満たされるように、システム内の変数に値を割り当てることが可能でなければなりません。
したがって、各方程式に対してThetaがThetaと構文的に同一になり、同様に、各不等式に対してThetaがThetaと構文的に異なるような代入Thetaが存在する場合、制約システムは満たされます。 v = c vcw != d wd
残念ながら、私は制約プログラミングにかなり慣れていないため、問題に遭遇しました。
この場合、AST定数を整数にマップする方法は完全には明らかではありません。定数の配列のインデックスまたはハッシュ関数を使用する必要がありますか?
ロングタイプの扱いが不明。int ベースのソルバーを書き換えて long ベースにするか、浮動小数点ソルバーを使用しますか?
また、整数データと浮動小数点データの組み合わせを処理する方法も明確ではありません。簡単な解決策は、整数制約と浮動小数点制約の両方に浮動小数点ソルバーを使用することです。本当ですか？または、制約の浮動小数点部分と整数部分を別々に解決できますか?
誰か助けてくれませんか？いくつかの方向性、ヒント...
1)現在、source=8 / target=8スキームは受け入れられています。