Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:fixed-width_bitvectors [2008/03/13 11:25] vkuncak |
sav08:fixed-width_bitvectors [2008/03/13 11:28] vkuncak |
||
|---|---|---|---|
| Line 46: | Line 46: | ||
| ++How to express inverse operations for nested terms?|Flat form of formulas.++ | ++How to express inverse operations for nested terms?|Flat form of formulas.++ | ||
| - | Additional pre-processing is useful: | + | Additional pre-processing is useful. Much more on such encodings we will see later, and can also be found here: |
| * [[http://www.springerlink.com/content/t57g3616p4756140/|Bitvectors and Arrays]] | * [[http://www.springerlink.com/content/t57g3616p4756140/|Bitvectors and Arrays]] | ||
| + | * [[http://www.decision-procedures.org/]] | ||
| Later we will see how to prove that linear arithmetic holds for //all// bounds and not just given one. | Later we will see how to prove that linear arithmetic holds for //all// bounds and not just given one. | ||