An Evaluation Algorithm for Datalog with Equality

TL;DR

This paper introduces an efficient evaluation algorithm for relational Horn logic (RHL), an extension of Datalog that includes equality reasoning, enabling advanced applications like points-to analysis and type inference.

Contribution

It presents a novel evaluation algorithm for RHL that integrates congruence closure techniques, expanding Datalog's capabilities for equality reasoning and complex analysis tasks.

Findings

Incorporates congruence closure into Datalog evaluation for efficiency.

Enables implementation of points-to analysis and type inference using RHL.

Forms the foundation of the Eqlog Datalog engine.

Abstract

We describe an evaluation algorithm for relational Horn logic (RHL). RHL extends Datalog with quantification over sorts, existential quantification in conclusions and, crucially, the ability to infer equalities. These capabilities allow RHL evaluation to subsume and expand applications of Datalog and congruence closure algorithms. We explain how aspects of a fast congruence closure algorithm can be incorporated into Datalog evaluation to obtain an efficient RHL evaluation algorithm. We then sketch how Steensgaard's points-to analysis and type inference can be implemented using RHL evaluation. RHL and the evaluation algorithm described here are the foundation of the Eqlog Datalog engine.