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

Davis-Putnam Mode #87

Open
wants to merge 62 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
62 commits
Select commit Hold shift + click to select a range
d75a851
add ⊤ and ⊥
jeninyg Mar 27, 2023
6a510a3
Validate tautology
jssunray34 Mar 27, 2023
aca67bc
Create new modifyDecomposition and add call to validateReduction
jssunray34 Apr 2, 2023
c5b800c
Fix undefined error
jssunray34 Apr 2, 2023
2c8523c
Add reduction rule tests
jssunray34 Apr 2, 2023
036853f
Handle result of validation
jssunray34 Apr 2, 2023
4db7430
add support for DP validator + reducer
jeninyg Apr 2, 2023
d867fc2
Add absorption check
jssunray34 Apr 3, 2023
ac01341
return reduced statement if no base checks passes
jeninyg Apr 3, 2023
eef29d7
Merge branch 'tautology_dp' into DP_complex_reducer
jeninyg Apr 4, 2023
4981043
prettier
jeninyg Apr 4, 2023
91855d0
add Modes to nav bar
mduboef Apr 6, 2023
42be310
Merge pull request #84 from Bram-Hub/Mason-Toggle
mduboef Apr 6, 2023
0615d32
update .gitignore
jeninyg Apr 6, 2023
8b0884b
Add antecedents and decomposition to tree nodes
jssunray34 Apr 8, 2023
f2b5555
isReduced check start
jeninyg Apr 9, 2023
aa97eba
Add support for taut/con
jssunray34 Apr 9, 2023
ed84a24
isDecomposed()
jeninyg Apr 9, 2023
35d8265
isDecomposed
jeninyg Apr 10, 2023
fd766b5
Get tautology check to work
jssunray34 Apr 10, 2023
779d023
debug
jeninyg Apr 10, 2023
eef3e67
prettier
jeninyg Apr 10, 2023
bfa50a8
Modify and add tree node labels
jssunray34 Apr 11, 2023
c02419e
Merge branch 'tautology_dp' into DP_complex_reducer
jeninyg Apr 11, 2023
ed75b71
Merge pull request #83 from Bram-Hub/DP_complex_reducer
jssunray34 Apr 11, 2023
57eb3fc
Code cleanup
jssunray34 Apr 11, 2023
1b508ec
prettier
jssunray34 Apr 11, 2023
729e8bc
Add functionality for closed terminator
jssunray34 Apr 25, 2023
f0a76e5
Create README files
jssunray34 Apr 25, 2023
dee25ce
Update DP_developer_guide.md
jssunray34 Apr 25, 2023
46feaa9
Fix check for branch literal
jssunray34 Apr 26, 2023
0c69c2c
Fix test suite
jssunray34 Apr 26, 2023
d91c9eb
Clean up code/remove extraneous comments/add comments
jssunray34 Apr 26, 2023
242482a
Remove debug prints
jssunray34 Apr 26, 2023
578b224
Fix branch literal check
jssunray34 Apr 26, 2023
77f64c4
Update decomposition text
jssunray34 Apr 26, 2023
661d774
Code cleanup
jssunray34 Apr 26, 2023
9d54094
prettier
jssunray34 Apr 26, 2023
c6b4593
Update DP_developer_guide.md
jssunray34 Apr 26, 2023
b580623
Update README
jssunray34 Apr 26, 2023
bb457a9
Update README
jssunray34 Apr 26, 2023
00312a8
Update README
jssunray34 Apr 26, 2023
8bd4f5a
Fix typos in developer README
jssunray34 Apr 26, 2023
b106f0e
Global button
mduboef Apr 27, 2023
1c6fa21
Make button global
mduboef Apr 27, 2023
6c787d7
Merge pull request #85 from Bram-Hub/closed_terminator_fix
jssunray34 Apr 27, 2023
011e506
Update DP_userguide.md
jeninyg Apr 27, 2023
b6f1a02
Button Text & tree.ts checks
mduboef Apr 27, 2023
70c130e
Merge branch 'tautology_dp' into Mason-Toggle
jssunray34 Apr 28, 2023
bd76981
Merge pull request #86 from Bram-Hub/Mason-Toggle
jssunray34 Apr 28, 2023
5f192e0
Enable switching between modes
jssunray34 Apr 28, 2023
af5d03c
Add test DP trees
jssunray34 Apr 28, 2023
1586016
Fix bug with closed terminator and highlight toggle button on hover
jssunray34 Apr 28, 2023
3434faa
Fix bug with deleting statements
jssunray34 Apr 28, 2023
811b51d
Update README
jssunray34 Apr 28, 2023
f8479fa
Make it truth tree mode by default
jssunray34 Apr 28, 2023
46dfe18
Merge branch 'tautology_dp' of https://github.com/Bram-Hub/Willow int…
jssunray34 Apr 28, 2023
ca5e537
Update README
jssunray34 Apr 28, 2023
80c86e6
Update user guide
jssunray34 Apr 28, 2023
2e02ccf
Update user guide
jssunray34 Apr 28, 2023
cae7cbb
Update user guide
jssunray34 Apr 28, 2023
24b2e83
Update developer guide
jssunray34 Apr 28, 2023
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 developer guide
jssunray34 authored Apr 28, 2023

Verified

This commit was signed with the committer’s verified signature.
agostbiro Agost Biro
commit 24b2e8314a0394250b03a1333b85bf96fa4b8996
2 changes: 2 additions & 0 deletions DP_developer_guide.md
Original file line number Diff line number Diff line change
@@ -6,6 +6,8 @@

When designing an implementation of Davis-Putnam (DP) supported by Willow, we wanted to utilize as much of the existing functionality as possible. Below are the major changes and additions that were made.

**Note**: old `.willow` files are no longer supported. This is due to DP statements having 2 antecedents (a parent statement and literal branch), changing the structure of the tree.

1. **By default two branches are created**: This feature was not a requirement for our project, but it made our lives easier. Plus, it was requested by Bram. :)

https://user-images.githubusercontent.com/55996087/235219000-896ab2e9-242e-4622-b0d1-42ff31878bb8.mov