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