z3py

1열

1답변

Z3을 사용하여 배열 속성 조각에서 수식의 적합성을 확인하고 있습니다. Z3가 반환하는 배열 변수에 대한 모델은 대개 다른 if 식, if-then-else 사례 분석 등을 사용하여 표현됩니다. Z3이 출력하는 모델을 구문 분석하여 입력 SMT-LIB 수식을 만족하는 배열을 만들고 싶습니다. 명시 적으로. A -> { 1 -> 3 2 ->

6열

2답변

Z3으로 오버플로 확인

Z3을 처음 접했고 온라인 Python 튜토리얼을 확인하고있었습니다. 그런 다음 BitVecs에서 오버플로 동작을 확인할 수 있다고 생각했습니다. 는이 코드 썼다 x = BitVec('x', 3) y = Int('y') solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1))) 및 I는 기대 하였다 Y = 7 X

5열

2답변

BitVector로 부호있는 정수를 모델링하는 방법은 무엇입니까?

a이 8 비트의 정수인 254이라고 가정합니다. a이 부호있는 정수인 경우 실제로는 -2으로 간주됩니다. 반대로 a이 서명되지 않은 경우 254으로 유지됩니다. Z3으로 BitVector 이론에 서명/부호없는 정수 문제를 모델링하려고하지만 BitVector에서 허용하지 않습니다. 사실입니까? 그럼 Z3py에서 이것을 모델링하는 방법에 대한 아이디어는? 고마

0열

1답변

z3py에서 Extract 노드의 경계를 검색하십시오.

z3py를 사용하고 있습니다. 내 질문은, 어떻게 Extract 노드의 경계를 검색합니까? 내가 Extract이 인수에 대응 세와 함수가 될 것이라고 생각하지만, 그렇지 않은 : >>> x = BitVecVal(3, 32) >>> e = Extract(15, 0, x) >>> e.decl() Extract >>> e.decl().arity() 1

2열

1답변

z3py를 사용하여 가장 약한 전제 조건 찾기

z3py를 사용하여 작업 및 사후 조건이 주어진 경우 가장 약한 전제 조건을 찾고 싶습니다. 는 가장 약한 전제 조건 N의 ==이 방법은 일부 게시물 조건이 아닌 다른 사람을 위해 작동하는 전술 solve-eqs 사용 4. 될 작업 N = N + 1 및 사후 조건 N == 5을 감안할 때. 게시 조건 N < 5을 사용할 때 [[Not(4 <= N)]]이 나

0열

1답변

Z3py 폴란드어 표기법 출력

z3py 표현식의 기본 출력은 중위 표기법입니다. 출력 형식을 폴란드어 표기법으로 설정하는 옵션이 있습니까? 비슷한 옵션이 있다고 가정합니다. set_option(html_mode=False) 그러나 설정할 수있는 옵션에 대해 자세히 설명하는 지원 문서를 찾을 수 없었습니다. 현재 표현의 내부 표현을 얻으려면 .sexpr()을 사용하고 있습니다. 그러나 필

0열

1답변

Z3-Py를 사용하여 수량 한정 기호를 제거하는 방법은 무엇입니까? 나는 다음과 같은 코드를 사용하여 정량없는 공식을 얻기 위해 노력하고 있어요

: S, E, I, R = Reals('S E I R') b, n, s, g, m = Reals('b n s g m') SS = Then('qe', 'smt').solver() SS.add(Exists([S,E,I,R], And(m+g*R-m*S-b*I*S == 0, b*I*S-(m+s)*E==0, s*E-(n+m)*I==0, n*I-(m+g

0열

1답변

이 코드가 Unsat (ForAll 및 Implies를 사용하는 수식)를 반환하는 이유는 무엇입니까?

c == a + 4 및 t == c + b이 주어진 경우, a == -4 인 경우 t == b이 주어집니다. 위의 2 방정식을 주어진 의미, 그리고 t == b 의미를 반대하려고, 나는 a 값을 찾으려고합니다. 나는를 내포합니다 FORALL 및 이 작업을 수행하는 코드 아래에 있습니다 from z3 import * a, b, c, t = BitVecs(

1열

1답변

Z3py에서 왜 분단을 해석되지 않은 함수로 단순화합니까?

TL : simplify을 사용할 때 비트 벡터 분할 노드가 Z3_OP_BSDIV에서 Z3_OP_UNINTERPRETED으로 변경됩니다. 어떻게 해석 할 수없는 작전에서 부서 작전을 말할 수 있습니까? 설명 : 다음 세션이 그 비트 벡터 부문은 해석 보여 주지만, simplify() 사용 후,이 해석되지 않습니다. 아래의 변수 d을 어떻게 사용하는지 확인하

0열

1답변

Z3Py - 표현식이 포함 된 모든 수식을 가져옵니다.

Z3Py에서 일부 변수/표현식이 발생하는 모든 수식의 목록을 가져올 수 있습니까? 예 : s.add(x < 0) s.add(x > y) print s[y] >>> x > y