z3

    0열

    3답변

    z3의 계승을 포함하여 수학적 진술을 증명할 수 있습니까? (더 놀라움을 그 증거를 제시하지 않더라도

    나는 다음 울프 람 알파를 증명하는 것이 참으로 true임을 식별 할 수있을 것으로 보인다 노력하지 있어요 및 최대 값을 결정할 수 없습니다 가) : declare(n, integer) $ assume(n > 0) $ is(equals(2^n - n - 1 - sum(binomial(n,k), k, 2, n), 0)); => unknown 지금 나
    z3 maxima theorem-proving wolframalpha 2017-01-23

    0열

    1답변

    Z3 C++ API는 직렬화 된 출력의 바이너리가 "unsat"를 산출하는 동안 "unknown"을 산출합니다.

    Z3 C++ API를 사용하여 특정 제약 조건 집합을 만들 때 "unknown"이 발생합니다. 그러나 연산자 < <()을 사용하여 z3::solver 개체를 serialize하고 출력을 z3 이진수로 전달하면 "unsat"이 예상대로 생성됩니다. 재미있게도, < <() 대신 z3::solver::to_smt2()을 사용하면 Z3 바이너리는 "을 알 수 없음
    c++ z3 2017-01-26

    0열

    1답변

    z3 C++ 인터페이스를 통해 SMT2 파일을 해석기로 읽을 수 있습니까?

    큰 시스템에 포함 된 z3 코드가 상당히 긴 시간 제한에도 불구하고 특정 제약 조건 세트 (C++ 인터페이스를 통해 추가 된)에 대한 솔루션을 찾지 못하는 문제가 있습니다. 구속 조건을 파일에 덤프 할 때 (솔버에서 check()) 호출 직전에 to_smt2() 메서드를 사용하고 독립 실행 형 z3 실행 파일을 통해 파일을 실행하면 약 4 초 내에 시스템을
    c++ z3 2017-01-27

    2열

    1답변

    동적 네트워크에서 신념을 확인하는 Z3Py 예제

    Z3 (또는 Z3Py의 특정 사항)을 더 잘 이해하기 위해 Paper Checking Beliefs in dynamic Networks에서 직접 작성한 예제를 구현하고자했습니다.이 sat Or(And(Var(0) == 5, Var(1) == 2), And(Var(0) == 4, Var(1) == 2), And(Var(0) == 4, Va
    python z3 z3py 2017-01-30

    0열

    1답변

    z3에서 각 변수의 값 범위를 제한 할 수 있습니까?

    예를 들어, 제한이 x + y > 100입니다. 나는 z3가 나를 x의 값을 1이나 2가되도록하고 싶지 않고, z3가 y의 값을 1이나 2가되도록 내 보내지 않기를 바란다. 그래서, x와 y는 우리가 Z3에 이러한 제한을 적용 할 수 있습니다 1 2. 제외하고는 모든 숫자가 될 수 있습니까? 감사합니다.
    z3 z3py 2017-01-31

    1열

    1답변

    z3을 사용하여 Int 도메인 가져 오기

    정수 변수의 특정 도메인을 z3으로 가져 오는 방법이 있습니까? (변수가 유한 도메인에 속한다고 가정) 1 <= X <= 5 2 <= Y <= 8 X + Y == T 내가 얻을 싶습니다 : 는 I는이 제약 설정 다음 한 3 <= T <= 13 심지어 간단한 경우 : 1 <= X <= 10 5 <= X <= 15 내가 싶어를 : 5 <= X
    z3 2017-02-06

    2열

    2답변

    SSA에서 z3 bvsmod 동작 이해

    z3을 사용하여 배우려고합니다. 그래서이 질문은 어리석은 일입니다. 다음 코드에서 bvsmod를 bvadd와 비교했을 때 Z3에서 x___0에 대한 예기치 않은 값이 나타나는 이유는 무엇입니까? SSA를 사용하여 여기에서 실행 흐름을 구현합니다. Z3 지침 : (set-option :pp.bv-literals false) ; ; The code ; x
    z3 2017-02-09

    2열

    1답변

    z3 C++ 인터페이스에서 증명을 활성화하려면 어떻게합니까?

    Z3에서 C++ 인터페이스를 통해 교정을 활성화하려면 어떻게합니까? 나는 다음을 설정하려고 시도했다. 사실을 증명해 보이지만, 그 라인의 주석을 풀면 나중에 proof()를 호출하는 라인의 주석 처리를 제거하기 전에! 추측을 솔루션에 추가하려고 할 때 충돌이 발생한다. 예 C++ 파일의 기능을 바탕으로 : void prove_example2(std::os
    c++ z3 2017-02-11

    0열

    1답변

    재귀 함수가있는 버그?

    z3에서 재귀 함수를 사용하려고합니다. 모델 구성에 버그가 있는지 궁금합니다. 고려 : 여기 (define-fun-rec f ((x Int)) Int (ite (> x 1) (f (- x 1)) 1)) (check-sat) (get-value ((f 0))) f 실제로 단지 바보 같은 방식으로 정의
    recursion z3 2017-02-11

    0열

    1답변

    Z3의 부분 할당

    Z3 SAT 솔버를 사용하여 만족스러운 부울 수식 (형식 : CNF)을 확인했습니다. 수식이 만족 스럽다면 부분 할당을 얻는 데 관심이 있습니다. 내가 OR 게이트에 대한 간단한 수식에 model.partial=true을 시도하고 어떤 부분 할당을받지 못했습니다. 이 작업을 수행하는 방법을 제안 할 수 있습니까? 나는 그것이 부분적이라는 것 이외에 과제에
    z3 sat 2017-01-02
최근 질문