I think this is pretty much the most efficient way in terms of solver performance. Internally, most bit-vector problems are translated into Boolean problems and there is nothing in your encoding that would cause any disproportionate blow-up. In terms of implementation simplicity, you could consider using named assertions (see e.g. here), but I don't think it would greatly simplify your example.
Mixing bitvectors and simple boolean variables
Question
Using the c# API
of the Z3
solver, I would like to combine bitvectors and ordinary boolean variables. To do that, I've tried to express an equivalence between vector elements and the booleans:
Context ctx = new Context();
BitVecSort bvs = ctx.MkBitVecSort(729);
BitVecNum bvTrue = ctx.MkBV(1, 1); // single-bit vector true
BitVecExpr x = (BitVecExpr)ctx.MkConst("x", bvs);
BitVecExpr y = (BitVecExpr)ctx.MkConst("y", bvs);
BoolExpr eq = ctx.MkEq(x, y);
BoolExpr bx = ctx.MkBoolConst("bx");
BoolExpr by = ctx.MkBoolConst("by");
Solver s = ctx.MkSolver("QF_BV");
BitVecExpr exx = ctx.MkExtract(0, 0, x);
BoolExpr x1 = ctx.MkEq(exx, bvTrue);
BoolExpr bx0 = ctx.MkEq(bx, x1);
BitVecExpr exy = ctx.MkExtract(0, 0, y);
BoolExpr y1 = ctx.MkEq(exy, bvTrue);
BoolExpr by0 = ctx.MkEq(by, y1);
s.Assert(by);
s.Assert(bx0);
s.Assert(by0);
s.Assert(eq);
Status res = s.Check();
Console.WriteLine("bx " + s.Model.Eval(bx));
Console.WriteLine("by " + s.Model.Eval(by));
A similar question was raised for SMT
models.
Is there an easier and perhaps more efficient way to relate a bitvector element to a boolean variable rather than to go via Context.MkExtract
and Context.MkEq
?
La solution
Licencié sous: CC-BY-SA avec attribution
Non affilié à StackOverflow