diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-23 20:58:08 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2015-01-14 06:33:49 -0500 |
commit | 0042f301908763cf1edb8a2d56b3f373a0055908 (patch) | |
tree | 4f2a66c39bf5511c3f00dca9f4d1bc475435359a /src/main | |
parent | ba1ae20edf3f4b2321a05b39cb218940e926d436 (diff) |
sygus input language and benchmark
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/driver_unified.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 9035ed8b8..c011671f8 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -34,6 +34,7 @@ #include "expr/command.h" #include "util/configuration.h" #include "options/options.h" +#include "theory/quantifiers/options.h" #include "main/command_executor.h" #ifdef PORTFOLIO_BUILD @@ -198,6 +199,9 @@ int runCvc4(int argc, char* argv[], Options& opts) { } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { opts.set(options::inputLanguage, language::input::LANG_CVC4); + } else if((len >= 3 && !strcmp(".sy", filename + len - 3)) + || (len >= 3 && !strcmp(".sl", filename + len - 3))) { + opts.set(options::inputLanguage, language::input::LANG_SYGUS); } } } @@ -206,6 +210,12 @@ int runCvc4(int argc, char* argv[], Options& opts) { opts.set(options::outputLanguage, language::toOutputLanguage(opts[options::inputLanguage])); } + // if doing sygus, turn on CEGQI by default + if(opts[options::inputLanguage] == language::input::LANG_SYGUS && + !opts.wasSetByUser(options::ceGuidedInst)) { + opts.set(options::ceGuidedInst, true); + } + // Determine which messages to show based on smtcomp_mode and verbosity if(Configuration::isMuzzledBuild()) { DebugChannel.setStream(CVC4::null_os); |