C# 문을 z3 형식으로 변환

Question

C#으로 코드를 작성하고 있습니다.

코드에는 다양한 IF 조건이 있습니다. 이러한 조건을 z3 제약 조건 해결사에 전달하고 만족 여부를 확인하고 만족할만한 값을 얻고 싶습니다. (나는이 값을 코드에서 더 사용한다.)

코드에서 IF 조건을 취하여 z3 구문에서 이와 동일한 어설 션을 작성하면 올바르게 작동한다. 하지만 나는 C#에서 문장이 주어 졌음을 의미하는 일반화를 원한다. 나는 z3 구문에서 해당 문장을 생성하려고한다.

어쨌든 내가 할 수 있습니까?

Answer 1

C# 언어는 런타임시 if 문을 감지 할 수 있도록 필요한 후크를 제공하지 않습니다. 당신이 당신을 발견 할 수없는 것은 Z3에게 말할 수 없습니다.

Roslyn을 사용하여 C# 코드가 포함 된 문자열을 AST로 구문 분석하고이를 Z3으로 변환 할 수 있습니다. 그것은 단순한 경우에 그렇게하기가 어렵지 않을 것입니다. 이는주기적인 제어 흐름을 위해 고장입니다. 변수, 연산자, if, switch과 같은 일반적인 비순환 구조에 대해서는이 함수를 사용할 수 있습니다.