From: Morgan Deters Date: Fri, 21 Sep 2012 20:34:19 +0000 (+0000) Subject: SMT-LIBv2 compliance updates: X-Git-Tag: cvc5-1.0.0~7794 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b5e4b809d1913c9cfc5cf95c04e9fc34c1ca42f3;p=cvc5.git SMT-LIBv2 compliance updates: * chainability of =, <, <=, >, >= via the new CHAINABLE kind and TheoryBuiltin rewriter support (resolves bug #383) * with --smtlib2, force interactive mode off by default Also: * fix a few bugs causing crashes * better "alias" processing for options * configure-time fixes to readline detection (this commit was certified error- and warning-free by the test-and-commit script.) --- diff --git a/config/readline.m4 b/config/readline.m4 index 6cfe6a982..30d285b29 100644 --- a/config/readline.m4 +++ b/config/readline.m4 @@ -3,8 +3,9 @@ # Look for readline and link it in, but allow user to disable. AC_DEFUN([CVC4_CHECK_FOR_READLINE], [ AC_MSG_CHECKING([whether user requested readline support]) -AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check]) LIBREADLINE= +have_libreadline=0 +READLINE_LIBS= if test "$with_readline" = no; then AC_MSG_RESULT([no, readline disabled by user]) else @@ -13,16 +14,15 @@ else else AC_MSG_RESULT([yes, readline enabled by user]) fi - AC_CHECK_LIB([readline], [readline], - [AC_CHECK_HEADER([readline/readline.h], - [READLINE_LIBS="-lreadline -lncurses -ltermcap -ltinfo"], - [if test "$with_readline" != check; then - AC_MSG_FAILURE([cannot find libreadline!]) - fi])], - [if test "$with_readline" != check; then - AC_MSG_FAILURE([cannot find libreadline!]) - fi], [-lncurses -ltermcap -ltinfo]) + READLINE_LIBS= + CVC4_TRY_READLINE_WITH([]) + CVC4_TRY_READLINE_WITH([-ltinfo]) + CVC4_TRY_READLINE_WITH([-lncurses -ltermcap]) + CVC4_TRY_READLINE_WITH([-lncurses -ltermcap -ltinfo]) if test -z "$READLINE_LIBS"; then + if test "$with_readline" != check; then + AC_MSG_FAILURE([cannot find libreadline! (or can't get it to work)]) + fi with_readline=no else # make sure it works in static builds, too @@ -34,7 +34,7 @@ else LDFLAGS="-static $LDFLAGS" LIBS="$READLINE_LIBS $LIBS" AC_LINK_IFELSE([AC_LANG_PROGRAM([#include ], - [readline("")])], + [readline("")])], [ AC_MSG_RESULT([yes, it works]) with_readline=yes ], [ AC_MSG_RESULT([no]) @@ -50,13 +50,23 @@ else fi fi if test "$with_readline" = yes; then - HAVE_LIBREADLINE=1 + have_libreadline=1 else - HAVE_LIBREADLINE=0 + have_libreadline=0 READLINE_LIBS= fi - AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], ${HAVE_LIBREADLINE}, [Define to 1 to use libreadline]) - AC_SUBST([READLINE_LIBS]) fi ])# CVC4_CHECK_FOR_READLINE +# CVC4_TRY_READLINE_WITH(LIBS) +# ---------------------------- +# Try AC_CHECK_LIB(readline) with the given linking libraries +AC_DEFUN([CVC4_TRY_READLINE_WITH], [ +if test -z "$READLINE_LIBS"; then + AC_CHECK_LIB([readline], [readline], + [AC_CHECK_HEADER([readline/readline.h], + [READLINE_LIBS="-lreadline $1"], + [])], + [], [$1]) +fi +])# CVC4_TRY_READLINE_WITH diff --git a/configure.ac b/configure.ac index 310cd4095..3ef0ac689 100644 --- a/configure.ac +++ b/configure.ac @@ -852,7 +852,10 @@ fi # Checks for libraries. # Check for libreadline (defined in config/readline.m4) +AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check]) CVC4_CHECK_FOR_READLINE +AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline]) +AC_SUBST([READLINE_LIBS]) AC_SEARCH_LIBS([clock_gettime], [rt], [AC_DEFINE([HAVE_CLOCK_GETTIME], [1], diff --git a/src/options/base_options b/src/options/base_options index f7d1a77d4..cd1bec00a 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -40,19 +40,33 @@ # | :read-write # | :link linked-options.. # -# alias smt-option-name = (smt-option-name[=argument])+ -# alias (-short-option | --long-option) = (-option[=argument] | --long-option[=argument])+ +# common-alias ALIAS_SPECIFICATION +# alias ALIAS_SPECIFICATION +# expert-alias ALIAS_SPECIFICATION +# undocumented-alias ALIAS_SPECIFICATION # -# The alias command creates a new SmtEngine option name, or short option, or long option, -# and binds it to act the same way as if the options to the right of "=" were passed. -# For example, if there are options to --disable-warning-1 and --disable-warning-2, etc., -# a useful alias might be: +# ALIAS_SPECIFICATION ::= (-short-option | --long-option) = (-option[=argument] | --long-option[=argument])+ +# | (-short-option=ARG | --long-option=ARG) = (-option[=ARG|argument] | --long-option[=ARG|argument])+ +# +# The alias command creates a new short or long option, and binds it +# to act the same way as if the options to the right of "=" were passed. +# For example, if there are options to --disable-warning-1 and +# --disable-warning-2, etc., a useful alias might be: # # alias --disable-all-warnings = --disable-warning-1 --disable-warning-2 # -# Aliases cannot take arguments, and command-line aliases cannot set SmtEngine properties, -# and SmtEngine aliases cannot set command-line properties. For these things, you need a -# custom handler. +# It's also possible to pass an argument through to another option. +# This alias makes "--output-language" synonymous with "--output-lang". +# Without the "=L" parts, --output-language would not take an argument, +# and option processing would fail (because --output-lang expects one). +# +# alias --output-language=L = --output-lang=L +# +# You can also ignore such an argument: +# +# alias --some-option=VALUE = --other-option --option2=foo --option3=bar +# +# or use it for multiple options on the right-hand side, etc. # # warning message # @@ -74,9 +88,14 @@ option err std::ostream* :default &std::cerr :include common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "util/language.h" :default language::input::LANG_AUTO :read-write force input language (default is "auto"; see --lang help) common-option outputLanguage output-language --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "util/language.h" :default language::output::LANG_AUTO :read-write - force input language (default is "auto"; see --lang help) + force output language (default is "auto"; see --output-lang help) option languageHelp bool +# Allow also --language and --output-language, it's a common mistake to +# type these, but no need to document it. +undocumented-alias --language=L = --lang=L +undocumented-alias --output-language=L = --output-lang=L + option verbosity verbosity int :read-write :default 0 :predicate CVC4::options::setVerbosity :predicate-include "options/base_options_handlers.h" the verbosity level of CVC4 common-option - -v --verbose void :handler CVC4::options::increaseVerbosity @@ -86,6 +105,8 @@ common-option - -q --quiet void :handler CVC4::options::decreaseVerbosity common-option statistics statistics --stats bool give statistics on exit +undocumented-alias --statistics = --stats +undocumented-alias --no-statistics = --no-stats common-option parseOnly parse-only --parse-only bool :read-write exit after parsing input @@ -104,7 +125,7 @@ option - debug -d --debug=TAG argument :handler CVC4::options::addDebugTag option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h" print the "success" output required of SMT-LIBv2 -alias --smtlib2 = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental +alias --smtlib2 = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --no-interactive SMT-LIBv2 compliance mode (implies other options) endmodule diff --git a/src/options/mkoptions b/src/options/mkoptions index 93885d75f..9e5fb2b81 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -543,7 +543,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o if [ "$type" = bool ]; then all_modules_option_handlers="${all_modules_option_handlers}${cases} #line $lineno \"$kf\" - assignBool(options::$internal, argv[old_optind == 0 ? 1 : old_optind], true, NULL);$run_links + assignBool(options::$internal, option, true, NULL);$run_links break; " elif [ -n "$expect_arg" -a "$internal" != - ]; then @@ -552,12 +552,12 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(option, optarg, smt);" + $handler(option, optionarg, smt);" done else run_handlers=" #line $lineno \"$kf\" - handleOption<$type>(option, optarg);" + handleOption<$type>(option, optionarg);" fi if [ -n "$predicates" ]; then for predicate in $predicates; do @@ -568,7 +568,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o fi all_custom_handlers="${all_custom_handlers} #line $lineno \"$kf\" -template <> options::${internal}__option_t::type runHandlerAndPredicates(options::${internal}__option_t, std::string option, std::string optarg, SmtEngine* smt) { +template <> options::${internal}__option_t::type runHandlerAndPredicates(options::${internal}__option_t, std::string option, std::string optionarg, SmtEngine* smt) { #line $lineno \"$kf\" options::${internal}__option_t::type retval = $run_handlers #line $lineno \"$kf\" @@ -576,7 +576,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options }" all_modules_option_handlers="${all_modules_option_handlers}${cases} #line $lineno \"$kf\" - assign(options::$internal, argv[old_optind == 0 ? 1 : old_optind], optarg, NULL);$run_links + assign(options::$internal, option, optionarg, NULL);$run_links break; " elif [ -n "$expect_arg" ]; then @@ -589,7 +589,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(argv[old_optind == 0 ? 1 : old_optind], optarg, smt);" + $handler(option, optionarg, smt);" done fi all_modules_option_handlers="${all_modules_option_handlers}${cases} @@ -607,7 +607,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(argv[old_optind == 0 ? 1 : old_optind], smt);" + $handler(option, smt);" done fi all_modules_option_handlers="${all_modules_option_handlers}${cases} @@ -621,7 +621,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options if [ "$type" = bool ]; then all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate} #line $lineno \"$kf\" - assignBool(options::$internal, argv[old_optind == 0 ? 1 : old_optind], false, NULL);$run_links_alternate + assignBool(options::$internal, option, false, NULL);$run_links_alternate break; " else @@ -646,7 +646,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - Options::current().assignBool(options::$internal, \"$smtname\", optarg == \"true\", smt);$run_links + Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_links return; }" elif [ -n "$expect_arg" -a "$internal" != - ]; then @@ -655,7 +655,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(\"$smtname\", optarg, smt); + $handler(\"$smtname\", optionarg, smt); " done fi @@ -663,7 +663,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - Options::current().assign(options::$internal, \"$smtname\", optarg, smt);$run_links + Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_links return; }" elif [ -n "$expect_arg" ]; then @@ -671,7 +671,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(\"$smtname\", optarg, smt); + $handler(\"$smtname\", optionarg, smt); " done smt_setoption_handlers="${smt_setoption_handlers} @@ -727,12 +727,34 @@ template <> void Options::assign(options::${internal}__option_t, std::string opt fi } +function common-alias { + # common-alias -option[=arg] = (-option[=arg])+ + handle_alias COMMON "$@" +} + function alias { - # alias (smtname | -option) = (smtname [arg] | -option [arg])+ + # alias -option[=arg] = (-option[=arg])+ + handle_alias STANDARD "$@" +} + +function expert-alias { + # expert-alias -option[=arg] = (-option[=arg])+ + handle_alias EXPERT "$@" +} + +function undocumented-alias { + # undocumented-alias -option[=arg] = (-option[=arg])+ + handle_alias UNDOCUMENTED "$@" +} + +function handle_alias { + # handle_alias CATEGORY -option[=arg] = (-option[=arg])+ check_module_seen check_doc - category=STANDARD + category="$1" + shift + internal=- smtname= short_option= @@ -752,16 +774,24 @@ function alias { options_already_documented=false alternate_options_already_documented=false + if [ "$category" = UNDOCUMENTED ]; then + expect_doc=false + else + expect_doc=true + fi + expect_doc_alternate=false + if [ $# -lt 3 ]; then echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2 exit 1 fi - options= - while [ $# -gt 0 -a "$1" != = ]; do - options="$options $1" - shift - done - if [ $# -eq 0 ]; then + if [ "$1" = '=' ]; then + echo "$kf:$lineno: error: malformed \"alias\" command; expected option name" >&2 + exit 1 + fi + option="$1" + shift + if [ "$1" != '=' ]; then echo "$kf:$lineno: error: malformed \"alias\" command; expected \`='" >&2 exit 1 fi @@ -771,42 +801,76 @@ function alias { exit 1 fi cases= - for option in $options; do - if ! expr "$option" : - &>/dev/null; then - echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2 - exit 1 - fi - if expr "$option" : -- &>/dev/null; then + if ! expr "$option" : - &>/dev/null; then + echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2 + exit 1 + fi + if expr "$option" : -- &>/dev/null; then + if expr "$option" : '.*=' &>/dev/null; then + expect_arg_long=required_argument + arg="$(echo "$option" | sed 's,[^=]*=\(.*\),\1,')" + option="$(echo "$option" | sed 's,--,,;s,=.*,,')" + echo "warning: not yet handling long-option alias =$arg" >&2 + else + expect_arg_long=no_argument + arg= option="$(echo "$option" | sed 's,--,,')" - all_modules_long_options="${all_modules_long_options} - { \"$(echo "$option" | sed 's,=.*,,')\", no_argument, NULL, $n_long }," + fi + all_modules_long_options="${all_modules_long_options} + { \"$(echo "$option" | sed 's,=.*,,')\", $expect_arg_long, NULL, $n_long }," cases="${cases} case $n_long:// --$option" - let ++n_long - long_option="${long_option:+$long_option | --}$option" - else - if ! expr "$option" : '-.$' &>/dev/null; then + let ++n_long + long_option="${long_option:+$long_option | --}$option" + else + if ! expr "$option" : '-.$' &>/dev/null; then + if ! expr "$option" : '-.=' &>/dev/null; then echo "$kf:$lineno: error: expected short option specification, got \`$option'" >&2 exit 1 fi + expect_arg=: + arg="$(echo "$option" | sed 's,[^=]*=,,')" + option="$(echo "$option" | sed 's,-\(.\)=.*,\1,')" + echo "warning: not yet handling short-option alias =$arg" >&2 + else + expect_arg= + arg= option="$(echo "$option" | sed 's,-,,')" - all_modules_short_options="${all_modules_short_options}$option" + fi + all_modules_short_options="${all_modules_short_options}$option$expect_arg" cases="${cases} case '$option':" - short_option="${short_option:+$short_option | -}$option" - fi - done + short_option="${short_option:+$short_option | -}$option" + fi + while [ $# -gt 0 ]; do + linkopt="$1" + # on the RHS, we're looking for =ARG, where "ARG" is *exactly* what + # was given on the LHS + if expr "$linkopt" : '.*=' &>/dev/null; then + linkarg="$(echo "$linkopt" | sed 's,[^=]*=,,')" + if [ "$linkarg" = "$arg" ]; then + # we found =ARG + linkopt="$(echo "$linkopt" | sed 's,=.*,,')" + else + # false positive: =SOMETHING, where SOMETHING != ARG + linkarg= + fi + fi links="$links #line $lineno \"$kf\" - preemptGetopt(extra_argc, extra_argv, \"$1\");" + preemptGetopt(extra_argc, extra_argv, \"$linkopt\");" + if [ "$linkarg" ]; then + # include also the arg + links="$links +#line $lineno \"$kf\" + preemptGetopt(extra_argc, extra_argv, optionarg.c_str());" + fi shift done all_modules_option_handlers="$all_modules_option_handlers$cases$links break; " - expect_doc=true - expect_doc_alternate=false } function warning { diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index bae0ef169..dd8a7af57 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -67,15 +67,15 @@ CVC4_THREADLOCAL(Options*) Options::s_current = NULL; */ template struct OptionHandler { - static T handle(std::string option, std::string optarg); + static T handle(std::string option, std::string optionarg); };/* struct OptionHandler<> */ /** Variant for integral C++ types */ template struct OptionHandler { - static T handle(std::string option, std::string optarg) { + static T handle(std::string option, std::string optionarg) { try { - Integer i(optarg, 10); + Integer i(optionarg, 10); if(! std::numeric_limits::is_signed && i < 0) { // unsigned type but user gave negative argument @@ -107,8 +107,8 @@ struct OptionHandler { /** Variant for numeric but non-integral C++ types */ template struct OptionHandler { - static T handle(std::string option, std::string optarg) { - std::stringstream in(optarg); + static T handle(std::string option, std::string optionarg) { + std::stringstream in(optionarg); long double r; in >> r; if(! in.eof()) { @@ -138,7 +138,7 @@ struct OptionHandler { /** Variant for non-numeric C++ types */ template struct OptionHandler { - static T handle(std::string option, std::string optarg) { + static T handle(std::string option, std::string optionarg) { T::unsupported_handleOption_call___please_write_me; // The above line causes a compiler error if this version of the template // is ever instantiated (meaning that a specialization is missing). So @@ -151,14 +151,14 @@ struct OptionHandler { /** Handle an option of type T in the default way. */ template -T handleOption(std::string option, std::string optarg) { - return OptionHandler::is_specialized, std::numeric_limits::is_integer>::handle(option, optarg); +T handleOption(std::string option, std::string optionarg) { + return OptionHandler::is_specialized, std::numeric_limits::is_integer>::handle(option, optionarg); } /** Handle an option of type std::string in the default way. */ template <> -std::string handleOption(std::string option, std::string optarg) { - return optarg; +std::string handleOption(std::string option, std::string optionarg) { + return optionarg; } /** @@ -166,12 +166,12 @@ std::string handleOption(std::string option, std::string optarg) { * If a user specifies a :handler or :predicates, it overrides this. */ template -typename T::type runHandlerAndPredicates(T, std::string option, std::string optarg, SmtEngine* smt) { +typename T::type runHandlerAndPredicates(T, std::string option, std::string optionarg, SmtEngine* smt) { // By default, parse the option argument in a way appropriate for its type. // E.g., for "unsigned int" options, ensure that the provided argument is // a nonnegative integer that fits in the unsigned int type. - return handleOption(option, optarg); + return handleOption(option, optionarg); } template @@ -384,6 +384,7 @@ std::vector Options::parseOptions(int argc, char* main_argv[]) thro for(;;) { int c = -1; optopt = 0; + std::string option, optionarg; Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind << ", extra_argc == " << extra_argc << std::endl; if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) { #if HAVE_DECL_OPTRESET @@ -400,6 +401,16 @@ std::vector Options::parseOptions(int argc, char* main_argv[]) thro "+:${all_modules_short_options}", cmdlineOptions, NULL); Debug("preemptGetopt") << "in preempt code, c == " << c << " (`" << char(c) << "') optind == " << optind << std::endl; + if(optopt == 0 || + ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) { + // long option + option = argv[old_optind == 0 ? 1 : old_optind]; + optionarg = (optarg == NULL) ? "" : optarg; + } else { + // short option + option = std::string("-") + char(optopt); + optionarg = (optarg == NULL) ? "" : optarg; + } if(optind >= extra_argc) { Debug("preemptGetopt") << "-- no more preempt args" << std::endl; unsigned i = 1; @@ -435,31 +446,25 @@ std::vector Options::parseOptions(int argc, char* main_argv[]) thro cmdlineOptions, NULL); main_optind = optind; Debug("options") << "[ next option will be at pos: " << optind << " ]" << std::endl; - if(optind < argc) Debug("options") << "next is option: " << argv[optind] << std::endl; if(c == -1) { Debug("options") << "done with option parsing" << std::endl; break; } + option = argv[old_optind == 0 ? 1 : old_optind]; + optionarg = (optarg == NULL) ? "" : optarg; } - Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "')" << std::endl; + Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "'), " << option << std::endl; switch(c) { ${all_modules_option_handlers} -#line 451 "${template}" +#line 463 "${template}" case ':': // This can be a long or short option, and the way to get at the // name of it is different. - if(optopt == 0 || - ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) { - // was a long option - throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument"); - } else { - // was a short option - throw OptionException(std::string("option `-") + char(optopt) + "' missing its required argument"); - } + throw OptionException(std::string("option `") + option + "' missing its required argument"); case '?': default: @@ -467,13 +472,13 @@ ${all_modules_option_handlers} !strncmp(argv[optind - 1], "--thread", 8) && strlen(argv[optind - 1]) > 8 ) { if(! isdigit(argv[optind - 1][8])) { - throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer"); + throw OptionException(std::string("can't understand option `") + option + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer"); } std::vector& threadArgv = d_holder->threadArgv; char *end; long tnum = strtol(argv[optind - 1] + 8, &end, 10); if(tnum < 0 || (*end != '\0' && *end != '=')) { - throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer"); + throw OptionException(std::string("can't understand option `") + option + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer"); } if(threadArgv.size() <= size_t(tnum)) { threadArgv.resize(tnum + 1); @@ -483,13 +488,13 @@ ${all_modules_option_handlers} } if(*end == '\0') { // e.g., we have --thread0 "foo" if(argc <= optind) { - throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument"); + throw OptionException(std::string("option `") + option + "' missing its required argument"); } Debug("options") << "thread " << tnum << " gets option " << argv[optind] << std::endl; threadArgv[tnum] += argv[(*optind_ref)++]; } else { // e.g., we have --thread0="foo" if(end[1] == '\0') { - throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument"); + throw OptionException(std::string("option `") + option + "' missing its required argument"); } Debug("options") << "thread " << tnum << " gets option " << (end + 1) << std::endl; threadArgv[tnum] += end + 1; @@ -498,14 +503,7 @@ ${all_modules_option_handlers} break; } - // This can be a long or short option, and the way to get at the name of it is different. - if(optopt == 0 || - ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) { - // was a long option - throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "'"); - } else { // was a short option - throw OptionException(std::string("can't understand option `-") + char(optopt) + "'"); - } + throw OptionException(std::string("can't understand option `") + option + "'"); } } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5950f568f..03aa7acc1 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -584,6 +584,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] expr = EXPR_MANAGER->mkAssociative(kind,args); } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) { expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); + } else if( ( kind == CVC4::kind::IFF || kind == CVC4::kind::EQUAL || + kind == CVC4::kind::LT || kind == CVC4::kind::GT || + kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) && + args.size() > 2 ) { + expr = MK_EXPR(CVC4::kind::CHAIN, MK_CONST(kind), args); } else { PARSER_STATE->checkOperator(kind, args.size()); expr = MK_EXPR(kind, args); diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 6dbf4ed03..b14f6a9c8 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -73,7 +73,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo if (depth == 0) { out << "(...)"; } else { - depth --; + --depth; } // null @@ -221,6 +221,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo case kind::APPLY: toStream(op, n.getOperator(), depth, types, true); break; + case kind::CHAIN: + case kind::DISTINCT: // chain and distinct not supported directly in CVC4, blast them away with the rewriter + toStream(out, theory::Rewriter::rewrite(n), depth, types, true); + return; case kind::SORT_TYPE: { string name; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 842325869..7f973aaee 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -208,6 +208,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::APPLY: break; case kind::EQUAL: case kind::DISTINCT: out << smtKindString(k) << " "; break; + case kind::CHAIN: break; case kind::TUPLE: break; // bool theory diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e28520e70..364a786cf 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1656,7 +1656,6 @@ Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) { Assert(e.isNull() || e.getExprManager() == d_exprManager); SmtScope smts(this); - finalOptionsAreSet(); doPendingPops(); @@ -1725,7 +1724,6 @@ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) { Assert(e.getExprManager() == d_exprManager); SmtScope smts(this); - finalOptionsAreSet(); doPendingPops(); @@ -2159,11 +2157,11 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) { vector SmtEngine::getAssertions() throw(ModalException, AssertionException) { + SmtScope smts(this); finalOptionsAreSet(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetAssertionsCommand(); } - SmtScope smts(this); Trace("smt") << "SMT getAssertions()" << endl; if(!options::interactive()) { const char* msg = diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp index deec881e4..187b29114 100644 --- a/src/smt/smt_options_template.cpp +++ b/src/smt/smt_options_template.cpp @@ -46,7 +46,7 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) Dump("benchmark") << SetOptionCommand(key, value); } - string optarg = value.getValue(); + string optionarg = value.getValue(); ${smt_setoption_handlers} diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 1218f3809..da31d157f 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -300,6 +300,8 @@ operator TUPLE 1: "a tuple" operator LAMBDA 2 "lambda" +parameterized CHAIN BUILTIN 2: "chain operator" + constant TYPE_CONSTANT \ ::CVC4::TypeConstant \ ::CVC4::TypeConstantHashFunction \ @@ -342,6 +344,7 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule +typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule constant SUBTYPE_TYPE \ ::CVC4::Predicate \ diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index f62140263..a23a1b8f2 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -51,6 +51,25 @@ Node TheoryBuiltinRewriter::blastDistinct(TNode in) { return out; } +Node TheoryBuiltinRewriter::blastChain(TNode in) { + + Assert(in.getKind() == kind::CHAIN); + + Kind chainedOp = in.getOperator().getConst(); + + if(in.getNumChildren() == 2) { + // if this is the case exactly 1 pair will be generated so the + // AND is not required + return NodeManager::currentNM()->mkNode(chainedOp, in[0], in[1]); + } else { + NodeBuilder<> conj(kind::AND); + for(TNode::iterator i = in.begin(), j = i + 1; j != in.end(); ++i, ++j) { + conj << NodeManager::currentNM()->mkNode(chainedOp, *i, *j); + } + return conj; + } +} + }/* CVC4::theory::builtin namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index acf535388..b7199474b 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -32,22 +32,29 @@ namespace builtin { class TheoryBuiltinRewriter { static Node blastDistinct(TNode node); + static Node blastChain(TNode node); public: - static inline RewriteResponse postRewrite(TNode node) { - return RewriteResponse(REWRITE_DONE, node); - } - - static inline RewriteResponse preRewrite(TNode node) { + static inline RewriteResponse doRewrite(TNode node) { switch(node.getKind()) { case kind::DISTINCT: return RewriteResponse(REWRITE_DONE, blastDistinct(node)); + case kind::CHAIN: + return RewriteResponse(REWRITE_DONE, blastChain(node)); default: return RewriteResponse(REWRITE_DONE, node); } } + static inline RewriteResponse postRewrite(TNode node) { + return doRewrite(node); + } + + static inline RewriteResponse preRewrite(TNode node) { + return doRewrite(node); + } + static inline void init() {} static inline void shutdown() {} diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index b7fd3c351..97af23f67 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -24,6 +24,7 @@ #include "expr/node.h" #include "expr/type_node.h" #include "expr/expr.h" +#include "theory/rewriter.h" #include @@ -168,6 +169,54 @@ public: } };/* class LambdaTypeRule */ +class ChainTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::CHAIN); + + if(!check) { + return nodeManager->booleanType(); + } + + TypeNode tn; + try { + // Actually do the expansion to do the typechecking. + // Shouldn't be extra work to do this, since the rewriter + // keeps a cache. + tn = nodeManager->getType(Rewriter::rewrite(n), check); + } catch(TypeCheckingExceptionPrivate& e) { + std::stringstream ss; + ss << "Cannot typecheck the expansion of chained operator `" << n.getOperator() << "':" + << std::endl; + // indent the sub-exception for clarity + std::stringstream ss2; + ss2 << e; + std::string eStr = ss2.str(); + for(size_t i = eStr.find('\n'); i != std::string::npos; i = eStr.find('\n', i)) { + eStr.insert(++i, "| "); + } + ss << "| " << eStr; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + + // This check is intentionally != booleanType() rather than + // !(...isBoolean()): if we ever add a type compatible with + // Boolean (pseudobooleans or whatever), we have to revisit + // the above "!check" case where booleanType() is returned + // directly. Putting this check here will cause a failure if + // it's ever relevant. + if(tn != nodeManager->booleanType()) { + std::stringstream ss; + ss << "Chains can only be formed over predicates; " + << "the operator here returns `" << tn << "', expected `" + << nodeManager->booleanType() << "'."; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + + return nodeManager->booleanType(); + } +};/* class ChainTypeRule */ + class SortProperties { public: inline static bool isWellFounded(TypeNode type) { diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index d531a79a4..50527e51a 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -127,7 +127,8 @@ BUG_TESTS = \ bug322b.cvc \ bug339.smt2 \ bug365.smt2 \ - bug382.smt2 + bug382.smt2 \ + bug383.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug383.smt2 b/test/regress/regress0/bug383.smt2 new file mode 100644 index 000000000..b0349c008 --- /dev/null +++ b/test/regress/regress0/bug383.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_LIA) +(set-info :status sat) +(declare-fun f1 () Int) +(declare-fun f2 () Int) +(declare-fun f3 () Int) +(assert (< 1 f1 f2 f3 5)) +(check-sat) +(exit)