Decidability of SMT problems

[GrafBlutwurst]

Hi Z3-Team

I'd like to apologize if this is the wrong place to ask since this isn't really a code related issue.

I'm currently working on a project in which i encode a satisfiability algorithm for a particular flavor of dynamic logic in Z3 and am trying to argue if that SAT problem is decidable by showing that i reduce it only to parts of Z3 that are decidable. To that end i have been reading through the available documentation of Z3 as well as the SMT-lib2 but haven't had much luck. So i was wondering:

1. Is there documentation or a paper somewhere with what is implemented in Z3 and which theories or fragments thereof are decidable and which aren't?
2. Or is there even a configuration option for Z3 that would immediatly error out if I'm using a theory that isn't decidable?

A bit of additional background information. I'm working on a dynamic logic over finite trees, specifically JSON. So I'm using the theory of data types to model json as well as non-linear real arithmetic, linear integer arithmetic, strings and booleans to be able to specify various properties.

[NikolajBjorner]

Quantifier -free : UF, LRA, LIA, NRA, DT, BV, AX (arrays with extensionality) are decidable.
Strings: very little is decidable and the implementation is not a decision procedure even for decidable cases.
Some quantified formulas are decidable. It depends on their shape. Prominent examples are EPR formulas. https://z3prover.github.io/slides/q.html

[GrafBlutwurst]

Thanks for moving this to discussions, answering my question. I only use contains and substring of the string theory and my intuition tells me that that fragment should be decidable, that is assuming that universality of regular expressions is decidable in Z3.