mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
Added QF_BVFP logic alias for QF_FPBV
This commit is contained in:
parent
9de0e9087e
commit
f2f6fc1994
|
@ -528,6 +528,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
|
|||
s == "LRA" ||
|
||||
s == "QF_FP" ||
|
||||
s == "QF_FPBV" ||
|
||||
s == "QF_BVFP" ||
|
||||
s == "HORN";
|
||||
}
|
||||
|
||||
|
@ -547,6 +548,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
|
|||
s == "QF_AUFBV" ||
|
||||
s == "QF_BVRE" ||
|
||||
s == "QF_FPBV" ||
|
||||
s == "QF_BVFP" ||
|
||||
s == "HORN";
|
||||
}
|
||||
|
||||
|
|
|
@ -116,7 +116,7 @@ namespace smt {
|
|||
setup_LRA();
|
||||
else if (m_logic == "QF_FP")
|
||||
setup_QF_FP();
|
||||
else if (m_logic == "QF_FPBV")
|
||||
else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP")
|
||||
setup_QF_FPBV();
|
||||
else
|
||||
setup_unknown();
|
||||
|
|
|
@ -81,7 +81,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
|
|||
return mk_ufbv_tactic(m, p);
|
||||
else if (logic=="QF_FP")
|
||||
return mk_qffp_tactic(m, p);
|
||||
else if (logic == "QF_FPBV")
|
||||
else if (logic == "QF_FPBV" || logic == "QF_BVFP")
|
||||
return mk_qffpbv_tactic(m, p);
|
||||
else if (logic=="HORN")
|
||||
return mk_horn_tactic(m, p);
|
||||
|
|
Loading…
Reference in a new issue