z3 - 우수한 라이브러리

z3

1열

1답변

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

1열

1답변

z3의 상호 재귀 적 데이터 유형과 내장 유형과의 상호 작용

현재 Z3을 사용하여 유형이 다른 언어에 대한 간단한 프로그램 논리를 다형성 목록으로 인코딩하려고합니다. 내가 이해하는 한, the Z3 tutorial by Moura and Bjorner에서 "배열과 같은 다른 유형 안에 재귀 적 데이터 유형 정의를 중첩 할 수 없습니다." 그래서 , 나는 다음과 같은 OCaml의 유형이 있다고 가정 : 내가 사용 Z3

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

0열

1답변

Z3에서 요소가없는 정렬을 제안 할 수없는 이유는 무엇입니까?

Z3Py를 사용하여 Z3에서 결정할 프로그램을 빌드하려고 시도했습니다. Human이 비어 있음을 의미합니다. from z3 import * from z3_helper import Z3Helper Human = DeclareSort("Human") is_mortal = Function("is_mortal", Human, BoolSort()) h =

2열

1답변

Z3 C++ API를 사용하여 입력 매개 변수를 기반으로 한 이론을 증명하는 방법?

내가 다음 달성하기 위해 Z3 C에게 ++ API를 사용하는 것을 시도하고있다 : (set-option :produce-proofs true) (declare-const Weight Int) (declare-const WeightLimit Int) (declare-const P1 Bool) (assert (= WeightLimit 10)) (

1열

1답변

수식을 풀 때 Z3에게 어디에서 시작해야한다고 말할 수 있습니까?

저는 현재 Z3에 주어진 주장이 많은 불평등과 평등을 포함하는 상황을 다루고 있습니다. 그것들은 등식에 사용 된 변수에 값을 할당하여 공식을 해결하는 것이 가장 효율적이라는 방식으로 서로 의존적입니다. Z3의 휴리스틱 스를 변경하여 솔버가 항상이 공식에서 "시작"을 선택하도록 할 수있는 방법이 있습니까? 제 생각에는 언급 된 동등한 것을 포함하는 목표를 처

0열

2답변

Z3에 UnsignedIntSort가 있습니까?

저는 솔버에서 이산 시간을 모델링하는 함수를 사용하고 있습니다. 문제는 바로 지금 우리가 z3.Function('f', IntSort(), IntSort())과 같은 함수를 사용하고, 함수에 대한 음의 입력 값은 시간이 t = 0에서 시작하기 때문에 실제로 적용 할 수 없다는 것입니다. 솔버가 고려하지 않아야하는 부정적인 시간 솔루션을 찾기 때문에 문제를

0열

1답변

혼합 정수 연산 - Z3의 증명

이 질문에 그것이 Z3 해결사 도구와 함께 사용하도록하고 C++ API를 것을 고려하시기 바랍니다을 읽기 전에 (정상 C++ 구문 없습니다, 그래서 모든 것을 다시 정의) 는 누군가는 설명 할 수 부울 논리를 정수와 어떻게 섞을 수 있습니까 (현명한 프로그래밍)? 예 : y = (x > 10 and x < 100) //y hsould be true or f

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 (+

1열

1답변

왜이 간단한 Z3 증명은 그렇게 느린 것입니까? 온라인 REPL에

다음 Z3 코드 번 아웃 : 그래서 레알에 함수를 찾고이 버전, 수행 ; I want a function (declare-fun f (Int) Int) ; I want it to be linear (assert (forall ((a Int) (b Int)) ( = (+ (f a) (f b)) (f (+ a b)) ))) ; I want