From 598fc810b57462552f69f69110fbc0930d772d8d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 20 Feb 2019 15:34:47 +0100
Subject: [PATCH] adding FP
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/solver/smt_logics.cpp | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp
index d0fd8f809..a8dcf2f90 100644
--- a/src/solver/smt_logics.cpp
+++ b/src/solver/smt_logics.cpp
@@ -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) {