저는 z3 C++ API를 사용하고 있습니다. 이 단순한 거짓 표현을 만들면 :알기 쉬운 결과로 알 수없는 결과가 발생합니다.
z3::expr x = C->int_const("x");
z3::expr p = z3::forall(x, x==0);
그리고 시도하려고하면 알 수없는 결과가 나옵니다. 저는 전략과 전술의 전문가는 아니지만 올바른 전략을 사용하면 z3이이를 해결할 수 있다고 확신합니다.
은 또한, 물론, 같은 runknown의 esult을 가진z3::expr p = !z3::forall(x, x==0);
을 시도했다.
내가 Z3에 익숙하지 않은 해요,하지만 일반적인 C++ 관점에서,하지 x==0 먼저 평가 것, 는는 전화가 implies(x, 1)에 해당되지 않을 것 즉?
Z3_ast consequent = Z3_mk_eq(ctx, x, 0);
Z3_ast theorem = Z3_mk_implies(ctx, x, consequent);
을하지만 위의 두 정확하지 : 빠른 검색에서 당신이 예를 들어, Z3 개체로 문의 각 부분을 구성 할 수 있습니다 보인다. x 및 0 매개 변수 자체는 내재 된 값 또는 참조와 반대되는 의미있는 문장을 캡슐화하는 Z3_ast의 인스턴스 여야합니다.
사실이 아니며 유효합니다. z3 구조. 내가 forall로 존재를 대체한다면, 그것은 예상대로 사실로 해결됩니다. 심하게 표현을했기 때문에 혼란스러워 할 수 있습니다. 나는 그것을 지금 새롭게했다. –
흠, 내가 틀렸을 가능성이 큽니다. 하지만 z3가 C++의'=='연산자를 오버로드 한 다음 그것을 평가하는 대신 x == 0' 문을 생성한다고 말하고 있습니까? –
정확히 C++ api가 그렇게합니다.) 거의 모든 것을 오버라이드합니다. –
관련 질문보기 : http://stackoverflow.com/questions/14988298/what-are-the-limits-of-reasoning-in-quantified-arithmetic-in-smt –