cvc4

2열

1답변

sec. The SMT-LIBv2 Language and Tools: A Tutorial의 3.9.3는 SMT-LIBv2이 같은 복합 종류를 선언 할 수 있습니다 : 나는 CVC4을 사용하고 있으며이 구문을 받아 들일 것으로 보인다 (set-logic QF_UF) (declare-sort Triple 3) (declare-fun state() (Trip

0열

1답변

는 CVC4 C로 코드를 컴파일 할 수 없습니다 ++ API

난 그냥 g++ helloworld.cpp -lcvc4 -o helloworld -lcvc4 -Wno-deprecated을 사용하여이 파일 helloworld.cpp #include <iostream> #include <cvc4/cvc4.h> using namespace CVC4; int main() { ExprManager em;

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해야 하는가?

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 해석기 또는 제안 된 구문에 대한 지원을 해석기

1열

1답변

QF_NRA에 0으로 나누기가 포함되어 있습니까?

QF_NRA에 0으로 나누기가 포함되어 있습니까? SMT-LIB 표준은이 점에서 혼란 스럽습니다. paper where the standard is defined은이 점에 관해서는 간단히 언급하지 않고 있습니다. 실제로 NRA와 QF_NRA는 해당 문서의 어느 곳에도 나타나지 않습니다. 일부 정보는 standard website에 제공됩니다. 실제 값은 다

1열

1답변

SMT-LIB의 QF_NRA 로직이 결정 가능합니까?

SMT-LIB의 QF_NRA 로직이 결정 가능합니까? 나는 타르 스키가 실수로 다항식의 시스템을 결정할 수 있다는 비선형 산수를 결정할 수 있다는 것을 증명했습니다. 그러나 QF_NRA에는 부서가 포함되어 있기 때문에 QF_NRA가이 우산 아래 있다는 것은 명백하지 않습니다. 따라서 첫 번째 질문은 QF_NRA의 분할이 분모가 잠재적으로 0 인 변수에 의한

1열

1답변

CVC4 : 한정어로 bool을 통해 함수를 합성하는 설정?

저는 현재 다음과 같은 형식의 공식을 해결하기 위해 CVC4을 사용하고 있습니다 : 여기 exists f1, ..., fn . P(f1, ..., fn) /\ forall (b1...bk) . Q(f1,...fn,b1,...bk) 의 f1...fn는 Bool 몇개의 기능이 Bool에, 그리고 b1...bk 부울 값입니다. 내 문제는 SMT의 UF 조각에

0열

1답변

C++ API를 사용하여 cvc4에서 비트 벡터를 회전하는 방법

C++ API를 사용하여 cvc4에서 비트 벡터를 회전하려고 시도하지만 API는 연산자 표현식에서 다소 혼란 스럽습니다. 다음 코드 (발췌) 사용 : #include <iostream> #include <cvc4/cvc4.h> using namespace std; using namespace CVC4; int main() { ExprMa

1열

2답변

Z3/cvc4에서 대수를 대수로 계산할 때 사용할 수있는 함수가 있습니까?

기지 2에 로그를 계산하는 단순화를 증명하고 싶습니다. z3/cvc4에서 계산할 수있는 함수가 있습니까?

5열

2답변

정확히 수량 한정 기호는 SMT가 완성 되었습니까?

저는 다양한 SMT 솔버, 주로 Z3, CVC4 및 VeriT를 살펴 보았습니다. 그들은 수량 한정자로 SMT 문제를 풀 수있는 능력에 대해 모호한 설명을 가지고 있습니다. 그들의 문서는 기본적으로 예제 기반 (Z3)이거나 학술 논문으로 구성되어 실제로 구현 될 수도 실제로 구현되지 않을 수도있는 변경을 설명합니다. 나는 같은 1 차 논리의 decidabl