smt

2열

1답변

에 배열로 재귀 유형을 정의 할 수 없습니다 : (declare-datatypes() ((Tree (leaf (content Int)) (node (left Tree) (right Tree))))) 그러나 나는 다음을 정의 할 수 없습니다. 먼저 뭔가를 선언해야합니까? 아니면 허용되지 않는 경우 동일한 정의를 얻는 방법 (

0열

1답변

솔버 객체 용 인터페이스를 생성하고 사용하는 방법 (Z3 해석기)

저는 C#을 처음 사용합니다. 솔버 객체를 사용하는 몇 가지 메소드가있는 클래스가 있습니다. 하지만, 각각의 방법에 대해 다시 그것을 사용하는 솔버 객체의 인스턴스를 생성해야합니다. 인터페이스를 사용하여이를 피하는 방법을 말해 줄 수 있습니까? 인터페이스를 만드는 것은 문제가 아니지만 일단 인터페이스가 만들어지면 어떻게 사용합니까? 예 : 이것은이 ISol

2열

1답변

y = 1/x, x = 0 실수로 만족? SMT-LIB에서

: (declare-fun y() Real) (declare-fun x() Real) (assert (= 0.0 x)) (assert (= y (/ 1.0 x))) (check-sat) 이 모델은 SAT 또는 UNSAT해야 하는가?

2열

1답변

Z3 : Z3 소개 int2bv?

Z3 (smt2 형식) 작업과 다소 혼동 스럽습니다 int2bv. 나는 그런 smt2 표현 쓴 : 나는 Z3와 그것을 해결 때 (declare-const t1 Int) (assert (= ((_ int2bv 2) t1) #b11)) (check-sat) (get-model) 를, 그것을 가지고 : sat (model (define-fun

1열

1답변

Z3에서 외부 SAT 솔버 호출

내가 근무하는 회사에서 여러 SAT 솔버에 액세스 할 수 있습니다. 각 SAT 솔버가 Z3 SMT 솔버의 성능에 어떤 영향을 주는지 분석하고 싶습니다. Z3에서 외부 SAT 솔버를 호출 할 수 있습니까? 그렇지 않은 경우 외부 솔버를 호출하도록 Z3을 수정해야합니까?

3열

1답변

Z3 성능 : 많은 어설 션 대 대형 연결

내 연구에서는 자동으로 SMT2를 생성 한 다음 Z3으로 전달합니다. 생성 된 코드는 기본적으로 하나의 매우 큰 연결 (and ...) 많은 제약이 있습니다. 많은 어설 션을 생성하는 것과는 대조적으로,이를 수행하여 중요한 성능을 잃게됩니까?

1열

1답변

왜 Z3은 일부 작업에서`is_int`가 닫혔다는 것을 증명/승인 할 수 없습니까? 예를 들어

, 다음 쿼리 시간이 초과 : 지금까지 내가 읽은로 (declare-const x Real) (declare-const y Real) (assert (is_int x)) (assert (is_int y)) (assert (not (is_int (+ x y)))) (check-sat) , Z3의 Real 수학적 실수와 미묘한 의미하지 기계 것들이

1열

2답변

Z3-str/Z3str2 : Z3의 나머지 부분과 함께 사용할 수 있습니까?

문자열 해결사가 필요하며 Z3-str 또는 그 후속 Z3str2를 고려하고 있습니다. 이 확장 프로그램을 나머지 Z3 (즉, Z3에 구현 된 다른 모든 이론 해결사)과 함께 동시에 사용할 수 있습니까? 아니면 이러한 문자열 확장 만 준 독립 사용할 수 있습니까?

1열

1답변

SMTLIB2/Z3의 다형 함수

Z3 또는 SMTLIB2에서 "다형성"함수를 만들 수 없다는 점을 이해합니다. 예 : 내가 좋아하는 뭔가를 쓰고 싶습니다 (declare-fun Prop (A) Bool) (declare-fun x1 () Int) (declare-fun x2 () Bool) (assert (and (Prop x1) (Prop x2))) (I 확인 첫째을 두 배로

0열

1답변

Java 용 IP Solver를 쉽게 사용할 수 있습니까?

자바 프로그램에서 0-1 정수 프로그래밍 솔버를 도구로 사용하고 싶습니다. 웹에서 사용하기 쉬운 것을 찾을 수 없습니다. 내가 sat4j에서 의사 부울 라이브러리를 시도했지만 이것은 잘 설명되어 있지 않으며 일부 클래스는 API의 설명과 일치하지 않습니다 (일부 메소드 서명이 다릅니다). 의견이 있으십니까?