From 6ef9e0834a417f22e21afb6de4a71cfe169dbd4b Mon Sep 17 00:00:00 2001 From: Asger Gitz-Johansen Date: Fri, 16 Sep 2022 19:53:22 +0200 Subject: [PATCH] fix: symbol_table_t now contains delay information --- include/clock.h | 9 +++-- include/drivers/z3_driver.h | 3 -- {src => include}/operations.h | 0 include/symbol_table.h | 8 +++- src/clock.cpp | 24 ++++++++---- src/drivers/z3_driver.cpp | 9 +---- src/main.cpp | 4 +- src/symbol_table.cpp | 71 +++++++++++++++++++++++------------ 8 files changed, 82 insertions(+), 46 deletions(-) rename {src => include}/operations.h (100%) diff --git a/include/clock.h b/include/clock.h index efe7763..2aa0839 100644 --- a/include/clock.h +++ b/include/clock.h @@ -29,14 +29,17 @@ namespace expr { unsigned int time_units = 0; void reset(); void delay(unsigned int delta); + void delay(long delta); + void delay(int delta); auto operator+=(const unsigned int& delta) -> clock_t&; auto operator==(const clock_t& o) const -> bool; auto operator!=(const clock_t& o) const -> bool; + auto operator=(const clock_t& o) -> clock_t&; + auto operator=(const int& o) -> clock_t&; }; - - auto operator"" _ms(unsigned long long val) -> clock_t; - auto operator<<(std::ostream& o, const clock_t& c) -> std::ostream&; auto stoclk(const char* str) -> clock_t; + auto operator<<(std::ostream& o, const expr::clock_t& c) -> std::ostream&; } +auto operator"" _ms(unsigned long long val) -> expr::clock_t; #endif //EXPR_CLOCK_H diff --git a/include/drivers/z3_driver.h b/include/drivers/z3_driver.h index aa4a557..b049c45 100644 --- a/include/drivers/z3_driver.h +++ b/include/drivers/z3_driver.h @@ -42,14 +42,11 @@ namespace expr { auto as_z3_expression(const identifier_t& ref) -> z3::expr; auto as_z3_expression(const symbol_value_t& val) -> z3::expr; - auto get_delay_amount() const -> symbol_value_t; - symbol_table_t result{}; protected: z3::context c{}; z3::solver s; std::string delay_identifier; - symbol_value_t delay_amount; const symbol_table_t& known; const symbol_table_t& unknown; void solve(); diff --git a/src/operations.h b/include/operations.h similarity index 100% rename from src/operations.h rename to include/operations.h diff --git a/include/symbol_table.h b/include/symbol_table.h index c022d51..0af5442 100644 --- a/include/symbol_table.h +++ b/include/symbol_table.h @@ -77,7 +77,13 @@ namespace expr { auto is_overlapping(const symbol_table_t& other) -> bool; auto is_overlapping_and_not_idempotent(const symbol_table_t& other) -> bool; auto is_completely_overlapping(const symbol_table_t& other) -> bool; - void delay(unsigned int time_units); + void delay(); + void delay_but_dont_reset_amount(); + void delay(const expr::symbol_value_t& time_units); + void set_delay_amount(const expr::symbol_value_t& time_units); + auto get_delay_amount() const -> std::optional; + private: + std::optional delay_amount{}; }; auto operator+(const symbol_table_t &a, const symbol_table_t &b) -> symbol_table_t; diff --git a/src/clock.cpp b/src/clock.cpp index 8a59974..4d2d224 100644 --- a/src/clock.cpp +++ b/src/clock.cpp @@ -21,15 +21,21 @@ * SOFTWARE. */ #include "clock.h" -#include +#include namespace expr { void clock_t::reset() { time_units = 0; } + void clock_t::delay(int delta) { + time_units += delta; + } void clock_t::delay(unsigned int delta) { time_units += delta; } + void clock_t::delay(long delta) { + time_units += delta; + } auto clock_t::operator+=(const unsigned int& delta) -> clock_t& { delay(delta); return *this; @@ -40,16 +46,14 @@ namespace expr { auto clock_t::operator!=(const clock_t& o) const -> bool { return !(*this == o); } - - auto operator"" _ms(unsigned long long val) -> clock_t { - clock_t v{}; v.time_units = val; - return v; + auto clock_t::operator=(const expr::clock_t& o) -> clock_t& = default; + auto clock_t::operator=(const int& o) -> clock_t& { + time_units = o; + return *this; } - - auto operator<<(std::ostream& o, const clock_t& c) -> std::ostream& { + auto operator<<(std::ostream& o, const expr::clock_t& c) -> std::ostream& { return o << c.time_units; } - auto stoclk(const char* str) -> clock_t { std::string s{str}; auto loc = s.find( "_ms", 0 ); @@ -61,3 +65,7 @@ namespace expr { return c; } } +auto operator"" _ms(unsigned long long val) -> expr::clock_t { + expr::clock_t v{}; v.time_units = val; + return v; +} diff --git a/src/drivers/z3_driver.cpp b/src/drivers/z3_driver.cpp index b72672b..10254a9 100644 --- a/src/drivers/z3_driver.cpp +++ b/src/drivers/z3_driver.cpp @@ -26,7 +26,7 @@ namespace expr { z3_driver::z3_driver(const symbol_table_t& known_env, const symbol_table_t& unknown_env) // TODO: delay_identifier should be randomly generated : driver{{known_env, unknown_env}}, c{}, s{c}, - delay_identifier{"d"}, delay_amount{0_ms}, known{known_env}, unknown{unknown_env} {} + delay_identifier{"d"}, known{known_env}, unknown{unknown_env} {} z3_driver::~z3_driver() = default; @@ -77,11 +77,10 @@ namespace expr { auto xx = m[i]; auto interp = xx.is_const() ? m.get_const_interp(xx) : m.get_func_interp(xx).else_value(); if(xx.name().str() == delay_identifier) - delay_amount = as_symbol_value(interp); + result.set_delay_amount(as_symbol_value(interp)); else result[xx.name().str()] = as_symbol_value(interp); } - break; } } @@ -155,8 +154,4 @@ namespace expr { [](auto&&){ throw std::logic_error("tree node type not recognized"); } ), static_cast(tree.node)); } - - auto z3_driver::get_delay_amount() const -> symbol_value_t { - return delay_amount; - } } diff --git a/src/main.cpp b/src/main.cpp index b32cd5c..9b7f509 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -129,7 +129,9 @@ int main (int argc, char *argv[]) { if(cli_arguments["driver"].as_string() == "z3") { auto drv_z = std::dynamic_pointer_cast(drv); std::cout << "result: \n" << drv_z->result; - std::cout << "delay_amount: " << drv_z->get_delay_amount(); + + std::cout << "\n==========\n"; + std::cout << "env + result: \n" << (env + drv_z->result); } #endif std::cout << "\n" << t.milliseconds_elapsed() << "ms" << std::endl; diff --git a/src/symbol_table.cpp b/src/symbol_table.cpp index 0ebdf54..9b8f044 100644 --- a/src/symbol_table.cpp +++ b/src/symbol_table.cpp @@ -31,6 +31,8 @@ namespace expr { auto symbol_table_t::put(const symbol_table_t &other) -> symbol_table_t & { for (auto &e: other) this->insert_or_assign(e.first, e.second); + if(other.delay_amount.has_value()) + delay(other.delay_amount.value()); return *this; } @@ -42,6 +44,8 @@ namespace expr { for (auto &e: other) if(contains(e.first)) this->insert_or_assign(e.first, e.second); + if(other.delay_amount.has_value()) + delay(other.delay_amount.value()); return *this; } @@ -62,13 +66,36 @@ namespace expr { return std::any_of(other.begin(), other.end(), comparator); } - void symbol_table_t::delay(unsigned int time_units) { + void symbol_table_t::delay() { + delay_but_dont_reset_amount(); + delay_amount = {}; + } + + void symbol_table_t::delay_but_dont_reset_amount() { + if(delay_amount.has_value()) + delay(delay_amount.value()); + } + + void symbol_table_t::delay(const expr::symbol_value_t& time_units) { + auto tu = std::visit(ya::overload( + [](const int& i) -> long{ return i; }, + [](const clock_t& c) -> long { return c.time_units; }, + [](auto&& v) -> long{ throw std::logic_error(std::string{"cannot delay with a symbol_value of type: "} + typeid(v).name()); } + ), time_units); for(auto& e : *this) std::visit(ya::overload( - [&time_units](clock_t& v){ v.delay(time_units); }, + [&tu](clock_t& v){ v.delay(tu); }, [](auto&&){}), e.second); } + void symbol_table_t::set_delay_amount(const expr::symbol_value_t& time_units) { + delay_amount = {time_units}; + } + + auto symbol_table_t::get_delay_amount() const -> std::optional { + return delay_amount; + } + symbol_table_t operator+(const symbol_table_t &a, const symbol_table_t &b) { symbol_table_t r{}; r += a; @@ -76,19 +103,20 @@ namespace expr { return r; } - std::ostream &operator<<(std::ostream &os, const symbol_value_t &v) { - std::visit(ya::overload{ - [&os](const bool &b) { os << std::boolalpha << b << " " << typeid(b).name(); }, - [&os](const std::string &s) { os << "\"" << s << "\" s"; }, - [&os](const expr::clock_t &s) { os << "\"" << s << "\" c"; }, - [&os](auto &&v) { os << v << " " << typeid(v).name(); }}, - static_cast(v)); - return os; + auto operator<<(std::ostream &os, const symbol_value_t &v) -> std::ostream& { + return std::visit(ya::overload{ + [&os](const bool &b) -> std::ostream& { return os << std::boolalpha << b << " " << typeid(b).name(); }, + [&os](const std::string &s) -> std::ostream& { return os << "\"" << s << "\" s"; }, + [&os](const expr::clock_t &s) -> std::ostream& { return os << "" << s << " c"; }, + [&os](auto &&v) -> std::ostream& { return os << v << " " << typeid(v).name(); } + }, static_cast(v)); } - std::ostream &operator<<(std::ostream &os, const symbol_table_t &m) { + auto operator<<(std::ostream &os, const symbol_table_t &m) -> std::ostream& { for (auto &v: m) os << v.first << " :-> " << v.second << "\n"; + if(m.get_delay_amount().has_value()) + os << "delay_amount :-> " << m.get_delay_amount().value(); return os; } @@ -144,10 +172,7 @@ namespace expr { } auto operator<<(std::ostream &o, const underlying_syntax_node_t &n) -> std::ostream & { - std::visit(ya::overload( - [&o](auto &&x) { o << x; } - ), n); - return o; + return std::visit(ya::overload([&o](auto &&x) -> std::ostream& { return o << x; }), n); } auto operator<<(std::ostream &o, const syntax_tree_t &tree) -> std::ostream & { @@ -162,15 +187,13 @@ namespace expr { } auto std::hash::operator()(const expr::symbol_value_t& v) const -> size_t { - size_t result{}; - std::visit(ya::overload( - [&result](const int& v){result = std::hash{}(v);}, - [&result](const float& v){result = std::hash{}(v);}, - [&result](const bool& v){result = std::hash{}(v);}, - [&result](const std::string& v){result = std::hash{}(v);}, - [&result](const expr::clock_t& c){result = std::hash{}(c.time_units);} + return std::visit(ya::overload( + [](const int& v){ return std::hash{}(v); }, + [](const float& v){ return std::hash{}(v); }, + [](const bool& v){ return std::hash{}(v); }, + [](const std::string& v){ return std::hash{}(v); }, + [](const expr::clock_t& c){ return std::hash{}(c.time_units); } ), static_cast(v)); - return result; } auto std::hash::operator()(const expr::symbol_table_t& v) const -> size_t { @@ -179,5 +202,7 @@ auto std::hash::operator()(const expr::symbol_table_t& v) result = ya::hash_combine(result, symbol.first); result = ya::hash_combine(result, symbol.second); } + if(v.get_delay_amount().has_value()) + result = ya::hash_combine(result, v.get_delay_amount().value()); return result; }