z3 java API中的划分

Question

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

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

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

在tutor中，除法和整数除法似乎是分开的两部分：(assert (= r1 (Diva4)；整数除法(assert (>= b (/ c3.0)在Z3 java api中的除法在哪里？

Answer 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