Type checking with datatypes

[LeventErkok]

For this benchmark:

(set-option :produce-models true)
(set-logic ALL)
(declare-datatypes ((S 1)) ((par (T) ((X (getX T))))))
(declare-fun x () (S Int))
(define-fun  y () (S (S Int)) (X x))
(assert ((_ is X) y))
(check-sat)
(get-model)

I'm getting:

(error "line 6 column 15: ambiguous function declaration reference, provide full signature to disumbiguate (<symbol> (<sort>*) <sort>) X")

There seems to be at least two issues here:

1. The type shouldn't be ambiguous; as y has a fully specified type.
2. Even if I'm willing to provide a signature, I can't figure out how to write one. I tried variations on (as X (S Int) (S (S Int))) but couldn't get past the syntax-error checking phase.

As a data-point, cvc4 is happy with the benchmark as is. Though I know this is rather a weak argument and they had issues as well.

If Z3 is complaining rightly, what sort of ascription can I provide to help it along?

[NikolajBjorner]

Z3's parser does type resolution left to right, so it doesn't know y when it parses (_ is X). Here is what you can do:

  (define-sort S1I () (S Int))
  (define-sort S2I () (S (S Int)))
  (assert ((_ is (X (S1I) S2I)) y))
  (check-sat)
  (get-model)

or you can:

  (assert ((_ is (X ((S Int)) (S (S Int)))) y))

You can also just write:

 (assert (is-X y))

but this is not SMT-LIB2.

[LeventErkok]

Thanks! the is-X syntax works just fine and easy for me to use.

It'd be nice to be SMTLib compliant of course, but feel free to close this ticket if there isn't enough ROI for you; especially given there's a good work around.

[NikolajBjorner]

Note that

   (assert ((_ is (X ((S Int)) (S (S Int)))) y))

is the SMT-LIB2 syntax. So a tool that produces strings may use this across solvers. Your attempt was missing a parenthesis: one parenthesis for domain sorts, one parenthesis for (S Int).

[LeventErkok]

Thank you! This does indeed work and I switched my code to use it. Much appreciated.