Estoy usando Z3 con SMT2 a través de C API / JNA / Scala y parece funcionar bastante bien.

Quiero intentar la resolución incremental. Así que al principio traduzco esto usandoZ3_parse_smtlib2_string:

(declare-fun x () Int)
(assert (>= x 0))
(check-sat)
(get-model)

Entonces vuelvo unaZ3_ast, ponlo en un solver viaZ3_solver_assert, compruébelo con Z3_solver_check y recupere un modelo a través deZ3_solver_get_model (Si el cheque devuelto es satisfactorio, como es el caso en este ejemplo). Hasta ahora no hay problema.

Pero cuando quiero afirmar algo adicional como este:

(assert (= x 1))

Me quedo estancado en el punto dondeZ3_parse_smtlib2_string Se llama, porque se queja, que x es una constante desconocida. Si añado también añado eldeclarar-diversión al segundo fragmento recibo un error de argumento no válido. ¿No debería esta variable ya existir en el entorno? ¿Tengo que configurar los parámetros adicionales deZ3_parse_smtlib2_string? ¿Cómo puedo obtener esos de la fórmula analizada previamente?

También usando(set-option: global-decls true) No funcionó como Z3 me dice que estoel valor de la opción no se puede modificar después de la inicialización.

¿Alguien tiene una idea de cómo resolver este problema?