Z3：在java中找到所有令人满意的模型

Question

以下解决方案我无法在 java 中实现。请帮我。下面是我正在尝试实现的 sn-p 代码。

我发现了同样的问题： Z3: finding all satisfying models

(Z3Py) checking all solutions for equation

BitVecExpr a = ctx.mkBVConst("a",8);
BitVecExpr b = ctx.mkBVConst("b",8);
BitVecExpr c = ctx.mkBVConst("c",8);
Solver s = ctx.mkSolver();

//s.add(ctx.mkEq(c,ctx.mkBVXOR(a,b)));      // I am able to get distinct value for a and b for XOR.
//s.add(ctx.mkEq(c,ctx.mkBVOR(b,a)));       // If i swap the position of the a and b then i was able to generate distinct pattern. For example for this add method of OR my code was working.
s.add(ctx.mkEq(c,ctx.mkBVOR(a,b)));         // Not working getting same model.
s.add(ctx.mkEq(c,ctx.mkBV(11,8)));

if (s.check() == Status.SATISFIABLE)
{
System.out.println("status :"+ s.check());
Model m = s.getModel();
System.out.println("Model :"+ m);
}

BitVecExpr test1[] = {a,b};

s.add(ctx.mkDistinct(test1));     // If i use this line then only i get distinct pattern

if (s.check() == Status.SATISFIABLE)
{
System.out.println("status :"+ s.check());
Model m = s.getModel();
System.out.println("Model :"+ m);
}

我在 java 中也没有 model()[] 方法。在 java 中我有 getModel() 方法，没有任何参数。

还有一个问题。我们如何在 add 中实现 '!='。例如。

s.add(或(a != s.model()[a], b != s.model()[b])) 对于 == 我们有 mkEq() 方法，但是我找不到任何与 '!=' 相关的方法。

我尝试使用： s.add(ctx.mkOr(ctx.mkEq(a,ctx.mkNot(s.getModel())),ctx.mkEq(a,ctx.mkNot(s.getModel()))));

为此我收到编译错误。我应该得到它，因为它不可能以这种方式实现。

Answer 1

BitVecExpr a = ctx.mkBVConst("a",2);
BitVecExpr b = ctx.mkBVConst("b",2);
BitVecExpr c = ctx.mkBVConst("c",2);
Model m = null;
Solver s = ctx.mkSolver();

s.add(ctx.mkEq(c,ctx.mkBVXOR(a,b)));
s.add(ctx.mkEq(c,ctx.mkBV(3,2)));

while(s.check() == Status.SATISFIABLE){
    System.out.println("status :"+ s.check());
    m = s.getModel();
    System.out.println("m.eval(a) " + m.eval(a,false));
    System.out.println("m.eval(b) " + m.eval(b,false));
    System.out.println("m.eval(c) " + m.eval(c,false));

    Integer b_int = Integer.parseInt(m.eval(b,false).toString());   
    Integer a_int = Integer.parseInt(m.eval(a,false).toString());   
    BoolExpr b_bol = ctx.mkEq(b,(BitVecExpr) ctx.mkBV(b_int,2));
    BoolExpr a_bol = ctx.mkEq(a,(BitVecExpr) ctx.mkBV(a_int,2));
    s.add(ctx.mkOr(ctx.mkEq(b_bol,ctx.mkFalse()),ctx.mkEq(a_bol,ctx.mkFalse())));
}

以上代码对我有用。大家有什么建议吗。