混合位向量和简单的布尔变量

本文关键字：布尔 变量 简单 向量 混合 | 更新日期: 2023-09-27 17:55:31

使用Z3求解器的c# API，我想将位向量和普通布尔变量结合起来。为此，我尝试表达向量元素和布尔值之间的等价性：

            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));

对SMT模型提出了类似的问题。

有没有一种更简单、也许更有效的方法来将位向量元素与布尔变量相关联，而不是通过Context.MkExtract和Context.MkEq？

混合位向量和简单的布尔变量

我认为就求解器性能而言，这几乎是最有效的方法。在内部，大多数位向量问题都转换为布尔问题，并且编码中没有任何内容会导致任何不成比例的爆炸。在实现简单性方面，您可以考虑使用命名断言（例如，请参阅此处），但我认为这不会大大简化您的示例。

相关文章：