英文:
The division in the z3 java API
问题
我刚刚发现 Z3 JAVA API 中的 "mkDiv()" 函数指的是整数除法，而不是常规除法。例如：
ArithExpr a = ctx.mkDiv(ctx.mkInt(3), ctx.mkInt(5)).simplify();
上述代码中，a 的结果是 "0" 而不是 "3/5"。
在 教程 中，除法和整数除法似乎是两个不同的部分：
(assert (= r1 (div a 4))) ; 整数除法
(assert (>= b (/ c 3.0)))
在 Z3 的 Java API 中，常规除法应该如何实现呢？
英文:
I just found the division in Z3 JAVA API named "mkDiv()" refers to the integer division but not the normal one. For example:
ArithExpr a = ctx.mkDiv(ctx.mkInt(3),ctx.mkInt(5)).simplify();
the result of a is "0" but "3/5".
In the tutor, the division and integer division seem to be 2 part separately:
(assert (= r1 (div a 4))) ; integer division
(assert (>= b (/ c 3.0)))
where is the division in the Z3 java api?
答案1
得分: 0
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
英文:
mkDiv will do the right thing based on its arguments. Since you are passing integers, it'll do integer division. To use real division, you need to pass real values as arguments:
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());
};
};
This prints:
3/5
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论