Est-il possible d'utiliser solver.unsat_core sans utiliser solver.assert_and_track?

Question

Existe-t-il un moyen de faire fonctionner le code suivant et d'imprimer un cœur Unsat valide?

from z3 import * 

a = Int('a') 
b = Int('b') 

s = Solver() 
s.add(a == 1) 
s.add(a == 2) 
s.add(b == 3) 

s.check() 

# This prints [], and I would like it to print [a == 1, a == 2] 
print(s.unsat_core()) 

Je sais que je pourrais le faire à la place:

from z3 import * 

a = Int('a') 
b = Int('b') 

s = Solver() 
s.assert_and_track(a == 1, 'p1') 
s.assert_and_track(a == 2, 'p2') 
s.assert_and_track(b == 3, 'p3') 

s.check() 
# This prints [p1, p2] 
print(s.unsat_core()) 

Mais pour le vrai projet sur lequel je travaille, il serait pénible de passer et donner des noms à toutes les contraintes (en raison de leur volume, ainsi que comment ils sont générés.)

Answer 1

Non sauf si vous l'implémentez vous-même. extraction de base unsat exige l'étiquetage des contraintes, voir en haut de la page 67 de ce document: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

Cela dit, vous pouvez construire une « base de données » de vos affirmations en définissant votre propre version de add qui fait d'abord un nom et l'insère, puis effectue la recherche inversée dans une fonction my_unsat_core que vous définissez de manière similaire. Si vous deviez implémenter ceci de manière générique, les gens de Z3 pourraient être intéressés à l'incorporer dans leur API aussi. Serait un bon ajout.