는 예, Z3 팀은 같은 일을 할 수있는 다양한 방법을 제공하고 있습니다. 주된 차이점은 Z3_mk_forall_const이 정상 메커니즘을 사용하여 정의 된 상수 목록을 취하는 반면 Z3_mk_forall은 Z3_mk_bound을 사용하여 만든 바운드 변수 목록을 필요로한다는 것입니다.
사용하기 쉬운 메커니즘은 특정 응용 프로그램에 따라 다릅니다. 특히, 한정자를 만들려는 기호의 수가 작고 고정 된 숫자가있을 때 Z3_mk_forall_const은 더 자연 스럽습니다. 반대로, Z3_mk_forall은 한정 기호의 기호 수가 다를 수있는 상황에서 더 자연 스러울 수 있습니다.이 경우 인덱스로 처리 할 바운드 변수의 배열을 생성하는 것은 매우 자연스러운 일입니다.
다른 장점과 단점이 있습니다. 예를 들어 다음 질문을 참조하십시오. "How to declare constants to use as bound variables in Z3_mk_forall_const?" 질문에서 Asker는 글로벌 컨텍스트에 많은 변수를 도입하는 것을 피하고자합니다. 이는 Z3_mk_forall_const을 사용해야합니다. 응답자 (Christoph)는 대신 Z3_mk_forall을 사용하는 것을 제안하지만 중첩 된 한정 기호의 경우 각 한정 기호가 다르게 인덱싱되므로 결과가 이상적이지 않습니다. Christoph는 또한 대답에서 내부적으로 Z3_mk_forall_const에 기반한 접근 방식이 Z3_mk_forall에 해당하는 것으로 번역되었으므로 실제적인 차이는 없습니다. 그러나 API 차이점은 프로그래머에게 큰 차이를 줄 수 있습니다.
C++ API에서 프로그래머에게 제공되는 메커니즘이 훨씬 더 간단합니다.
:
// 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();
}
나는 또한 도움이 질문을 발견 : 여기에 사용하는 예는 세 가지 방법이 있습니다
Z3 소스에 제공된 예제 및 의견도 도움이되었습니다. 특히 examples/c/test_capi.c, examples/c++/example.cpp 및 src/api/z3_api.h에 도움이되었습니다.