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.

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

new feature: rewrite rules #15

Draft
wants to merge 24 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
5262b67
update rewriter concept
timbeurskens Feb 22, 2022
6f1513d
add peano natural numbers example
timbeurskens Feb 23, 2022
29a7585
update experimental readme
timbeurskens Feb 24, 2022
9995e1b
work on rewriter
Feb 24, 2022
811822e
implement syntax for rule rewriting
timbeurskens Feb 26, 2022
508306b
reformat
timbeurskens Feb 26, 2022
009e2e0
work on parse-tree modification for rewrite rules
Feb 26, 2022
0d03003
move parameters to object self
Feb 27, 2022
e482239
Merge branch 'master' into rewrite-rules
timbeurskens Mar 1, 2022
4c5b018
Merge branch 'master' into rewrite-rules
timbeurskens Mar 1, 2022
1e79571
update versioning for cli to follow package version. bump queengen ve…
timbeurskens Mar 1, 2022
18ed980
update transitivity description
timbeurskens Mar 1, 2022
f7bd859
reformat rewriter
timbeurskens Mar 7, 2022
d9eef8c
reformat library file
timbeurskens Mar 7, 2022
52dce9e
Merge branch 'master' into rewrite-rules
timbeurskens Mar 7, 2022
a76fa1c
reorder libs
timbeurskens Mar 7, 2022
b1d3b3e
Merge branch 'master' into rewrite-rules
timbeurskens Mar 28, 2022
8cb722d
fix issues after merge
timbeurskens Mar 28, 2022
7a81989
Merge branch 'master' into rewrite-rules
timbeurskens Apr 5, 2022
e092ba1
Merge branch 'master' into rewrite-rules
timbeurskens Apr 16, 2022
7f4f076
Merge branch 'master' into rewrite-rules
timbeurskens Jun 20, 2022
1000817
add missing match arms
timbeurskens Jun 20, 2022
4c706c7
extend background info for rewrite rules
timbeurskens Jul 21, 2022
ecd60c2
update description and dependencies
timbeurskens Jul 26, 2022
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
update description and dependencies
timbeurskens committed Jul 26, 2022
commit ecd60c2161b92267a71778022dc3c7171f98ec4e
16 changes: 8 additions & 8 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

3 changes: 3 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
@@ -185,6 +185,8 @@ It is therefore possible that the rewrite operator and the implication operator
For extra clarity, the rewrite operator `->` differs from the implication operator `=>` in this design document.
For every formula requiring a rewrite, every rewrite rule must be satisfied (conjunction of all rules).

_this information is outdated_

Rewrite rules should be specified in a separate file with the `-r` or `--rules` parameter _Note: this complicates unix piping unfortunately._ The formula to be evaluated should not contain any rewrite rules. Rewrite rules are allowed in input formulas (and actually encouraged!).

**Rewriting:**
@@ -194,6 +196,7 @@ The environment is updated (recursively), where the rule application is now an a
Until the formula is closed (no remaining variables), the algorithm tries to match any open rewrite rule to an assumption in the environment.
If a match has been found for some rewrite rule `x -> y`, `x` is replaced by `true`. If no match can be found for the rule, `x` is replaced by `false`.
A rewrite rule `false -> y` can be rewritten to `true` by `rewrite elimination`. A rewrite rule `true -> y` can be rewritten to `y` by `rewrite elimination`.
This approach could result in hidden bugs: if none of the rules match, the formula evaluates to `true` and terminates. In reality, the formula is likely unsolvable. A possible solution: the original formula is kept, subject to the environment of all rewrite rules (and introduced assumption(s) as a rewrite rule mapping to true). This environment is then recursively solved by invoking the SAT solver and rewriter alternatingly.

The rewrite system allows for modularity in theories: the peano axioms can be expressed in a separate `peano.l` theory file, which can be dynamically loaded upon invoking `rsbdd -l peano.l` (or the shorthand `rsbdd -lpeano`). Any evaluations will be subject to the included theories, e.g. `rsbdd -lpeano -e "1+1=2"`.