时间戳

首页 > 解决方案 > z3 java API中的划分

java - z3 java API中的划分

问题描述

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

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

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

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

标签： javaz3division

解决方案

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

推荐阅读