# 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
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
LDFLAGS="-static $LDFLAGS"
LIBS="$READLINE_LIBS $LIBS"
AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <readline/readline.h>],
- [readline("")])],
+ [readline("")])],
[ AC_MSG_RESULT([yes, it works])
with_readline=yes ],
[ AC_MSG_RESULT([no])
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
# 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],
# | :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
#
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
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
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
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
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
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\"
}"
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
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}
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}
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
#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
for handler in $handlers; do
run_handlers="$run_handlers
#line $lineno \"$kf\"
- $handler(\"$smtname\", optarg, smt);
+ $handler(\"$smtname\", optionarg, smt);
"
done
fi
#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
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}
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=
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
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 {
*/
template <class T, bool is_numeric, bool is_integer>
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 <class T>
struct OptionHandler<T, true, true> {
- 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<T>::is_signed && i < 0) {
// unsigned type but user gave negative argument
/** Variant for numeric but non-integral C++ types */
template <class T>
struct OptionHandler<T, true, false> {
- 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()) {
/** Variant for non-numeric C++ types */
template <class T>
struct OptionHandler<T, false, false> {
- 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
/** Handle an option of type T in the default way. */
template <class T>
-T handleOption(std::string option, std::string optarg) {
- return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optarg);
+T handleOption(std::string option, std::string optionarg) {
+ return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optionarg);
}
/** Handle an option of type std::string in the default way. */
template <>
-std::string handleOption<std::string>(std::string option, std::string optarg) {
- return optarg;
+std::string handleOption<std::string>(std::string option, std::string optionarg) {
+ return optionarg;
}
/**
* If a user specifies a :handler or :predicates, it overrides this.
*/
template <class T>
-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<typename T::type>(option, optarg);
+ return handleOption<typename T::type>(option, optionarg);
}
template <class T>
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
"+:${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;
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:
!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<std::string>& 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);
}
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;
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 + "'");
}
}
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);
if (depth == 0) {
out << "(...)";
} else {
- depth --;
+ --depth;
}
// null
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;
case kind::APPLY: break;
case kind::EQUAL:
case kind::DISTINCT: out << smtKindString(k) << " "; break;
+ case kind::CHAIN: break;
case kind::TUPLE: break;
// bool theory
Assert(e.isNull() || e.getExprManager() == d_exprManager);
SmtScope smts(this);
-
finalOptionsAreSet();
doPendingPops();
Assert(e.getExprManager() == d_exprManager);
SmtScope smts(this);
-
finalOptionsAreSet();
doPendingPops();
vector<Expr> 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 =
Dump("benchmark") << SetOptionCommand(key, value);
}
- string optarg = value.getValue();
+ string optionarg = value.getValue();
${smt_setoption_handlers}
operator LAMBDA 2 "lambda"
+parameterized CHAIN BUILTIN 2: "chain operator"
+
constant TYPE_CONSTANT \
::CVC4::TypeConstant \
::CVC4::TypeConstantHashFunction \
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 \
return out;
}
+Node TheoryBuiltinRewriter::blastChain(TNode in) {
+
+ Assert(in.getKind() == kind::CHAIN);
+
+ Kind chainedOp = in.getOperator().getConst<Kind>();
+
+ 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 */
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() {}
#include "expr/node.h"
#include "expr/type_node.h"
#include "expr/expr.h"
+#include "theory/rewriter.h"
#include <sstream>
}
};/* 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) {
bug322b.cvc \
bug339.smt2 \
bug365.smt2 \
- bug382.smt2
+ bug382.smt2 \
+ bug383.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
--- /dev/null
+(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)
projects / cvc5.git / commitdiff