Z3 Максимизировать в C++

Question

В Z3, очевидно, будет оценено следующее: максимум с 2, с моделью x = true и y = true.

(declare-const x Bool) 
(declare-const y Bool) 
(declare-const z Bool) 
(assert(= z false)) 
(maximize(
    + 
    (ite (= x true) 1 0) 
    (ite (= y true) 1 0) 
    (ite (= z true) 1 0) 
) 
) 
(check-sat) 
(get-model) 

Как я мог реализовать это с использованием API C/C++? Я пытался просто разбор с помощью этого:

Z3_ast parsed = Z3_parse_smtlib2_string(c,<The above Z3>,0,0,0,0,0,0); 
z3::expr simpleExample(c, parsed); 
s.add(simpleExample); 

Но он печатает «unsupported \n ;maximize».

Я бы не хотел конструировать выражение вручную - вместо использования сконструированного файла. Я просто не знал, какие функции или операторы expr использовать для «maximize».

ADDENDUM: В свете недавних ответов и обсуждений кажется ясным, что то, что я запрашиваю, не является нормальной функциональностью на данный момент. Итак, я изменяю вопрос, чтобы задать конкретные детали способа сделать эту работу так, как сейчас.

Answer 1

Спасибо за указание этот вопрос. Функции оптимизации не являются частью SMT-LIB2. Это пользовательские расширения. Кроме того, функция, которая анализирует тесты SMT-LIB2, не имеет никакого значения , чтобы отразить оптимизационные прагмы. Причина, по которой анализатор API не распознает , состоит в том, что эти функции оптимизации не регистрируются этим парсером (они зарегистрированы в синтаксическом анализаторе командной строки). Конечно, они не зарегистрированы в анализаторе в ветке «нестабильной», и они также не зарегистрированы в синтаксическом анализаторе в ветке «opt», который содержит расширения оптимизации. У меня было почти искушение «исправить» это, основываясь на вашем сообщении, но теперь я не уверен , почему это было бы полезно, поскольку этот парсер не имеет возможности использовать эти расширения. Z3 имеет другие расширения, которые также не отображаются для анализатора SMT-LIB2. Итак, теперь я склонен держать анализатор открытым API, чтобы принимать только SMT-LIB2.

Обратите внимание, что Кристоф указывает, что функции оптимизации являются лишь частью ветви «opt». Приглашаем вас попробовать, но он по-прежнему довольно много болтает. API до тех пор, пока я касается «функции полной» (чтобы ответить (1)). Вы можете использовать его с Python, Java и .NET. Интеграция OCaml ожидает других изменений в API OCaml. У меня не было возможности предоставить обширную документацию для API-интерфейсов, но есть краткое руководство для расширений SMT-LIB на http://rise4fun.com/Z3/tutorial/optimization.

Answer 2

Функции оптимизации в Z3 находятся в тяжелой конструкции в ветке `opt 'и не интегрированы с нестабильными или ведущими ветвями. Вполне возможно, что еще не все функциональные возможности были добавлены в API. Смотрите также ответы николай на эти вопросы:

Encoding “at-most-k/at-least-k booleans are true” constraints in Z3

Simplex in z3 via for-all