fix: symbol_table_t now contains delay information

sillydan1 · Sep 16, 2022 · 6ef9e08 · 6ef9e08
1 parent 92806fa
commit 6ef9e08
Show file tree

Hide file tree

Showing 8 changed files with 82 additions and 46 deletions.
diff --git 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
@@ -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 → include/operations.h b/src/operations.h → include/operations.h
diff --git 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<expr::symbol_value_t>;
+    private:
+        std::optional<expr::symbol_value_t> 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
@@ -21,15 +21,21 @@
  * SOFTWARE.
  */
 #include "clock.h"
-#include <iostream>
+#include <ostream>
 
 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
@@ -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<const underlying_syntax_node_t&>(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
@@ -129,7 +129,9 @@ int main (int argc, char *argv[]) {
         if(cli_arguments["driver"].as_string() == "z3") {
             auto drv_z = std::dynamic_pointer_cast<z3_driver>(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
@@ -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,33 +66,57 @@ 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<expr::symbol_value_t> {
+        return delay_amount;
+    }
+
     symbol_table_t operator+(const symbol_table_t &a, const symbol_table_t &b) {
         symbol_table_t r{};
         r += a;
         r += b;
         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<const underlying_symbol_value_t &>(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<const underlying_symbol_value_t &>(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<expr::symbol_value_t>::operator()(const expr::symbol_value_t& v) const -> size_t {
-    size_t result{};
-    std::visit(ya::overload(
-            [&result](const int& v){result = std::hash<int>{}(v);},
-            [&result](const float& v){result = std::hash<float>{}(v);},
-            [&result](const bool& v){result = std::hash<bool>{}(v);},
-            [&result](const std::string& v){result = std::hash<std::string>{}(v);},
-            [&result](const expr::clock_t& c){result = std::hash<unsigned int>{}(c.time_units);}
+    return std::visit(ya::overload(
+            [](const int& v){ return std::hash<int>{}(v); },
+            [](const float& v){ return std::hash<float>{}(v); },
+            [](const bool& v){ return std::hash<bool>{}(v); },
+            [](const std::string& v){ return std::hash<std::string>{}(v); },
+            [](const expr::clock_t& c){ return std::hash<unsigned int>{}(c.time_units); }
     ), static_cast<const expr::underlying_symbol_value_t&>(v));
-    return result;
 }
 
 auto std::hash<expr::symbol_table_t>::operator()(const expr::symbol_table_t& v) const -> size_t {
@@ -179,5 +202,7 @@ auto std::hash<expr::symbol_table_t>::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;
 }