混合位向量和簡單的布爾變量

Question

使用Z3求解器的c# API，我想結合bitvectors和普通的布爾變量。爲了做到這一點，我試圖表達矢量元素和布爾值之間的等價：

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

一個similar question有人提出了SMT模型。

將bitvector元素與布爾變量相關聯，而不是通過Context.MkExtract和Context.MkEq來更容易或更有效嗎？

Answer 1

我認爲這在解算器性能方面非常有效。在內部，大多數位向量問題都被轉換爲布爾問題，編碼中沒有任何東西會導致任何不成比例的放大。在實現簡單性方面，您可以考慮使用命名斷言（請參閱，例如here），但我認爲這不會大大簡化您的示例。