0

Below solution i am not able to implement in java. Please help me. Below is snippet code which i am trying to implement.

I found the same question: 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);
}

Also i don't have model()[] method in java.In java i have getModel() method without any arguments.

One more question. How can we implement '!=' inside add. For example.

s.add(Or(a != s.model()[a], b != s.model()[b])) For == we have mkEq() method, But i was unable to find any method related to '!='.

I tried using: s.add(ctx.mkOr(ctx.mkEq(a,ctx.mkNot(s.getModel())),ctx.mkEq(a,ctx.mkNot(s.getModel()))));

For which i am getting compilation error. Which i should get because its not possible to implement in that way.

Community
  • 1
  • 1
Ajit
  • 31
  • 6

1 Answers1

0
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())));
}

Above code worked for me. Do you guys have any suggestion.

Ajit
  • 31
  • 6
  • @usr please let me know if i am doing anything wrong in my answer. Also do let me know if u have any suggestion. – Ajit Sep 01 '15 at 19:28
  • maybe use ctx.mkNot(x) instead of ctx.mkEq(x, ctx.mkFalse()) you can also retrieve integers using methods defined on expressions instead of using pretty printing + parsing. – Nikolaj Bjorner Sep 08 '15 at 03:38
  • @NikolajBjorner That really make sense. thanks i will in cooperate that change in my design. – Ajit Sep 15 '15 at 18:23