1 KiB
# This is a specification for evaluating and improving theory_nseq.
. Build a debug version of z3 in the z3\build directory
. Build a release version of z3 in the z3\release directory
. To use zipt run .\ZIPT\bin\Debug\net8.0\ZIPT.exe -v
. To profile debug theory_seq use C:\c3\build\z3.exe -T:10 -st -tr:seq
. To profile debug theory_nseq use C:\c3\build\z3.exe -T:10 -st smt.seq.solver=nseq -tr:seq
. QF_S benchmarks are in C:\c3\tests\non-incremental\QF_S
# Task
. Pick 50 benchmarks from QF_S
. Run theory_seq, theory_nseq and zipt on each benchmark
. Create a report with timing information and status (sat/unsat/unknown/bug/crash)
. Select at most 3 benchmarks where theory_nseq is worse than either theory_seq or zipt.
. profile these benchmarks using debug builds of z3 and zipt in trace mode. Copy .z3-trace files to allow inspection.
. Use information from the trace files to create a report of what needs to be implemented for theory_nseq based on zipt.