z3 Java API中的划分

编程问答 2022-06-07

问题描述

我刚刚发现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的划分在哪里？

解决方法

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
divisionjavajavaz3