Skip to content

Commit f34218e

Browse files
TomaqaTomaqa
committed
[[stash]]
1 parent ce8ba63 commit f34218e

File tree

11 files changed

+280
-4
lines changed

11 files changed

+280
-4
lines changed

‎.clang-files‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@
1414
./src/common/ApiException.h
1515
./src/common/FlaPartitionMap.cc
1616
./src/common/FlaPartitionMap.h
17+
./src/common/Float.cc
18+
./src/common/Float.h
1719
./src/common/InternalException.h
1820
./src/common/Number.h
1921
./src/common/PartitionInfo.cc

‎CMakeLists.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,7 @@ endif()
120120
add_subdirectory(${CMAKE_SOURCE_DIR})
121121

122122
################# TESTING #############################################
123+
set(PACKAGE_TESTS OFF)
123124
if(PACKAGE_TESTS)
124125
if (NOT BUILD_SHARED_LIBS)
125126
message(FATAL_ERROR "Building tests requires shared libraries")

‎src/common/CMakeLists.txt‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ add_library(common OBJECT "")
33
target_sources(common
44
PUBLIC
55
"${CMAKE_CURRENT_LIST_DIR}/FastRational.cc"
6+
"${CMAKE_CURRENT_LIST_DIR}/Float.cc"
67
"${CMAKE_CURRENT_LIST_DIR}/FlaPartitionMap.cc"
78
"${CMAKE_CURRENT_LIST_DIR}/Real.h"
89
PRIVATE
@@ -22,7 +23,7 @@ target_sources(common
2223
)
2324

2425
install(FILES
25-
Integer.h Number.h FastRational.h StringMap.h Timer.h inttypes.h
26+
Integer.h Number.h FastRational.h Float.h StringMap.h Timer.h inttypes.h
2627
TreeOps.h Real.h FlaPartitionMap.h PartitionInfo.h ApiException.h TypeUtils.h
2728
NumberUtils.h NatSet.h ScopedVector.h
2829
DESTINATION ${INSTALL_HEADERS_DIR}/common)

‎src/common/Float.cc‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
#include "Float.h"
2+
3+
#include <common/ApiException.h>
4+
5+
#include <iostream>
6+
#include <iomanip>
7+
#include <sstream>
8+
#include <string>
9+
10+
namespace opensmt {
11+
using namespace std::literals::string_literals;
12+
13+
Float::Float(char const * str) {
14+
auto & val = value();
15+
16+
std::istringstream is(str);
17+
is >> val;
18+
if (is && is.eof()) {
19+
assert(normalized(val));
20+
return;
21+
}
22+
23+
Value rhs;
24+
char c = is.get();
25+
assert(is);
26+
if (c != '/') {
27+
throw ApiException("Expected '/' after "s + std::to_string(val) + ", got: " + std::string(str));
28+
}
29+
is >> std::noskipws >> rhs;
30+
if (is && is.eof()) {
31+
val /= rhs;
32+
assert(normalized(val));
33+
return;
34+
}
35+
36+
throw ApiException("Cannot convert to float: "s + std::string(str));
37+
}
38+
39+
std::string Float::get_str() const {
40+
std::ostringstream os;
41+
print(os);
42+
auto str = os.str();
43+
//- assert(value() != 0.0 || str == "0");
44+
//- assert(value() != -0.0 || str == "0");
45+
assert(!isZero() || str == "0");
46+
return str;
47+
}
48+
49+
void Float::print(std::ostream & os) const {
50+
//- assert(value() != -0.0 || isZero());
51+
//- if (isZero()) {
52+
//- os << "0";
53+
//- return;
54+
//- }
55+
//- !!!
56+
//- else if (value() == 0.5) os << "1/2";
57+
//- std::cerr << value() << std::endl;
58+
assert(!isZero() || !std::signbit(value()));
59+
//- os << std::fixed << std::setprecision(20) << value();
60+
os << std::setprecision(std::numeric_limits<Value>::max_digits10) << value();
61+
}
62+
}

‎src/common/Float.h‎

Lines changed: 177 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,177 @@
1+
#ifndef OPENSMT_FLOAT_H
2+
#define OPENSMT_FLOAT_H
3+
4+
//- !!!
5+
#include "InternalException.h"
6+
7+
#include <string>
8+
#include <concepts>
9+
#include <cassert>
10+
#include <cmath>
11+
12+
namespace opensmt {
13+
class Float {
14+
public:
15+
struct Hash;
16+
17+
using Value = double;
18+
19+
static_assert(std::floating_point<Value>);
20+
21+
Float() = default;
22+
~Float() = default;
23+
Float(Float const &) = default;
24+
Float(Float &&) = default;
25+
Float & operator =(Float const &) = default;
26+
Float & operator =(Float &&) = default;
27+
28+
constexpr Float(Value) noexcept;
29+
constexpr Float(std::floating_point auto val) : Float(Value(val)) { }
30+
constexpr Float(std::integral auto val) : Float(Value(val)) { }
31+
explicit constexpr Float(std::integral auto den, std::integral auto num);
32+
explicit Float(char const *);
33+
34+
Value value() const noexcept { return _value; }
35+
Value & value() noexcept { return _value; }
36+
37+
int sign() const {
38+
auto const val = value();
39+
if (val > 0) return 1;
40+
if (val < 0) return -1;
41+
return 0;
42+
}
43+
44+
bool isZero() const { return value() == 0; }
45+
bool isOne() const { return value() == 1; }
46+
47+
bool isInteger() const {
48+
auto const val = value();
49+
return val == std::trunc(val);
50+
}
51+
52+
bool operator ==(Float const & other) const { return value() == other.value(); }
53+
bool operator !=(Float const & other) const { return value() != other.value(); }
54+
bool operator < (Float const & other) const { return value() < other.value(); }
55+
bool operator > (Float const & other) const { return value() > other.value(); }
56+
bool operator <=(Float const & other) const { return value() <= other.value(); }
57+
bool operator >=(Float const & other) const { return value() >= other.value(); }
58+
59+
int compare(Float const & other) const {
60+
if (*this > other) return 1;
61+
if (*this < other) return -1;
62+
return 0;
63+
}
64+
65+
Float operator -() const { return -value(); }
66+
Float operator +() const { return value(); }
67+
Float operator +(Float const & other) const { return value() + other.value(); }
68+
Float operator -(Float const & other) const { return value() - other.value(); }
69+
Float operator *(Float const & other) const { return value() * other.value(); }
70+
Float operator /(Float const & other) const { return value() / other.value(); }
71+
Float & operator +=(Float const & other) { value() += other.value(); return *this; }
72+
Float & operator -=(Float const & other) { value() -= other.value(); return *this; }
73+
Float & operator *=(Float const & other) { value() *= other.value(); return *this; }
74+
Float & operator /=(Float const & other) { value() /= other.value(); return *this; }
75+
76+
//- !!!!
77+
Float operator %(Float const & other) const { throw InternalException("forbidden"); }
78+
79+
Float abs() const {
80+
return std::abs(value());
81+
}
82+
83+
Float inverse() const {
84+
return 1./value();
85+
}
86+
87+
Float ceil() const {
88+
return std::ceil(value());
89+
}
90+
91+
Float floor() const {
92+
return std::floor(value());
93+
}
94+
95+
void negate() & {
96+
if (isZero()) return;
97+
value() = -value();
98+
assert(normalized(value()));
99+
}
100+
101+
void reset() & noexcept {
102+
value() = 0;
103+
}
104+
105+
double get_d() const { return value(); }
106+
107+
std::string get_str() const;
108+
void print(std::ostream &) const;
109+
friend std::ostream & operator <<(std::ostream & os, Float const & x) {
110+
x.print(os);
111+
return os;
112+
}
113+
114+
//- !!!!!!!
115+
Float get_den() const { throw InternalException("forbidden"); }
116+
protected:
117+
static constexpr bool normalized(Value) noexcept;
118+
static constexpr Value normalize(Value) noexcept;
119+
private:
120+
Value _value;
121+
};
122+
}
123+
124+
namespace opensmt {
125+
struct Float::Hash {
126+
std::size_t operator ()(Float const & x) const noexcept {
127+
return std::hash<Float::Value>{}(x.value());
128+
}
129+
};
130+
131+
constexpr Float::Float(Value val) noexcept : _value{normalize(val)} { }
132+
133+
constexpr Float::Float(std::integral auto den, std::integral auto num) : Float(Value(den)/Value(num)) {
134+
assert(normalized(value()));
135+
}
136+
137+
constexpr bool Float::normalized(Value val) noexcept {
138+
return !std::signbit(val) || val < 0;
139+
}
140+
141+
constexpr Float::Value Float::normalize(Value val) noexcept {
142+
static_assert(0. == -0.);
143+
if (val == 0) {
144+
static_assert(normalized(0));
145+
return 0;
146+
}
147+
assert(normalized(val));
148+
return val;
149+
}
150+
151+
inline Float abs(Float const & x) { return x.abs(); }
152+
153+
inline int cmpabs(Float const & a, Float const & b) {
154+
return abs(a).compare(abs(b));
155+
};
156+
157+
inline void addition (Float & dst, Float const & a, Float const & b) { dst = a + b; }
158+
inline void subtraction (Float & dst, Float const & a, Float const & b) { dst = a - b; }
159+
inline void multiplication(Float & dst, Float const & a, Float const & b) { dst = a * b; }
160+
inline void division (Float & dst, Float const & a, Float const & b) { dst = a / b; }
161+
inline void additionAssign (Float & a, Float const & b) { a += b; }
162+
inline void subtractionAssign (Float & a, Float const & b) { a -= b; }
163+
inline void multiplicationAssign(Float & a, Float const & b) { a *= b; }
164+
inline void divisionAssign (Float & a, Float const & b) { a /= b; }
165+
166+
//- !!!!!!!
167+
inline Float gcd (Float const &, Float const &) { throw InternalException("forbidden"); }
168+
inline Float lcm (Float const &, Float const &) { throw InternalException("forbidden"); }
169+
inline Float fastrat_fdiv_q(Float const &, Float const &) { throw InternalException("forbidden"); }
170+
}
171+
172+
namespace std {
173+
template <>
174+
struct hash<opensmt::Float> : opensmt::Float::Hash {};
175+
}
176+
177+
#endif //OPENSMT_FLOAT_H

‎src/common/Number.h‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,13 @@
55
#ifndef OPENSMT_NUMBER_H
66
#define OPENSMT_NUMBER_H
77

8-
#define FAST_RATIONALS 1
8+
//- #define FAST_RATIONALS
9+
#define FLOATS
910

1011
#ifdef FAST_RATIONALS
1112
#include "FastRational.h"
13+
#elif defined(FLOATS)
14+
#include "Float.h"
1215
#else
1316
#include <gmpxx.h>
1417
#endif
@@ -17,6 +20,9 @@ namespace opensmt {
1720
#ifdef FAST_RATIONALS
1821
using Number = FastRational;
1922
using NumberHash = FastRationalHash;
23+
#elif defined(FLOATS)
24+
using Number = Float;
25+
using NumberHash = Float::Hash;
2026
#else
2127
using Number = mpq_class;
2228
#endif

‎src/logics/ArithLogic.cc‎

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -554,6 +554,13 @@ PTRef ArithLogic::mkConst(SRef sort, Number const & c) {
554554
for (auto i = numbers.size(); i <= id; i++) {
555555
numbers.emplace_back();
556556
}
557+
//- std::cerr << c << std::endl;
558+
//- std::cerr << val << std::endl;
559+
//- std::cerr << *numbers[id] << std::endl;
560+
//- double i;
561+
//- std::cerr << modf(c.value(), &i) << " + " << long(i) << std::endl;
562+
//- std::cerr << modf(numbers[id]->value(), &i) << " + " << long(i) << std::endl;
563+
//- std::cerr << std::endl;
557564
if (numbers[id] == nullptr) { numbers[id] = new Number(val); }
558565
assert(c == *numbers[id]);
559566
markConstant(id);
@@ -1213,9 +1220,11 @@ pair<Number, PTRef> ArithLogic::sumToNormalizedIntPair(PTRef sum) {
12131220
if (not allIntegers) {
12141221
// first ensure that all coeffs are integers
12151222
// this would probably not work when `Number` is not `FastRational`
1216-
using Integer = FastRational; // TODO: change when we have FastInteger
1223+
//- using Integer = FastRational; // TODO: change when we have FastInteger
1224+
using Integer = Number; // TODO: change when we have FastInteger
12171225
auto lcmOfDenominators = Integer(1);
1218-
auto accumulateLCMofDenominators = [&lcmOfDenominators](FastRational const & next) {
1226+
//- auto accumulateLCMofDenominators = [&lcmOfDenominators](FastRational const & next) {
1227+
auto accumulateLCMofDenominators = [&lcmOfDenominators](Number const & next) {
12191228
if (next.isInteger()) {
12201229
// denominator is 1 => lcm of denominators stays the same
12211230
return;

‎src/tsolvers/lasolver/Simplex.cc‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -354,6 +354,7 @@ bool Simplex::valueConsistent(LVRef v) const {
354354
sum += term.coeff * model->read(term.var);
355355
}
356356

357+
//- std::cerr << "<" << value << "> == <" << sum << ">" << std::endl;
357358
assert(value == sum);
358359
return value == sum;
359360
}

‎test/unit/test_LRALogicMkTerms.cc‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -183,6 +183,12 @@ TEST_F(LRALogicMkTermsTest, test_NonLinearException)
183183
TEST_F(LRALogicMkTermsTest, test_ConstantSimplification)
184184
{
185185
PTRef two = logic.mkConst("2");
186+
std::cerr << logic.printTerm_(two, true, true) << std::endl;
187+
std::cerr << two.x << std::endl;
188+
std::cerr << logic.printTerm_(logic.mkConst("1/2"), true, true) << std::endl;
189+
std::cerr << logic.mkConst("1/2").x << std::endl;
190+
std::cerr << logic.printTerm_(logic.mkRealDiv(logic.getTerm_RealOne(), two), true, true) << std::endl;
191+
std::cerr << logic.mkRealDiv(logic.getTerm_RealOne(), two).x << std::endl;
186192
EXPECT_EQ(logic.mkConst("1/2"), logic.mkRealDiv(logic.getTerm_RealOne(), two));
187193
EXPECT_EQ(two, logic.mkRealDiv(logic.mkConst("4"), two));
188194
}

‎test/unit/test_Rationals.cc‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@
55

66
namespace opensmt {
77

8+
#ifdef FAST_RATIONALS
9+
810
TEST(Rationals_test, test_division_int32min)
911
{
1012
// INT32_MIN
@@ -504,4 +506,6 @@ TEST(Rationals_test, testNormalization) {
504506
EXPECT_EQ(normalizedDen, 1000000);
505507
}
506508

509+
#endif // FAST_RATIONALS
510+
507511
}

0 commit comments

Comments
 (0)