Как распечатать результаты решателя z3 print (s.model ()) по порядку? - PullRequest
Новая
       7

Как распечатать результаты решателя z3 print (s.model ()) по порядку?

0 голосов
/ 30 августа 2018

Предположим, у меня есть список из 10 переменных 

v = [Real('v_%s' % (i+1)) for i in range(10)]

и я хочу добавить простое ограничение, подобное этому 

s = Solver()
for i in range(10):
    s.add(v[i] == i)
if s.check() == sat:
    print(s.model())

Итак, удовлетворительная модель - v_1 = 0, v_2 = 1 .... v_10 = 9. Однако вывод print(s.model()) полностью неупорядочен, что приводит меня в замешательство, когда в большой модели у меня много переменных. Для этого примера вывод моего компьютера v_5, v_7, v_4, v_2, v_1, v_3, v_6, v_8, v_9, v_10, но я хочу вывести переменные этой модели в порядке, подобном v_1, v_2, ..., v_10. Может кто-нибудь сказать мне, есть ли у z3Py такого рода функции или нет? Спасибо!

1 Ответ

0 голосов
/ 30 августа 2018

Вы можете превратить модель в список и отсортировать ее по своему усмотрению: 

from z3 import *

v = [Real('v_%s' % (i+1)) for i in range(10)]

s = Solver()
for i in range(10):
    s.add(v[i] == i)
if s.check() == sat:
    m = s.model()
    print (sorted ([(d, m[d]) for d in m], key = lambda x: str(x[0])))

Это печатает: 

[(v_1, 0), (v_10, 9), (v_2, 1), (v_3, 2), (v_4, 3), (v_5, 4), (v_6, 5), (v_7, 6), (v_8, 7), (v_9, 8)]

Обратите внимание, что имена отсортированы лексикографически, поэтому v_10 следует после v_1 и до v_2. Если вы хотите, чтобы v_10 пришел в конце, вы можете выполнить дальнейшую обработку в соответствии с вашими потребностями.

...