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

feat: remove explicit literals #115

Draft
wants to merge 70 commits into
base: main
Choose a base branch
from
Draft

feat: remove explicit literals #115

wants to merge 70 commits into from

Conversation

ImkoMarijnissen
Copy link
Contributor

@ImkoMarijnissen ImkoMarijnissen commented Nov 8, 2024 •
edited
Loading

TODOS

  • compute_new and all the others should be removed or refactored
  • There used to be an option for turning off clause-minimisation
  • TODOs in conflict analysis
  • Restore test cases in constraint satisfaction solver
  • Proof logging
  • Core extraction
  • get_conflict_info now clones but should not
  • Doc tests
  • Refactor get_reason_simple
  • Check python interface
  • Remove the backtracking method from conflict analysis context

Issues:

@ImkoMarijnissen ImkoMarijnissen marked this pull request as draft November 8, 2024 13:54
ImkoMarijnissen and others added 15 commits November 11, 2024 09:07
@ImkoMarijnissen
refactor: removing conflict analysis files + moving minimisers to sep…
12c5c0a 
…arate folder
@ImkoMarijnissen
docs: add documentation to conflict analysis + removing printing comm…
41c5ac9 
…ents
@ImkoMarijnissen
fix: fix documentation comments + explaining reasoning in comments + …
1a92e76 
…fixing assertion to match with expected behaviour
@ImkoMarijnissen
fix: wrong assertion, should accept both lower-bounds and not-equals
d48a419
@ImkoMarijnissen
refactor: eagerly replacing implied predicate rather than scanning ov…
030c0a5 
…er nogood
@maartenflippo
refactor: toward fixing the reason system
5dc8ac0
@maartenflippo
Merge branch 'feat/remove-explicit-literals' of github.com:ConSol-Lab…
af63c8f 
…/Pumpkin into feat/remove-explicit-literals
@ImkoMarijnissen
feat: adding back core extraction and the corresponding test cases
8902550
@ImkoMarijnissen
docs: fix documentation test cases
7678b0d
@ImkoMarijnissen
fix: fixing bug in element constraint + updating test solver to use i…
e7a7c6c 
…nternal propagator store
@maartenflippo
refactor: remove all reason.*_new methods
3c00cdf
@maartenflippo
refactor: remove engine::sat module
78c601b
@ImkoMarijnissen
chore: adding back statistic logging + renaming some resolution resol…
12edafb 
…ver fields for clarification
@maartenflippo
refactor: rename ConflictAnalysisNogoodContext to ConflictAnalysisCon…
821868e 
…text
@maartenflippo
Merge branch 'feat/remove-explicit-literals' of github.com:ConSol-Lab…
33392a9 
…/Pumpkin into feat/remove-explicit-literals
maartenflippo and others added 30 commits November 15, 2024 10:06
@maartenflippo
refactor: remove commented code
2796539
@maartenflippo
refactor: deny attributes without reason and fix resulting errors
e0054b7
@ImkoMarijnissen
chore: refactoring autonomous search + cleanup
aae3143
@maartenflippo
docs: conflict resolution documentation
9d6e026
@maartenflippo
refactor: branching module organisation
88b3fc1
@ImkoMarijnissen
refactor: extracting cores + adding docs + cleanup
4d99bce
@ImkoMarijnissen
refactor: moving to enum for the conflict resolver
5e5dd34
@ImkoMarijnissen
chore: refactor of main input
a1af32e
@ImkoMarijnissen
fix: lower-bound unit nogood id could be attached to equality predica…
38492f5 
…te + final element in the heap could be not-equals predicate
@ImkoMarijnissen
refactor: small docs updates + using single pop method which returns …
3b36748 
…option
@ImkoMarijnissen
fix: change lower-bound to upper-bound due to typo
f455d0b
@ImkoMarijnissen
fix: issue in debug helper with rejecting conflict found
894b695
@ImkoMarijnissen
refactor: remove backtrack method from conflict analysis context to a…
b63cd5d 
…void code duplication
@ImkoMarijnissen
refactor: only match one one the type of domain rather than multiple …
4a2d5b9 
…times per loop
@ImkoMarijnissen
refactor: change default brancher to smallest and indomain min
c5659cd
@ImkoMarijnissen
refactor: change default brancher to smallest and indomain min
e882ba6
@ImkoMarijnissen
fix: cannot restart while not having assigned all of the assumptions
b816845
@ImkoMarijnissen
refactor: changing back to old duplicated code due to efficiency issues
561f8a6
@ImkoMarijnissen
fix: change name of executable in msc file to pumpkin-solver
99fa64c
@ImkoMarijnissen
feat: adding statistics for lbd of learned nogoods
bb6f082
@ImkoMarijnissen
fix: put debug assert only in the case that the proof is not being co…
77b8c60 
…mpleted
@ImkoMarijnissen
fix: bumping pyo3 version to avoid clippy warning
ec16d71
@ImkoMarijnissen
fix: detection of underflows and overflows for linear inequalities
c2f7b19
@ImkoMarijnissen
fix: detection of underflows and overflows for linear inequalities
909dba9
@ImkoMarijnissen
fix: debug check should not check whether watcher exists for deleted …
57c5e7f 
…nogoods
@ImkoMarijnissen
Adding back documentation of options
ce73267
@ImkoMarijnissen
chore: remove left over clausal propagator files
98dd426
@ImkoMarijnissen
refactor: allowing nogood removal at higher decision levels than the …
0f5223d 
…root
@ImkoMarijnissen
fix: creating the empty integer clone did not take into account clear…
bb34656 
…ing the updates
@ImkoMarijnissen
fix: checking exactly whether the lazy reason for a propagation was t…
1cfd54a 
…he current nogood when checking whether it is propagating
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@maartenflippo maartenflippo Awaiting requested review from maartenflippo

@EmirDe EmirDe Awaiting requested review from EmirDe

At least 1 approving review is required to merge this pull request.

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
2 participants
@ImkoMarijnissen @maartenflippo