smt

0열

1답변

dReal SMT 솔버가 반례를 반환합니까? 나는 produce-models은 사실이지만 반례를 생성하는 방법을 모른다. 또한 dReach 도구에는 --visualize 옵션이 있으므로 dReal이 일부 모델 정보를 생성해야하는 것처럼 보일 수 있습니다. 그러나 .smt2 파일을 실행할 때 반증을 볼 방법을 찾을 수 없습니다.

1열

1답변

Z3py 수식에서 ZeroExt (n, a)를 올바르게 사용하는 방법?

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

-2열

1답변

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

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

1열

1답변

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

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

-1열

1답변

z3의 'smt_tactic'은 QF_BV 수식을 어떻게 해결합니까?

z3이 'qfbv'전략 대신 'smt_tacitc'를 사용하여 QF_BV 공식을 해결할 때 비트 블래스트하고 SAT 엔진을 사용합니까? verbose leval을 10으로 설정하면 비트 블라스팅을 볼 수 없습니다.

0열

1답변

SMT-LIB 2.6 선언 데이터 형식 문의 SMT 솔버 지원

SMT-LIB 버전 2.6의 draft은 (declare-datatypes) 문을 지정합니다. 이 기능의 경우 original announcement에서 제안 된 구문은 당시 Z3 및 CVC4에서 지원하는 구문과 다릅니다. 현재 SMT-LIB 2.6 초안의 제안 구문을 지원하는 SMT-LIB 지원이있는 SMT 해석기 또는 제안 된 구문에 대한 지원을 해석기

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열

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 성능 문제를 분석하는 방법은 무엇입니까?

37 개의 비슷한 SMT2 문제가 있습니다. 각각 및 을으로 풀어 놓았습니다. 문제는 점진적인 SMT 문제 해결을 사용하고 모든 (check-sat)은 unsat을 반환합니다. 컴팩트 버전은 QF_AUFBV 로직을 사용하고, 풀 버전은 QF_ABV를 사용합니다. z3, yices 및 boolector에서 실행했습니다 (그러나 boolector는 풀린 버전