Graph coloring example #198
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Contributor
Author
|
Just noticed that the readme contains outdated information and needs to be updated. |
matthiasgreen
commented
Sep 15, 2025
|
|
||
| fn int_eq<Lbl: Label>(a: IAtom, b: IAtom, model: &mut Model<Lbl>) -> ReifExpr { | ||
| if USE_EQUALITY_LOGIC.get() { | ||
| if a.is_const() && !b.is_const() && b.shift == 0 { |
Contributor
Author
There was a problem hiding this comment.
b.shift can be added/substracted? to a.shift constant in ReifExpr::EqVal(...)
Member
There was a problem hiding this comment.
Could you implement this before I merge?
arbimo
requested changes
Sep 24, 2025
| mod encode; | ||
| mod parse; | ||
|
|
||
| pub static SPECIAL_BRANCHER: EnvParam<bool> = EnvParam::new("ARIES_COLORING_SPECIAL_BRANCHER", "true"); |
Member
There was a problem hiding this comment.
The purpose of EnvParam is to allow exposing deeply buried parameters of the solver. Here you do not have this problem so it should be exposed as a command line parameter (with clap crate?).
| pub fn from_file(path: &Path) -> Self { | ||
| let mut res: Problem = Default::default(); | ||
| assert!(path.is_file()); | ||
| let lines = read_lines(path).expect("File provided was not able to be read."); |
Member
There was a problem hiding this comment.
Suggested change
| let lines = read_lines(path).expect("File provided was not able to be read."); | |
| let lines = read_lines(path).expect("File provided could not be read."); |
| res | ||
| } | ||
|
|
||
| #[allow(unused)] |
|
|
||
| fn int_eq<Lbl: Label>(a: IAtom, b: IAtom, model: &mut Model<Lbl>) -> ReifExpr { | ||
| if USE_EQUALITY_LOGIC.get() { | ||
| if a.is_const() && !b.is_const() && b.shift == 0 { |
Member
There was a problem hiding this comment.
Could you implement this before I merge?
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
A simple crate which encodes and solves graph coloring problems. Used to profile equality logic. A modification was made to the model's eq expression in order for IVar equality to be modeled with Eq logic.