This prototype, written in Standard ML (SML), takes in two SML programs and outputs an SMT formula which is valid only if the two programs are equivalent. One can then check whether the output SMT formula is valid by using an SMT Solver such as z3. Two programs can be recognized as equivalent only if they can be proven to be equivalent (by virtue of z3 proving that the produced SMT formula is valid), and if they structured similarly (indicating underlying algorithmic similarities).
This requires that SML and z3 should be installed. Once installed, Zeus can be initiated by the command sml -m "sources.cm". This will bring up an interactive REPL from which Zeus can be run.
To compare two individual programs to each other:
First put the two programs you want to compare in two different files and give the expressions you wish to compare a shared name. Then, from the top-level REPL, run Top.isomorphic "file1" "file2" "name_of_expression";. This will output true if the two expressions are found to be equivalent, and false otherwise.
For example:
Top.isomorphic "examples/sort/mergesort1.sml" "examples/sort/mergesort2.sml" "sort"; should output true and
Top.isomorphic "examples/sort/mergesort1.sml" "examples/sort/quicksort1.sml" "sort"; should output false
To compare multiple programs against each other and produce buckets of equivalent programs:
First, put all of the programs you want to compare in different files in a shared directory and give the expressions you wish to compare a shared name. Then, from the top-level REPL, run Top.bucketize_dir "directory_name" "name_of_expression";.
For example:
Top.bucketize_dir "examples/simple" "x"; should output 3 buckets, containing 4, 3, and 2 members, each corresponding to files in which the expression x is given values of 1, 2, and 3 respectively.
If you would like to see the SMT formula generated by comparing a pair programs, you can change Settings.save_SMT_formula from false to true in Settings.sml. With this setting set to true, whenever Zeus is used to compare two programs, instead of just printing whether the two programs are recognized as equivalent, Zeus will additionally print a commnad of the form z3 -smt2 [file where SMT formula is generated] > [file where z3 output is sent]. When Settings.save_SMT_formula is set to false, these temporary files are deleted before printing the final response, but when set to true, these files are not deleted so that you can see the SMT formula and output generated. As a minor note, although this README and the paper Program Equivalence for Assisted Grading of Functional Programs refers to the validity of the output formula, z3 checks for satisfiability. To deal with this, after producing an output formula, Zeus negates the formula and checks for satisfiability. If the negated formula is unsatisfiable, the original formula is valid, and if the negated formula is satisfiable, the original formula is not valid. So the output "unsat" from z3 can be interpreted as saying the two programs are equivalent, and the output "sat" from z3 can be interpreted as saying the two programs are not equivalent.
If, while comparing multiple programs against each other with the Top.bucketize_dir command, you would like to see which particular files are being compared against one another, and the outcome of those comparisons, you can change Settings.verbose from false to true in Settings.sml. This will cause the Top.bucketize_dir command to, rather than just print X's and O's for instances of failing and succeeding to detect equivalence, print which programs are being compared and whether they were identified as equivalent.