Skip to content

Transform constraints to z3 constraints which is the final step #80110

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

Closed
wants to merge 37 commits into from

Conversation

migeed-z
Copy link
Contributor

@migeed-z migeed-z commented Jun 23, 2022

Stack from ghstack (oldest at bottom):

Differential Revision: D37387508

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

@facebook-github-bot
Copy link
Contributor

facebook-github-bot commented Jun 23, 2022

🔗 Helpful links

✅ No Failures (0 Pending)

As of commit 23cf49f (more details on the Dr. CI page):

Expand to see more

💚 💚 Looks good so far! There are no failures yet. 💚 💚


This comment was automatically generated by Dr. CI (expand for details).

Please report bugs/suggestions to the (internal) Dr. CI Users group.

Click here to manually regenerate this comment.

migeed-z added a commit that referenced this pull request Jun 23, 2022
migeed-z added a commit that referenced this pull request Jun 23, 2022
@migeed-z
Copy link
Contributor Author

@migeed-z has imported this pull request. If you are a Facebook employee, you can view this diff on Phabricator.

1 similar comment
@migeed-z
Copy link
Contributor Author

@migeed-z has imported this pull request. If you are a Facebook employee, you can view this diff on Phabricator.

migeed-z added 11 commits June 23, 2022 17:25
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. 

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. 

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. 

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. 

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. 

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. 

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. 

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. 

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. 

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. 

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. 

[ghstack-poisoned]
migeed-z added 8 commits June 27, 2022 18:09
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
migeed-z added 4 commits June 29, 2022 12:26
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
Copy link
Collaborator

@jamesr66a jamesr66a left a comment

Choose a reason for hiding this comment

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

This is a lot of code, but I like the test coverage so approving. I trust that this will be validated more in the future with the e2e cases

… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
@migeed-z
Copy link
Contributor Author

migeed-z commented Jul 1, 2022

@pytorchbot merge -g

@pytorchmergebot
Copy link
Collaborator

@pytorchbot successfully started a merge job. Check the current status here

… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
@pytorchmergebot
Copy link
Collaborator

Merge failed due to New commits were pushed while merging. Please rerun the merge command.
Raised by https://github.com/pytorch/pytorch/actions/runs/2593467529

… step"


Differential Revision: [D37387508](https://our.internmc.facebook.com/intern/diff/D37387508)

We transform our constraints in a way that can be understood by z3. For example, for a dimension type, instead of Dyn, we encode it as a pair of integers. Some of the other operations are a 1:1 transformation.

contains tests for alexnet and resnet as well as smaller examples

[ghstack-poisoned]
@migeed-z
Copy link
Contributor Author

migeed-z commented Jul 1, 2022

@pytorchbot merge -g

@pytorchmergebot
Copy link
Collaborator

@pytorchbot successfully started a merge job. Check the current status here

@github-actions
Copy link
Contributor

github-actions bot commented Jul 1, 2022

Hey @migeed-z.
You've committed this PR, but it does not have both a 'release notes: ...' and 'topics: ...' label. Please add one of each to the PR. The 'release notes: ...' label should represent the part of PyTorch that this PR changes (fx, autograd, distributed, etc) and the 'topics: ...' label should represent the kind of PR it is (not user facing, new feature, bug fix, perf improvement, etc). The list of valid labels can be found here for the 'release notes: ...' and here for the 'topics: ...'.
For changes that are 'topic: not user facing' there is no need for a release notes label.

@facebook-github-bot facebook-github-bot deleted the gh/migeed-z/6/head branch July 4, 2022 14:18
facebook-github-bot pushed a commit that referenced this pull request Jul 6, 2022
…) (#80110)

Summary:
Pull Request resolved: #80110
Approved by: https://github.com/anijain2305, https://github.com/jamesr66a

Test Plan: contbuild & OSS CI, see https://hud.pytorch.org/commit/pytorch/pytorch/31952b56ebc438a2a331db4221fe03576896fa44

Reviewed By: mehtanirav

Differential Revision: D37578968

Pulled By: migeed-z

fbshipit-source-id: 35507af3210e110ffee558e9ec07b1a4eb5d76a0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants