Efficient E-Matching for SMT Solvers

329 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

The lean mathematical library (2019, methodology): “res, utilities, debugging tools, and special purpose automation. All of the following tactics are implemented in Lean as metaprograms, with the exceptions of the core simplification routine,E-matching[19],andcongruenceclosure[54],which are exposed in the metalanguage as atomic procedures. 6.1 Simpli”
MaxSMT-Based Type Inference for Python 3 (2018, methodology): “We use e-matching [6] for instantiating the quantifiers used in the axiomatization of the subtype function (cf.”
egg: Fast and extensible equality saturation (2020, methodology): “This makes egg more efficient for the purpose of equality saturation. egg implements the pattern compilation strategy introduced by de Moura et al. [de Moura and Bjùrner 2007] that is used in state of the art theorem provers [De Moura and Bjùrner 2008].”
Handbook of Satisfiability (2021, unknown): “Several modern SMT solvers have adopted and extended these techniques [73, 23, 105].”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, methodology): “, E-matching [89], require knowledge of the state and terms known by the other theory solvers, this module has access to all equality information from all theory solvers.”
Z3: An Efficient SMT Solver (2008, methodology): “Z3 uses novel algorithms for quantifier instantiation [4] and theory combination [5].”