z3py, дать случайное решение с использованием семян - PullRequest
Новая
       9

z3py, дать случайное решение с использованием семян

1 голос
/ 03 февраля 2020 
from z3 import *

a = Int('a')

s = Solver()
s.add(a > 0)
set_option('smt.arith.random_initial_value', True)
set_option('auto_config', False)
set_option('smt.phase_selection', 5)
set_option('smt.random_seed', 1)

while s.check() == sat:
    m = s.model()
    print m[a]
    s.add(a != m[a])

Результат 

1
2
3
4
5
...

Как я могу сделать случайную работу? Пожалуйста, приведите пример в Python с использованием z3py ... Я уже знаю, как сделать это в smt ... Но мне очень трудно понять, как перевести скрипт smt в python.

1 Ответ

2 голосов
/ 03 февраля 2020

Кажется, что это дубликат Z3py, случайная генерация другого решения

Вы пытаетесь задать другой вопрос? Пожалуйста, измените вопрос, если да, если нет, вы можете удалить его.

...