z3py

1열

1답변

바이너리에 숨겨진 keygen 알고리즘의 암호를 찾으려고합니다. 그래서, 나는 어셈블리에서 공식을 추출하고이를 해결하기 위해 작은 파이썬 스크립트 (정확하게, 희망) 번역 : Traceback (most recent call last): File "./alt.py", line 13, in <module> state[i+1] = (ZeroE

1열

1답변

z3py : z3py에서 사용 된 로직을 어떻게 설정합니까? 다음 코드를 사용하여

: import z3 solver = z3.Solver(ctx=z3.Context()) #solver = z3.Solver() Direction = z3.Datatype('Direction') Direction.declare('up') Direction.declare('down') Direction = Direction.create() C

2열

1답변

배열의 제 N 소자 얼마나 많은 I는 Z3 배열을 Z3

의 조건을 만족 찾기 간단한 산술 : lambda i: Or(i == 0, i > 2) 내가 원하는이 만족 인덱스 N에 인덱스 0의 요소의 총 수를 아는 것입니다 조건 (일반적인 파이썬 목록이라면 len(filter(lambda i: i == 0 or i > 2, x))처럼 보일 것입니다. z3에서이를 수행하는 방법을 알 수 없습니다. z3.z3type

0열

1답변

z3py의 Z3-LIB에서 (_ map op) 사용 방법

Z3-LIB는 (_ map op)와 같은 확장 배열 이론의 연산자를 지원합니다. 하지만 Z3py에서이 연산자를 어떻게 사용할 수 있습니까?

2열

1답변

Z3PY 방정식, 내가하고 싶은 Z3PY에서 일하고 있어요

크기 제한은 v0 = Int('v0') const = 0x12345678 I wrote this : s.add((const*(v0 + const*(func(v0*const) - v0)) - v0) == somevalueof64bits) 내 문제가있는 방정식의 계산의 크기를 제한하는 방법을 알고 그 (CONST * (V0 '의 계산 +

3열

2답변

Z3 QBF 수식을 직접 pcnf로 변환

저는 Z3 정리 프로버 (Z3Py : 파이썬의 Z3 API 사용)를 사용하여 QBF (Quantified Boolean formula)를 만듭니다. Q3에서 qbf 수식을 Prenex normal form으로 직접 변환 할 수있는 방법이 있습니까?

5열

1답변

Z3py는 "문자열"과 "시퀀스"를 지원합니까

Z3에서는 문자열과 시퀀스를 지원합니다. 그러나 Z3py도이를 지원합니까, 아니면 파이썬에서 문자열이나리스트를 사용해야합니까? 최신 버전에서 새 버전이 String 및 Sequence의 이론을 지원하는 것으로 보였지만 사용 방법을 모르겠습니다. 누구든지 시퀀스에 대한 예를 들어 주겠습니까?

0열

1답변

Z3 해결사 차이 로직 파이썬 API를

내가 파이썬에서 이런 일을하려고했습니다 : 나는 솔버 (solver.set('smt.arith.solver', 1))을 위해 그것을 할 수있었습니다 (set-option :smt.arith.solver 1) (declare-const x Int) (declare-const y Int) (assert (>= 10 x)) (assert (>= x (+

3열

2답변

Z3 Prover가 잘못된 솔루션을 반환합니다.

저는 Python으로 Z3 Thoerem Prover로 방정식을 풀려고합니다. 하지만 내가 얻는 해결책은 잘못되었습니다. from z3 import * solv = Solver() x = Int("x") y = Int("y") z = Int("z") s = Solver() s.add(x/(y+z)+y/(x+z)+z/(x+y)==10, x>0,

1열

1답변

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

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