0
자바 부울 표현식을 Z3이 이해할 수있는 형식으로 변환하는 데 문제가 있습니다. 프로젝트의 요구 사항 중 일부로 인해 표현을 평가하는 데 다른 도구를 사용할 수 없습니다. 표현식에는 식별자 만 사용할 수 있고 함수 나 복잡한 유형은 사용할 수 없습니다. 나는 생각했다자바 부울 표현식을 SMTlib으로 변환
가능성은 다음과 같습니다
는 살짝 데친 또는 유사한 도구를 사용하여 파서를 구축 할 수 있습니다. 이것에 대한 단점은 연산자를 SMT와 동등한 것으로 변환 한 다음에 괄호를 추가 한 후에 이동해야한다는 것입니다. 따라서이 솔루션과 AST 처리와 관련된 작업이 나에게 과로한 것처럼 보입니다. 또한 중첩 된 레벨에 모두 맞을 수있는 문법을 정의하는 것이 다소 복잡한 것으로 나타났습니다.
토큰을 가져오고 Shunting-yard algorithm과 유사한 알고리즘으로 재정렬하려면 렉서 또는 다른 종류의 도구를 사용하십시오. 이 경우 입력에 문제가 발생하지 않도록 모든 괄호를 사용해야 할 수도 있습니다.
표현식을 구문 분석하여 편집 할 수있는 라이브러리를 사용하십시오. 지금까지는 표현식을 평가할 수있는 도구 외에는 아무것도 찾지 못했습니다.
표기법을 직접 변환 할 수있는 것을 사용하십시오. 나는 찾고 있었지만 나는 그것을 발견 할 수 없었다. 그것은 내 하루를 만들 것입니다.
나는 비슷한 질문을 찾았지만 아무 것도 발견하지 못했습니다. 나는 당신이 가질 수있는 어떤 아이디어에 감사 할 것입니다. 미리 감사드립니다!
감사합니다! 나는 그 프로젝트에 관해 몰랐다. 그러나 나는 그것이 내가 필요로하는 것을 정확하게한다라고 생각한다. – sui