Z3 prime numbers

Question

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

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.

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

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.

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.

Answer 1

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

Answer 2

The following formula does not achieve what your comment specifies:

; recursively call divides on y++ 
;; as long as y < x
;; Change later to y < sqrt(x)
(declare-fun hasFactors (Int Int) Bool)
(assert
   (and (and (not (divides x y)) 
      (not (hasFactors x (+ y 1)))) (< y x))
)

The first problem is that x, y are free. They are declared as constants before. Your comment says you want to recursively call divides, incrementing y until it reaches x. You can use quantified formulas to specify a relation that satisfies this property. You would have to write something along the lines of:

   (assert (forall ((x Int) (y Int)) (iff (hasFactors x y) (and (< y x) (or (divides y x) (hasFactors x (+ y 1))))))

You would also have to specify which formulas you want to check before calling check-sat. Finding prime numbers using an SMT solver is of course not going to be practical, but will illustrate some of the behavior you get when Z3 instantiates quantifiers, which depending on problem domain and encoding can be either quick or very expensive.

Answer 3

Thanks for the partial solution! A complete solution for isPrime is:

http://rise4fun.com/Z3/jBr0

(define-fun isPrime ((x Int)) Bool
  (and 
    (> x 1) 
    (not (exists ((z Int) (y Int))
      (and (< y x) (< z x) (> y 1) (> z 1) (= x (* y z)))))))

Took me more than I care to admit to get it right.