smt

5열

1답변

SMTLIB 배열을 사용하는 동안 Z3의 이론과 광산에 대한 이해가 달라졌습니다. 나는 공식 웹 사이트 [1]에서 찾을 수 SMTLIB 배열 이론을 사용하고 있습니다. 내 문제는 간단한 예를 들어 설명하는 것이 가장 좋습니다. (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0)

3열

2답변

Z3과 SMT-LIB를 사용하여 최대 2 개의 값을 얻으십시오.

smt-lib2를 사용하여 최대 수식을 얻으려면 어떻게해야합니까? 물론 (declare-fun x() Int) (declare-fun y() Int) (declare-fun z() Int) (assert (= x 2)) (assert (= y 4)) (assert (= z (max x y)) (check-sat) (get-model) (exi

4열

1답변

코멘트가 중간 (`체크 - 체크)`이라면 쿼리 결과가 변경되는 이유는 무엇입니까?

UNSAT 쿼리를 디버깅하는 동안 쿼리 상태에 흥미로운 차이가 있음을 발견했습니다. 쿼리 구조는 다음과 같습니다. assert(...) (push) ; commenting any of these two calls (check-sat) ; makes the whole query UNSAT, otherwise it is SAT assert(...)

1열

1답변

Microsoft Z3 : 표현식을 특정 변수로 변환

저는 동적 관측에 대한 간단한 분석을 위해 Microsoft의 Z3을 사용하고 있습니다. 이것의 일부로, 하나의 변수 집합을 다른 변수 집합으로 변환 할 수 있다면 도움이 될 것입니다. 나는 Z3 정말 새로운 해요,하지만 난 그게 일부 내부 단순화 규칙과 같이 몇 가지 변환을 할 수 있다면 기본적으로, 나는 궁금하네요 ... 공식을 변형시키는 다른 방법이

2열

1답변

Z3에서 열거 유형 간의 하위 유형 관계 표현

Z3에서 열거 유형 간의 하위 유형 관계를 표현하는 가장 좋은 방법은 무엇입니까? (declare-datatypes() ((Animal Eagle Snake Scorpion))) 한 다음 새 하위 만들 :이 (declare-datatypes() ((Mammal Cat Rat Bat))) 그래서 형 동물의 4 개 별개의 상수가 있다는 주장이 있음을 특

1열

2답변

Z3 및 smtlib을 사용하여 혼합 된 값으로 구성/모델을 계산하십시오.

속성 값을 어떻게 계산합니까? 나는이 개 모델 얻을 것이와 (declare-fun x() bool) (declare-fun y() bool) (declare-fun z() bool) (assert (AND x (OR y z))) : 여기 예입니다 (declare-fun x() bool) (declare-fun y() bool) (declare-

0열

1답변

너무 많은 가능한 구성이 주로 I 추측 논리 문제 스칼라^Z3

를 사용 ...이 smtlib 수식을 사용 : 이러한 구조의 용어 (declare-fun a() Bool) (declare-fun b() Bool) (declare-fun c() Bool) (declare-fun d() Bool) (assert (xor (and a (xor b c)) d)) (투입 내 의견으로는, 적어도) : XOR |

1열

1답변

z3의 기호 변수

z3 솔버가 "기호화 된"솔루션을 생성 할 수있는 방법이 있습니까? 예를 들어, 방정식 : 1 + X = C 용액 X = C-1이지만, Z3 [c = 0, x = -1] 항상 같은 특정 모델을 방출한다. c를 기호 변수로 "정의"하는 방법?

1열

4답변

SMT 솔버의 부울 수식에 대한 최적 솔루션을 찾는 것이 가능합니까?

I 인해 편집의 이유로 해결하기 큰 부울 식을 가지고, 여기 화상을 붙여 가지고 을 또한 이미 함수 area 4의 치수를 측정 할 정수 : area(c,d,e,f)=|c−d|×|e−f| 난 그냥 수식이 만족할 수 있는지 알아내는 것보다 더 많은 일을하고 싶은 : 나는 TRUE 및 area(c,d,e,f) 어떤의 크기보다 크거나 같은 가장 큰 공식을 만드는

1열

2답변

Z3에서 코드 조각을 최적화하는 방법은 무엇입니까?

나는 내가 때문에 한정사와 의미의 추측 an optimization problem for a boolean formula (set-option :PI_NON_NESTED_ARITH_WEIGHT 1000000000) (declare-const a0 Int) (assert (= a0 2)) (declare-const b0 Int) (assert (= b0