여러 번 실행하면 Z3이 다른 모델을 생성합니다.

Question

저는 ZA와 JAVA 바인딩을 2 년 동안 사용해 왔습니다. 어떤 이유로 든 SMTLib2 코드를 직접 String으로 생성 한 다음 parseSMTLib2String을 사용하여 해당 Z3 Expr을 작성했습니다. 내가 기억할 수있는 한,이 메소드로 정확히 동일한 입력을 두 번 입력 할 때마다 항상 동일한 모델을 갖게됩니다.

하지만 최근에 Java API를 직접 변경하고 ctx.mk...()으로 표현식을 작성하기로 결정했습니다. 기본적으로 String을 생성하고 파싱하지는 않지만 Z3이 Z3 Expr을 빌드하는 작업을 수행하게합니다.

이제 솔버가 실제로 똑같은 코드를 저장하는지 확인하는 동안 다른 모델을 얻게됩니다. 내 자바 코드는 다음과 같이 보입니다 :

static final Context context = new Context(); 
static final Solver solver = context.mkSolver(); 

public static void someFunction(){ 
    solver.add(context.mk...()); // Add some bool expr to the solver 
    Status status = solver.check(); 
    if(status == SATISFIABLE){ 
     System.out.println(solver.getModel()); // Prints different model with same expr 
    } 
} 

내가 만들고있어 1 개 이상의 런타임시 호출 '된 SomeFuncion() "및 점검 표현 context.mk...() 변경. 그러나 프로그램을 두 번 실행하면 동일한 표현 순서가 확인되고 실행마다 다른 모델이 표시되는 경우가 있습니다.

auto-config 매개 변수를 비활성화하고 임의의 시드를 설정하려고 시도했지만 Z3은 여전히 ​​다른 모델을 생성합니다. 나는 바운드 된 정수 변수와 해석되지 않은 함수만을 사용하고 있습니다. 잘못된 방식으로 API를 사용하고 있습니까?

필요한 경우이 질문에 전체 SMTLib2 코드를 추가 할 수 있지만 실제로는 짧지 않고 여러 해석 호출이 포함되어 있습니다 (어느 모델이 한 실행에서 다른 실행으로 다른 모델을 생성하는지조차 알지 못합니다. 그냥 일부는 알고).

정확하게 다음 문장을 읽어야하지만 "Z3은 결정적이며 동일한 입력에 대해 동일한 모델을 만들어야합니다."라는 대답이 구식이거나 (정확하게 이해할 경우) 답변을 찾지 못했습니다. :

Z3 timing variation

Randomness in Z3 Results

different run time for the same code in Z3

편집 : 놀랍게도 다음 코드를 사용하면 항상 동일한 모델을 얻는 것처럼 보이고 Z3은 이제 결정적으로 보입니다. 그러나 잠시 동안 컨텍스트를 메모리에 유지해야하기 때문에 메모리 사용량이 이전 코드와 비교할 때 커집니다. 적은 메모리 사용량으로 동일한 동작을 달성하기 위해 내가 할 수있는 아이디어는 무엇입니까? 여기

public static void someFunction(){ 
    Context context = new Context(); 
    Solver solver = context.mkSolver(); 
    solver.add(context.mk...()); // Add some bool expr to the solver 
    Status status = solver.check(); 
    if(status == SATISFIABLE){ 
     System.out.println(solver.getModel()); // Seem to always print the same model :-) 
    } 
} 

내가 메소드를 호출에서 얻을 "SomeFunction을"여러 번 메모리 소비입니다 :만큼이 같은 문제에 SAT 및 UNSAT 사이를 전환하지 않는 한

Answer 1

, 그것은 아니다 곤충. 당신이 링크 된 답변

하나는 무슨 일이 일어나고 있는지에 대해 설명합니다.

Randomness in Z3 Results

는 "우리가 같은 실행 경로에 두 번 같은 문제를 해결할 수 있다면, Z3는 서로 다른 모델을 생산할 수 있음을 의미하며, Z3의 양수인 내부 고유 ID를 표현식에 적용합니다.내부 ID는 Z3에서 사용되는 일부 휴리스틱 스에서 연결을 끊는 데 사용됩니다. 프로그램의 루프가 표현식을 작성/삭제하고 있음에 유의하십시오. 따라서 각 반복에서 제약 조건을 나타내는 식의 내부 ID가 다를 수 있으므로 결과가 서로 다른 솔루션을 생성 할 수 있습니다. "

구문 분석 중에는 동일한 ID를 할당하는 반면 API는 다를 수 있지만 나는 믿기가 좀 어려울 것입니다 ...

SMT 인코딩에서이 문제가 발생했다면 API에서 표현식을 인쇄 한 다음 구문 분석 할 수 있습니다.

Answer 2

이 이상한 반대의 행동을 일으키는 코드의 특정 부분을 발견했다고 생각합니다. 어쩌면 Z3 전문가가 내가 completel인지 말해 줄 수 있습니다. y 틀렸어.

우선, 내 프로그램을 한 번 실행해도 동일한 코드 (수동 생성 코드 또는 API로 생성 된 코드)가 두 번 시도되면 다른 모델로 끝나는 경우가 있습니다. 그것은 제가 전에는 눈치 채지 못했던 것이고, 이것은 실제로 저에게는 실제 문제가 아닙니다.

하지만 내 주된 관심사는 내 프로그램을 두 번 실행하면 두 번의 실행 중에 똑같은 코드를 검사하면 어떻게됩니까? 내가 수동으로 코드를 생성있을 때

, 나는이 같은 함수 정의와 끝까지 : 지금까지 내가 말할 수있는

(declare-fun var!0() Int) 
(declare-fun var!2() Int) 
(declare-fun var!42() Int) 

(assert (and 
    (or (= var!0 0) (= var!0 1)) 
    (or (= var!2 0) (= var!2 1)) 
    (or (= var!42 0) (= var!42 1)) 
)) 

(define-fun fun ((i! Int)) Int 
    (ite (= i! 0) var!0 
     (ite (= i! 1) var!2 
      (ite (= i! 2) var!42 -1) 
     ) 
    )    
) 

을 (그리고 나는 그것에 대해 읽은 (here 참조를 위해)) , API는 "fun"함수를 정의한 방식을 처리하지 않습니다.

(declare-fun var!0() Int) 
(declare-fun var!2() Int) 
(declare-fun var!42() Int) 

(assert (and 
    (or (= var!0 0) (= var!0 1)) 
    (or (= var!2 0) (= var!2 1)) 
    (or (= var!42 0) (= var!42 1)) 
)) 

(declare-fun fun (Int) Int) 
(assert (forall 
    ((i! Int)) 
    (ite (= i! 0) (= (fun i!) var!0) 
     (ite (= i! 1) (= (fun i!) var!2) 
      (ite (= i! 2) (= (fun i!) var!42) (= (fun i!) -1)) 
     ) 
    ) 
)) 

첫 번째 방법으로, 항상 (또는 적어도 너무 자주는 아니라고 다른 실행에 대한 동일한 코드를 확인하는 것 같다 : 그래서 내가 API로를 정의하는 한 일을 그런 식이었다 나를 위해 진짜 문제) 같은 모델을 제공합니다.

두 번째 방법을 사용하면 다른 실행에 대해 동일한 코드를 확인하면 매우 자주 모델이 제공됩니다.

실제로 Z3이 실제로 어떻게 작동하는지에 관해 내가 드러낸 것의 뒤에 어떤 논리가 있는지 누가 알 수 있습니까?

가능한 한 재현성이 있어야 결과가 나오기 때문에 수동 코드 생성으로 돌아가서 완벽하게 작동하는 것 같습니다. API에서 함수를 직접 정의하고 "forall"메서드를 사용하지 않고도 방금 설명한 내용이 사실인지 아닌지 확인하고 싶습니다.