E-MATCHING FOR SMT SOLVERS

Patent №

US 8,103,674

Granted

2012-01-24

Filed 2007

Owner

MICROSOFT CORPORATION

AI components

3

ml · nlp · hardware

Assignment

Recorded

Dataset

AIPD

2023_r1 edition

Application

11962847

Embodiments are introduced which provide for creation of an E-matching code tree index which works on E-graphs to make E-matching more efficient. Use of the E-matching code tree allows performing matching of several patterns simultaneously. Embodiments are also described which provide for the generation of inverted path indexes. An inverted path index may be used to filter an E-graph to determine terms which may potentially match patterns when an E-graph is updated.

AI classification

Natural language1.00
AI hardware0.96
Machine learning0.60
Planning0.49
Knowledge representation0.41
Evolutionary computation0.03
Speech0.00
Vision0.00

Ownership

MICROSOFT CORPORATION

assignment · 202870904

Assignors

DE MOURA, LEONARDO M., BJORNER, NIKOLAJ S.

On an employer assignment, the assignors are typically the inventors.

© 2026 NYSGPT2525 LLC