Wert zuweisen Ich bin neu in Z3.Bool Variable in Z3 C api
Ich definiere eine Bool-Typ-Variable a:
Z3_sort bool_type = Z3_mk_bool_sort (ctx);
Z3_ast a = Z3_mk_const (ctx, Z3_mk_string_symbol (ctx, "a"), bool_type);
Meine Frage ist, wie kann ich einen anderen Wert zuweisen, scheint, ich kann Z3_L_TRUE nicht direkt zuweisen.
Irgendwelche Vorschläge? Vielen Dank!
Mein erster Vorschlag ist die Verwendung der C++ - API anstelle der C-API. Die Verwendung der C-API ist ziemlich fehleranfällig. Die Verteilung wird mit Beispielen für die Verwendung sowohl die C und die C++ API:
https://github.com/Z3Prover/z3/blob/master/examples/c/test_capi.c
und
https://github.com/Z3Prover/z3/blob/master/examples/c++/example.cpp
Sie werden es sehen Beispiele von logischen Variablen erstellen, wie Sie tun, und Hinzufügen von Assertionen, die logische Variablen beschränken. Es ist einfacher, logische Modellierung mit der textbasierten API zu verstehen. Das heißt, ich schlage vor, Sie verwenden das SMT-LIB-Format, um zu modellieren, was Sie vorhaben, , und dies gibt Ihnen eine Möglichkeit zu extrapolieren, was mit den programmatischen APIs zu tun ist.
In Bezug auf Ihre Frage: Es gibt keine Vorstellung von "Zuweisung" in der logischen Modellierung. Sie können die Gleichheit sicher behaupten. Außerdem ist Z3_L_TRUE ein Returncode, der bei der Erfüllbarkeitsprüfung verwendet wird. Sie können eine logische Konstante "true" mit der Methode Z3_mk_true erstellen.