Я работаю над преобразователем исходного кода для 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 добавляется к системе ограничений , затем ветви, а ограничение x != c, в свою очередь, добавляется к система ограничений (формула) ветви else.
Итак, новая формула ветви then: x == c /\ formula (положительная часть формулы - это соединение равенств);
новая формула ветви else: x != c \/ formula (отрицательная часть формулы - это соединение дизъюнкций неравенств).
Изменить: соответствие системе ограничений.
Чтобы система ограничений была выполнимой, должна быть возможность присвоить значения переменным в системе так, чтобы ограничения удовлетворялись.
Таким образом, система ограничений удовлетворяется, если существует такая замена Theta, что для каждого уравнения v = c Theta v будет синтаксически идентичным Тета c и аналогично для каждого нарушения w != d Тета w будет синтаксически отличаться от Тета d.
К сожалению, я новичок в программировании с ограничениями и столкнулся с проблемами.
Мне не совсем понятно, как в этом случае сопоставить константы AST с целыми числами. Должен ли я просто использовать индекс массива констант или какую-нибудь хеш-функцию?
Непонятно, как обрабатывать тип long. Переписать решатель на основе int, сделав его длинным или использовать решатель с плавающей запятой?
Также неясно, как обрабатывать комбинированные данные целых и с плавающей запятой. Насколько я понимаю, простое решение заключается в использовании решателя с плавающей запятой как для целочисленных, так и для плавающих ограничений. Это правда? Или я могу решить часть ограничений с плавающей запятой и целочисленной отдельно?
Пожалуйста, кто-нибудь может мне помочь? Некоторые направления, подсказки ...
1) В настоящее время принята схема source=8 / target=8.
