рассказывая о разнице между слабыми переменными и исходными переменными в Z3

Я пытаюсь создать новый вид нарезки, чтобы заменить нарезки gomory, реализованные в Z3. Я разработал свой разрез для работы с исходным ограничением, введенным пользователем. К сожалению, я обнаружил, что предварительная обработка Z3 ограничений добавляет резервные переменные и изменяет структуру ограничений. Я могу адаптировать свой алгоритм для работы со структурой ограничений Z3 и резервными переменными, но важная часть алгоритма требует знания того, какие переменные являются резервными, а какие исходными. Я не смог найти в исходном коде Z3 ничего, что помогло бы мне это сделать. Я также пытался найти решение в Интернете, но ничего не нашел.

Кто-нибудь знает, как это можно сделать?

Спасибо


z3
person omerkatz    schedule 09.04.2013    source источник
comment
Добавляете ли вы свои сокращения перед вызовом Z3? Или вы модифицируете класс theory_arith? Вы просмотрели файл src/smt/theory_arith_int.h?   -  person Leonardo de Moura    schedule 09.04.2013
comment
Я пытаюсь изменить класс thoery_arith. Я уже изучил файл 'src/smt/theory_srith_int.h' и код в нем, который генерирует гомори-срезы, но не нашел в этом файле ответа на свою проблему   -  person omerkatz    schedule 09.04.2013

Ответы (1)


arrow_upward
3
arrow_downward

В методе mk_gomory_cut(row const & r) в файле src/smt/theory_arith_int.h, r находится строка таблицы Simplex. Более того, базовая переменная x_i является целочисленной, но ей присвоено нецелочисленное значение.

Итератор it используется для обхода записей строк. Каждая запись представляет собой пару a_ij и x_j, где a_ij — число, а x_j — (теоретическая) переменная.

Theory_arith — это плагин для решателя, определенный в файле src/smt/smt_context.h. Этот решатель сочетает в себе множество теоретических плагинов, таких как theory_arith. Он поддерживает отображение выражений в переменные теории. Это сопоставление хранится в объекте с именем enode.

Метод get_enode(v) извлекает enode, связанный с теоретической переменной v. Более того, get_enode(v)->get_owner() возвращает выражение, связанное с теоретической переменной v.

Теперь предположим, что мы хотим проверить, является ли теоретическая переменная v резервом или нет. Во-первых, мы можем получить связанное выражение, используя:

   app * t = to_app(get_enode(v)->get_owner())

Я использовал to_app, потому что теоретические плагины обрабатывают только базовые термины (т. е. они не содержат свободных переменных). Переменная v является резервом, если t представляет собой составной арифметический термин, такой как (+ a b) или (* a b c). То есть, slack — это, по сути, «имя» составного арифметического термина. Мы можем проверить это, используя:

  t->get_family_id() == get_id()

Если это выражение оценивается как true, то t является составным арифметическим термином и, следовательно, v является временным резервом.

Примечание: get_id() — это метод theory_arith. На самом деле, этот метод есть в каждом плагине для теории.

person Leonardo de Moura    schedule 09.04.2013