0
내 코드에 제약 조건을 추가하는 동안 동일한 제약 조건을 여러 번 표현식 벡터에 추가해야한다는 것을 알았습니다. 중복 된 표현식을 제거 할 수 있도록 두 표현식이 정확히 동일한 지 여부를 감지하는 API가 있습니까?Z3 두 표현식이 같은지 확인하십시오
A
답변
0
표현식은 항상 고유 한 포인터로 내부화됩니다. 따라서 동일한 하위 표현식을 사용하여 두 개의 표현식을 작성하면 그 표현식은 동일하게됩니다. 당신은 단순히 포인터 평등을 사용할 수 있습니다.
표현식에도 "식별자"가 있습니다. 식별자를 얻기위한 C 호출은 Z3_ast_get_id라고하며 다른 프로그래밍 언어의 다른 API에는 에 해당하는 호출이 있습니다 (C++에서부터 C# 및 Java의 Z3_ast_get_id를 사용해야하지만 "Id"/ "id"라고 함).
관련 문제
- 1. 두 테이블이 같은지 확인하십시오.
- 2. 두 배열이 같은지 확인하십시오.
- 3. 개미 : 두 숫자가 같은지 확인하십시오.
- 4. 두 이진 트리가 같은지 확인하십시오.
- 5. 두 개의 쿼리가 같은지 확인하십시오.
- 6. 코코아에서 두 파일이 같은지 확인하십시오.
- 7. 두 개의 MovieClip이 같은지 확인하십시오.
- 8. 두 일반 유형이 같은지 확인하십시오.
- 9. COM 포인터가 같은지 확인하십시오.
- 10. C++에서 두 유형이 같은지 확인하십시오.
- 11. 텍스트 상자의 두 값이 같은지 확인하십시오.
- 12. 두 파이썬 정규식 패턴이 같은지 확인하십시오
- 13. 두 개의 jar 클래스가 같은지 확인하십시오.
- 14. 두 개의 2D 배열이 같은지 확인하십시오.
- 15. 두 개의 숫자 목록이 같은지 확인하십시오.
- 16. 세트의 두 숫자가 nlgn에서 x와 같은지 확인하십시오
- 17. 두 개의 워크 시트가 같은지 확인하십시오.
- 18. php - 두 배열의 값이 같은지 확인하십시오.
- 19. 두 배열의 일부가 Java에서 같은지 확인하십시오
- 20. PHP 단어가 같은지 확인하십시오.
- 21. Bool이 정수와 같은지 확인하십시오.
- 22. 문자열이 정규식과 같은지 확인하십시오.
- 23. 모든 숫자가 같은지 확인하십시오.
- 24. Z3 : 모델이 고유한지 확인하십시오.
- 25. sage math : 두 표현식이 같은지 확인하는 방법은 무엇입니까?
- 26. Javascript 난수가 마지막과 같은지 확인하십시오.
- 27. Scheme : 비교/두리스트가 같은지 확인하십시오.
- 28. 일부 십진수 값이 같은지 확인하십시오.
- 29. 배열의 값이 서로 같은지 확인하십시오.
- 30. javascript var이 문자열과 같은지 확인하십시오.
또 하나의 질문으로, ** Z3_get_ast_id **의 반환 유형은 부호가 없으므로 2^32 ID가 있음을 확인했습니다. 두 개의 표현식이 2^32 개 이상의 표현식과 같을 수 있습니까? –