User propagators for satisfiability modulo custom theories

Abstract

Die Möglichkeit des vollautomatisierten Beweisens oder Widerlegens von logischen Formeln ist bereits seit längerem Realität geworden. Solver finden heutzutage ihre Anwendung sowohl in der wissenschaftlichen Forschung, als auch in nichtwissenschaftlicher Anwendungssoftware. Die Bandbreite verschiedener Solver und Technologien (SAT, SMT, MIP, CSP, ...) ist groß, wodurch für viele Kategorien von Problemen bereits effiziente Software verfügbar ist; allerdings ist dies nicht in allen Fällen so. Ausgefallenere Problemstellungen können oftmals, wenn überhaupt, nur unter Inkaufnahme von schlechterer Leistung mit bestehenden Systemen gelöst werden. Ein Ansatz, dieses Problem zu lösen, ist es, die benötigten Erweiterungen in bereits bestehende und im Allgemeinen auch schnelle Solver zu integrieren. Diese Arbeit präsentiert User-Propagation, welche im Z3 SMT-Solver implementiert wurde. Diese ermöglicht es Benutzern ohne direkte Änderungen an dem Quellcode des Solvers, in den Argumentationsprozess des Solvers einzugreifen, um so weitere Funktionen (Theorien) hinzuzufügen oder die Performanz beim Lösen konkreter Probleme zu verbessern.Die Arbeitsweise des User-Propagators wird einerseits theoretisch beleuchtet, andererseits werden auch mögliche Probleme und Eigenheiten anhand von konkreten Anwendungsfällen diskutiert.

Finding proofs or counterexamples completely automatically has been reality for quite some time now. In the present days, solvers are used in scientific research, as well as in non-scientific application software. The range of different logic solvers and technologies (SAT, SMT, MIP, CSP, ...) is large. That is why efficient software is already available for solving many categories of problems; but not for all. Users occasionally provide problems that the solver either cannot process at all, or cannot process efficiently. One way to solve this problem is for the user to integrate the requisite extensions into established and general-purpose solvers. This work presents user propagation, which has been implemented in the Z3 SMT solver. User propagation allows users to intervene in the solver's reasoning process without having to change the solver's source code. This way, new features (theories) can be implemented or the solving performance can be improved by exploiting domain-specific knowledge.The operation of the user propagator is first explained theoretically, then some implementation problems and peculiarities are discussed on the basis of concrete use cases.