如何增量使用z3和沒有命題值的模型？

Question

請問如何遞增地使用求解器Z3？ 此外，當我使用v.name()時，如何得到沒有命題值的模型？ 如，撥打程序cout<<v.name()<<m.get_const_interp(v);後，我們可以得到型號爲 x = 3, p = true, y = 4，因爲我不需要p = true，我可以從這組模型中刪除嗎？

Answer 1

我已經添加了新的C++示例，演示瞭如何使用Z3 C++ API進行增量式求解。新的例子已經可用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"; 
}