Invariants from API != Z3 binary

[leonardoalt]

I'm using Z3/Spacer via the C++ API, and after an UNSAT query, get_answer() returns F1. When I dump the smtlib2 file (https://pastebin.com/Zz8wTFBJ) and solve it with the Z3 binary, it returns F2, which looks a lot nicer (I'm interested in invariants for interface_C_65_0).

F1:

(let ((a!1 (exists ((x!1 Int) (x!2 Int))
             (let ((a!1 (or (= x!1 0) (not (<= (div x!2 x!1) 0))))
                   (a!2 (not (<= (* (div x!2 x!1) x!1) 0)))
                   (a!3 (or (not (<= (div x!2 x!1)
                                     115792089237316195423570985008687907853269984665640564039457584007913129639935))
                            (not (<= 0 (div x!2 x!1))))))
             (let ((a!4 (ite a!3
                             (<= (mod (div x!2 x!1)
                                      115792089237316195423570985008687907853269984665640564039457584007913129639936)
                                 0)
                             (<= (div x!2 x!1) 0))))
               (and a!1
                    (or a!2 (<= x!1 0))
                    (not (= x!1 0))
                    (>= x!2 0)
                    (>= x!1 0)
                    (<= x!2
                        115792089237316195423570985008687907853269984665640564039457584007913129639935)
                    (<= x!1
                        115792089237316195423570985008687907853269984665640564039457584007913129639935)
                    (not (<= x!1 0))
                    a!4)))))
      (a!2 (forall ((A Int) (B Int))
             (let ((a!1 (or (= B 0) (not (<= (div A B) 0))))
                   (a!2 (not (<= (* (div A B) B) 0))))
               (= (interface_C_65_0 A B) (and a!1 (or a!2 (<= B 0)))))))
      (a!3 (forall ((A Int) (B Int))
             (let ((a!1 (or (= B 0) (not (<= (div A B) 0))))
                   (a!2 (not (<= (* (div A B) B) 0))))
               (= (function_average_64_0 A B) (and a!1 (or a!2 (<= B 0)))))))
      (a!4 (forall ((A Int) (B Int))
             (let ((a!1 (or (= B 0) (not (<= (div A B) 0))))
                   (a!2 (not (<= (* (div A B) B) 0))))
               (= (function_fallback_38_0 A B) (and a!1 (or a!2 (<= B 0))))))))
  (and (= error_0 a!1)
       a!2
       a!3
       a!4
       (forall ((A Int) (B Int)) (= (constructor_C_65_0 A B) true))))

F2:

(forall ((A Int) (B Int))
  (let ((a!1 (+ A (* (- 1) (ite (>= B 0) B (* (- 1) B))))))
    (= (interface_C_65_0 A B) (>= a!1 0))))

Any insights on the difference?

[agurfinkel]

In theory, there should not be a difference between C++ and command line interface. In practice, it depends how you use the C++ interface.

If you can share your C++ code, I can take a deeper look. It is also convenient to try the python interface. It should have same behavior as C++, but is easier to share.

On Thu, May 23, 2019 at 15:09 Leonardo notifications@github.com wrote:

I'm using Z3/Spacer via the C++ API, and after an UNSAT query, get_answer() returns F1. When I dump the smtlib2 file ( https://pastebin.com/Zz8wTFBJ) and solve it with the Z3 binary, it returns F2, which looks a lot nicer (I'm interested in invariants for interface_C_65_0).

F1:

(let ((a!1 (exists ((x!1 Int) (x!2 Int)) (let ((a!1 (or (= x!1 0) (not (<= (div x!2 x!1) 0)))) (a!2 (not (<= ( (div x!2 x!1) x!1) 0))) (a!3 (or (not (<= (div x!2 x!1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (not (<= 0 (div x!2 x!1)))))) (let ((a!4 (ite a!3 (<= (mod (div x!2 x!1) 115792089237316195423570985008687907853269984665640564039457584007913129639936) 0) (<= (div x!2 x!1) 0)))) (and a!1 (or a!2 (<= x!1 0)) (not (= x!1 0)) (>= x!2 0) (>= x!1 0) (<= x!2 115792089237316195423570985008687907853269984665640564039457584007913129639935) (<= x!1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (not (<= x!1 0)) a!4))))) (a!2 (forall ((A Int) (B Int)) (let ((a!1 (or (= B 0) (not (<= (div A B) 0)))) (a!2 (not (<= ( (div A B) B) 0)))) (= (interface_C_65_0 A B) (and a!1 (or a!2 (<= B 0))))))) (a!3 (forall ((A Int) (B Int)) (let ((a!1 (or (= B 0) (not (<= (div A B) 0)))) (a!2 (not (<= ( (div A B) B) 0)))) (= (function_average_64_0 A B) (and a!1 (or a!2 (<= B 0))))))) (a!4 (forall ((A Int) (B Int)) (let ((a!1 (or (= B 0) (not (<= (div A B) 0)))) (a!2 (not (<= ( (div A B) B) 0)))) (= (function_fallback_38_0 A B) (and a!1 (or a!2 (<= B 0)))))))) (and (= error_0 a!1) a!2 a!3 a!4 (forall ((A Int) (B Int)) (= (constructor_C_65_0 A B) true))))

F2:

(forall ((A Int) (B Int)) (let ((a!1 (+ A ( (- 1) (ite (>= B 0) B ( (- 1) B)))))) (= (interface_C_65_0 A B) (>= a!1 0))))

Any insights on the difference?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/Z3Prover/z3/issues/2295?email_source=notifications&email_token=ABOM3Z6DEFEFLGWPDGZYTLDPWZ3PXA5CNFSM4HO667OKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4GVNXDWQ, or mute the thread https://github.com/notifications/unsubscribe-auth/ABOM3Z5NJ3GUBQEQZJ5LVHTPWZ3PXANCNFSM4HO667OA .

-- On the move ...

[leonardoalt]

Sure, I can share it, but the rules are created dynamically from a Solidity source code. The code is in this branch: https://github.com/ethereum/solidity/tree/smt_chc The Solidity input that led to this example is https://pastebin.com/sGKC0we9

[leonardoalt]

The docs for function Z3_API Z3_fixedpoint_query_from_lvl in api/z3_spacer.h say:

query returns
- \c Z3_L_FALSE if the query is unsatisfiable.
- \c Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.

I'm now wondering whether it makes sense to call get_answer() when unsat.

[leonardoalt]

Ok I checked spacer_context.cpp and display_certificate has the same behavior as get_answer.

[agurfinkel]

When query is unsat, get_answer will return the definition of the predicates that witnesses that query cannot be reached. This is an inductive invariant. When query is sat, get_answer will return a resolution refutation showing how to reach the query. The refutation format is still a little in flux. If you have issues with the current format, let me know.

[agurfinkel]

For the repro, perhaps you can generate a log using Z3_open_log. This would be easier than rebuilding the compiler.

[agurfinkel]

I just realized that the example uses non-linear arithmetic (div x!2 x!1). This is not supported and causes strange behaviour in the solver. In particular, assertions are triggered all over the place. I am not confident that the final computed solution is correct.

Is it possible to encode your problem without using non-linear arithmetic?

[leonardoalt]

Unfortunately in this case not, since the assertion is about the division. But I do have more examples without nonlinear. I'll check whether the same behavior happens there (API invariants different from command line).

I think the invariant in this case is right though. It is a bit weaker than what I would expect (A >= B), but I think it's sound.

[leonardoalt]

@agurfinkel I changed the way the rules are built and I'm now getting nice looking invariants from the API too, so closing this. Thanks!