z3 java API中的划分

【问题标题】：The division in the z3 java APIz3 java API中的划分
【发布时间】：2020-10-18 08:54:39
【问题描述】：

我刚刚发现Z3 JAVA API中名为“mkDiv()”的除法是指整数除法，而不是普通的除法。例如：

ArithExpr a = ctx.mkDiv(ctx.mkInt(3),ctx.mkInt(5)).simplify();

a 的结果是“0”但“3/5”。

在tutor 中，除法和整数除法似乎分别是 2 部分： (断言 (= r1 (div a 4))) ;整数除法 (断言 (>= b (/c 3.0))) Z3 java api中的分区在哪里？

【问题讨论】：

标签： java z3 division

【解决方案1】：

mkDiv 将根据其参数做正确的事情。由于您要传递整数，因此它将进行整数除法。要使用实数除法，您需要将实数作为参数传递：

import com.microsoft.z3.*;
  
class A {
   public static void main(String [] args) {
      Context ctx = new Context();
      ArithExpr a = ctx.mkDiv(ctx.mkReal(3),ctx.mkReal(5));
      System.out.println(a.simplify());
   };
};

打印出来：

3/5

【讨论】：