mirror of
https://github.com/Z3Prover/z3
synced 2025-04-20 23:56:37 +00:00
Minor
This commit is contained in:
parent
e3566288a4
commit
a3a3921234
|
@ -1075,10 +1075,9 @@ namespace sls {
|
|||
b += strval0(y);
|
||||
}
|
||||
|
||||
// std::cout << "Repair down " << mk_pp(eq, m) << ": \"" << a << "\" = \"" << b << "\"" << std::endl;
|
||||
|
||||
if (a == b)
|
||||
return update(eq->get_arg(0), a) && update(eq->get_arg(1), b);
|
||||
return true;
|
||||
// return update(eq->get_arg(0), a) && update(eq->get_arg(1), b);
|
||||
|
||||
unsigned diff = edit_distance(a, b);
|
||||
|
||||
|
@ -1473,7 +1472,6 @@ namespace sls {
|
|||
zstring sb = strval0(b);
|
||||
unsigned lena = sa.length();
|
||||
unsigned lenb = sb.length();
|
||||
verbose_stream() << "repair prefixof " << mk_bounded_pp(e, m) << "\n";
|
||||
if (ctx.is_true(e)) {
|
||||
unsigned n = std::min(lena, lenb);
|
||||
if (!is_value(a)) {
|
||||
|
|
|
@ -103,6 +103,7 @@ bool smt_logics::logic_has_bv(symbol const & s) {
|
|||
s == "QF_UFBV" ||
|
||||
s == "QF_ABV" ||
|
||||
s == "QF_AUFBV" ||
|
||||
s == "QF_UFBVDT" ||
|
||||
s == "QF_BVRE" ||
|
||||
s == "QF_FPBV" ||
|
||||
s == "FP" ||
|
||||
|
@ -149,7 +150,7 @@ bool smt_logics::logic_has_fpa(symbol const & s) {
|
|||
}
|
||||
|
||||
bool smt_logics::logic_has_uf(symbol const & s) {
|
||||
return s == "QF_UF" || s == "UF" || s == "QF_UFDT" || s == "SMTFD";
|
||||
return s == "QF_UF" || s == "UF" || s == "QF_UFDT" || s == "QF_UFBVDT" || s == "SMTFD";
|
||||
}
|
||||
|
||||
bool smt_logics::logic_has_horn(symbol const& s) {
|
||||
|
@ -161,6 +162,6 @@ bool smt_logics::logic_has_pb(symbol const& s) {
|
|||
}
|
||||
|
||||
bool smt_logics::logic_has_datatype(symbol const& s) {
|
||||
return s == "QF_FD" || s == "QF_UFDT" || logic_is_all(s) || s == "QF_DT" || logic_has_horn(s);
|
||||
return s == "QF_FD" || s == "QF_UFDT" || s == "QF_UFBVDT" || logic_is_all(s) || s == "QF_DT" || logic_has_horn(s);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue