Added pre_node and post_node hooks to walkers. Used mainly in compiler

src/expr/walkers/simple_expr_walker.cc

@@ -42,8 +42,6 @@ void SimpleWalker::walk ()
     while(f_recursion_stack.size() != rec_goal) {
 
     loop:
-        debug_hook();
-
         activation_record curr = f_recursion_stack.top();
         if (curr.pc != DEFAULT) {
 
@@ -131,7 +129,9 @@ void SimpleWalker::walk ()
             }
         }
 
-        assert(curr.expr);
+        assert(NULL != curr.expr);
+        pre_node_hook(curr.expr);
+
         switch (curr.expr->f_symb) {
 
         // unary temporal
@@ -621,6 +621,9 @@ void SimpleWalker::walk ()
 
         } // switch
 
+        assert(NULL != curr.expr);
+        post_node_hook(curr.expr);
+
         f_recursion_stack.pop();
     } // while (!empty)
 

src/expr/walkers/simple_expr_walker.hh

@@ -34,11 +34,17 @@
 class SimpleWalker : public Walker{
 protected:
 
+    /* global hooks */
     virtual void pre_hook()
     {}
     virtual void post_hook()
     {}
-    virtual void debug_hook()
+
+
+    /* step-by-step hooks */
+    virtual void pre_node_hook(Expr_ptr expr)
+    {}
+    virtual void post_node_hook(Expr_ptr expr)
     {}
 
     virtual void walk();

src/model/compilers/compiler.cc

@@ -140,8 +140,6 @@ void Compiler::walk_neg_postorder(const Expr_ptr expr)
         algebraic_neg(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_not_preorder(const Expr_ptr expr)
@@ -158,8 +156,6 @@ void Compiler::walk_not_postorder(const Expr_ptr expr)
         algebraic_not(expr); // bitwise
     }
     else assert(false); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_add_preorder(const Expr_ptr expr)
@@ -178,8 +174,6 @@ void Compiler::walk_add_postorder(const Expr_ptr expr)
         algebraic_plus(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_sub_preorder(const Expr_ptr expr)
@@ -198,8 +192,6 @@ void Compiler::walk_sub_postorder(const Expr_ptr expr)
         algebraic_sub(expr);
     }
     else assert( false ); // unexpected
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_div_preorder(const Expr_ptr expr)
@@ -218,8 +210,6 @@ void Compiler::walk_div_postorder(const Expr_ptr expr)
         algebraic_div(expr);
     }
     else assert( false ); // unexpected
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_mul_preorder(const Expr_ptr expr)
@@ -238,8 +228,6 @@ void Compiler::walk_mul_postorder(const Expr_ptr expr)
         algebraic_mul(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_mod_preorder(const Expr_ptr expr)
@@ -255,8 +243,6 @@ void Compiler::walk_mod_postorder(const Expr_ptr expr)
         algebraic_mod(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_and_preorder(const Expr_ptr expr)
@@ -275,8 +261,6 @@ void Compiler::walk_and_postorder(const Expr_ptr expr)
         algebraic_and(expr); // bitwise
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_or_preorder(const Expr_ptr expr)
@@ -295,8 +279,6 @@ void Compiler::walk_or_postorder(const Expr_ptr expr)
         algebraic_or(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_xor_preorder(const Expr_ptr expr)
@@ -315,8 +297,6 @@ void Compiler::walk_xor_postorder(const Expr_ptr expr)
         algebraic_xor(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_xnor_preorder(const Expr_ptr expr)
@@ -335,8 +315,6 @@ void Compiler::walk_xnor_postorder(const Expr_ptr expr)
         algebraic_xnor(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_implies_preorder(const Expr_ptr expr)
@@ -355,8 +333,6 @@ void Compiler::walk_implies_postorder(const Expr_ptr expr)
         algebraic_implies(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_iff_preorder(const Expr_ptr expr)
@@ -379,8 +355,6 @@ void Compiler::walk_lshift_postorder(const Expr_ptr expr)
         algebraic_lshift(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_rshift_preorder(const Expr_ptr expr)
@@ -396,8 +370,6 @@ void Compiler::walk_rshift_postorder(const Expr_ptr expr)
         algebraic_rshift(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_eq_preorder(const Expr_ptr expr)
@@ -419,8 +391,6 @@ void Compiler::walk_eq_postorder(const Expr_ptr expr)
         algebraic_equals(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_ne_preorder(const Expr_ptr expr)
@@ -442,8 +412,6 @@ void Compiler::walk_ne_postorder(const Expr_ptr expr)
         algebraic_not_equals(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_gt_preorder(const Expr_ptr expr)
@@ -462,8 +430,6 @@ void Compiler::walk_gt_postorder(const Expr_ptr expr)
         algebraic_gt(expr);
     }
     else assert( false );
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_ge_preorder(const Expr_ptr expr)
@@ -482,8 +448,6 @@ void Compiler::walk_ge_postorder(const Expr_ptr expr)
         algebraic_ge(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_lt_preorder(const Expr_ptr expr)
@@ -500,12 +464,8 @@ void Compiler::walk_lt_postorder(const Expr_ptr expr)
     }
     else if (is_binary_algebraic(expr)) {
         algebraic_lt(expr);
-        memoize_result(expr);
-        return;
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_le_preorder(const Expr_ptr expr)
@@ -524,8 +484,6 @@ void Compiler::walk_le_postorder(const Expr_ptr expr)
         algebraic_le(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_ite_preorder(const Expr_ptr expr)
@@ -550,8 +508,6 @@ void Compiler::walk_ite_postorder(const Expr_ptr expr)
         algebraic_ite(expr);
     }
     else assert( false ); // unreachable
-
-    memoize_result(expr);
 }
 
 bool Compiler::walk_cond_preorder(const Expr_ptr expr)

src/model/compilers/compiler.hh

@@ -80,7 +80,8 @@ protected:
     void pre_hook();
     void post_hook();
 
-    void debug_hook();
+    void pre_node_hook(Expr_ptr expr);
+    void post_node_hook(Expr_ptr expr);
 
     // expr walker interface
     bool walk_next_preorder(const Expr_ptr expr);

src/model/compilers/integer.cc

@@ -43,6 +43,12 @@ void Compiler::integer_neg(const Expr_ptr expr)
     PUSH(lhs.Negate());
 }
 
+void Compiler::integer_not(const Expr_ptr expr)
+{
+    POP_ADD(lhs);
+    PUSH(lhs.BWCmpl());
+}
+
 void Compiler::integer_plus(const Expr_ptr expr)
 {
     POP_TWO(rhs, lhs);
@@ -118,7 +124,7 @@ void Compiler::integer_xnor(const Expr_ptr expr)
 void Compiler::integer_implies(const Expr_ptr expr)
 {
     POP_TWO(rhs, lhs);
-    PUSH(lhs.BWCmpl().BWXor(rhs)); /* bitwise integer arithmetic */
+    PUSH(lhs.BWCmpl().BWOr(rhs)); /* bitwise integer arithmetic */
 
     f_type_stack.pop_back(); // consume one, leave the other
 }

src/model/compilers/internals.cc

@@ -351,9 +351,20 @@ Expr_ptr Compiler::make_temporary_encoding(ADD dds[], unsigned width)
     return expr;
 }
 
-void Compiler::debug_hook()
+void Compiler::pre_node_hook(Expr_ptr expr)
+{
+
+}
+
+void Compiler::post_node_hook(Expr_ptr expr)
 {
+    memoize_result(expr);
+}
+
 #if 0
+
+void Compiler::debug_hook()
+{
     activation_record curr = f_recursion_stack.top();
     DEBUG << "compiler debug hook, expr = " << curr.expr << endl;
 
@@ -372,8 +383,8 @@ void Compiler::debug_hook()
         DEBUG << *i << endl;
     }
     DEBUG << "--------------------" << endl;
-#endif
 }
+#endif
 
 /* two operands, both booleans */
 bool Compiler::is_binary_boolean(const Expr_ptr expr)

src/model/inferrer.cc

@@ -73,9 +73,14 @@ void Inferrer::pre_hook()
 void Inferrer::post_hook()
 {}
 
+void Inferrer::pre_node_hook(Expr_ptr expr)
+{}
+void Inferrer::post_node_hook(Expr_ptr expr)
+{}
+
+#if 0
 void Inferrer::debug_hook()
 {
-#if 0
     activation_record curr = f_recursion_stack.top();
     DEBUG << "inferrer debug hook, expr = " << curr.expr << endl;
 
@@ -85,8 +90,8 @@ void Inferrer::debug_hook()
         DEBUG << *i << endl;
     }
     DEBUG << "--------------------" << endl;
-#endif
 }
+#endif
 
 Type_ptr Inferrer::check_expected_type(expected_t expected)
 {

src/model/inferrer.hh

@@ -51,7 +51,8 @@ protected:
     void pre_hook();
     void post_hook();
 
-    void debug_hook();
+    void pre_node_hook(Expr_ptr expr);
+    void post_node_hook(Expr_ptr expr);
 
     // walker interface
     bool walk_F_preorder(const Expr_ptr expr);