feat: add special case in z3_driver for clocks

Since you cant delay a single clock individually, we have to add a special unknown "delay_identifier" int_const to see if the expression is sat/unsat if we can delay a bit

include/drivers/z3_driver.h

@@ -42,10 +42,14 @@ 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();

src/drivers/z3_driver.cpp

@@ -24,7 +24,9 @@
 
 namespace expr {
     z3_driver::z3_driver(const symbol_table_t& known_env, const symbol_table_t& unknown_env)
-     : driver{{known_env, unknown_env}}, c{}, s{c}, known{known_env}, unknown{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} {}
 
     z3_driver::~z3_driver() = default;
 
@@ -74,7 +76,10 @@ namespace expr {
                 for(int i = 0; i < m.size(); i++) {
                     auto xx = m[i];
                     auto interp = xx.is_const() ? m.get_const_interp(xx) : m.get_func_interp(xx).else_value();
-                    result[xx.name().str()] = as_symbol_value(interp);
+                    if(xx.name().str() == delay_identifier)
+                        delay_amount = as_symbol_value(interp);
+                    else
+                        result[xx.name().str()] = as_symbol_value(interp);
                 }
                 break;
         }
@@ -105,7 +110,10 @@ namespace expr {
 
     auto z3_driver::as_z3_expression(const identifier_t& ref) -> z3::expr {
         if(known.contains(ref.ident))
-            return as_z3_expression(known.at(ref.ident));
+            return std::visit(ya::overload(
+                    [this,&ref](const expr::clock_t& v) { return as_z3_expression(known.at(ref.ident)) + c.int_const(delay_identifier.c_str()); },
+                    [this,&ref](auto&& x) { return as_z3_expression(known.at(ref.ident)); }
+                    ), static_cast<const underlying_symbol_value_t&>(known.at(ref.ident)));
         auto it = find(ref.ident);
         return std::visit(ya::overload(
                 [this, &ref](const int& _)          { return c.int_const(ref.ident.c_str()); },
@@ -147,4 +155,8 @@ 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;
+    }
 }

src/main.cpp

@@ -129,6 +129,7 @@ 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();
         }
 #endif
         std::cout << "\n" << t.milliseconds_elapsed() << "ms" << std::endl;