diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-26 19:42:25 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-26 19:42:25 +0000 |
commit | 6fdc62f34bb1d04b84dfd628ec16335b8f02385e (patch) | |
tree | 44755057990ad99f6f47904a0201d33c9be18c9c /src/util | |
parent | 1ed3b1803bd0a25c56a62d290cd5dcb64c5085ce (diff) |
Global registry of SAT solvers, where they are registered at compile time. The available SAT solvers can be seen with the --show-sat-solvers option.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/options.cpp | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index d3426e152..b6956a31b 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -35,6 +35,7 @@ #include "util/options.h" #include "util/output.h" #include "util/dump.h" +#include "prop/sat_solver_factory.h" #include "cvc4autoconfig.h" @@ -163,6 +164,7 @@ Additional CVC4 options:\n\ --debug | -d debug something (e.g. -d arith), can repeat\n\ --show-debug-tags show all avalable tags for debugging\n\ --show-trace-tags show all avalable tags for tracing\n\ + --show-sat-solvers show all available SAT solvers\n\ --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\ --print-expr-types print types with variables when printing exprs\n\ --lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\ @@ -324,6 +326,7 @@ enum OptionValue { USE_MMAP, SHOW_DEBUG_TAGS, SHOW_TRACE_TAGS, + SHOW_SAT_SOLVERS, SHOW_CONFIG, STRICT_PARSING, DEFAULT_EXPR_DEPTH, @@ -399,6 +402,7 @@ static struct option cmdlineOptions[] = { { "no-theory-registration", no_argument, NULL, NO_THEORY_REGISTRATION }, { "show-debug-tags", no_argument , NULL, SHOW_DEBUG_TAGS }, { "show-trace-tags", no_argument , NULL, SHOW_TRACE_TAGS }, + { "show-sat-solvers", no_argument , NULL, SHOW_SAT_SOLVERS }, { "show-config", no_argument , NULL, SHOW_CONFIG }, { "segv-nospin", no_argument , NULL, SEGV_NOSPIN }, { "help" , no_argument , NULL, 'h' }, @@ -930,6 +934,21 @@ throw(OptionException) { exit(0); break; + case SHOW_SAT_SOLVERS: + { + vector<string> solvers; + prop::SatSolverFactory::getSolverIds(solvers); + printf("Available SAT solvers: "); + for (unsigned i = 0; i < solvers.size(); ++ i) { + if (i > 0) { + printf(", "); + } + printf("%s", solvers[i].c_str()); + } + printf("\n"); + exit(0); + break; + } case SHOW_CONFIG: fputs(Configuration::about().c_str(), stdout); printf("\n"); |