I'm confused and struggling to understand how two different input formats for Z3 fixedpoint engine are related. Short example: suppose I want to prove the existance of negative numbers. I declare a function that returns 1 for non-negative numbers and 0 for negative and then asking solver to fail if there are arguments for which function returns 0. But there is one restriction: I want solver to respond sat
when there exists at least one negative number and unsat
if all numbers are non-negative.
It is trivially with using declare-rel
and query
format:
(declare-rel f (Int Int))
(declare-rel fail ())
(declare-var n Int)
(declare-var m Int)
(rule (=> (< n 0) (f n 0)))
(rule (=> (>= n 0) (f n 1)))
(rule (=> (and (f n m) (= m 0)) fail))
(query fail)
But it becomes tricky while using pure SMT-LIB2 format (with forall
). For example, straightforward
(set-logic HORN)
(declare-fun f (Int Int) Bool)
(declare-fun fail () Bool)
(assert (forall ((n Int))
(=> (< n 0) (f n 0))))
(assert (forall ((n Int))
(=> (>= n 0) (f n 1))))
(assert (forall ((n Int) (m Int))
(=> (and (f n m) (= m 0)) fail)))
(assert (not fail))
(check-sat)
returns unsat
. Unsurprisingly, changing (= m 0)
to (= m 1)
results the same. We can get sat
only implying fail
from (= m 2)
. The problem is that I can't understand, how to ask solver using this format.
How I'm understanding it at the moment, while using forall
-form we can ask to find only ∀-solutions, i.e. the answer sat
means that solver managed to find interpretation (or invariant) satisfiying all assertions for all values, and unsat
means that there are no such functions. In other words, it tries to prove, putting the 'proof' (the invariant) into the model (obviously, when sat
).
On the contrary, when query
ing the solution in the declare-rel
format solver searches the solution for some variables, just like the constraints are under the ∃-quantifier. In other words, it gives the counter-example. It can only print the invariant in case of unsat
.
I have a couple of questions:
- Am I understanding it correct? I feel like I miss some key ideas. For example, a general idea of how to express
(query ...)
in terms of(assert (forall ...))
will be really helpfull (and will answer question 2 automaticly). - Is there a way to solve such ∃-constraints (outputting
sat
when counterexample was found) with pure SMT-LIB2 format? If yes then how?