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

20210622 chrono-BT again #118

Merged
merged 37 commits into from
Jul 9, 2021
Merged

20210622 chrono-BT again #118

merged 37 commits into from
Jul 9, 2021

Conversation

shnarazk
Copy link
Owner

@shnarazk shnarazk commented Jul 5, 2021 •
edited
Loading

It seems that all bugs #115, #113, #115, #116, #117 were caused by pointing a wrong index by q_head in cancel_until.
so it's time to close them and this branch. So The blocker is:

  • resolve RAT-check failed #122
  • pass ucpc T56.2.0.cnf
  • pass ucpc aes.cnf taking 20000 sec at least. 🎉 🎉 🎉 🎉
  • pass ucpc aes.cnf again 🎉 🎉 🎉 🎉 🎉 🎉 🎉 🎉 🎉
  • and pass ucpc aes.cnf once more. 🎉 🎉 🎉 🎉 🎉 🎉 🎉 🎉 🎉🎉 🎉 🎉 🎉 🎉 🎉 🎉 🎉 🎉🎉 🎉 🎉 🎉 🎉 🎉 🎉
  • unif-k3-r4.25-v360-c1530-S1028159446-096.cnf
  • unif-k3-r4.25-v360-c1530-S253750560-086.cnf
  • unif-k3-r4.25-v360-c1530-S1369720750-015.cnf
  • unif-k3-r4.25-v360-c1530-S305156909-031.cnf
  • unif-k3-r4.25-v360-c1530-S1906521511-089.cnf
  • unif-k3-r4.25-v360-c1530-S367138237-029.cnf
  • unif-k3-r4.25-v360-c1530-S2025517367-061.cnf
  • unif-k3-r4.25-v360-c1530-S404185236-001.cnf
  • unif-k3-r4.25-v360-c1530-S23373420-028.cnf
  • unif-k3-r4.25-v360-c1530-S680239195-053.cnf

@shnarazk
fix wrong accesses to entries in cdb.bi_clause
f89953b
@shnarazk
(handle_conflict) tried to assert a var without backtrack
9215406
@shnarazk
(AssignReason) no more default
d75235b
@shnarazk
(transform_by_restoring_watch_cache) tiny change
5f452b5
@shnarazk
another site using a wrong access to cdb.bi_clause
d494871
@shnarazk
+assertions
eff8d6a
@shnarazk
assertions; records of propagations
a5a705c
@shnarazk
revise clause transitions with more assertions
fb087fb
@shnarazk
revise chronoBT
15d98c2
@shnarazk
resolve #114
1e5ac29
@shnarazk
add interactive assignment browser
d56a426
@shnarazk
(PropagateIF::assign_by_implication) revise arguments' types to encap…
32c1651 
…sulate AssignReason
@shnarazk
ditto
49f658f
@shnarazk
(cancel_until) commit the remaining changes
eed3111
@shnarazk
+-assertions
5f2b30b
@shnarazk
(propagate_sandbox, vivify) stop calling ad-hoc functions
fbd47d9
@shnarazk
cargo clippy
3b07f42
@shnarazk
(strengthen_clause) check the return value of `transform_by_eliminati…
a513e99 
…on` rigidly
@shnarazk
(handle_conflict, conflict_analyze) REVISED
0459682
@shnarazk
rewrite to handle inconsistent messages by rustc and cargo clippy
7279eb8
@shnarazk
(clear_asserted_literals) revise
92073c7
@shnarazk
(vivify.rs) revised
9774424
@shnarazk
cargo clippy
33a4313
@shnarazk
-assertions
48b9dcf
@shnarazk
resolve #117
c25e8fa
@shnarazk shnarazk added the bug Something isn't working label Jul 5, 2021
@shnarazk shnarazk self-assigned this Jul 5, 2021
This was linked to issues Jul 5, 2021
Assigned but not propagated! #117
Closed
A cache of a literal watch can hold a literal which is satisfied at a higher level #116
Closed
Correctness of the model extender #115
Closed
This was linked to issues Jul 5, 2021
Fail to propagate by (bi)clauses #113
Closed
Some transition fails to update watch literal pairs rigidly #119
Closed
@shnarazk shnarazk linked an issue Jul 5, 2021 that may be closed by this pull request
Assignment traversing needs a special handling for ChronoBT #120
Closed
@shnarazk shnarazk linked an issue Jul 7, 2021 that may be closed by this pull request
RAT-check failed #122
Closed
5 tasks
@shnarazk
Copy link
Owner Author

shnarazk commented Jul 9, 2021

fix the longstanding bug about chronoBT.

@shnarazk shnarazk merged commit 16c4e20 into 20210606-watch-cache-optimization Jul 9, 2021
shnarazk added a commit that referenced this pull request Jul 9, 2021
@shnarazk
fix bugs about chronoBT (#118, #123)
aae6ef3 
- revise `ClauseDBIF` to encapsulate internal state transitions
- `AssignReason` has 4 states
- re-implement `AssignStack::extend_model` using `Range` and iterators
@shnarazk shnarazk mentioned this pull request Jul 10, 2021
Merged
15 tasks
shnarazk added a commit that referenced this pull request Jul 10, 2021
@shnarazk
Splr-0.10.0 from dev-0.7.1 (#88)
6eb33fb 
- fix bugs about clause eliminator (#94)
- fix bugs about chronoBT (#118, #123)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@shnarazk shnarazk

Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
1 participant
@shnarazk