Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Rewriter only uses first-order matching #115

Closed
brianhuffman opened this issue Mar 16, 2016 · 1 comment
Closed

Rewriter only uses first-order matching #115

brianhuffman opened this issue Mar 16, 2016 · 1 comment
Labels
type: enhancement Issues describing an improvement to an existing feature or capability

Comments

@brianhuffman
Copy link
Contributor

The saw-core rewriter currently only supports first-order patterns, i.e. patterns without lambdas in them. If the left-hand side of a rewrite rule contains a non-first-order subterm, then that subterm will only match terms that are exactly equal to it.

This means that, for example, the following rewrite rule (which is universally quantified over x) would not match the term map (\y -> 5+y) [1,2,3]:

\x -> map (\y -> x + y) [1, 2, 3] == [x+1, x+2, x+3]

The best thing would be to support "higher order pattern unification", which is implemented in several interactive theorem provers such as Isabelle.
brianhuffman pushed a commit to GaloisInc/saw-core that referenced this issue Mar 16, 2016
improved matcher for rewriteSharedTerm now handles some patterns with…
94e51a8 
… lambdas.

This is a small step toward GaloisInc/saw-script#115.

Note that this matcher cannot handle higher order patterns like

  foo (\x -> ?f x + ?g x)

This matcher can only handle simple patterns like

  foo (\x -> x + ?y)

where the unification variables are not applied to bound variables.
@atomb atomb added the type: enhancement Issues describing an improvement to an existing feature or capability label May 2, 2017
@brianhuffman
Copy link
Contributor Author

Matching with higher-order patterns was implemented in GaloisInc/saw-core@8622d85.

brianhuffman pushed a commit that referenced this issue Apr 26, 2021
Merge pull request #115 from GaloisInc/issue114
40da877 
Fix incorrect implementation of `intModUnOp` in sbv backend.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
type: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@atomb @brianhuffman