식에 조건부 (=>)가 포함되어 있는지 확인하는 방법 Z3py를 확인하는 방법

저는 부울 수식을 통과하기 위해 Z3py를 사용하고 있습니다. 수식에 조건부가 포함되어 있는지 확인하는 방법 z3.py 소스 코드를 확인한 결과 is_and(), is_or(), is_not(), is_implies()와 관련이 없습니다. 어떤 생각? 감사.식에 조건부 (=>)가 포함되어 있는지 확인하는 방법 Z3py를 확인하는 방법

출처

2017-12-05 Pushpa

,하지만! -> c'는 기본적으로'AVC '...''a'와'c'는 모두 될 수 있습니다. 예를 들어 ** bvc는'! b -> c'이고'! c -> b','! av! bvc'는'a -> (! bvc)'이고 또한'b -> (! avc)'와'! c -> (! av! b)'그리고'(a & b) -> c'또한'...' 그래서'is_or()'는 충분해야합니다. –

오, 나는 암시 적 제거를위한 코드를 작성하고 있습니다. 그래서 먼저 코드에 함축 된 의미 (정확한 조건)가 포함되어 있는지 구문 분석해야합니다. 그런 다음 a => b를 a 또는 b로 변환합니다. 감사. – Pushpa

내 의견은 관련성이 없으므로 모든 것이 아니라 명시적인 의미 만 파악하면 충분히 행복하다는 뜻입니다. :) –

"is_app_of"함수를 사용하여 표현식의 내장 함수를 결정할 수 있습니다. 따라서,

def is_and(a): 
    return is_app_of(a, Z3_OP_AND)

`로 이미 z3.py 파일에 구현, 내가 z3``의 전문가가 아니에요 유사

def is_implies(a): 
    return is_app_of(a, Z3_OP_IMPLIES)

출처

2017-12-05 23:54:20

감사. 잘 알고 있습니다. – Pushpa

식에 조건부 (=>)가 포함되어 있는지 확인하는 방법 Z3py를 확인하는 방법

답변

관련 문제