mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

add SMTLIB2.6 names for QF_SLIA and string-int conversion operators (#4341)

Browse source
This commit is contained in:
Murphy Berzish 2020-05-16 16:31:47 -05:00 • committed by GitHub
parent 21c4d451d8
commit 6f0a367357
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 14 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/seq_decl_plugin.cpp
View file

@ -622,8 +622,8 @@ void seq_decl_plugin::init() {
m_sigs[OP_STRING_CONST] = nullptr; m_sigs[OP_STRING_CONST] = nullptr;
m_sigs[_OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT); m_sigs[_OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT);
m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT); m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
m_sigs[OP_STRING_ITOS] = alloc(psig, m, "int.to.str", 0, 1, &intT, strT); m_sigs[OP_STRING_ITOS] = alloc(psig, m, "str.from_int", 0, 1, &intT, strT);
m_sigs[OP_STRING_STOI] = alloc(psig, m, "str.to.int", 0, 1, &strT, intT); m_sigs[OP_STRING_STOI] = alloc(psig, m, "str.to_int", 0, 1, &strT, intT);
m_sigs[OP_STRING_LT] = alloc(psig, m, "str.<", 0, 2, str2T, boolT); m_sigs[OP_STRING_LT] = alloc(psig, m, "str.<", 0, 2, str2T, boolT);
m_sigs[OP_STRING_LE] = alloc(psig, m, "str.<=", 0, 2, str2T, boolT); m_sigs[OP_STRING_LE] = alloc(psig, m, "str.<=", 0, 2, str2T, boolT);
m_sigs[_OP_STRING_CONCAT] = alloc(psig, m, "str.++", 1, 2, str2T, strT); m_sigs[_OP_STRING_CONCAT] = alloc(psig, m, "str.++", 1, 2, str2T, strT);
@ -928,7 +928,13 @@ void seq_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
} }
} }
op_names.push_back(builtin_name("str.in.re", _OP_STRING_IN_REGEXP)); op_names.push_back(builtin_name("str.in.re", _OP_STRING_IN_REGEXP));
op_names.push_back(builtin_name("str.in-re", _OP_STRING_IN_REGEXP));
op_names.push_back(builtin_name("str.to.re", _OP_STRING_TO_REGEXP)); op_names.push_back(builtin_name("str.to.re", _OP_STRING_TO_REGEXP));
op_names.push_back(builtin_name("str.to-re", _OP_STRING_TO_REGEXP));
op_names.push_back(builtin_name("str.to-int", OP_STRING_STOI));
op_names.push_back(builtin_name("str.to.int", OP_STRING_STOI));
op_names.push_back(builtin_name("str.from-int", OP_STRING_ITOS));
op_names.push_back(builtin_name("int.to.str", OP_STRING_ITOS));
op_names.push_back(builtin_name("re.nostr", _OP_REGEXP_EMPTY)); op_names.push_back(builtin_name("re.nostr", _OP_REGEXP_EMPTY));
op_names.push_back(builtin_name("re.complement", OP_RE_COMPLEMENT)); op_names.push_back(builtin_name("re.complement", OP_RE_COMPLEMENT));
} }

2
src/cmd_context/check_logic.cpp
View file

@ -182,7 +182,7 @@ struct check_logic::imp {
m_bvs = true; m_bvs = true;
m_quantifiers = true; m_quantifiers = true;
} }
else if (logic == "QF_S") { else if (logic == "QF_S" || logic == "QF_SLIA") {
m_uf = true; m_uf = true;
m_bvs = true; m_bvs = true;
m_ints = true; m_ints = true;

4
src/smt/smt_setup.cpp
View file

@ -129,7 +129,7 @@ namespace smt {
setup_QF_FP(); setup_QF_FP();
else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP") else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP")
setup_QF_FPBV(); setup_QF_FPBV();
else if (m_logic == "QF_S") else if (m_logic == "QF_S" || m_logic == "QF_SLIA")
setup_QF_S(); setup_QF_S();
else if (m_logic == "QF_DT") else if (m_logic == "QF_DT")
setup_QF_DT(); setup_QF_DT();
@ -177,7 +177,7 @@ namespace smt {
setup_QF_BVRE(); setup_QF_BVRE();
else if (m_logic == "QF_AUFLIA") else if (m_logic == "QF_AUFLIA")
setup_QF_AUFLIA(st); setup_QF_AUFLIA(st);
else if (m_logic == "QF_S") else if (m_logic == "QF_S" || m_logic == "QF_SLIA")
setup_QF_S(); setup_QF_S();
else if (m_logic == "AUFLIA") else if (m_logic == "AUFLIA")
setup_AUFLIA(st); setup_AUFLIA(st);

5
src/solver/smt_logics.cpp
View file

@ -85,6 +85,7 @@ bool smt_logics::logic_has_arith(symbol const & s) {
s == "QF_FPBV" || s == "QF_FPBV" ||
s == "QF_BVFP" || s == "QF_BVFP" ||
s == "QF_S" || s == "QF_S" ||
s == "QF_SLIA" ||
logic_is_allcsp(s) || logic_is_allcsp(s) ||
s == "QF_FD" || s == "QF_FD" ||
s == "HORN" || s == "HORN" ||
@ -135,11 +136,11 @@ bool smt_logics::logic_has_array(symbol const & s) {
} }
bool smt_logics::logic_has_seq(symbol const & s) { bool smt_logics::logic_has_seq(symbol const & s) {
return s == "QF_BVRE" || s == "QF_S" || logic_is_allcsp(s); return s == "QF_BVRE" || s == "QF_S" || s == "QF_SLIA" || logic_is_allcsp(s);
} }
bool smt_logics::logic_has_str(symbol const & s) { bool smt_logics::logic_has_str(symbol const & s) {
return s == "QF_S" || logic_is_allcsp(s); return s == "QF_S" || s == "QF_SLIA" || logic_is_allcsp(s);
} }
bool smt_logics::logic_has_fpa(symbol const & s) { bool smt_logics::logic_has_fpa(symbol const & s) {