#include<iostream>
#include "util/memory_manager.h"
#include "util/trace.h"
#include "util/debug.h"
#include "util/util.h"
#include "ast/pp.h"
#include "shell/smtlib_frontend.h"
#include "shell/z3_log_frontend.h"
#include "util/warning.h"
#include "util/z3_version.h"
#include "shell/dimacs_frontend.h"
#include "shell/datalog_frontend.h"
#include "shell/opt_frontend.h"
#include "cmd_context/tptp_frontend.h"
#include "util/timeout.h"
#include "util/z3_exception.h"
#include "util/error_codes.h"
#include "util/file_path.h"
#include "util/gparams.h"
#include "util/env_params.h"
#include "util/file_path.h"
#include "shell/drat_frontend.h"
#if defined( _WINDOWS ) && defined( __MINGW32__ ) && ( defined( __GNUG__ ) || defined( __clang__ ) )
#include <crtdbg.h>
#endif
typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_DRAT, IN_TPTP } input_kind;
static char const * g_input_file = nullptr;
static char const * g_drat_input_file = nullptr;
static bool g_standard_input = false;
static input_kind g_input_kind = IN_UNSPECIFIED;
extern bool g_display_statistics;
extern bool g_display_model;
static bool g_display_istatistics = false;
static void error(const char * msg) {
std::cerr << "Error: " << msg << "\n";
std::cerr << "For usage information: z3 -h\n";
exit(ERR_CMD_LINE);
}
#define STRINGIZE(x) #x
#define STRINGIZE_VALUE_OF(x) STRINGIZE(x)
void display_usage() {
std::cout << "Z3 [version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER;
std::cout << " - ";
#if defined(__LP64__) || defined(_WIN64)
std::cout << "64";
#else
std::cout << "32";
#endif
std::cout << " bit";
#ifdef Z3GITHASH
std::cout << " - build hashcode " << STRINGIZE_VALUE_OF(Z3GITHASH);
#endif
std::cout << "]. (C) Copyright 2006-2016 Microsoft Corp.\n";
std::cout << "Usage: z3 [options] [-file:]file\n";
std::cout << "\nInput format:\n";
std::cout << " -smt2 use parser for SMT 2 input format.\n";
std::cout << " -dl use parser for Datalog input format.\n";
std::cout << " -dimacs use parser for DIMACS input format.\n";
std::cout << " -wcnf use parser for Weighted CNF DIMACS input format.\n";
std::cout << " -opb use parser for PB optimization input format.\n";
std::cout << " -lp use parser for a modest subset of CPLEX LP input format.\n";
std::cout << " -log use parser for Z3 API trace input format.\n";
std::cout << " -tptp use parser for TPTP input format (fof/cnf/tff/thf fragments).\n";
std::cout << " -in read formula from standard input.\n";
std::cout << " -model display model for satisfiable SMT.\n";
std::cout << "\nMiscellaneous:\n";
std::cout << " -h, -? prints this message.\n";
std::cout << " -version prints version number of Z3.\n";
std::cout << " -v:level be verbose, where <level> is the verbosity level.\n";
std::cout << " -nw disable warning messages.\n";
std::cout << " -p display Z3 global (and module) parameters.\n";
std::cout << " -pd display Z3 global (and module) parameter descriptions.\n";
std::cout << " -pm:name display Z3 module ('name') parameters.\n";
std::cout << " -pmmd:name display Z3 module ('name') parameters in Markdown format.\n";
std::cout << " -pp:name display Z3 parameter description, if 'name' is not provided, then all module names are listed.\n";
std::cout << " -tactics[:name] display built-in tactics or if argument is given, display detailed information on tactic.\n";
std::cout << " -simplifiers[:name] display built-in simplifiers or if argument is given, display detailed information on simplifier.\n";
std::cout << " -probes display avilable probes.\n";
std::cout << " --" << " all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.\n";
std::cout << "\nResources:\n";
std::cout << " -T:timeout set the timeout (in seconds).\n";
std::cout << " -t:timeout set the soft timeout (in milli seconds). It only kills the current query.\n";
std::cout << " -memory:Megabytes set a limit for virtual memory consumption.\n";
std::cout << "\nOutput:\n";
std::cout << " -st display statistics.\n";
#if defined(Z3DEBUG) || defined(_TRACE)
std::cout << "\nDebugging support:\n";
#endif
#ifdef _TRACE
std::cout << " -tr:tag enable trace messages tagged with <tag>.\n";
#endif
#ifdef Z3DEBUG
std::cout << " -dbg:tag enable assertions tagged with <tag>.\n";
#endif
std::cout << "\nParameter setting:\n";
std::cout << "Global and module parameters can be set in the command line.\n";
std::cout << " param_name=value for setting global parameters.\n";
std::cout << " module_name.param_name=value for setting module parameters.\n";
std::cout << "Use 'z3 -p' for the complete list of global and module parameters.\n";
}
static bool validate_is_ulong(char const* s) {
for (; *s; ++s)
if (*s < '0' || *s > '9')
return false;
return true;
}
static bool is_tptp_extension(char const* ext) {
static char const* tptp_extensions[] = {"p", "tptp", "fof", "cnf", "tff", "thf"};
for (char const* known_ext : tptp_extensions) {
if (strcmp(ext, known_ext) == 0)
return true;
}
return false;
}
static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv) {
long timeout = 0;
int i = 1;
char * eq_pos = nullptr;
while (i < argc) {
char * arg = argv[i];
if (arg[0] == '-' && arg[1] == '-' && arg[2] == 0) {
if (g_input_file) {
warning_msg("input file was already specified.");
break;
}
i++;
input_file = "";
for (; i < argc; ++i) {
input_file += argv[i];
if (i < argc - 1)
input_file += " ";
}
g_input_file = input_file.c_str();
break;
}
if (arg[0] == '-'
#ifdef _WINDOWS
|| arg[0] == '/'
#endif
) {
char * opt_name = arg + 1;
if (*opt_name == '-')
opt_name++;
char * opt_arg = nullptr;
char * colon = strchr(arg, ':');
if (colon) {
opt_arg = colon + 1;
*colon = 0;
}
if (strcmp(opt_name, "h") == 0 || strcmp(opt_name, "?") == 0 || strcmp(opt_name, "help") == 0) {
display_usage();
exit(0);
}
if (strcmp(opt_name, "version") == 0) {
std::cout << "Z3 version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER;
std::cout << " - ";
#if defined(__LP64__) || defined(_WIN64)
std::cout << "64";
#else
std::cout << "32";
#endif
std::cout << " bit";
#ifdef Z3GITHASH
std::cout << " - build hashcode " << STRINGIZE_VALUE_OF(Z3GITHASH);
#endif
std::cout << "\n";
exit(0);
}
else if (strcmp(opt_name, "smt2") == 0) {
g_input_kind = IN_SMTLIB_2;
}
else if (strcmp(opt_name, "dl") == 0) {
g_input_kind = IN_DATALOG;
}
else if (strcmp(opt_name, "in") == 0) {
g_standard_input = true;
}
else if (strcmp(opt_name, "dimacs") == 0) {
g_input_kind = IN_DIMACS;
}
else if (strcmp(opt_name, "wcnf") == 0) {
g_input_kind = IN_WCNF;
}
else if (strcmp(opt_name, "pbo") == 0) {
g_input_kind = IN_OPB;
}
else if (strcmp(opt_name, "lp") == 0) {
g_input_kind = IN_LP;
}
else if (strcmp(opt_name, "log") == 0) {
g_input_kind = IN_Z3_LOG;
}
else if (strcmp(opt_name, "tptp") == 0) {
g_input_kind = IN_TPTP;
}
else if (strcmp(opt_name, "st") == 0) {
g_display_statistics = true;
gparams::set("stats", "true");
}
else if (strcmp(opt_name, "model") == 0) {
g_display_model = true;
}
else if (strcmp(opt_name, "ist") == 0) {
g_display_istatistics = true;
}
else if (strcmp(opt_name, "v") == 0) {
if (!opt_arg)
error("option argument (-v:level) is missing.");
if (!validate_is_ulong(opt_arg))
error("invalid argument for -v option, it must be a non-negative integer.");
long lvl = strtol(opt_arg, nullptr, 10);
set_verbosity_level(lvl);
}
else if (strcmp(opt_name, "file") == 0) {
g_input_file = opt_arg;
}
else if (strcmp(opt_name, "T") == 0) {
if (!opt_arg)
error("option argument (-T:timeout) is missing.");
if (!validate_is_ulong(opt_arg))
error("invalid argument for -T option, it must be a non-negative integer.");
timeout = strtol(opt_arg, nullptr, 10);
}
else if (strcmp(opt_name, "t") == 0) {
if (!opt_arg)
error("option argument (-t:timeout) is missing.");
gparams::set("timeout", opt_arg);
}
else if (strcmp(opt_name, "nw") == 0) {
enable_warning_messages(false);
}
else if (strcmp(opt_name, "p") == 0) {
gparams::display(std::cout, 0, false, false);
exit(0);
}
else if (strcmp(opt_name, "pd") == 0) {
gparams::display(std::cout, 0, false, true);
exit(0);
}
else if (strcmp(opt_name, "pmmd") == 0) {
if (opt_arg)
gparams::display_module_markdown(std::cout, opt_arg);
else {
gparams::display_modules(std::cout);
std::cout << "\nUse -pm:name to display all parameters available at module 'name'\n";
}
exit(0);
}
else if (strcmp(opt_name, "pm") == 0) {
if (opt_arg) {
gparams::display_module(std::cout, opt_arg);
}
else {
gparams::display_modules(std::cout);
std::cout << "\nUse -pm:name to display all parameters available at module 'name'\n";
}
exit(0);
}
else if (strcmp(opt_name, "pp") == 0) {
if (!opt_arg)
error("option argument (-pp:name) is missing.");
gparams::display_parameter(std::cout, opt_arg);
exit(0);
}
#ifdef _TRACE
else if (strcmp(opt_name, "tr") == 0) {
if (!opt_arg)
error("option argument (-tr:tag) is missing.");
enable_trace(opt_arg);
}
#endif
else if (strcmp(opt_name, "dbg") == 0) {
if (!opt_arg)
error("option argument (-dbg:tag) is missing.");
enable_debug(opt_arg);
}
else if (strcmp(opt_name, "memory") == 0) {
if (!opt_arg)
error("option argument (-memory:val) is missing.");
gparams::set("memory_max_size", opt_arg);
}
else if (strcmp(opt_name, "tactics") == 0) {
if (!opt_arg)
help_tactics();
else
help_tactic(opt_arg, false);
}
else if (strcmp(opt_name, "simplifiers") == 0) {
if (!opt_arg)
help_simplifiers();
else
help_simplifier(opt_arg, false);
}
else if (strcmp(opt_name, "tacticsmd") == 0 && opt_arg)
help_tactic(opt_arg, true);
else if (strcmp(opt_name, "probes") == 0)
help_probes();
else {
std::cerr << "Error: invalid command line option: " << arg << "\n";
std::cerr << "For usage information: z3 -h\n";
exit(ERR_CMD_LINE);
}
}
else if (argv[i][0] != '"' && (eq_pos = strchr(argv[i], '='))) {
std::string parameter_name(argv[i], eq_pos);
bool known_parameter = false;
try {
gparams::get_value(parameter_name.c_str());
known_parameter = true;
}
catch (gparams::exception const&) {
if (parameter_name.find('.') != std::string::npos &&
parameter_name.find_first_of("/\\") == std::string::npos)
throw default_exception("unknown parameter '" + parameter_name + "'");
}
if (known_parameter) {
*eq_pos = 0;
gparams::set(argv[i], eq_pos + 1);
i++;
continue;
}
static char const * known_input_extensions[] = {
"smt2", "smt", "dimacs", "cnf", "wcnf", "opb", "lp", "log", "drat", "p"
};
bool is_filepath = strchr(argv[i], '/') || strchr(argv[i], '\\');
if (!is_filepath) {
char const * ext = get_extension(argv[i]);
if (ext)
for (char const * known_ext : known_input_extensions)
if (strcmp(ext, known_ext) == 0) {
is_filepath = true;
break;
}
}
char const * arg_ext = get_extension(arg);
if (arg_ext && strcmp(arg_ext, "drat") == 0) {
g_input_kind = IN_DRAT;
g_drat_input_file = arg;
}
else if (is_filepath && !g_input_file) {
g_input_file = arg;
}
else {
char * key = argv[i];
*eq_pos = 0;
char * value = eq_pos+1;
gparams::set(key, value);
}
}
else {
char const * arg_ext = get_extension(arg);
if (arg_ext && strcmp(arg_ext, "drat") == 0) {
g_input_kind = IN_DRAT;
g_drat_input_file = arg;
}
else if (g_input_file)
warning_msg("input file was already specified.");
else
g_input_file = arg;
}
i++;
}
if (timeout)
set_timeout(timeout * 1000);
}
int STD_CALL main(int argc, char ** argv) {
try {
unsigned return_value = 0;
memory::initialize(0);
memory::exit_when_out_of_memory(true, "ERROR: out of memory");
std::string input_file;
parse_cmd_line_args(input_file, argc, argv);
env_params::updt_params();
if (g_input_file && g_standard_input) {
error("using standard input to read formula.");
}
if (!g_input_file && !g_standard_input) {
error("input file was not specified.");
}
if (g_input_kind == IN_UNSPECIFIED) {
g_input_kind = IN_SMTLIB_2;
char const * ext = get_extension(g_input_file);
if (ext) {
if (strcmp(ext, "datalog") == 0 || strcmp(ext, "dl") == 0) {
g_input_kind = IN_DATALOG;
}
else if (strcmp(ext, "dimacs") == 0 || strcmp(ext, "cnf") == 0) {
g_input_kind = IN_DIMACS;
}
else if (strcmp(ext, "wcnf") == 0) {
g_input_kind = IN_WCNF;
}
else if (strcmp(ext, "opb") == 0) {
g_input_kind = IN_OPB;
}
else if (strcmp(ext, "lp") == 0) {
g_input_kind = IN_LP;
}
else if (strcmp(ext, "log") == 0) {
g_input_kind = IN_Z3_LOG;
}
else if (strcmp(ext, "smt2") == 0) {
g_input_kind = IN_SMTLIB_2;
}
else if (is_tptp_extension(ext)) {
g_input_kind = IN_TPTP;
}
}
}
switch (g_input_kind) {
case IN_SMTLIB_2:
memory::exit_when_out_of_memory(true, "(error \"out of memory\")");
return_value = read_smtlib2_commands(g_input_file);
break;
case IN_DIMACS:
return_value = read_dimacs(g_input_file);
break;
case IN_WCNF:
return_value = parse_opt(g_input_file, wcnf_t);
break;
case IN_OPB:
return_value = parse_opt(g_input_file, opb_t);
break;
case IN_LP:
return_value = parse_opt(g_input_file, lp_t);
break;
case IN_DATALOG:
read_datalog(g_input_file);
break;
case IN_Z3_LOG:
replay_z3_log(g_input_file);
break;
case IN_DRAT:
return_value = read_drat(g_drat_input_file);
break;
case IN_TPTP:
return_value = read_tptp(g_input_file);
break;
default:
UNREACHABLE();
}
disable_timeout();
memory::finalize();
#ifdef _WINDOWS
_CrtDumpMemoryLeaks();
#endif
return return_value;
}
catch (z3_exception & ex) {
std::cerr << "ERROR: " << ex.what() << "\n";
if (ex.has_error_code())
return ex.error_code();
else
return ERR_INTERNAL_FATAL;
}
}