Има ли начин да се използва z3 за преобразуване на формула в CNF (използвайки кодиране в стил Tseitsin)? Търся нещо като командата simplify, но гарантираща, че върнатата формула е CNF.
Преобразувайте формулата в CNF
Отговори (1)
Можете да използвате командата apply, за да го направите. Можем да предоставим произволни тактики/стратегии на тази команда. За повече информация относно тактиките и стратегиите в Z3 4.0 вижте урока http://rise4fun.com/Z3/tutorial/strategies
Командата (help-tactic) може да се използва за показване на всички налични тактики в Z3 4.0 и техните параметри. Programmatic е по-удобен за използване и гъвкав. Ето урок, базиран на новия API на Python: http://rise4fun.com/Z3Py/tutorial/strategies. Същите възможности са налични в .Net и C/C++ API.
Следният скрипт демонстрира как да конвертирате формула в CNF с помощта на тази рамка:
person
Leonardo de Moura
schedule
12.06.2012
Страхотно благодаря! Точно това търсех. Само още една забележка: Има ли начин да накарам z3 да ми каже функцията, която представлява всяка от новите променливи (k!0, k!1, ...)? Или трябва да направя обратен инженеринг на това от аксиомите на Цейтин?
- person Georg; 12.06.2012
Не, ние не предоставяме тази информация. Z3 обаче произвежда конвертор на модел за всяка стъпка на предварителна обработка. Конверторът на модел е функция, която преобразува модела за получената формула в модел за оригиналната формула. За преобразуване на CNF, конверторът на модела е прост. Той просто премахва интерпретацията на новите променливи
k!0, k!1, ... По този начин не предоставя информацията, която искате.
- person Leonardo de Moura; 13.06.2012
Добре, все пак много благодаря. Реконструирането на функцията за новите променливи от аксиомите на Цейтин така или иначе изглежда доста лесно.
- person Georg; 13.06.2012
@LeonardodeMoura Последната връзка е повредена ;(
- person RexYuan; 13.11.2017
