mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
More renaming QF_FPA -> QF_FP
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
21a847d299
commit
afae49b9ed
|
@ -512,8 +512,8 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
|
|||
s == "UFNIA" ||
|
||||
s == "LIA" ||
|
||||
s == "LRA" ||
|
||||
s == "QF_FPA" ||
|
||||
s == "QF_FPABV" ||
|
||||
s == "QF_FP" ||
|
||||
s == "QF_FPBV" ||
|
||||
s == "HORN";
|
||||
}
|
||||
|
||||
|
@ -532,7 +532,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
|
|||
s == "QF_ABV" ||
|
||||
s == "QF_AUFBV" ||
|
||||
s == "QF_BVRE" ||
|
||||
s == "QF_FPABV" ||
|
||||
s == "QF_FPBV" ||
|
||||
s == "HORN";
|
||||
}
|
||||
|
||||
|
@ -557,7 +557,7 @@ bool cmd_context::logic_has_seq() const {
|
|||
}
|
||||
|
||||
bool cmd_context::logic_has_floats() const {
|
||||
return !has_logic() || m_logic == "QF_FPA" || m_logic == "QF_FPABV";
|
||||
return !has_logic() || m_logic == "QF_FP" || m_logic == "QF_FPBV";
|
||||
}
|
||||
|
||||
bool cmd_context::logic_has_array_core(symbol const & s) const {
|
||||
|
@ -668,7 +668,7 @@ bool cmd_context::supported_logic(symbol const & s) const {
|
|||
logic_has_arith_core(s) || logic_has_bv_core(s) ||
|
||||
logic_has_array_core(s) || logic_has_seq_core(s) ||
|
||||
logic_has_horn(s) ||
|
||||
s == "QF_FPA" || s == "QF_FPABV";
|
||||
s == "QF_FP" || s == "QF_FPBV";
|
||||
}
|
||||
|
||||
bool cmd_context::set_logic(symbol const & s) {
|
||||
|
|
|
@ -680,11 +680,11 @@ namespace smt {
|
|||
setup_mi_arith();
|
||||
}
|
||||
|
||||
void setup::setup_QF_FPA() {
|
||||
void setup::setup_QF_FP() {
|
||||
m_context.register_plugin(alloc(smt::theory_fpa, m_manager));
|
||||
}
|
||||
|
||||
void setup::setup_QF_FPABV() {
|
||||
void setup::setup_QF_FPBV() {
|
||||
setup_QF_BV();
|
||||
m_context.register_plugin(alloc(smt::theory_fpa, m_manager));
|
||||
}
|
||||
|
|
|
@ -75,8 +75,8 @@ namespace smt {
|
|||
void setup_QF_AX(static_features const & st);
|
||||
void setup_QF_AUFLIA();
|
||||
void setup_QF_AUFLIA(static_features const & st);
|
||||
void setup_QF_FPA();
|
||||
void setup_QF_FPABV();
|
||||
void setup_QF_FP();
|
||||
void setup_QF_FPBV();
|
||||
void setup_LRA();
|
||||
void setup_AUFLIA(bool simple_array = true);
|
||||
void setup_AUFLIA(static_features const & st);
|
||||
|
|
Loading…
Reference in a new issue