CODEWITHSUNDEEP
z3
Motorhead
Motorhead

Reputation: 968

What happened to the custom theory solver methods in the Z3 API?

I have been reading Nikolai's article on Engineering Theories with Z3 for how to interface a custom decision procedure with Z3. In there several methods such as AssertTheoryAxiom, NewAssignment, and FinalCheck etc are mentioned. However I have been unable to locate them in the most recent (new?) Z3 API at http://research.microsoft.com/en-us/um/redmond/projects/z3/namespace_microsoft_1_1_z3.html. Could someone let me know where they or their replacements are? 2. On a related note I see several new concepts in the interface such as Probes and Tactics. Are these described or explained anywhere?

Upvotes: 1

Views: 263

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

The interface for custom decision procedure is currently deprecated. They can still be used with the old solver API. See the following posts for additional information:

Here is the full list of deprecated APIs. Regarding tactics and probes, see this article, and the Z3 tutorials (Python and SMT 2.0) about it.

Upvotes: 1

Related Questions