E-matching for SMT solvers
US8103674B2 · kind B2 · utility
6Cited by
11References
12Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Dec 21, 2007 |
| Grant date | Jan 24, 2012 |
| Priority date | — |
| Expiry date | Aug 4, 2029 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F8/443
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
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.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.