как вызвать Z3 программно

Question

Привет, я новичок в Z3 SMT Solver. Я знаю, что вы можете вызывать Z3 программно, используя соответствующие API. Но я хочу сделать следующее с Z3 SMT solver:

1. как программно кормить Z3 одним входным файлом?
2. как я могу постепенно получить решение (я)?

Например:

while ((check-sat) returns sat)
  get the assignments for all boolean vairables

Наконец, как я могу попросить Z3 сохранить результаты в одном выходном файле после решения формулы?

Какие-нибудь идеи или документы, на которые я могу посмотреть?

Спасибо, миллион !!!

Answer 1

Дистрибутив Z3 содержит несколько примеров (программный API).

• examples / c / test_capi.c: множество небольших примеров с использованием интерфейса C.
• examples / dotnet / test_managed.cs: ​​похожие примеры в C #
• examples / maxsat / maxsat.c: процедуры MaxSAT (в C) поверх API Z3.
• examples / ocaml / test_mlapi.ml: примеры вML
• examples / теория / test_user_theory.c: пример, показывающий, как реализовать внешнюю теорию (плагин).