Z3质数 [英] Z3 prime numbers

问题描述

我正在尝试学习z3，这是我编写的第一个程序.

I am trying to learn z3, and this is the first program I write.

在本练习中，我试图确定x是否为素数.如果x为质数，则返回SAT，否则返回UNSAT及其两个因子.

In this exercise, I am trying to determine if x is prime. If x is prime, return SAT, otherwise, return UNSAT alongside with two of its factors.

这是我到目前为止所拥有的 http://rise4fun.com/Z3/STlX

Here is what I have so far http://rise4fun.com/Z3/STlX

我的问题是我认为代码现在没有做任何事情.无论我做什么，它都会返回SAT.即如果我断言7为素数，则返回SAT，如果我断言7不是素数，则返回SAT.

My problem is I don't think the code is doing anything right now. It returns SAT for whatever I do. i.e if I assert that 7 is prime, it returns SAT, if I assert 7 is not prime, it returns SAT.

我不确定递归在z3中如何工作，但是我已经看到了一些示例，并且我试图模仿它们如何进行递归.

I am not sure how recursion works in z3, but I've seen some examples, and I tried to mimic how they did the recursion.

如果你们能够看一下并指示我哪里出问题了，我将非常感激.

If you guys are able to take a look and instruct me where I went wrong, I would be really appreciative.

推荐答案

我很习惯递归地思考，在篡改了几个小时之后，我发现了另一种实现它的方法.对于任何有兴趣的人，这是我的实现.

I'm so used to thinking recursively, after tampering for a few hours, I found another way to implement it. For anyone who's interested, here is my implementation.

http://rise4fun.com/Z3/1miFN

这篇关于Z3质数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！