Discrete implementation

.gitignore

@@ -1,6 +1,9 @@
 data/*
 build/
 .vscode/
+misc/
+debugger
+debugger.cpp
 
 *Zone.Identifier
 

CMakeLists.txt

@@ -13,12 +13,16 @@ endif()
 set(CMAKE_CXX_STANDARD 20)
 set(CMAKE_CXX_STANDARD_REQUIRED ON)
 
-# Define the Header-Only Library
-# "INTERFACE" means "I have no .cpp files to compile, just headers"
-add_library(do-verify INTERFACE)
+# Define the library with source files
+add_library(do-verify STATIC
+    src/interval_set.cpp
+    src/MTLEngine.cpp
+    src/binary_row_reader.cpp
+    src/json_reader.cpp
+)
 
 # Tell CMake where the headers are
-target_include_directories(do-verify INTERFACE
+target_include_directories(do-verify PUBLIC
     $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include>
     $<INSTALL_INTERFACE:include>
 )
@@ -32,7 +36,13 @@ FetchContent_Declare(
 )
 FetchContent_MakeAvailable(Catch2)
 
+
+add_executable(do-verify-bin 
+    src/main.cpp
+)
+
+target_link_libraries(do-verify-bin PRIVATE do-verify)
+
 # Add Subdirectories
 enable_testing()
 add_subdirectory(tests)
-add_subdirectory(benchmarks)

include/do-verify/MTLEngine.hpp

@@ -7,7 +7,7 @@
 
 #define B_INFINITY std::numeric_limits<int>::max()
 
-namespace dense_vector {
+namespace do_verify {
 
 enum class NodeType {
     PROPOSITION,
@@ -21,7 +21,7 @@ enum class NodeType {
     TEST,
 };
 
-struct Node {
+struct DenseNode {
     db_interval_set::IntervalSet state;
     db_interval_set::IntervalSet output;
     NodeType type;
@@ -31,138 +31,22 @@ struct Node {
     int b;
 };
 
-inline int add_with_inf(int a, int b) {
-    if (a == B_INFINITY || b == B_INFINITY) {
-        return B_INFINITY;
-    }
-    else {
-        return a + b;
-    }
-};
-
-db_interval_set::IntervalSet run_evaluation(std::vector<Node> &nodes, db_interval_set::IntervalSetHolder &setHolder, const int startTime, const int endTime, const std::vector<bool> &propositionInputs) {
-    for(int node_index = 0; node_index < nodes.size(); node_index++) {
-        Node &curNode = nodes[node_index];
-        switch (curNode.type)
-        {           // TODO hocaya sor: datada bir time ve true, false geldiği zaman o timeden önce mi öyle sonra mı?
-                    // timescales'de timeless'lar var nasıl implemente edicem
-
-                    // once -> eventually
-                    // historically -> always
-                    // -> -> implies
-        case NodeType::PROPOSITION:
-            if (propositionInputs[node_index]) curNode.output = db_interval_set::fromInterval(setHolder, {startTime, endTime});
-            else curNode.output = db_interval_set::empty(setHolder);
-            break;
-        case NodeType::AND:
-            curNode.output = db_interval_set::intersectSets(setHolder, nodes[curNode.leftOperandIndex].output, nodes[curNode.rightOperandIndex].output);
-            break;
-        case NodeType::OR:
-            curNode.output = db_interval_set::unionSets(setHolder, nodes[curNode.leftOperandIndex].output, nodes[curNode.rightOperandIndex].output);
-            break;
-        case NodeType::NOT:
-            curNode.output = db_interval_set::negateSet(setHolder, nodes[curNode.rightOperandIndex].output, {startTime, endTime});
-            break;    
-        case NodeType::IMPLIES:
-        {
-            // A IMPLIES B is equivalent to (NOT A) OR B
-            auto notLeft = db_interval_set::negateSet(setHolder, nodes[curNode.leftOperandIndex].output, 
-                                                     {startTime, endTime});
-
-            auto right = nodes[curNode.rightOperandIndex].output;
-            curNode.output = db_interval_set::unionSets(setHolder, notLeft, right);
-            break;
-        } 
-
-        case NodeType::EVENTUALLY:
-            {
-            auto rightOutput = nodes[curNode.rightOperandIndex].output;
-
-            curNode.output = db_interval_set::empty(setHolder);
-
-            auto iterator = db_interval_set::createSegmentIterator(db_interval_set::empty(setHolder), rightOutput, {startTime, endTime});
-            int i = 0;
-            while (db_interval_set::getNextSegment(iterator)) {
-                if (iterator.interval.end == iterator.interval.start) continue;             
-                if (iterator.rightTruthy) {
-                    curNode.state = db_interval_set::unionSets(setHolder, curNode.state,
-                            db_interval_set::fromInterval(setHolder, {iterator.interval.start + curNode.a, add_with_inf(iterator.interval.end, curNode.b)}));
-                        int a = 0;
-                        }
-                i++;
-
-
-                auto segmentOutput = db_interval_set::intersectSets(setHolder, curNode.state, 
-                    db_interval_set::fromInterval(setHolder, {iterator.interval.start, iterator.interval.end}));
-                curNode.output = db_interval_set::unionSets(setHolder, curNode.output, segmentOutput);
-
-            }
-            curNode.state = db_interval_set::intersectSets(setHolder, curNode.state,
-            db_interval_set::fromInterval(setHolder, {endTime, B_INFINITY}));
-            break;
-        }
-        case NodeType::ALWAYS:
-            {
-            auto rightOutput = nodes[curNode.rightOperandIndex].output;
-
-            curNode.output = db_interval_set::empty(setHolder);
+int add_with_inf(int a, int b);
 
-            auto iterator = db_interval_set::createSegmentIterator(db_interval_set::empty(setHolder), rightOutput, {startTime, endTime});
-
-            while (db_interval_set::getNextSegment(iterator)) {
-                if (iterator.interval.end == iterator.interval.start) continue;             
-                if (!iterator.rightTruthy) {
-                    curNode.state = db_interval_set::unionSets(setHolder, curNode.state,
-                            db_interval_set::fromInterval(setHolder, {iterator.interval.start + curNode.a, add_with_inf(iterator.interval.end, curNode.b)}));
-                }
+db_interval_set::IntervalSet run_evaluation(std::vector<DenseNode> &nodes, db_interval_set::IntervalSetHolder &setHolder, const int startTime, const int endTime, const std::vector<bool> &propositionInputs);
 
-                auto segmentOutput = db_interval_set::negateSet(setHolder, curNode.state, {iterator.interval.start, iterator.interval.end});
-                curNode.output = db_interval_set::unionSets(setHolder, curNode.output, segmentOutput);
-
-            }
-            curNode.state = db_interval_set::intersectSets(setHolder, curNode.state,
-            db_interval_set::fromInterval(setHolder, {endTime, B_INFINITY}));
-            break;
-        }
-        case NodeType::SINCE:
-            {
-            auto leftOutput = nodes[curNode.leftOperandIndex].output;
-            auto rightOutput = nodes[curNode.rightOperandIndex].output;
-            curNode.output = db_interval_set::empty(setHolder);
 
-            auto iterator = db_interval_set::createSegmentIterator(leftOutput, rightOutput, {startTime, endTime});
-
-            while (db_interval_set::getNextSegment(iterator)) {
-                if (iterator.interval.end == iterator.interval.start) continue;             
-                if (iterator.leftTruthy && iterator.rightTruthy) {
-                    curNode.state = db_interval_set::unionSets(setHolder, curNode.state,
-                            db_interval_set::fromInterval(setHolder, {iterator.interval.start + curNode.a, add_with_inf(iterator.interval.end, curNode.b)}));
-                }
-                else if (!iterator.leftTruthy && iterator.rightTruthy) {
-                    curNode.state = db_interval_set::fromInterval(setHolder, {iterator.interval.end + curNode.a, add_with_inf(iterator.interval.end, curNode.b)});
-                }
-                else if (iterator.leftTruthy && !iterator.rightTruthy) {
-                }
-                else {
-                    curNode.state = db_interval_set::empty(setHolder);
-                }
+struct DiscreteNode {
+    db_interval_set::IntervalSet state;
+    bool output;
+    NodeType type;
+    unsigned int leftOperandIndex;
+    unsigned int rightOperandIndex;
+    int a;
+    int b;
+};
 
-                auto segmentOutput = db_interval_set::intersectSets(setHolder, curNode.state, 
-                    db_interval_set::fromInterval(setHolder, {iterator.interval.start, iterator.interval.end}));
-                curNode.output = db_interval_set::unionSets(setHolder, curNode.output, segmentOutput);
-
-            }
-            curNode.state = db_interval_set::intersectSets(setHolder, curNode.state,
-            db_interval_set::fromInterval(setHolder, {endTime, B_INFINITY}));
-            break;
-            }
-        case NodeType::TEST:
-            break;
-        }
-
-    }
-    return nodes[nodes.size() - 1].output;
-}
 
+bool run_evaluation(std::vector<DiscreteNode> &nodes, db_interval_set::IntervalSetHolder &setHolder, const int time, const std::vector<bool> &propositionInputs);
 
-}
+} // namespace do_verify

include/do-verify/binary_row_reader.hpp

@@ -1,3 +1,5 @@
+#pragma once
+
 #include <iostream>
 #include <fstream>
 #include <vector>
@@ -16,32 +18,6 @@ struct TimescalesInput {
 };
 #pragma pack(pop)
 
-std::vector<TimescalesInput> readInputFile(std::string fileName) {
-
-    // 2. Open File
-    // std::ios::ate is NOT used here because we need to read from the start
-    std::ifstream file(fileName, std::ios::binary);
-
-    // 3. Read the Header (The Count)
-    uint32_t total_lines = 0;
-    file.read(reinterpret_cast<char*>(&total_lines), sizeof(total_lines));
-
-    // 4. Allocate Memory
-    // We resize the vector to hold exactly the number of records.
-    // This performs a single heap allocation.
-    std::vector<TimescalesInput> data;
-    data.resize(total_lines);
-
-    // 5. Bulk Read (The "Cast" into Memory)
-    // We calculate the total bytes needed: count * 8 bytes
-    // We read directly from disk into the vector's internal array.
-    long bytes_to_read = total_lines * sizeof(TimescalesInput);
-    file.read(reinterpret_cast<char*>(data.data()), bytes_to_read);
-
-    file.close();
-
-
-    return data;
-}
+std::vector<TimescalesInput> readInputFile(std::string fileName);
 
-}
+} // namespace binary_row_reader