Satisfiability Modulo Custom Theories in Z3 (Tool Paper) (VMCAI 2023)

Sun 15 - Sat 21 January 2023 Boston, Massachusetts, United States

Who

Nikolaj Bjørner, Clemens Eisenhofer, Laura Kovács

Track

VMCAI 2023

Time Zone

The program is currently displayed in (GMT-05:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Mon 16 Jan 2023 16:30 - 17:00 at Arlington - Solvers Chair(s): Aws Albarghouthi

Abstract

We introduce user-propagators as a new feature of the Z3 SMT solver. User-propagation allows users to write custom theory extensions for Z3, by implementing callbacks via the Z3 API. These callbacks are invoked by Z3 and eliminate eager processing and instantiation of theory axioms with quantifiers. We report on application scenarios of user-propagation and describe further use-cases.

Nikolaj Bjørner

Microsoft Research

Clemens Eisenhofer

Laura Kovács

TU Wien

Austria