smt

0열

1답변

Z3 고정 소수점 엔진을 사용하는 ∃-queries 및 ∀-queries

Z3 고정 소수점 엔진의 두 가지 입력 형식이 서로 어떻게 관련되어 있는지 혼란스럽고 분투하고 있습니다. 간단한 예 : 음수의 존재를 증명하고 싶다고 가정 해 봅시다. 음수가 아닌 경우 1을 반환하고 음수 인 경우 0을 반환하는 함수를 선언하고 함수가 0을 반환하는 인수가 있으면 해결자가 실패하도록 요청하는 함수를 선언합니다. 그러나 하나의 제한이 있습니다

3열

1답변

Z3 용 C API에서`Z3_mk_forall`과`Z3_mk_forall_const`의 차이점은 무엇입니까?

2 가지 기능으로 혼란 스럽습니다. 그들은 서로 비슷한 인수를 취하는 것처럼 보이고 (서로 직접적으로 변환 가능), 각각은 AST를 반환합니다. 함수가 똑같은 일을합니까? 그렇지 않은 경우 각각 언제 필요합니까? 2의 서명 : Z3_ast Z3_mk_forall (Z3_context c, unsigned weight, uns

0열

1답변

z3 잘못 UNSAT을 말합니다

아래의 문제에 대한 해결책이 있지만 z3에 UNSAT이 나와 있습니다. (set-logic QF_UFNRA) (declare-fun a() Real) (declare-fun b() Real) (declare-fun c() Real) (declare-fun d() Real) (declare-fun e() Real) (declare-fun f() R

2열

1답변

z3py에서 대수 수식을 나타내는 법

저는 z3py에 새로 입문했습니다. z3py에서 다음 대수 표현식을 코딩하려고합니다. log(x,y) 스택 오버플로를 많이 검색하여 비슷한 질문을했지만, 불행히도 충분한 만족스러운 답변을 얻을 수 없었습니다. 제발 도와주세요!

1열

1답변

z3 api를 사용하여 LRA를 해결하면 터미널에서 z3을 사용하는 것보다 느리게 실행됩니다.

임의의 일반화 된 스트립 패키징 문제 (LRA)를 해결하기 위해 Z3을 사용하려고하며 C 프로그램에서 Z3 API를 호출합니다. 여기에 코드가 나와 있습니다. Z3_context ctx; Z3_ast fs; LOG_MSG("smt2parser_example"); FILE *fp = fopen("smttest","r"); if(fp == NULL)

1열

1답변

z3 smt 증명자가 왜 그런 간단한 수식에 실패합니까?

필자는 필자의 석사 학위 논문을 작성하면서 Microsoft의 z3 smt 입증 자와 실험을 해 보았습니다. 나의 유스 케이스에서는 수량 제 (equality를 가진 1 차 논리)를 포함하는 간단한 수식에 대해 satisfiability (모델 없음)를 점검해야한다. Z3는이 일을 제외하고, 밀리 초 몇 내 모든 예제를 해결하는 좋은 일을한다 : foral

1열

1답변

Z3 (버젼 4)의 unsat 코어

저는 지난 1 년 동안 Z3 버전 4.0의 Ocaml API를 사용하여 왔습니다. 주로 비트 벡터 이론이었습니다. 이제 Z3.solver_check을 수행 한 후 unsat 코어를 추출해야하지만 불행히도 버전 4에는이 기능이 없습니다. 수식에있는 각 비트 벡터 수식을 사용하기 위해 가정을 사용하여 다시 작성한 다음 unsat 코어를 얻지 만 코드의 중요한

0열

1답변

z3의 실행 시간 또는 DPLL (T) 알고리즘의 실행 시간을 예측할 수 있습니까? 심지어 최악의 경우

저는 Microsoft z3의 프로토 타입을 시각화하려고합니다. z3 또는 알고리즘의 실행 시간을 예측할 수 있는지 궁금합니다. 최악의 경우 실행 시간을 얻을 수 있다면 좋을 수도 있습니다. 또한 z3에서 이론적 인 솔버 (solver)에 의해 각 검사 과정의 실행 시간을 얻는 방법이 있습니까? 답변 해 주셔서 감사합니다.

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;

3열

2답변

솔버의 결정에 따라 get-model 또는 unsat-core 실행

SMT-LIB 2.0 스크립트에서 솔버의 최종 적합성 결정 (sat, unsat, ...)에 액세스 할 수 있는지 궁금합니다. 예를 들어, 다음 코드를 (set-option :produce-unsat-cores true) (set-option :produce-models true) (set-logic QF_UF) (declare-fun p() Bool