Cómo hacer que z3 devuelva múltiples núcleos unsat, múltiples tareas satisfactorias
Estoy trabajando en un componente de una herramienta de investigación; Estoy interesado en recuperar (para QF_LRA)
-múltiples (mínimos o no) núcleos UNSAT y
-múltiples tareas SAT
He revisado el foro para discusiones anteriores sobre este tema, por ejemplo,Cómo obtener diferentes núcleos unsat cuando se usa z3 en la lógica QF_LRA
Se refieren a los tutoriales de Python z3, por ejemplo,http://rise4fun.com/Z3Py/tutorial/musmss
que parece estar fuera de línea por ahora. He intentado otras sugerencias de github, etc. para encontrar el tutorial mencionado, pero no he tenido suerte.
Estoy usando la API z3 de Java; pero feliz de cambiar a alternativas.