實現算術等於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); 
    }