Skip to content

Parser #16

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
arincdemir merged 7 commits into from
Mar 7, 2026
Merged

Parser #16

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
d7d0f63
put dogan hoca's parser code into mine. I will need to adapt it
arincdemir Feb 23, 2026
26a08f0
removed the extra grammar rules from dogan hoca's grammar
arincdemir Feb 23, 2026
ea031fb
modified the parsing handler functions to work with my discrete nodes
arincdemir Feb 24, 2026
83ef890
added a test cpp file for testing whether formulas are parsed correctly
arincdemir Feb 24, 2026
370b2e5
fixed the parser adding duplicate propositions. Also leftOperandIndex…
arincdemir Feb 24, 2026
2adc955
changed the code to work with the input index of proposition nodes be…
arincdemir Feb 25, 2026
60b6097
fixed parser putting unary operators operands on the leftOperand. Als…
arincdemir Feb 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 18 additions & 1 deletion CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,15 @@ endif()
set(CMAKE_CXX_STANDARD 20)
set(CMAKE_CXX_STANDARD_REQUIRED ON)

include(FetchContent)

FetchContent_Declare(
cpp-peglib
GIT_REPOSITORY https://github.com/yhirose/cpp-peglib.git
GIT_TAG v1.9.1
)
FetchContent_MakeAvailable(cpp-peglib)

# Define the library with source files
add_library(do-verify STATIC
src/interval_set.cpp
Expand All @@ -27,8 +36,9 @@ target_include_directories(do-verify PUBLIC
$<INSTALL_INTERFACE:include>
)

target_link_libraries(do-verify PUBLIC peglib)

# Fetch Catch2 (ONCE for the whole project)
include(FetchContent)
FetchContent_Declare(
Catch2
GIT_REPOSITORY https://github.com/catchorg/Catch2.git
Expand All @@ -37,6 +47,7 @@ FetchContent_Declare(
FetchContent_MakeAvailable(Catch2)



add_executable(do-verify-bin
src/main.cpp
)
Expand All @@ -52,6 +63,12 @@ add_executable(do-verify-perf
target_compile_options(do-verify-perf PRIVATE -g -fno-omit-frame-pointer)
target_link_libraries(do-verify-perf PRIVATE do-verify)

add_executable(test-parse
src/test_parse.cpp
)
target_compile_options(test-parse PRIVATE -g -O0)
target_link_libraries(test-parse PRIVATE do-verify)

# Add Subdirectories
enable_testing()
add_subdirectory(tests)
Expand Down
34 changes: 17 additions & 17 deletions benchmarks/benchmark_engine.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ TEST_CASE("Dense AbsentAQ", "[dense_benchmarks][AbsentAQ]") {
BENCHMARK_ADVANCED("AbsentAQ " + benchmarkName)(Catch::Benchmark::Chronometer meter) {
IntervalSetHolder holder = newHolder(1000);
DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
DenseNode once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, TIMINGS};
DenseNode notNode{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
DenseNode since{empty(holder), empty(holder), NodeType::SINCE, 3, 0, 0, B_INFINITY};
Expand Down Expand Up @@ -117,8 +117,8 @@ TEST_CASE("Dense AbsentBQR", "[dense_benchmarks][AbsentBQR]") {
const int since_b = TIMINGS;

DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0}; // 1
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0}; // 2
DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // 3
DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // 4
DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; // 5
Expand Down Expand Up @@ -171,8 +171,8 @@ TEST_CASE("Dense AbsentBR", "[dense_benchmarks][AbsentBR]") {
const int inner_always_b = TIMINGS;

DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0}; // 1
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0}; // 2
DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // 3
DenseNode inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 3, 0, inner_always_b}; // 4
DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0}; // 5
Expand Down Expand Up @@ -221,8 +221,8 @@ TEST_CASE("Dense AlwaysAQ", "[dense_benchmarks][AlwaysAQ]") {
const int once_b = TIMINGS;

DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0}; // 1
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0}; // 2
DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, once_b}; // 3
DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, 0, B_INFINITY}; // 4
DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 3, 4, 0, 0}; // 5
Expand Down Expand Up @@ -272,8 +272,8 @@ TEST_CASE("Dense AlwaysBQR", "[dense_benchmarks][AlwaysBQR]") {
const int since_b = TIMINGS;

DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0}; // 1
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0}; // 2
DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // 3
DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // 4
DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; // 5
Expand Down Expand Up @@ -326,8 +326,8 @@ TEST_CASE("Dense AlwaysBR", "[dense_benchmarks][AlwaysBR]") {
const int inner_always_b = TIMINGS;

DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0}; // 1
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0}; // 2
DenseNode inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, inner_always_b}; // 3
DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 3, 0, 0}; // 4
DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 4, 0, B_INFINITY}; // 5
Expand Down Expand Up @@ -375,8 +375,8 @@ TEST_CASE("Dense RecurBQR", "[dense_benchmarks][RecurBQR]") {
const int inner_once_b = TIMINGS;

DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0}; // 1
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0}; // 2
DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // 3
DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // 4
DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; // 5
Expand Down Expand Up @@ -478,9 +478,9 @@ TEST_CASE("Dense RespondBQR", "[dense_benchmarks][RespondBQR]") {
const int since_a = TIMINGS;

DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1
DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 3
DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0}; // 1
DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0}; // 2
DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 3, 0, 0, 0}; // 3
DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // 4
DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // 5
DenseNode and_A1{empty(holder), empty(holder), NodeType::AND, 3, 4, 0, 0}; // 6
Expand Down Expand Up @@ -541,7 +541,7 @@ TEST_CASE("Dense RespondGLB", "[dense_benchmarks][RespondGLB]") {
const int since_a = TIMINGS;

DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0
DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1
DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0}; // 1
DenseNode once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, once_a, once_b}; // 2
DenseNode implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 1, 2, 0, 0}; // 3
DenseNode not_s{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // 4
Expand Down
40 changes: 38 additions & 2 deletions include/do-verify/MTLEngine.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
#include <vector>
#include <algorithm>
#include "do-verify/interval_set.hpp"
#include <string>
#include <limits>

#define B_INFINITY std::numeric_limits<int>::max()
Expand All @@ -21,12 +22,20 @@ enum class NodeType {
TEST,
};

struct ParsedNode {
NodeType type;
unsigned int leftOperandIndex; // For propositions, this is the input index
unsigned int rightOperandIndex; // unary operator operand sits here
int a;
int b;
};

struct DenseNode {
db_interval_set::IntervalSet state;
db_interval_set::IntervalSet output;
NodeType type;
unsigned int leftOperandIndex;
unsigned int rightOperandIndex;
unsigned int rightOperandIndex; // unary operator operand sits here
int a;
int b;
};
Expand All @@ -41,12 +50,39 @@ struct DiscreteNode {
bool output;
NodeType type;
unsigned int leftOperandIndex;
unsigned int rightOperandIndex;
unsigned int rightOperandIndex; // unary operator operand sits here
int a;
int b;
};


bool run_evaluation(std::vector<DiscreteNode> &nodes, db_interval_set::IntervalSetHolder &setHolder, const int time, const std::vector<bool> &propositionInputs);


/*
struct DenseMonitor {
std::vector<DenseNode> nodes;
db_interval_set::IntervalSetHolder setHolder;
std::map<std::string, unsigned int> proposition_map;

public:

DenseMonitor(std::string pattern, std::vector<std::string> proposition_names_in_input_order) {
ptl_parser parser;
setHolder = db_interval_set::newHolder(1000);
nodes = parser.parse_dense(pattern, setHolder);
proposition_map = parser.get_proposition_map();
// Here we change the leftOperandIndex's of Proposition nodes to their respective input indexes.
// TODO: They will use that in evaluation to get their boolean value from the inputs
for (int i = 0; i < proposition_names_in_input_order.size(); i++) {
nodes[proposition_map[proposition_names_in_input_order[i]]].leftOperandIndex = i;
}
}

db_interval_set::IntervalSet evaluate(const int startTime, const int endTime, const std::vector<bool> &propositionInputs) {
return run_evaluation(nodes, setHolder, startTime, endTime, propositionInputs);
}
};
*/

} // namespace do_verify
Loading