To make sure everything's working, run: pipenv run pytest The documentation explains what this means, but the short version is that to run the code for this homework, either preface commands with pipenv run (e.g., pipenv run python se.py or pipenv run pytest), or run pipenv shell to spawn a new shell inside your virtual environment, where you can just run bare commands like python se.py or pytest. Pipenv creates a virtual environment to avoid clogging up your system's Python install with our dependencies. This might take a while if it needs to compile the Z3 SMT solver from source (e.g., on an Apple Silicon Mac). Now let's install all the packages we need, including for SAT and SMT solving: pipenv install For example, the repository it created for me is called hw2-sat-smt-jamesbornholt, so I would do: git clone hw2-sat-smt-jamesbornholt We'll be using GitHub Classroom to check out and submit this homework.įollow the GitHub Classroom URL on Canvas to create your private copy of the homework repository, and then clone that repository to your machine. Then get Pipenv by running: pip install pipenv Or by running: python -m ensurepip -upgrade Get Pip from either your OS package manager (usually called something like python-pip) You'll also need Pip and Pipenv to set up the dependencies. So make sure you have Python 3 available (at least version 3.7 versions 2.x won't work). Part 2: SMT solving and symbolic executionīoth the SAT and SMT parts of this homework are written in Python,.Later homeworks (and the tools we'll read about) often delegate this reduction to a framework,īut it's helpful to understand how those frameworks workĪnd the interface they use to the underlying solver. In both cases, the focus is on how to reduce a higher-level problem to lower-level SAT or SMT constraintsĪnd then interpret the results returned by the solver.
We'll be solving two problems, one with a SAT solver and one with an SMT solver. The goal of this homework is to introduce you to SAT and SMT solvers and how to use them. Or indirectly use one through a higher-level framework like Rosette or Dafny. Many of the papers we'll read this semester either directly use a SAT or SMT solver,
They provide a type of "assembly language" for specifying and solving logical problems-many problemsĬan be encoded in the form of SAT or SMT constraints and then efficiently solved with an off-the-shelf solver. SAT and SMT solvers are widely used for software verification and synthesis, as well as many other problems. Grading: 5% of your course grade: 3% for Part 1 (SAT solving) and 2% for Part 2 (SMT solving) Homework 2: SAT & SMT solvers - CS 395T: Systems Verification and SynthesisĬS 395T: Systems Verification and Synthesis
0 kommentar(er)
