Interpolants with CHCs and Lists

[basus]

I am trying to get interpolants for a sequence of formulas using the approach outlined in Lazy Abstraction with Interpolants. I had posted a question earlier and was pointed to using the CHC solver, but I'm having some trouble figuring out how, especially since my use case involves both Z3 Lists and Arrays. Based on some issues I've seen, I'm doing something like the following:

(set-option :produce-proofs true)
(set-option :fp.engine bmc)

;; A bunch of declare-funs for interpolants
;; A bunch of asserts in Horn clause form
( assert (forall () (=> some-formula interpolant)))

(check-sat-using horn)

A bunch of evals for the interpolant functions

Can someone tell me if this the correct boilerplate I should be using?

[agurfinkel]

Hey @basus, hopefully this will help: https://github.com/agurfinkel/spacer-on-jupyter/blob/master/Dagstuhl2019.ipynb
There is an example of how to compute an interpolant. You have to use spacer as the engine. With bmc, the formula is unrolled and no intermediate solutions (i.e., interpolants) are computed.

Support for ADTs, and the combination of ADTs and Arrays is experimental at best. The current implementation might be sufficient for interpolation, but I think you would be the first user for it. We are working on improving support for ADTs, but the code is not yet in the main z3 repo.

If you run into problems, post a more complete example, and hopefully we will be able to help.

[basus]

Ah ok, I was following the Dagstuhl, but wasn't sure if I was translating it to SMT-lib syntax correctly. I'm currently getting a lot of unknown results, while bmc was producing sat. But I think my formulas are currently not quite right. I will try to fix them and see what happens. I'm also currently using version 4.8.10. Is that good, or should I use a nightly or source version?

[basus]

After working with this a little more, I am realizing the following:

If I set (set-logic HORN) then I get errors of the form (error "line 27 column 24: unknown sort 'List'"). When I do call (check-sat-using horn) I get a sat (which is what I expect), but I think that is spurious?

If I don't have (set-logic HORN) then I don't get those errors, however (check-sat-using horn) becomes unknown as soon as I add a constraint that uses list functions like head or tail.

I can work towards producing a minimal example, but can someone (@agurfinkel maybe?) tell me which of the above approaches I should focus on?

[agurfinkel]

A complete example would be easier to debug. I mostly use the solver through the API and not too familiar with all the errors that are possible from the command line interface.

As I said, ADTs are barely supported in Spacer. Furthermore, since this was a target for fuzzing, extra checks got added to conservatively return unknown.

If you send a complete example, we can sort this out.

[basus]

Ok, here's a minimal-ish example. It has a mix of arrays, lists and ints. If you drop the last assert, Z3 returns sat, but with it I get unknown. I suspect the problem is due to the use of head and tail in that last assert, but I don't know for sure.

(set-option :produce-proofs true)
(set-option :fp.engine spacer)

(declare-const memory_0 (Array Int Int))
(declare-const memory_1 (Array Int Int))
(declare-const memory_2 (Array Int Int))
(declare-const memory_3 (Array Int Int))
(declare-const memory_4 (Array Int Int))

(declare-const stack_0 (List Int))
(declare-const stack_1 (List Int))
(declare-const stack_2 (List Int))
(declare-const stack_3 (List Int))
(declare-const stack_4 (List Int))

(declare-const gas_1 Int)
(declare-const gas_2 Int)
(declare-const gas_3 Int)
(declare-const gas_4 Int)

(declare-fun itp0 ((Array Int Int) (List Int) Int ) Bool)
(declare-fun itp1 ((Array Int Int) (List Int) Int ) Bool)
(declare-fun itp2 ((Array Int Int) (List Int) Int ) Bool)
(declare-fun itp3 ((Array Int Int) (List Int) Int ) Bool)

;; Horn Clauses
(assert
 (forall ((memory_0 (Array Int Int)) (memory_1 (Array Int Int))
          (stack_0 (List Int)) (stack_1 (List Int))
          (gas_1 Int))

         (=> (and (= gas_1 500) (= stack_1 stack_0) (= memory_1 memory_0))
             (itp0 memory_1 stack_1 gas_1))))

(assert
 (forall ((memory_1 (Array Int Int)) (memory_2 (Array Int Int))
          (stack_1 (List Int)) (stack_2 (List Int))
          (gas_1 Int) (gas_2 Int))

         (=> (and (itp0 memory_1 stack_1 gas_1)
                  (and (= gas_2 (- gas_1 3))
                       (= stack_2 (insert 1 stack_1))
                       (= memory_2 memory_1)))
             (itp1 memory_2 stack_2 gas_2))))


(assert
 (forall ((memory_2 (Array Int Int)) (memory_3 (Array Int Int))
          (stack_2 (List Int)) (stack_3 (List Int))
          (gas_2 Int) (gas_3 Int))

         (=> (and (itp1 memory_2 stack_2 gas_2)
                  (and (= gas_3 (- gas_2 3))
                       (= stack_3 (insert 50 stack_2))
                       (= memory_3 memory_2)))
             (itp2 memory_3 stack_3 gas_3 ))))


(assert
 (forall ((memory_3 (Array Int Int)) (memory_4 (Array Int Int))
          (stack_3 (List Int)) (stack_4 (List Int))
          (gas_3 Int) (gas_4 Int))

         (=> (and (itp2 memory_3 stack_3 gas_3)
                  (and (not (= (head (tail stack_3)) 0))
                       (and (= gas_4 gas_3) (= stack_4 stack_3)
                            (= memory_4 memory_3))))
             (itp3 memory_4 stack_4 gas_4))))

(check-sat-using horn)

[basus]

Hi @agurfinkel I wanted to check in and see if you had a chance to look at the example I posted above? I get an unknown result with Z3 4.8.10.