Comment afficher la contrainte insat spécifique, pas le noyau entier (Z3, Python)

Question

Comment puis-je lister uniquement les résultats de contraintes spécifiques de mon noyau unsat? J'ai beaucoup de conditions et l'impression de tout le noyau n'imprime pas tout. J'ai lu que cela peut être fait avec les commandes assert_and_track et unsat_core. J'ai trouvé quelques exemples mais ils ne fonctionnent pas. Une expérience avec ça?

s.assert_and_track(A > B, 'p1') 
s.assert_and_track(B > C, 'p2') 
if s.check() == sat: 
    print('ok') 
else: 
    c = s.unsat_core 
    print(c) <- this print all core 

Alors, comment imprimer seulement p1 ou p2 (juste vrai/faux résultat)? par exemple. p2 = false, ou il peut être affiché tel qu'il est affiché en mode impression (c) - mais seulement pour p1.

Answer 1

La meilleure façon d'y parvenir est d'enregistrer simplement une carte d'étiquettes à des contraintes, pour ce exemples que nous pouvons faire

M = {} 
M['p1'] = (A > B) 
M['p2'] = (B > C) 
M['p3'] = (C > A) 

afin que plus tard, nous pouvons imprimer le cœur en fonction de ces contraintes, par exemple comme suit

core = s.unsat_core() 
for e in core: 
    print(M[str(e)]) 

Bien sûr, cela fonctionnera également si vous ne voulez imprimer que certaines entrées au lieu de toutes.