Z3: Поиск всей удовлетворяющей модели в java

Question

Ниже решения я не могу реализовать в java. Пожалуйста, помогите мне. Ниже приведен фрагмент кода, который я пытаюсь реализовать.

я нашел тот же вопрос: 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.In Java у меня есть getModel метод() без каких-либо аргументов ,

Еще один вопрос. Как мы можем реализовать '! =' Внутри add. Например.

s.add (or (a! = S.model() [a], b! = S.model() [b])) Для == у нас есть метод mkEq(), но я не смог найти любой метод, связанный с '! ='.

Я попытался с помощью: s.add (ctx.mkOr (ctx.mkEq (а, ctx.mkNot (s.getModel())), ctx.mkEq (а, 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()))); 
} 

Над кодом работал для меня. У вас есть какие-то предложения.