0

The problem I'm working on involves making sure that certain variables be perfect squares.

As far as I understood, there is no native support for sqrt in z3 (yet). My idea was to simply have an array with the first say 300 squares and check if the variable is included. How would I go about that?

As I'm frankly not extremely proficient in z3, there might be better suggestions on how to approach the problem, open for anything!

S. L.
  • 630
  • 8
  • 19

1 Answers1

1

Without knowing exactly what you are trying to do it is hard to come up with good advice here. But, perhaps you don't need sqrt? If all you want are numbers that are perfect squares, then you can go the other way around:

(declare-fun sqrtx () Int)
(declare-fun x     () Int)

; this will make sure x is a perfect square:
(assert (and (>= sqrtx 0) (= x (* sqrtx sqrtx))))

; make it interesting:
(assert (> x 10))

(check-sat)
(get-value (x sqrtx))

This prints:

sat
((x 16)
 (sqrtx 4))

In essence, for each "perfect-square" you want, you can declare a ghost variable and assert the required relation.

Note that this gives rise to nonlinearity (since you're multiplying two symbolic values), so the solver might have a hard time handling all your constraints. But without seeing what you're actually trying to do, I think this would be the simplest approach to having perfect squares and reasoning with them.

alias
  • 28,120
  • 2
  • 23
  • 40
  • I used your approach but getting an "incomplete theory arithmetic" exception (see code [here](https://stackoverflow.com/questions/54326110/z3-returns-model-not-available)) any idea why? – S. L. Jan 23 '19 at 13:14
  • 1
    You're running into what I alluded as "nonlinearity," unfortunately. SMT solvers are not good at solving non-linear integer problems, where you mutliply two symbolic integer values. – alias Jan 23 '19 at 17:19