CODEWITHSUNDEEP
z3smt
John Smith
John Smith

Reputation: 781

Limit scope of defined sort

I am trying to limit the scope of a newly defined sort via SMT-LIB. Doing so would simplify my script by reducing the amount of necessary assertions.

For this I played with define-sort and forall.

(define-sort R () Real)
(assert (forall ((x R)) (< 0 x)))
(declare-const r R)
(check-sat)

But z3 always returns unsat no matter what. So I guess this is not possible. Is it?

Upvotes: 0

Views: 186

Answers (1)

alias
alias

Reputation: 30418

Unfortunately, this is not possible in SMTLib. See this answer for details: Is there an UnsignedIntSort in Z3?

As Christoph pointed out your query is unsat because the quantified assertion is false; which puts the solver in the unsat state, regardless of what other constraints you might have.

In my experience, the best way to deal with these scenarios is to not use SMTLib directly; but instead a higher-level API and use the programmatic features afforded by those environments to spit out all the > 0 constraints as you need them. It's hairy and ugly, but it is the only way to deal with these in SMTLib as it stands today. The only solver that supported this sort of "predicate subtyping" was Yices v1.0 with its own input language, which is no longer supported.

Upvotes: 1

Related Questions