Как использовать Z3 C ++ API для доказательства теории, основанной на входном параметре?

Question

Как использовать Z3 C ++ API для доказательства теории, основанной на входном параметре?

Я пытаюсь использовать Z3 C ++ API для достижения следующих целей:

(set-option :produce-proofs true)

(declare-const Weight Int)
(declare-const WeightLimit Int)
(declare-const P1 Bool)

(assert (= WeightLimit 10))

(assert (= P1 (>= Weight WeightLimit)))
(assert (= P1 true))

;Facts - Input
(assert (= Weight 100))

(check-sat)

И я попал в следующую функцию:

void test() {
try {
context ctx;
Z3_string str = "(declare-const Weight Int) (declare-const WeightLimit Int) (declare-const P1 Bool) (assert (= WeightLimit 10)) (assert (= P1 (>= Weight WeightLimit))) (assert (= P1 true)) (assert (= Weight 100)) (check-sat)"; //Generated by some other function
expr fs(ctx, Z3_parse_smtlib2_string(Z3_context(ctx), str, 0, 0, 0, 0, 0, 0));

solver s(ctx);
s.add(fs);

switch (s.check()) {
case unsat:   std::cout << "not satisfied\n"; break;
case sat:     std::cout << "satisfied\n"; break;
case unknown: std::cout << "unknown\n"; break;
}

model m = s.get_model();
std::cout << m << "\n";

}
catch (z3::exception e) {
std::cout << e.msg() << std::endl;
}
}

Есть ли способ передать значение Weight в качестве входного параметра в функцию, вместо того, чтобы жестко его кодировать?

Кроме того, как я могу установить опцию, используя Z3 C ++ API? И как это повлияет, если я не установлю опцию?

2

c++smt z3

Решение

Другие решения

Других решений пока нет …

Источник

Accepted Answer

Что ж, это должно быть обработано функцией, которая генерирует эту строку в качестве вывода, ту, которую вы прокомментировали как «// генерируется какой-то другой функцией»

Вы бы просто передать Weight в качестве параметра этой функции, которая должна использовать правильное значение при генерации строки.

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

Другой альтернативой будет не передать строку, но лучше использовать API для фактического утверждения фактов по одному; но из вашего описания кажется, что это, вероятно, не выбор для вас.

0