저는 Z3을 처음 사용합니다.Z3에서 변수 bool에 값 지정 C api
나는 bool 유형 변수 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);
제 질문은 어떻게 다른 값을 할당 할 수 있습니까? Z3_L_TRUE를 직접 할당 할 수없는 것 같습니다.
제안 사항? 감사!
나의 첫 번째 제안은 C API 대신 C++ API를 사용하는 것입니다. C API를 사용하면 오류가 발생하기 쉽습니다. 분포는 C와 C++ API를 모두 사용하는 예제와 함께 제공 :
https://github.com/Z3Prover/z3/blob/master/examples/c/test_capi.c
및
https://github.com/Z3Prover/z3/blob/master/examples/c++/example.cpp
당신이하고있는 것처럼 당신은, 논리적 변수를 만드는 예제가 볼 수
, 논리 변수를 제한하는 어설 션을 추가하는 것입니다. 텍스트 기반 API를 사용하여 논리적 모델링을 이해하는 것이 더 쉽습니다. 즉, SMT-LIB 형식을 사용하여 사용자가 의도 한 것을 모델링하는 것이 좋습니다 ( ). 그러면 프로그래밍 방식 API로 수행 할 작업을 추정 할 수 있습니다.질문에 대한 : 논리적 모델링에는 "할당"이라는 개념이 없습니다. 평등을 확실히 주장 할 수 있습니다. 또한 Z3_L_TRUE는 satisfiability를 확인할 때 을 사용하는 반환 코드입니다. Z3_mk_true 메소드를 사용하여 논리 상수 "true"를 만들 수 있습니다.