Ограничивающая универсальная количественная переменная

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

Например, предположим, что у меня есть переменная типа Real с именем time, которая используется для моделирования времени в системе. Допустим, у меня есть утверждение, в котором говорится, что значение некоторой унарной функции func1 всегда должно быть между 1 и 100. Функция принимает на вход переменную времени. Выраженное в Z3, я закодировал свойство следующим образом:

  1. ForAll(time, And(func1(time) >= 1, func1(time) <= 100))

    Обратите внимание, что мне явно нужно, чтобы переменная времени была универсально определена количественно, потому что я хочу, чтобы Z3 выдал мне unsat, если я добавлю свойство следующего типа:

  2. Exists(time, func1(time) == 101)

    Насколько я понимаю, для Z3 все константы имеют математическую (теоретическую), а не компьютерную (практическую) реализацию, т.е. их значения не связаны (к сожалению, я не могу указать ресурс, где я это читал в данный момент). Предположим, что со временем я моделирую время в своих системах, и в соответствии с системными ограничениями оно не может работать более x часов, что я могу использовать и сказать, что значение времени находится между 0 и x * 60' * 60, чтобы получить максимум время выполнения в секундах. Я знаю, что могу утверждать допустимые значения времени с помощью следующего утверждения:

  3. And(time >= 0, time <= x*60*60)

    но повлияет ли это на универсальную количественную оценку, приведенную в 1?

Следовательно, это должно привести к ситуации, когда если вводится свойство 2 и для значения времени я указываю x*60*60 + 1, его не следует сбрасывать, поскольку ForAll действует только для значений времени.


z3 z3py quantifiers forall
person predragf    schedule 19.04.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

но повлияет ли это на универсальную количественную оценку, приведенную в 1)?

Обратите внимание, что

ForAll(time, And(func1(time) >= 1, func1(time) <= 100))

рассматривает переменную «время» как связанную. Формула имеет тот же смысл, что и:

ForAll(xx, And(func1(xx) >= 1, func1(xx) <= 100))

Когда вы утверждаете вышеизложенное, это означает, что любое воплощение xx выполняется (утверждается). В частности, вы можете создать экземпляр количественной переменной со свободной переменной «время» и, в частности, вы можете создать экземпляр с помощью x*60*60+1, создав утверждение:

 And(func1(x*60*60+1) >= 1, func1(x*60*60+1) <= 100)

Предположим, вы хотели сказать, что

 And(func1(xx) >= 1, func1(xx) <= 100))

выполняется для каждого значения xx между 0 и x*60*60, тогда вы можете написать:

ForAll(xx, Implies(And(xx >= 0, xx <= x*60*60), And(func1(xx) >= 1, func1(xx) <= 100)))

(к сожалению, я не могу указать ресурс, где я это прочитал в данный момент).

Учебники по разумной логике или основы книг по информатике должны объяснять это подробно. Z3 поддерживает стандартную многосортную логику первого порядка (с базовыми теориями).

person Nikolaj Bjorner    schedule 19.04.2016