Skip to content

Instantly share code, notes, and snippets.

@weirdsmiley

weirdsmiley/ADD_solver.ipynb

Last active August 3, 2021 14:24
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save weirdsmiley/ad6a9dbf3370e96d29f9e90068931d25 to your computer and use it in GitHub Desktop.
Save weirdsmiley/ad6a9dbf3370e96d29f9e90068931d25 to your computer and use it in GitHub Desktop.
Download ZIP
Display the source blob
Display the rendered blob
Raw
ADD_solver.ipynb
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@SavchenkoValeriy
Copy link

Number one problem here is the last clause in all three cases.

If we state that it is always, let's say A <= x + y <= B it will be put as And(x + y >= A, x + y <= B). We don't want to check that because z3 can obviously find an example of when it is true and be done. We need to check that z3 couldn't find any examples that contradict this statement ie its negation: Not(And(x + y >= A, x + y <= B)) == Or(Not(x + y >= A), Not(x + y <= B)) == Or(x + y < A, x + y > B)

In none of these cases you actually check for overflow. OverflowConstraint is more like HaveSameSign. Variables HasMinOverflowed and HasMaxOverflowed are pivotal to your solution, but these are not modeled here in any way.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment