From f4954e9d7ff40c2199c18bcf4d9a6bd886fefdf1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 13 Oct 2015 09:24:02 -0700
Subject: [PATCH] fix for fixed size rational difference logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_diff_logic.h | 13 +++++--------
1 file changed, 5 insertions(+), 8 deletions(-)
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index cb86e6679..ed96d050e 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -399,7 +399,6 @@ namespace smt {
};
struct sidl_ext {
- // TODO: It doesn't need to be a rational, but a bignum integer.
static const bool m_int_theory = true;
typedef s_integer numeral;
typedef s_integer fin_numeral;
@@ -415,13 +414,11 @@ namespace smt {
rdl_ext() : m_epsilon(rational(), true) {}
};
- struct srdl_ext {
- static const bool m_int_theory = false;
- typedef inf_s_integer numeral;
- typedef s_integer fin_numeral;
- numeral m_epsilon;
- srdl_ext() : m_epsilon(s_integer(0),true) {}
- };
+ //
+ // there is no s_rational class, so
+ // instead we use multi-precision rationals.
+ //
+ struct srdl_ext : public rdl_ext {};
typedef theory_diff_logic<idl_ext> theory_idl;
typedef theory_diff_logic<sidl_ext> theory_fidl;