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

Bound calculations #224

Merged
merged 61 commits into from
Mar 15, 2023
Merged

Bound calculations #224

merged 61 commits into from
Mar 15, 2023

Conversation

Wout4
Copy link
Collaborator

@Wout4 Wout4 commented Feb 13, 2023

No description provided.

@Wout4
Copy link
Collaborator Author

Wout4 commented Feb 13, 2023

branches from not_operator

@Wout4 Wout4 marked this pull request as ready for review March 3, 2023 12:40
Copy link
Collaborator

@tias tias left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have (attempted to) rebase it on top of the CountGlobals branch

some tests are failing though...

code looks otherwise OK but I would have to review it again after rebased on master with countglobals

# Conflicts:
#	cpmpy/expressions/globalconstraints.py
#	tests/test_globalconstraints.py
fixed bounds for Max
@Wout4
Copy link
Collaborator Author

Wout4 commented Mar 6, 2023

Rebased on master with countglobals.
Fixed the errors, was the missing get_bounds function of count, and a typo in the bounds for Maximum

Copy link
Collaborator

@tias tias left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

reworked a little bit, also left 2 final comments.

Otherwise looks good, cleans up flatten nicely

@@ -109,3 +109,12 @@ def eval_comparison(str_op, lhs, rhs):
raise Exception("Not a known comparison:", str_op)


def get_bounds(expr):
# can return floats, use floor and ceil when creating an intvar!
if hasattr(expr,'get_bounds'):
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am not convinced by this.

I think it would be clearer to do
if isinstance(expr): return expr.get_bounds(); else return expr,expr?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This would lead to circular import for Expression, I put the import in the get_bounds function

@@ -353,6 +353,9 @@ def _z3_expr(self, cpm_con, reify=False):
elif rhs_is_expr and rhs.name == "element":
arr, idx = rhs.args
return self._z3_expr(all([(idx == i).implies(Comparison(cpm_con.name, lhs, arr[i])) for i in range(len(arr))]))
if isinstance(lhs,GlobalConstraint) and lhs.name == "count":
# I think this case is covered in the next line
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this case is covered in th enext line, that this 'addition' is from a merge?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

true, I also removed the element case

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(we still have to change the element decomposition to allow indexes out of range, think ignace has that in another pr)

Copy link
Collaborator

@JoD JoD left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks like a nice improvement!

tests/test_expressions.py Show resolved Hide resolved
cpmpy/expressions/core.py Outdated Show resolved Hide resolved
cpmpy/expressions/core.py Outdated Show resolved Hide resolved
cpmpy/expressions/core.py Outdated Show resolved Hide resolved
cpmpy/expressions/core.py Outdated Show resolved Hide resolved
cpmpy/expressions/core.py Outdated Show resolved Hide resolved
cpmpy/expressions/core.py Outdated Show resolved Hide resolved
else:
assert is_num(expr), f"All Expressions should have a get_bounds function, `{expr}`"
if is_bool(expr):
return 0, 1
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a known bool, right? Then we can return 0, 0 or 1, 1, depending on whether the bool is true or false.

@JoD JoD mentioned this pull request Mar 13, 2023
Copy link
Collaborator

@JoD JoD left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pushed fixes. @IgnaceBleukx : can you do a quick sanity check on 5b3361d ? Then we can commit, and global decompose can grab the changes.

@IgnaceBleukx
Copy link
Collaborator

Looks good, maybe some documentation for the get_bounds function would be usefull tho. Especially as we do not guarantee the tightest possible bounds.

Did we do any profiling using bigtest? Maybe thats for a next iteration of this code? It will have a very high impact on the runtime of flatten i think!

Good to merge for me!

@JoD JoD merged commit 8fa6708 into master Mar 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
5 participants