mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-03 07:37:54 +00:00
Code Activity

benchmark patching

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-05-20 13:32:10 -07:00
parent bc6c38e7d3
commit 2ba86c1ac3
3 changed files with 583 additions and 390 deletions
Download patch file Download diff file Expand all files Collapse all files

929
src/cmd_context/tptp_frontend.cpp
View file

File diff suppressed because it is too large Load diff

33
src/shell/main.cpp
View file

@ -337,10 +337,35 @@ static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv)
} }
} }
else if (argv[i][0] != '"' && (eq_pos = strchr(argv[i], '='))) { else if (argv[i][0] != '"' && (eq_pos = strchr(argv[i], '='))) {
char * key = argv[i]; // If the argument looks like a file path (contains path separators
*eq_pos = 0; // or has a file extension), treat it as a filename rather than
char * value = eq_pos+1; // a parameter assignment. This handles files with '=' in their names.
gparams::set(key, value); bool is_filepath = strchr(argv[i], '/') || strchr(argv[i], '\\');
if (!is_filepath) {
char const * ext = get_extension(argv[i]);
if (ext && (strcmp(ext, "smt2") == 0 || strcmp(ext, "smt") == 0 ||
strcmp(ext, "dimacs") == 0 || strcmp(ext, "cnf") == 0 ||
strcmp(ext, "wcnf") == 0 || strcmp(ext, "opb") == 0 ||
strcmp(ext, "lp") == 0 || strcmp(ext, "log") == 0 ||
strcmp(ext, "drat") == 0 || strcmp(ext, "p") == 0))
is_filepath = true;
}
if (is_filepath) {
if (get_extension(arg) && strcmp(get_extension(arg), "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;
}
else {
char * key = argv[i];
*eq_pos = 0;
char * value = eq_pos+1;
gparams::set(key, value);
}
} }
else { else {
if (get_extension(arg) && strcmp(get_extension(arg), "drat") == 0) { if (get_extension(arg) && strcmp(get_extension(arg), "drat") == 0) {

11
src/solver/smt_logics.cpp
View file

@ -50,10 +50,7 @@ bool smt_logics::logic_has_arith(symbol const & s) {
str.find("IDL") != std::string::npos || str.find("IDL") != std::string::npos ||
str.find("RDL") != std::string::npos || str.find("RDL") != std::string::npos ||
str == "QF_BVRE" || str == "QF_BVRE" ||
str == "QF_FP" || logic_has_fpa(s) ||
str == "FP" ||
str == "QF_FPBV" ||
str == "QF_BVFP" ||
str == "QF_S" || str == "QF_S" ||
logic_is_all(s) || logic_is_all(s) ||
str == "QF_FD" || str == "QF_FD" ||
@ -102,11 +99,7 @@ bool smt_logics::logic_has_str(symbol const & s) {
bool smt_logics::logic_has_fpa(symbol const & s) { bool smt_logics::logic_has_fpa(symbol const & s) {
auto str = s.str(); auto str = s.str();
return str == "FP" || return str.find("FP") != std::string::npos ||
str == "QF_FP" ||
str == "QF_FPBV" ||
str == "QF_BVFP" ||
str == "QF_FPLRA" ||
logic_is_all(s); logic_is_all(s);
} }