Skip to content

Commit

Permalink
Merge pull request #15 from elsoroka/mykelk-highlight-1
Browse files Browse the repository at this point in the history
Update README.md
  • Loading branch information
elsoroka authored Sep 7, 2023
2 parents c38df61 + 6adfc5e commit 2bf5f78
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ You can read the documentation [here](https://elsoroka.github.io/Satisfiability.

### Solving the vector-valued Boolean problem
(x1 ∧ y1) ∨ (¬x1 ∧ y1) ∧ ... ∧ (xn ∧ yn) ∨ (¬xn ∧ yn)
```
```julia
@satvariable(x[1:n], Bool)
@satvariable(y[1:n], Bool)
expr = (x .∧ y) .∨ (¬x .∧ y)
Expand All @@ -25,7 +25,7 @@ println("x = $(value(x)), y = $(value(y))”)
### Investigating rounding of real numbers
This problem (from Microsoft's [Z3 tutorials](https://microsoft.github.io/z3guide/docs/theories/Arithmetic)) uses mixed integer and real variables to figure out whether there exists a constant `a` and two real numbers `xR` and `yR` such that `round(xR) + round(yR) > a` while `xR + yR < a`.
```
```julia
@satvariable(xR, Real)
@satvariable(yR, Real)
@satvariable(x, Int) # x represents a rounded version of xR
Expand Down Expand Up @@ -64,7 +64,7 @@ println(f(f(x.value)) == x.value) # true
### Proving a bitwise version of de Morgan's law.
In this example we want to show there is NO possible value of x and y such that de Morgan's bitwise law doesn't hold.
```
```julia
@satvariable(x, BitVector, 64)
@satvariable(y, BitVector, 64)
Expand Down

0 comments on commit 2bf5f78

Please sign in to comment.