1

Assume that I have asserted some formula P and, after checking satisfiability, obtained from Z3 a partial model for it, let's call it M.

Now, would it be possible to test whether another formula Q can be satisfied by extending, if necessary, the current model M. That is, I want to check whether the formula P and Q is satisfiable but fixing the values that have been assigned by the current partial model.

Alternatively, is it possible to ask Z3 to “complete” a specific partial model? (That is, I still want to obtain partial models; but, in a few cases, I would like to be able to extend a partial model so that I can then evaluate some arbitrary formula Q which might contain constants/functions not assigned by the current model)

4

1 回答 1

2

在你的情况下检查P,提取部分模型M,构造一个公式N,它只是在M中分配的等式的结合,然后检查N 和 Q吗?这应该可以使用 API 直接实现,但使用文本界面可能不太可能。

于 2011-11-28T09:24:04.900 回答