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

整数である第2オペランドを式にキャストしたいときには何か問題があります。誰かが私が間違っていることを知っていますか？

Answer 1

本当にiCtx.MkInt（pOperand2）を使用して、論理定数ではなく整数定数を作成したいと思います。その上に追加従って

、

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

     AddConstraintToSolver(lConstraint); 
    }