Używam Z3 z SMT2 przez C API / JNA / Scala i wydaje się działać całkiem dobrze.

Chcę spróbować przyrostowego rozwiązywania problemów. Więc najpierw tłumaczę to za pomocąZ3_parse_smtlib2_string:

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

Potem wracamZ3_ast, włóż go do solwera przezZ3_solver_assert, sprawdź to za pomocą Z3_solver_check i pobierz model przezZ3_solver_get_model (jeśli czek zwrócił zadowalający, co ma miejsce w tym przykładzie). Do tej pory nie ma problemu.

Ale kiedy chcę coś jeszcze potwierdzić:

(assert (= x 1))

Utknąłem w miejscu, gdzieZ3_parse_smtlib2_string nazywa się, ponieważ narzeka, że ​​x jest nieznaną stałą. Jeśli dodam, dodaj równieżdeklarować-zabawę do drugiego fragmentu otrzymuję nieprawidłowy błąd argumentu. Czy ta zmienna nie powinna istnieć już w środowisku? Czy muszę ustawić dodatkowe parametryZ3_parse_smtlib2_string? Jak mogę uzyskać te z wcześniej przeanalizowanej formuły?

Również używa(set-option: global-decls true) nie działa, ponieważ Z3 mówi mi, że towartości opcji nie można modyfikować po inicjalizacji.

Czy ktoś ma jakiś sposób na rozwiązanie tego problemu?