В метода mk_gomory_cut(row const & r) във файл src/smt/theory_arith_int.h, r е ред от симплексната таблица. Освен това базовата променлива x_i е цяло число, но е присвоена на нецелочислена стойност.
Итераторът it се използва за обхождане на записите в реда. Всеки запис е по същество двойка a_ij и x_j, където a_ij е число, а x_j е (теоретична) променлива.
Theory_arith е плъгин за решаващия инструмент, дефиниран във файла src/smt/smt_context.h. Този софтуер за решаване комбинира много теоретични плъгини като theory_arith. Той поддържа картографиране от изрази към теоретични променливи. Това съпоставяне се съхранява в обект, наречен enode.
Методът get_enode(v) извлича енода, свързан с теоретичната променлива 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). Това означава, че слабината е по същество „име“ за съставен аритметичен термин. Можем да тестваме това с помощта на:
t->get_family_id() == get_id()
Ако този израз се изчисли на true, тогава t е съставен аритметичен член и следователно v е пропуск.
Забележка: get_id() е метод на theory_arith. Всъщност всеки теоретичен плъгин има този метод.
person
Leonardo de Moura
schedule
09.04.2013
src/smt/theory_arith_int.h? - person Leonardo de Moura schedule 09.04.2013