Използвам z3py. Имам предикат над две цели числа, които трябва да бъдат оценени с помощта на персонализиран алгоритъм. Опитвах се да го внедря, без особен успех. Очевидно това, от което се нуждая, е процедурно прикачване, което вече е отхвърлено. Може ли някой да ми каже как мога да внедря това в z3py? Разбирам, че включва използването на тактики, но се страхувам, че не успях да разбера как да ги използвам. Нямам нищо против да използвам и остарелия начин, стига да работи.
Процедурно прикачване в Z3
Отговори (1)
Няма процесуална тактика за закрепване. Всички тактики са внедрени вътре в Z3; можете да композирате тактика отвън. Предишни версии на Z3 разкриха начин за регистриране на „потребителска теория“. Това беше отхвърлено, тъй като (1) източникът на Z3 вече е достъпен, така че потребителите могат да компилират директно със своите потребителски теории, (2) абстракцията на потребителската теория нямаше подходяща поддръжка за генериране на модел. Разбира се, можете да опитате предишни версии на Z3, които имат разширение за потребителска теория, но то не се поддържа.
person
Nikolaj Bjorner
schedule
13.01.2014
@nikolaj-bjorner Възможно ли е да се цитира ръководство за (1)?
- person Francesco Gramano; 02.07.2016
