CODEWITHSUNDEEP
z3z3-fixedpoint
ranma42
ranma42

Reputation: 31

How to get multiple constraints in Z3 Fixedpoint?

When running the fragment

(declare-rel mypred (Int Int))
(declare-var A Int)
(declare-var B Int)
(declare-var C Int)
(rule (mypred 1 0))
(rule (mypred 2 1))
(rule (mypred 3 2))
(rule (mypred 4 3))
(rule (mypred 5 4))
(rule (=> (and (mypred C B) (mypred A C)) (mypred A B)))

(query (and (mypred C 2) (mypred 2 B) (mypred B A))
  :print-answer true
)
(query (mypred A 2)
  :print-answer true
)

in z3 (for example on rise4fun http://rise4fun.com/Z3/ ), I get an answers:

sat
(and (query!0 1 1 3) (mypred 2 1) (mypred 3 2) (mypred 1 0))
sat
(and query!16!slice!18 (mypred!slice!17 2))

As expected both queries can be satisfied and Z3 correctly reports that, but I would also like to find out for which values of A,B,C they are satisfied, yet the answer does not provide a direct answer to this.

The arguments of "query!0" do not seem to be the same as those used in the original query and the second part of the answer matches the original query only after reordering. I'm actually coding this with the .NET API, so I can inspect the AST, but I want to avoid trying to match every element of the original query with each of those in the answer (so for example if there was a way to preserve the order, I would be quite happy).

The second query can be satisfied in multiple ways. I'm not currently interested in finding one of them (although this could come useful too), but I would like to know a way to automatically distinguish it from the case where the query has a unique solution.

Is this possible to achieve with Z3 Fixedpoints? How can I do that? (I've seen multiple questions getting the constraints, but I was unable to figure out the exact symbol<->value matching)

Upvotes: 3

Views: 270

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

There are two things to say about what you bring up:

  • The version of Z3 that you used on rise4fun provides non-informative answers in cases like the ones you give. The version checked into the unstable branch (built automatically on different platforms) produces the answer:

    sat

    (and (mypred 3 2) (mypred 1 0) (mypred 2 1))

    sat

    (mypred 3 2)

  • I don't have a satisfactory solution to display bindings of the form A |-> 3. Sorry.

Upvotes: 0

Related Questions