Infrastructure for portfolio solving (#8709)
authorGereon Kremer <gkremer@cs.stanford.edu>
Mon, 13 Jun 2022 09:56:54 +0000 (02:56 -0700)
committerGitHub <noreply@github.com>
Mon, 13 Jun 2022 09:56:54 +0000 (02:56 -0700)
commit4a34d8126ee7077dfeb58338a906a9d824a3db1c
treef525a79cd7bef944a6c1b3996603a11c2fcaac62
parent1b6fa3da6536191e6b69769c99a3994aab09cd4b
Infrastructure for portfolio solving (#8709)

We want to replace the set of competition scripts by an internal portfolio mechanism. It seems that this portfolio mechanism is best implemented from scratch in the driver instead of using, e.g., --tlimit or --tlimit-per.

This PR introduces the infrastructure for that, implementing the following approach:
first parse the input until a logic has been specified; if more than one configuration is to be used, parse the remaining commands into a vector; for every configuration, we fork the main process, and in the child process configure the solver and replay the vectors.
cmake/ConfigureCvc5.cmake
src/base/cvc5config.h.in
src/main/CMakeLists.txt
src/main/driver_unified.cpp
src/main/portfolio_driver.cpp [new file with mode: 0644]
src/main/portfolio_driver.h [new file with mode: 0644]
src/options/main_options.toml