Подсчет количества переменных в количественной формуле Z3

Я пытаюсь собрать все переменные в формулу (количественная формула в Z3py). Небольшой пример

w, x, y, z = Bools('w x y z')
fml = And( ForAll(x, ForAll(y, And(x, y))), ForAll(z, ForAll(w, And(z, w))) ) 

varSet = traverse( fml )

Код, который я использую для прохождения,

def traverse(e):
  r = set()
  def collect(e):
    if is_quantifier(e):
      # Lets assume there is only one type of quantifier
      if e.is_forall():
          collect(e.body())
    else:
      if ( is_and(e) ):
          n = e.num_args()
          for i in range(n):
              collect( e.arg(i) )
      if ( is_or(e) ):
          n = e.num_args()
          for i in range(n):
              collect( e.arg(i) )
      if ( is_not(e) ):
          collect( e.arg(0) )
      if ( is_var(e) ):
          r.add( e )
  collect(e)
  return r

И я получаю: set([Var(0), Var(1)]). Насколько я понимаю, это связано с тем, что Z3 использует индекс Де Брюйна. Можно ли этого избежать и получить нужный набор: set( [Var(0), Var(1), Var(2), Var(3)] ).


z3 z3py quantifiers
person Pushpa    schedule 22.12.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Ваш код правильный; в этом примере нет Var(2) или Var(3). Есть два квантора верхнего уровня, и индексы де Брейна в каждом из них равны 0 и 1. Эти два квантора не появляются в теле другого квантора, поэтому путаницы быть не может.

person Christoph Wintersteiger    schedule 22.12.2017
comment
Спасибо. Трудность в том, что я пытаюсь преобразовать формулу QBF в формулу без квантификаторов, и, следовательно, если Var(2) Var(3) заменить на 0 и 1, версия без квантификатора потеряет информацию. Например, в случае приведенной выше формулы версия без qbf: And(And(Var(0), Var(1)), And(Var(0), Var(1))). - person Pushpa; 22.12.2017
comment
Извините, так работают индексы де Брейна. Если формулы изменены, индексы должны быть скорректированы (и Z3 делает это во многих местах). Подумайте о подформулах, в которых используются одни и те же имена переменных, их тоже нужно было бы переименовать. - person Christoph Wintersteiger; 22.12.2017
comment
Спасибо, я понял, я спрашивал, есть ли выход? И ваш комментарий предполагает, что нет. - person Pushpa; 22.12.2017
comment
Есть, вам просто нужно переименовать/перенумеровать все переменные. В QBF префикс квантификатора объявляется заранее, глобально для всей формулы, но в Z3 квантификаторы объявляются локально для подвыражений. Когда вы создаете глобальный квантификатор, содержащий квантифицированные выражения, Z3 при необходимости перенумерует их. - person Christoph Wintersteiger; 22.12.2017