매트릭스와 벡터가 포함 된 표현식의 특성을 증명하고 싶습니다 (크기는 고정적이지만 크기는 고정적 일 수 있음). 나는 식의 결과가 대각 행렬이나 삼각 행렬이, 또는 명확한 긍정적임을 입증 할 예를 들어 ... 내가 인코딩 잘 알려진 속성을 원하는이를 위해 및 ||x + y|| <= ||x|| + ||y||
(A * B) * C = A * (B * C)
Z3은 종종 중간 기능 묶음으로 정의 된 백 모델을 제공합니다. 그래서 (define-const myArray (Array Bool Int) (_ as-array f))
(define-fun f (x Bool) Int (f!10 (k!26 x)))
... 그리고 예를 들어, 그것은 (내 잘못된 구문을 용서) 다음을 참조하는 것이 일반적이다. 라이브러리
기본 이론으로 정규 트리 문법을 사용하는 검증 작업을하고 있습니다. Z3을 사용하면 해석되지 않은 함수로 자신 만의 내용을 정의 할 수 있지만 의사 결정 절차가 재귀적일 때는 언제나 잘 작동하지 않습니다. 그들은 플러그인을 허용하는 데 사용했지만 그것은 depricated되었습니다, 제 생각에는. 내가 궁금한 점은, 사용자 정의 이론을위한 의사 결정 절차를
저는 현재 다음과 같은 형식의 공식을 해결하기 위해 CVC4을 사용하고 있습니다 : 여기 exists f1, ..., fn . P(f1, ..., fn) /\ forall (b1...bk) . Q(f1,...fn,b1,...bk)
의 f1...fn는 Bool 몇개의 기능이 Bool에, 그리고 b1...bk 부울 값입니다. 내 문제는 SMT의 UF 조각에
에서 헌장을 해석, 하나는과 같이 const 완전히 해석의를 선언 할 수 (declare-const x Int)
을 마찬가지로, 하나가 정의 할 수있는이 같은 하나의 완전 해석 : (define-fun y() Int 3)
; y == 3
을 감안할 때 대수 데이터 유형 인 경우 다음과 같이 완전히 해석 된 튜플을 가질 수 있습니다. (declare
저는 Z3에서 (배열을 사용하여 정의 된) 쌍 쌍 사이의 부분 관계 (아래 코드에서 C라고 함)를 정의하려고합니다. 반사성, transitivity 및 antisymmetry를 정의하는 3 assert를 썼지 만 Z3은 "unknown"을 반환하고 나는 그 이유를 이해하지 못합니다. (define-sort Set() (Array Int Bool))
(de
에 대한 일반 데이터 유형 모델링 SMT v2.6에서 일반 데이터 유형의 동작을 모델링하고 싶습니다. 저는 Z3를 구속 조건 해결사로 사용하고 있습니다. 나는 official example, 다음과 같은 방법으로 매개 변수화 데이터 형과 같은 일반적인 목록을 기반으로, 모델 : 나는 데이터 유형에 대한 일반적인 될 목록을 원하는 (declare-dataty
저는 다양한 SMT 솔버, 주로 Z3, CVC4 및 VeriT를 살펴 보았습니다. 그들은 수량 한정자로 SMT 문제를 풀 수있는 능력에 대해 모호한 설명을 가지고 있습니다. 그들의 문서는 기본적으로 예제 기반 (Z3)이거나 학술 논문으로 구성되어 실제로 구현 될 수도 실제로 구현되지 않을 수도있는 변경을 설명합니다. 나는 같은 1 차 논리의 decidabl
저는 Z3 솔버의 새 고객이며 Windows 10, VS2013 명령 프롬프트를 사용합니다. C를 사용하려고하는데 Z3 해결사를 사용하여 아래 문제를 해결하려고했습니다. 문제 설정 :a + 2*b + 3*c = 7 만족 a, b의 가능한 조합 c 무엇인가? 결과에서 void example(){
Z3_context ctx = mk_context();