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?

Answer 1

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.