В 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».

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