Amir Ebrahimi Amir Ebrahimi - 3 months ago 20
C# Question

Implement arithmetic equal in Z3

I am implementing using Z3 c# API and I want to implement a function with which a variable of type int can be assigned an integer value. What I have thought of is:

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

AddConstraintToSolver(lConstraint);
}


There is some thing wrong when I want to cast the second operand which is an integer into an expression. Does anyone know what I am doing wrong?

Answer

I guess you really want to use iCtx.MkInt(pOperand2) to create an integer constant as opposed to a logical constant.

Thus,

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

      AddConstraintToSolver(lConstraint);
   }
Comments