在 Z3 中实现算术相等

Question

我正在使用 Z3 c# API 实现，我想实现一个函数，可以为 int 类型的变量分配一个整数值。我想到的是：

public void AddEqualOperator2Constraints(Expr pOperand1, int pOperand2)
{
      Expr lOperand2 = iCtx.MkConst(pOperand2, iCtx.MkIntSort());
      BoolExpr lConstraint = iCtx.MkEq((ArithExpr)pOperand1, (ArithExpr)lOperand2);

      AddConstraintToSolver(lConstraint);
}

当我想将第二个操作数（整数）转换为表达式时出了点问题。有谁知道我做错了什么？

Answer 1

我猜你真的想用 iCtx.MkInt(pOperand2) 创建一个整数常量而不是逻辑常量。

因此，

   public void AddEqualOperator2Constraints(Expr pOperand1, int pOperand2)
   {
      BoolExpr lConstraint = iCtx.MkEq((ArithExpr)pOperand1,  iCtx.MkInt(pOperand2));

      AddConstraintToSolver(lConstraint);
   }

在 Z3 中实现算术相等

Implement arithmetic equal in Z3

c#

z3