Как добавить ограничение, которое требует, чтобы целочисленная переменная принадлежала массиву?

Предположим, у меня есть z3py целочисленная переменная x = Int('x') и целочисленный массив a = [1, 2, 3] . Затем я добавляю ограничение через s.add (x in a).

Я думаю, что это приемлемо, потому что x может быть 1 or 2 or 3. Но на самом деле это неудовлетворительно. Может ли кто-нибудь сказать мне, как я могу добавить ограничение, чтобы убедиться, что x in a?

Спасибо!

Вот код Python, который я использовал. Я думал, что ответ на выходе будет s является удовлетворительным, потому что x может быть равно 1, 2 или 3, тогда ограничение x in a выполнено. Но ответ на самом деле неудовлетворительный. Возможно, это неправильный способ указать это ограничение. Итак, мой вопрос заключается в том, как указать такое ограничение, чтобы гарантировать, что переменная может быть создана только со значением в определенном массиве.

from z3 import *
x = Int('x')

a = [1, 2, 3]

s = Solver()

s.add(x in a)

print(s.check())

python z3 smt z3py
person Francis    schedule 23.06.2018    source источник
comment
Я не понимаю вопроса.   -  person timgeb    schedule 23.06.2018
comment
Это не похоже на полный пример того, что делает ваш код: чего вы на самом деле пытаетесь достичь, что, по вашему мнению, требует использования числового списка вместо использования solve с адекватно определенными ограничениями < и >?   -  person Mike 'Pomax' Kamermans    schedule 23.06.2018
comment
@timgeb теги z3 и z3py здесь очень важны. ericpony.github.io/z3py-tutorial/guide-examples.htm   -  person Mike 'Pomax' Kamermans    schedule 23.06.2018
comment
@ Mike'Pomax'Kamermans ах, спасибо, что указали на это!   -  person timgeb    schedule 23.06.2018
comment
что такое s? в s.add(x in a)   -  person Onk_r    schedule 23.06.2018
comment
Извините! позвольте мне привести пример кода здесь:   -  person Francis    schedule 23.06.2018
comment
из z3 import * x = Int ('x') a = [1, 2, 3] s = Solver () s.add (x in a) print (s.check ())   -  person Francis    schedule 23.06.2018
comment
@Francis, пожалуйста, отредактируйте пример в своем вопросе. Комментарии не поддерживают код длиннее строки или около того.   -  person timgeb    schedule 23.06.2018
comment
@Francis не добавляйте свой код в виде одного или нескольких комментариев. Отредактируйте свое сообщение и поместите туда код в соответствии со статьей правил как задать хороший вопрос. И если вы не читали это, найдите минутку, чтобы сначала прочитать ее, потому что это важная статья политики, которую следует прочитать, прежде чем размещать вопросы.   -  person Mike 'Pomax' Kamermans    schedule 23.06.2018
comment
@ Mike'Pomax'Kamermans Спасибо! На самом деле я новичок. Прости за это!   -  person Francis    schedule 23.06.2018
comment
Не беспокойтесь - но мне все еще любопытно, что вы здесь делаете. Вы просто пытаетесь использовать z3 и видите, на что он способен, или вы работаете над чем-то, что требует разрешения x на 1, 2 и 3? Потому что, если это первое, то действительно важно не делать этого, просто решайте с ограничением, которое x>0 и x<4 вместо использования списка предопределенных чисел.   -  person Mike 'Pomax' Kamermans    schedule 23.06.2018
comment
@ Mike'Pomax'Kamermans Я работаю над чем-то, что требует этой функции. Если массив равен [1, 4, 7], то я не знаю других методов для определения такого ограничения.   -  person Francis    schedule 23.06.2018
comment
В соответствии со статьей о политике: это отличная информация, которую можно также разместить в своем сообщении, если вам понадобится задать вопросы в будущем: убедитесь, что если кажется, что вы делаете что-то, что имеет очевидное более простое решение, объясните, почему вы можете '' Я использую это решение =)   -  person Mike 'Pomax' Kamermans    schedule 23.06.2018

Ответы (3)


arrow_upward
4
arrow_downward

Это должно делать:

from z3 import *

a = [1,2,3]

s = Solver()
x = Int('x')
s.add(Or([x == i for i in a]))

# Enumerate all possible solutions:
while True:
    r = s.check()
    if r == sat:
        m = s.model()
        print m
        s.add(x != m[x])
    else:
        print r
        break

Когда я запускаю это, я получаю:

[x = 1]
[x = 2]
[x = 3]
unsat
person alias    schedule 23.06.2018

arrow_upward
0
arrow_downward

«x in a» - это выражение Python, которое оценивается как False перед тем, как вы утверждаете ограничение, поскольку переменная x не принадлежит массиву.

person Marco    schedule 23.06.2018

arrow_upward
0
arrow_downward

Один из способов - построить ограничение z3.And или z3.Or с помощью цикла

# Finds all numbers in the domain, for which it's square is also in the domain

import z3
exclude = [1,2]
domain  = list(range(128))
number  = z3.Int('number')
squared = number * number
solver  = z3.Solver()
solver.add(z3.Or([  number  == value for value in domain  ]))
solver.add(z3.Or([  squared == value for value in domain  ]))
solver.add(z3.And([ number  != value for value in exclude ]))
solver.add(z3.And([ squared != value for value in exclude ]))
solver.push()  # create stack savepoint

output = []
while solver.check() == z3.sat:
  value = solver.model()[number].as_long()
  solver.add( number != value )
  output.append(value)

solver.pop()  # reset stack to last solver.push()

print(output)
# [10, 0, 4, 6, 5, 11, 9, 8, 3, 7]

print(sorted(output))
# [0, 3, 4, 5, 6, 7, 8, 9, 10, 11]
person James McGuigan    schedule 19.09.2020