CS 4240: Compilers and Interpreters, BONUS Project, 1 Project Description Minimize the file a.smt2 such that it preserves the property defined in Definition 1. Definition 1 (Property). Let cvc4 be the provided solver program. We say that the file a.smt2 holds the property iff: • The command “cvc4 --lang=smt2.6 a.smt2” returns “sat”; and • If we replace “set-logic ALL” with “set-logic QF NIA” in a.smt2, the command “cvc4 --lang=smt2.6 a.smt2” returns “unknown”. We have also provided a bash script b.sh to help you check the property. If the file a.smt2 holds the property, the return code of b.sh will be 0. Otherwise, it will return 1. Therefore, an alternative way to define the project goal is that: Minimize the file a.smt2 such that the script b.sh will return 0. 1.1 Evaluation We will determine the file size by running the provided b.sh script. It will count the number of characters in a.smt2 using “wc -c a.smt2”. The original size of a.smt2 is 6547. For your property-preserving file a.smt2, • You will receive 50% of the credit if the file size is smaller than 560; or • You will receive 100% of the credit if the file size is smaller than 260. 2 Provided Code and Expected Output We have provided the solver (cvc4), the input file (a.smt2) and the property testing file (b.sh) at https://faculty.cc.gatech.edu/~qrzhang/course/cs4240/bonus22.tar.bz2. 1
We will use the command “bash b.sh”to decide if a.smt2 is property-preserving. The expected property-preserving output is given as follows: $ bash b.sh sat unknown Correct! The size of a.smt2 is 6547. $ echo $? 0 3 Submission • The minimized a.smt2 file; and • A document that describes the key steps to obtain the final a.smt2 file. 4 Collaboration For this BONUS project, you can form a team of at most two people. We will award identical grades to each member of a given project team, unless members of the team directly register a formal complaint. We assume that the work submitted by each team is their work solely. Any clarification question about the project handout should be posted on the course’s public Piazza message board. Under no condition is it acceptable to use code or source written by another team. 2
