E-matching for SMT solvers

摘要

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.