CODEWITHSUNDEEP
c#z3
Amir Ebrahimi
Amir Ebrahimi

Reputation: 115

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?

Upvotes: 1

Views: 138

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

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

Upvotes: 1

Related Questions