Пустые ядра Unsat при использовании тактики в z3 - PullRequest
Новая
       86

Пустые ядра Unsat при использовании тактики в z3

0 голосов
/ 20 января 2020

Solver возвращает пустое ядро ​​unsat при использовании тактики.

Случай 1: 

s = Solver()
x = Real('x')
B = Bool('b')
C = Bool('c')
s.add(B == (x > 1))
s.add(C == (x == -1))
s.check(B, C)

Случай 2: 

s = Then('simplify', 'solve-eqs', 'smt').solver()
x = Real('x')
B = Bool('b')
C = Bool('c')
s.add(B == (x > 1))
s.add(C == (x == -1))
s.check(B, C)

В обоих случаях проверка возвращает unsat (как и должно быть), но я получаю пустое ядро ​​unsat во втором случае, где я использую тактику. Есть ли способ получить недосказанное ядро ​​при использовании решателей с тактикой?

PS: Это действительно простые примеры для демонстрации. Я работаю над более серьезной проблемой, когда у меня есть ряд ограничений LRA (где тактика может быть полезна), и мне нужно извлечь ядра без ответа.

1 Ответ

0 голосов
/ 21 января 2020

Вам нужно явно включить ненасыщенные ядра, если вы используете тактику. Следующие работы: 

from z3 import *
s = Then('simplify', 'solve-eqs', 'smt').solver()
s.set(unsat_core=True)
x = Real('x')
B = Bool('b')
C = Bool('c')
s.add(B == (x > 1))
s.add(C == (x == -1))
s.check(B, C)

print s.unsat_core()

Обратите внимание на вызов s.set в третьей строке. Выход: 

$ python b.py
[b, c]
...