Support for custom domains - Githubissues

dvoits / z3test

Test and benchmark repository for Z3.

Other

0 stars 0 forks source link

Support for custom domains #36

Open dvoits opened 7 years ago

dvoits commented 7 years ago

Domain describes structure and semantics of input and output program data. For each experiment there is one domain.

Input:

Command line argument with special token to be replaced with an input benchmark file name when run.
Benchmark files extensions (one or several).

Output: It describes named values contained in a program output and extracted by two alternative ways:

"Value" can depend on exit code (specific code corresponds to specific value)
"Value" is a result of a given regular expression applied to a standard output

Values are represented as a JSON object, one object for each of the benchmarks.

wintersteiger commented 7 years ago

More examples: F* (custom I/O requirements) SAT solvers (the "canonical" example is MiniSAT, which follow the SAT competition requirements (there are also many that use parallelism) Other SMT solvers (very similar to Z3), e.g. those taking part in the SMT Competition