Ja, das Z3-Team mehr Möglichkeiten zur Verfügung gestellt, das Gleiche zu tun. Der Hauptunterschied besteht darin, dass Z3_mk_forall_const eine Liste der Konstanten verwendet, die mit den normalen Mechanismen definiert wurden, während Z3_mk_forall eine Liste der gebundenen Variablen erfordert, die mit Z3_mk_bound erstellt wurden.
Welcher Mechanismus einfacher zu verwenden ist, hängt von Ihrer spezifischen Anwendung ab. Insbesondere scheint es mir, dass Z3_mk_forall_const natürlicher wird, wenn es eine kleine, feste Anzahl von Symbolen gibt, über die Sie einen Quantifizierer erstellen möchten. Umgekehrt wird Z3_mk_forall wahrscheinlich natürlicher in der Situation sein, in der die Anzahl der Symbole im Quantifier variieren kann. In diesem Fall ist es ganz natürlich, ein Array von gebundenen Variablen zu generieren, die Sie mit Indizes adressieren.
Es gibt auch andere Vor- und Nachteile. Siehe zum Beispiel diese Frage: "How to declare constants to use as bound variables in Z3_mk_forall_const?" In dieser Frage möchte der Fragesteller vermeiden, eine Menge von Variablen in ihren globalen Kontext einzuführen, der notwendig sein wird, um Z3_mk_forall_const zu verwenden. Der Beantworter (Christoph) schlägt stattdessen die Verwendung von Z3_mk_forall vor, aber auch dies ist nicht ideal, da dies bei geschachtelten Quantifizierern dazu führt, dass jeder Quantifizierer anders indiziert wird. Christoph enthüllt auch in dieser Antwort, dass intern der auf Z3_mk_forall_const basierende Ansatz in etwas übersetzt wird, das zu Z3_mk_forall äquivalent ist, so dass unter der Haube wirklich kein Unterschied besteht. Die API-Unterschiede können jedoch für den Programmierer einen großen Unterschied machen.
Es gibt auch einen (viel einfacheren) Mechanismus, der dem Programmierer in der C++ API zur Verfügung gestellt wird, wenn Sie diesen benutzen können. Hier sind einige Beispiele mit den drei verschiedenen Methoden:
// g++ --std=c++11 z3-quantifier-support.cpp -I../src/api/ -I../src/api/c++/ libz3.so
#include <stdio.h>
#include "z3.h"
#include <iostream>
#include "z3++.h"
using namespace z3;
/**
* This is by far the most concise and easiest to use if the C++ API is available to you.
*/
void example_cpp_forall() {
context c;
expr a = c.int_const("a");
expr b = c.int_const("b");
expr x = c.int_const("x");
expr axiom = forall(x, implies(x <= a, x < b));
std::cout << "Result obtained using the C++ API with forall:\n" << axiom << "\n\n";
}
/**
* Example using Z3_mk_forall_const. Not as clean as the C++ example, but this was still
* significantly easier for me to get working than the example using Z3_mk_forall().
*/
void example_c_Z3_mk_forall_const() {
// Get the context
Z3_config cfg;
Z3_context ctx;
cfg = Z3_mk_config();
ctx = Z3_mk_context(cfg);
// Declare integers a, b, and x
Z3_sort I = Z3_mk_int_sort(ctx);
Z3_symbol a_S = Z3_mk_string_symbol(ctx, "a");
Z3_symbol b_S = Z3_mk_string_symbol(ctx, "b");
Z3_symbol x_S = Z3_mk_string_symbol(ctx, "x");
Z3_ast a_A = Z3_mk_const(ctx, a_S, I);
Z3_ast b_A = Z3_mk_const(ctx, b_S, I);
Z3_ast x_A = Z3_mk_const(ctx, x_S, I);
// Build the AST (x <= a) --> (x < b)
Z3_ast x_le_a = Z3_mk_le(ctx, x_A, a_A);
Z3_ast x_lt_b = Z3_mk_lt(ctx, x_A, b_A);
Z3_ast f = Z3_mk_implies(ctx, x_le_a, x_lt_b);
Z3_app vars[] = {(Z3_app) x_A};
Z3_ast axiom = Z3_mk_forall_const(ctx, 0, 1, vars, 0, 0, f);
printf("Result obtained using the C API with Z3_mk_forall_const:\n");
printf("%s\n\n", Z3_ast_to_string(ctx, axiom));
}
/**
* Example using Z3_mk_forall. For the example, this is the most cumbersome.
*/
void example_c_Z3_mk_forall() {
// Get the context
Z3_config cfg;
Z3_context ctx;
cfg = Z3_mk_config();
ctx = Z3_mk_context(cfg);
// Declare integers a and b
Z3_sort I = Z3_mk_int_sort(ctx);
Z3_symbol a_S = Z3_mk_string_symbol(ctx, "a");
Z3_symbol b_S = Z3_mk_string_symbol(ctx, "b");
Z3_ast a_A = Z3_mk_const(ctx, a_S, I);
Z3_ast b_A = Z3_mk_const(ctx, b_S, I);
// Declare bound variables, in this case, just x
Z3_symbol x_S = Z3_mk_string_symbol(ctx, "x");
Z3_ast x_A = Z3_mk_bound(ctx, 0, I);
// Z3_mk_forall requires all names, types, and bound variables to be provided in
// arrays. In this example, where there is only one quantified variable, this seems a
// bit cumbersome. If we were dealing with an varying number of quantified variables,
// then this would seem more reasonable.
const unsigned sz = 1;
const Z3_sort types[] = {I};
const Z3_symbol names[] = {x_S};
const Z3_ast xs[] = {x_A};
// Build the AST (x <= a) --> (x < b)
Z3_ast x_le_a = Z3_mk_le(ctx, x_A, a_A);
Z3_ast x_lt_b = Z3_mk_lt(ctx, x_A, b_A);
Z3_ast f = Z3_mk_implies(ctx, x_le_a, x_lt_b);
// In the Z3 docs for Z3_mk_pattern, the following sentence appears: "If a pattern is
// not provided for a quantifier, then Z3 will automatically compute a set of
// patterns for it." So I tried supplying '0' for the number of patterns, and 'NULL'
// for the list of patterns, and Z3_mk_forall still seems to function.
Z3_ast axiom = Z3_mk_forall(ctx, 0, 0, NULL, sz, types, names, f);
printf("Result obtained using the C API with Z3_mk_forall:\n");
printf("%s\n", Z3_ast_to_string(ctx, axiom));
}
int main() {
example_cpp_forall();
example_c_Z3_mk_forall_const();
example_c_Z3_mk_forall();
}
Ich fand auch diese Fragen hilfreich:
Die Beispiele und Kommentare in der Z3-Quelle waren ebenfalls hilfreich, insbesondere in examples/c/test_capi.c, examples/c++/example.cpp und src/api/z3_api.h.