z3py

0열

1답변

내가 Z3의 파이썬 API를 사용하고 [버전 4.4.2 - 64 비트]와 중첩 된 상점을 단순화하고 나는 Z3는이 경우 표현 단순화 이유를 이해하기 위해 노력하고있어 : >>> a = Array('a', IntSort(), IntSort()) >>> a = Store(a, 0, 1) >>> a = Store(a, 0, 3) >>> simplify(a)

0열

1답변

Z3py - 배열 변수에 대한 제약 조건을 풀 때 함수 k! 0 생성

연구 활동 중에 z3py (Python API for Z3 v4.4.2)를 조사하고 있습니다. 우리는 왜 z3이 질문보다 많은 배열 기능을 제공하는지 궁금합니다. ! Z3는 K를 사용하는 것 같다 >>> A = Array('A', IntSort(), IntSort()) >>> solve(A[0] == 0) [A = [0 -> 0, else -> 0],

2열

1답변

동적 네트워크에서 신념을 확인하는 Z3Py 예제

Z3 (또는 Z3Py의 특정 사항)을 더 잘 이해하기 위해 Paper Checking Beliefs in dynamic Networks에서 직접 작성한 예제를 구현하고자했습니다.이 sat Or(And(Var(0) == 5, Var(1) == 2), And(Var(0) == 4, Var(1) == 2), And(Var(0) == 4, Va

0열

1답변

z3에서 각 변수의 값 범위를 제한 할 수 있습니까?

예를 들어, 제한이 x + y > 100입니다. 나는 z3가 나를 x의 값을 1이나 2가되도록하고 싶지 않고, z3가 y의 값을 1이나 2가되도록 내 보내지 않기를 바란다. 그래서, x와 y는 우리가 Z3에 이러한 제한을 적용 할 수 있습니다 1 2. 제외하고는 모든 숫자가 될 수 있습니까? 감사합니다.

0열

1답변

Z3 sat 솔버 런타임을 계산하는 방법

방정식 세트를 풀기 위해 z3py를 사용하고 있습니다. 어떻게 런타임 순서를 계산합니까? 선형 방정식 집합에서 만족되어야하는 bitvecs 변수가 있습니다. 설명서 및 안내서는 런타임을 계산하는 방법을 제공하지 않습니다.

0열

1답변

문제 Z3 CC_NUM_THREADS를 사용하여 병렬 Z3를 구성하는 동안 = 3

문제 Z3 CC_NUM_THREADS를 사용하여 병렬 Z3를 구성하는 동안 = 3 나는 = 3 내 smt2 파일 다음과 같은 오류가 저런 애됩니다 CC_NUM_THREADS와 Z3 병렬 버전을 실행하려합니다 쪽으로. ERROR: unknown parameter 'cc_num_threads' Legal parameters are: auto_config (

0열

1답변

smt2 형식 예제에서 z3 해석기에 대한 여러 솔루션을 얻는 방법은 무엇입니까?

sm3 형식의 z3 해석기를 사용하여 비트 벡터 수식에 대한 여러 모델을 생성하는 방법은 무엇입니까? 비트 벡터 용 IDEA 코드를 구현하는 동안 하나의 모델이 생성됩니다. 가능한 모든 모델을 생성하는 방법은 있습니까? ex.smt2 파일 (set-logic QF_BV) (set-info :smt-lib-version 2.0) (declare-const

0열

1답변

Z3Py : eval 또는 z3.parse_smt2_string을 사용하여 표현식을 파싱

다른 것들 사이에서 큰 명제식을 z3 인스턴스로 변환해야하는 Python 프로그램을 작성 중입니다. 예를 들어 a = my_atomic_proposition("a") # Bool b = my_atomic_proposition("b", operator.ge, 42) # Real: c >= 42 c = my_atomic_proposition("c") # B

0열

1답변

z3py의 일부 Implies 조건에서 부울 수식 증명

Z3py를 처음 사용하면서 과제 (sat 및 unsat)에 대한 카운터 예제를 생성했습니다. unsat 솔루션에 대한 반례를 생성하는 함수가 있습니까?

-2열

1답변

다중 모델 시간을 단축하십시오.

여러 모델을 얻지 만 몇 시간이 걸립니다. 그래서 모든 모델을 가져 오는 시간을 줄이는 것이 좋습니다. 적은 시간에 Satisfy 방정식에 대한 모든 가능한 솔루션을 얻으시겠습니까? 가능한 모든 솔루션을 얻기위한 z3python의 기능이 있습니까? from z3 import * x0,x1,x2,x3,x4,x5=BitVecs('x0 x1 x2 x3 x4 x