z3을 점진적으로 사용하고 명제 값없이 모델링하는 방법

Question

점진적으로 Z3 솔버를 사용하는 방법을 알려주시겠습니까? 또한 v.name()을 사용할 때 명제 값이없는 모델을 어떻게 얻을 수 있습니까? 등 을 필요로하지 않으므로, cout<<v.name()<<m.get_const_interp(v); 프로그램을 호출 한 후 모델 집합에서 삭제할 수 있습니까?

Answer 1

Z3 C++ API를 사용하여 점진적으로 문제를 해결하는 방법을 보여주는 새로운 C++ 예제를 추가했습니다. 새로운 예제는 이미 online에 있습니다. 게시물 끝에 예제를 복사했습니다.

두 번째 질문에 대해 Z3에서 모델은 기본적으로 읽기 전용 개체입니다. 당신은 단순히 당신이 상관하지 않는 가치를 무시할 수 있습니다. 원하지 않는 값을 숨기는 모델 객체에 대한 래퍼를 작성할 수도 있습니다.

void incremental_example1() { 
    std::cout << "incremental example1\n"; 
    context c; 
    expr x = c.int_const("x"); 
    solver s(c); 
    s.add(x > 0); 
    std::cout << s.check() << "\n"; 
    // We can add more formulas to the solver 
    s.add(x < 0); 
    // and, invoke s.check() again... 
    std::cout << s.check() << "\n"; 
} 

void incremental_example2() { 
    // In this example, we show how push() and pop() can be used 
    // to remove formulas added to the solver. 
    std::cout << "incremental example2\n"; 
    context c; 
    expr x = c.int_const("x"); 
    solver s(c); 
    s.add(x > 0); 
    std::cout << s.check() << "\n"; 
    // push() creates a backtracking point (aka a snapshot). 
    s.push(); 
    // We can add more formulas to the solver 
    s.add(x < 0); 
    // and, invoke s.check() again... 
    std::cout << s.check() << "\n"; 
    // pop() will remove all formulas added between this pop() and the matching push() 
    s.pop(); 
    // The context is satisfiable again 
    std::cout << s.check() << "\n"; 
    // and contains only x > 0 
    std::cout << s << "\n"; 
} 

void incremental_example3() { 
    // In this example, we show how to use assumptions to "remove" 
    // formulas added to a solver. Actually, we disable them. 
    std::cout << "incremental example3\n"; 
    context c; 
    expr x = c.int_const("x"); 
    solver s(c); 
    s.add(x > 0); 
    std::cout << s.check() << "\n"; 
    // Now, suppose we want to add x < 0 to the solver, but we also want 
    // to be able to disable it later. 
    // To do that, we create an auxiliary Boolean variable 
    expr b = c.bool_const("b"); 
    // and, assert (b implies x < 0) 
    s.add(implies(b, x < 0)); 
    // Now, we check whether s is satisfiable under the assumption "b" is true. 
    expr_vector a1(c); 
    a1.push_back(b); 
    std::cout << s.check(a1) << "\n"; 
    // To "disable" (x > 0), we may just ask with the assumption "not b" or not provide any assumption. 
    std::cout << s.check() << "\n"; 
    expr_vector a2(c); 
    a2.push_back(!b); 
    std::cout << s.check(a2) << "\n"; 
}