mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

adding FP

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-20 15:34:47 +01:00
parent 3548057bd1
commit 598fc810b5
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/solver/smt_logics.cpp
View file

@ -80,6 +80,7 @@ bool smt_logics::logic_has_arith(symbol const & s) {
s == "LRA" ||
s == "UFIDL" ||
s == "QF_FP" ||
s == "FP" ||
s == "QF_FPBV" ||
s == "QF_BVFP" ||
s == "QF_S" ||
@ -101,6 +102,7 @@ bool smt_logics::logic_has_bv(symbol const & s) {
s == "QF_AUFBV" ||
s == "QF_BVRE" ||
s == "QF_FPBV" ||
s == "FP" ||
s == "QF_BVFP" ||
logic_is_allcsp(s) ||
s == "QF_FD" ||
@ -138,7 +140,7 @@ bool smt_logics::logic_has_str(symbol const & s) {
}
bool smt_logics::logic_has_fpa(symbol const & s) {
return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA" || logic_is_allcsp(s);
return s == "FP" || s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA" || logic_is_allcsp(s);
}
bool smt_logics::logic_has_uf(symbol const & s) {