z3py

3열

1답변

Z3의 버그입니까? Real 및 ForAll에 대한 잘못된 대답이 적용되었습니다.

포물선 y = (x + 2) ** 2-3의 최소값을 찾으려고합니다. 분명히 대답은 y == - 3, x == 일 것입니다. -2. 그러나 z3은 ForAll 어설 션을 충족시키지 않는 [x = 0, y = 1] 응답을 제공합니다. 내가 잘못 생각하나요? from z3 import * x, y, z = Reals('x y z') print(Tactic

2열

1답변

z3 표현식에 대해 여분의 \ n을 인쇄하는 Python 평가판

다음 코드에서 내 문제의 범위를 좁혔습니다. 문자열을 동등한 z3 표현식으로 변환하려고합니다. 문제는 변수 이름이 크면 'eval'은 표현식 사이에 여분의 \ n을 넣습니다. 그러나 더 작은 변수 이름을 사용하면 여분의 \ n이 없어집니다. 내 통제하에 있지 않기 때문에 더 큰 변수 이름이 필요합니다. 내가 더 큰 변수 이름이 코드의 출력은 올바르게 COD

3열

1답변

Z3의 배열에 대한 제약

배열과 관련하여 Z3의 작동 방식에 대한 두 가지 질문이 있습니다. 1) 모델에서 배열에는 해당 값과 함께 "else"요소가 있습니다. 수식에서 배열의 "else"요소에 대한 제약 조건을 지정하는 방법이 있습니까? 예를 들어 배열의 첫 번째 요소가 5보다 크고 다른 모든 요소가 5보다 작도록 지정할 수 있습니까? 커맨드 라인에서 Z3 통해 다음 식을 확인하

1열

1답변

로컬에서 Z3 SMT를 사용하는 방법

웹 사이트를 사용하는 대신 Z3 SMT를 로컬에서 사용하는 방법에 대해 알고 계신 분도 있습니까? z3.py를 사용하는 방법을 알고 있지만 SMT를 사용해야합니다. rise4fun.com이 다운되어 내 모델을 확인하기가 어렵습니다.

0열

1답변

Z3 Python API에서 sort로부터 상수 만들기

Z3 Sort와 문자열 s이 주어지면 그 종류의 Z3 상수를 s으로 만들려고합니다. 예를 들어 IntSort()이고 이름이 "x" 인 경우 정수형 상수 "x"을 얻고 싶습니다. Int('x')을 호출 할 수 있지만이 변수를 동적으로 생성하기 때문에 주어진 변수에 어떤 종류의 예측을 할 수 있는지 예측할 수 없습니다. 내가해야 할 일은 시스템에서 제공하는 것

4열

1답변

z3.And()가 느린 이유는 무엇입니까?

나는 Z3 파이썬 바인딩을 사용하여 z3.And(exprs)을 통해 And 식을 만듭니다. 여기서 exprs은 부울 변수에 대한 48000 항등 제약 조건의 파이썬 목록입니다. 이 작업은 2.6GHz 프로세서가있는 MBP에서 2 초가 걸립니다. 내가 잘못 할 수 있습니까? 이것이 z3 Python 바인딩에 문제가 있습니까? 그러한 구조를 최적화하는 방법에

5열

1답변

멀티 스레드 Z3?

저는 파이썬 프로젝트에서 현재 약간의 끔찍한 방법으로 작업 속도를 높이려고 노력 중입니다. Z3 솔버를 설정 한 다음 프로세스를 포크하고 Z3에서 하위 프로세스에서 해결을 수행하도록하고 모델의 피클 할 수있는 표현을 부모에게 전달하십시오. 이 방법은 훌륭하게 작동하며 내가하려는 일의 첫 번째 단계입니다. 상위 프로세스가 더 이상 CPU 바인딩되지 않습니다.

3열

1답변

z3.check()가 z3.push() 바로 앞에 오면 느려지는 이유는 무엇입니까?

아래의 Python 스 니펫은 Z3의 성능 향상 동작을 보여줍니다. push() 전화가 없으면 z3에서 수식을 0.1 초 단위로 확인합니다. push() (추가 어설 션 없음)으로 z3은 0.8 초가 걸립니다. s.append(f)과 s.push()을 교환해도 유사한 결과가 발생합니다. import time import z3 f = z3.parse_sm

1열

1답변

해 찾기에서 제약 조건에 추가 된 모든 변수를 가져 오는 방법은 무엇입니까?

Z3py를 사용하고 있고 해 찾기에서 모든 제약 조건의 모든 변수 집합을 얻으려고합니다. Solver.assertions()을 호출하여 ASTVector을 얻은 다음이 벡터를 반복하고 BoolRef 유형의 객체를 가져 오지만 그 다음에 붙어 있습니다. 예를 들어 BoolRef 인스턴스와 같은 반복적 인 반복을 통해 개별 변수를 얻으려면 어떻게해야합니까?

0열

1답변

Z3 (파이썬)의 실제 닫힌 필드에서 한정자 제거

Z3에는 이제 원통형 대수 분해를 기반으로하는 비선형 실수 산술에 대한 충족 성 엔진이 있습니다. 단순한 적합성 테스트와는 달리 수량 한정자 제거 결과를 얻을 수있는 방법이 있습니까? 것은이 작동하지 않음 다음 from z3 import * b,c,x = Reals('b c x') f = Exists(x, b*x+c==0); print Tactic('