Skip to content

Latest commit

 

History

History
27 lines (23 loc) · 1.24 KB

README.md

File metadata and controls

27 lines (23 loc) · 1.24 KB

HW 4: Analysis using Constraints

1. Read through paper:

2. Hand-constraint solving on given example:

A bit of a replication of what's in the paper and what we went over in class however I needed additional work in understanding what exactly was going on.

  1. Identification of constraints on our invariant I.
  2. Application of an invariant template: a1x + a2y + a3 ≥ 0 ∨ a4x + a5y + a6 ≥ 0
  3. Prep for Farkas' Lemma
  4. TODO - Apply Farkas' Lemma (Briefly kicked around some ideas for "automatically" doing these things however decided I wanted to try something more concrete)

3. Install z3 and play around with toy examples

Install z3, peruse the documentation and a couple of quick guides, and run some toy examples. See example files:

  • One trivially solved equation
  • One unsatisfiable equation
  • A couple of tests on basic laws or boolean algebra
  • Example from Gulwani paper (after using invariant template and applying Farkas' Lemma to the first constraint)