moved obj_equiv_class to ast

src/ast/CMakeLists.txt

@@ -23,6 +23,7 @@ z3_add_component(ast
     expr_map.cpp
     expr_stat.cpp
     expr_substitution.cpp
+    factor_equivs.cpp
     for_each_ast.cpp
     for_each_expr.cpp
     format.cpp

src/ast/factor_equivs.cpp

@@ -0,0 +1,111 @@
+/*++
+Copyright (c) 2017 Arie Gurfinkel
+
+Module Name:
+
+    factor_equivs.cpp
+
+Abstract:
+  Factor equivalence classes out of an expression.
+
+  "Equivalence class structure" for objs. Uses a union_find structure internally.
+  Operations are :
+  -Declare a new equivalence class with a single element
+  -Merge two equivalence classes
+  -Retrieve whether two elements are in the same equivalence class
+  -Iterate on all the elements of the equivalence class of a given element
+  -Iterate on all equivalence classes (and then within them)
+
+Author:
+
+    Julien Braine
+    Arie Gurfinkel
+
+Revision History:
+
+*/
+
+#include "ast/factor_equivs.h"
+#include "ast/arith_decl_plugin.h"
+
+/**
+   Factors input vector v into equivalence classes and the rest
+ */
+void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv) {
+    ast_manager &m = v.get_manager();
+    arith_util arith(m);
+    expr *e1, *e2;
+
+    flatten_and(v);
+    unsigned j = 0;
+    for (unsigned i = 0; i < v.size(); ++i) {
+        if (m.is_eq(v.get(i), e1, e2)) {
+            if (arith.is_zero(e1)) {
+                expr* t;
+                t = e1; e1 = e2; e2 = t;
+            }
+
+            // y + -1*x == 0
+            if (arith.is_zero(e2) && arith.is_add(e1) &&
+                to_app(e1)->get_num_args() == 2) {
+                expr *a0, *a1, *x;
+
+                a0 = to_app(e1)->get_arg(0);
+                a1 = to_app(e1)->get_arg(1);
+
+                if (arith.is_times_minus_one(a1, x)) {
+                    e1 = a0;
+                    e2 = x;
+                }
+                else if (arith.is_times_minus_one(a0, x)) {
+                    e1 = a1;
+                    e2 = x;
+                }
+            }
+            equiv.merge(e1, e2);
+        }
+        else {
+            if (j < i) {v[j] = v.get(i);}
+            j++;
+        }
+    }
+    v.shrink(j);
+}
+
+/**
+ * converts equivalence classes to equalities
+ */
+void equiv_to_expr(expr_equiv_class &equiv, expr_ref_vector &out) {
+    ast_manager &m = out.get_manager();
+    for (auto eq_class : equiv) {
+        expr *rep = nullptr;
+        for (expr *elem : eq_class) {
+            if (!m.is_value (elem)) {
+                rep = elem;
+                break;
+            }
+        }
+        SASSERT(rep);
+        for (expr *elem : eq_class) {
+            if (rep != elem) {out.push_back (m.mk_eq (rep, elem));}
+        }
+    }
+}
+
+/**
+ * expands equivalence classes to all derivable equalities
+ */
+bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out) {
+    ast_manager &m = out.get_manager();
+    bool dirty = false;
+    for (auto eq_class : equiv) {
+        for (auto a = eq_class.begin(), end = eq_class.end(); a != end; ++a) {
+            expr_equiv_class::iterator b(a);
+            for (++b; b != end; ++b) {
+                out.push_back(m.mk_eq(*a, *b));
+                dirty = true;
+            }
+        }
+    }
+    return dirty;
+}

src/ast/factor_equivs.h

@@ -3,9 +3,11 @@ Copyright (c) 2017 Arie Gurfinkel
 
 Module Name:
 
-    obj_equiv_class.h
+    factor_equivs.h
 
 Abstract:
+  Factor equivalence classes out of an expression.
+
   "Equivalence class structure" for objs. Uses a union_find structure internally.
   Operations are :
   -Declare a new equivalence class with a single element
@@ -17,19 +19,19 @@ Abstract:
 Author:
 
     Julien Braine
+    Arie Gurfinkel
 
 Revision History:
 
 */
 
-#ifndef OBJ_EQUIV_CLASS_H_
+#ifndef FACTOR_EQUIVS_H_
-#define OBJ_EQUIV_CLASS_H_
+#define FACTOR_EQUIVS_H_
 
 #include "util/union_find.h"
 #include "ast/ast_util.h"
 
-namespace spacer {
+///All functions naturally add their parameters to the union_find class
-//All functions naturally add their parameters to the union_find class
 template<typename OBJ, typename Manager>
 class obj_equiv_class {
     basic_union_find m_uf;
@@ -164,87 +166,18 @@ typedef obj_equiv_class<expr, ast_manager> expr_equiv_class;
 
 
 /**
-   Factors input vector v into equivalence classes and the rest
+ *  Factors input vector v into equivalence classes and the rest
  */
-inline void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv) {
+void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv);
-    ast_manager &m = v.get_manager();
-    arith_util arith(m);
-    expr *e1, *e2;
-
-    flatten_and(v);
-    unsigned j = 0;
-    for (unsigned i = 0; i < v.size(); ++i) {
-        if (m.is_eq(v.get(i), e1, e2)) {
-            if (arith.is_zero(e1)) {
-                expr* t;
-                t = e1; e1 = e2; e2 = t;
-            }
-
-            // y + -1*x == 0
-            if (arith.is_zero(e2) && arith.is_add(e1) &&
-                to_app(e1)->get_num_args() == 2) {
-                expr *a0, *a1, *x;
-
-                a0 = to_app(e1)->get_arg(0);
-                a1 = to_app(e1)->get_arg(1);
-
-                if (arith.is_times_minus_one(a1, x)) {
-                    e1 = a0;
-                    e2 = x;
-                }
-                else if (arith.is_times_minus_one(a0, x)) {
-                    e1 = a1;
-                    e2 = x;
-                }
-            }
-            equiv.merge(e1, e2);
-        }
-        else {
-            if (j < i) {v[j] = v.get(i);}
-            j++;
-        }
-    }
-    v.shrink(j);
-}
-
 /**
  * converts equivalence classes to equalities
  */
-inline void equiv_to_expr(expr_equiv_class &equiv, expr_ref_vector &out) {
+void equiv_to_expr(expr_equiv_class &equiv, expr_ref_vector &out);
-    ast_manager &m = out.get_manager();
-    for (auto eq_class : equiv) {
-        expr *rep = nullptr;
-        for (expr *elem : eq_class) {
-            if (!m.is_value (elem)) {
-                rep = elem;
-                break;
-            }
-        }
-        SASSERT(rep);
-        for (expr *elem : eq_class) {
-            if (rep != elem) {out.push_back (m.mk_eq (rep, elem));}
-        }
-    }
-}
 
 /**
  * expands equivalence classes to all derivable equalities
  */
-inline bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out) {
+bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out);
-    ast_manager &m = out.get_manager();
-    bool dirty = false;
-    for (auto eq_class : equiv) {
-        for (auto a = eq_class.begin(), end = eq_class.end(); a != end; ++a) {
-            expr_equiv_class::iterator b(a);
-            for (++b; b != end; ++b) {
-                out.push_back(m.mk_eq(*a, *b));
-                dirty = true;
-            }
-        }
-    }
-    return dirty;
-}
 
-}
 
 #endif

src/muz/spacer/spacer_context.cpp

@@ -50,7 +50,6 @@ Notes:
 #include "util/luby.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/expr_abstract.h"
-#include "muz/spacer/obj_equiv_class.h"
 
 namespace spacer {
 
@@ -1123,7 +1122,7 @@ lemma::lemma(pob_ref const &p) :
     m_pob(p), m_new_pob(m_pob) {SASSERT(m_pob);}
 
 lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) :
-    m_ref_count(0), 
+    m_ref_count(0),
     m(p->get_ast_manager()),
     m_body(m), m_cube(m),
     m_bindings(m), m_lvl(p->level()),

src/muz/spacer/spacer_generalizers.cpp

@@ -24,7 +24,7 @@ Revision History:
 #include "ast/expr_abstract.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/for_each_expr.h"
-#include "muz/spacer/obj_equiv_class.h"
+#include "ast/factor_equivs.h"
 
 
 namespace spacer {

src/muz/spacer/spacer_legacy_frames.cpp

@@ -34,7 +34,7 @@
 #include "util/luby.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/expr_abstract.h"
-#include "muz/spacer/obj_equiv_class.h"
+#include "ast/factor_equivs.h"
 
 
 namespace spacer {

src/muz/spacer/spacer_util.cpp

@@ -63,7 +63,7 @@ Notes:
 #include "tactic/arith/propagate_ineqs_tactic.h"
 #include "tactic/arith/arith_bounds_tactic.h"
 
-#include "muz/spacer/obj_equiv_class.h"
+#include "ast/factor_equivs.h"
 
 namespace spacer {
 

src/muz/transforms/dl_mk_array_eq_rewrite.cpp

@@ -22,11 +22,7 @@ Revision History:
 #include "muz/base/dl_context.h"
 #include "muz/base/fixedpoint_params.hpp"
 #include "muz/transforms/dl_mk_array_eq_rewrite.h"
-#include "../spacer/obj_equiv_class.h"
+#include "ast/factor_equivs.h"
-
-// NSB code review: avoid dependency on spacer inside this directory.
-// The python build system will rightfully complain if you include 
-// "muz/spacer/obj_equiv_class.h".
 
 namespace datalog {
 
@@ -65,7 +61,7 @@ namespace datalog {
             new_tail.push_back(r.get_tail(i));
         }
 
-        spacer::expr_equiv_class array_eq_classes(m);
+        expr_equiv_class array_eq_classes(m);
         for(unsigned i = nb_predicates; i < tail_size; i++) {
             expr* cond = r.get_tail(i);
             expr* e1, *e2;

src/muz/transforms/dl_mk_array_eq_rewrite.h

@@ -11,16 +11,14 @@ Author:
 
     Julien Braine
 
-Revision History:   
+Revision History:
 
 --*/
 
 #ifndef DL_MK_ARRAY_EQ_REWRITE_H_
 #define DL_MK_ARRAY_EQ_REWRITE_H_
 
-
 #include "muz/base/dl_rule_transformer.h"
-#include "../spacer/obj_equiv_class.h"
 
 namespace datalog {
 
@@ -30,7 +28,7 @@ namespace datalog {
        ast_manager&      m;
        context&          m_ctx;
        array_util        m_a;
-    
+
        //Rule set context
        const rule_set*   m_src_set;
        rule_set*         m_dst;
@@ -51,4 +49,3 @@ namespace datalog {
 };
 
 #endif /* DL_MK_ARRAY_EQ_REWRITE_H_ */
-

src/muz/transforms/dl_mk_array_instantiation.cpp

@@ -24,7 +24,6 @@ Revision History:
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/expr_abstract.h"
 #include "muz/base/fixedpoint_params.hpp"
-#include "../spacer/obj_equiv_class.h"
 
 namespace datalog {
 
@@ -244,7 +243,7 @@ namespace datalog {
   expr_ref_vector mk_array_instantiation::retrieve_all_selects(expr*array)
   {
     expr_ref_vector all_selects(m);
-    for(spacer::expr_equiv_class::iterator it = eq_classes.begin(array);
+    for(expr_equiv_class::iterator it = eq_classes.begin(array);
         it != eq_classes.end(array); ++it)
     {
       selects.insert_if_not_there(*it, ptr_vector<expr>());

src/muz/transforms/dl_mk_array_instantiation.h

@@ -70,8 +70,8 @@ Revision History:
 #define DL_MK_ARRAY_INSTANTIATION_H_
 
 
+#include "ast/factor_equivs.h"
 #include "muz/base/dl_rule_transformer.h"
-#include "../spacer/obj_equiv_class.h"
 
 namespace datalog {
 
@@ -89,7 +89,7 @@ namespace datalog {
 
        //Rule context
        obj_map<expr, ptr_vector<expr> > selects;
-        spacer::expr_equiv_class eq_classes;
+       expr_equiv_class eq_classes;
        unsigned cnt;//Index for new variables
        obj_map<expr, var*> done_selects;
        expr_ref_vector ownership;

src/util/trail.h

@@ -22,6 +22,7 @@ Revision History:
 #include "util/obj_hashtable.h"
 #include "util/region.h"
 #include "util/obj_ref.h"
+#include "util/vector.h"
 
 template<typename Ctx>
 class trail {
@@ -35,16 +36,16 @@ template<typename Ctx, typename T>
 class value_trail : public trail<Ctx> {
     T & m_value;
     T   m_old_value;
-    
+
 public:
     value_trail(T & value):
         m_value(value),
         m_old_value(value) {
     }
-    
+
     virtual ~value_trail() {
     }
-    
+
     virtual void undo(Ctx & ctx) {
         m_value = m_old_value;
     }
@@ -57,10 +58,10 @@ public:
     reset_flag_trail(bool & value):
         m_value(value) {
     }
-    
+
     virtual ~reset_flag_trail() {
     }
-    
+
     virtual void undo(Ctx & ctx) {
         m_value = false;
     }
@@ -74,7 +75,7 @@ public:
         m_ptr(ptr) {
         SASSERT(m_ptr == 0);
     }
-    
+
     virtual void undo(Ctx & ctx) {
         m_ptr = 0;
     }
@@ -98,8 +99,8 @@ public:
     virtual void undo(Ctx & ctx) {
         m_vector.shrink(m_old_size);
     }
-};    
+};
-        
+
 template<typename Ctx, typename T, bool CallDestructors=true>
 class vector_value_trail : public trail<Ctx> {
     vector<T, CallDestructors> & m_vector;
@@ -111,10 +112,10 @@ public:
         m_idx(idx),
         m_old_value(v[idx]) {
     }
-    
+
     virtual ~vector_value_trail() {
     }
-    
+
     virtual void undo(Ctx & ctx) {
         m_vector[m_idx] = m_old_value;
     }
@@ -150,7 +151,7 @@ public:
     push_back_vector(V & v):
         m_vector(v) {
     }
-    
+
     virtual void undo(Ctx & ctx) {
         m_vector.pop_back();
     }
@@ -165,15 +166,15 @@ public:
         m_vector(v),
         m_idx(idx) {
     }
-    
+
     virtual ~set_vector_idx_trail() {
     }
-    
+
     virtual void undo(Ctx & ctx) {
         m_vector[m_idx] = 0;
     }
 };
-    
+
 template<typename Ctx, typename T, bool CallDestructors=true>
 class pop_back_trail : public trail<Ctx> {
     vector<T, CallDestructors> & m_vector;
@@ -183,7 +184,7 @@ public:
     m_vector(v),
     m_value(m_vector.back()) {
     }
-    
+
     virtual void undo(Ctx & ctx) {
         m_vector.push_back(m_value);
     }
@@ -201,7 +202,7 @@ public:
     m_index(index),
     m_value(m_vector[index].back()) {
     }
-    
+
     virtual void undo(Ctx & ctx) {
         m_vector[m_index].push_back(m_value);
     }
@@ -216,7 +217,7 @@ public:
     push_back_trail(vector<T, CallDestructors> & v):
         m_vector(v) {
     }
-    
+
     virtual void undo(Ctx & ctx) {
         m_vector.pop_back();
     }
@@ -228,11 +229,11 @@ class push_back2_trail : public trail<Ctx> {
     vector_t & m_vector;
     unsigned   m_index;
 public:
-    push_back2_trail(vector_t & v, unsigned index) : 
+    push_back2_trail(vector_t & v, unsigned index) :
     m_vector(v),
     m_index(index) {
     }
-    
+
     virtual void undo(Ctx & ctx) {
         m_vector[m_index].pop_back();
     }
@@ -249,12 +250,12 @@ public:
         SASSERT(m_vector[m_idx] == false);
         m_vector[m_idx] = true;
     }
-    
+
     virtual void undo(Ctx & ctx) {
         m_vector[m_idx] = false;
     }
 };
-    
+
 template<typename Ctx, typename T>
 class new_obj_trail : public trail<Ctx> {
     T * m_obj;
@@ -262,7 +263,7 @@ public:
     new_obj_trail(T * obj):
         m_obj(obj) {
     }
-    
+
     virtual void undo(Ctx & ctx) {
         dealloc(m_obj);
     }
@@ -275,7 +276,7 @@ public:
     obj_ref_trail(obj_ref<T,M>& obj):
         m_obj(obj) {
     }
-    
+
     virtual void undo(Ctx & ctx) {
         m_obj.reset();
     }
@@ -300,7 +301,7 @@ class remove_obj_trail : public trail<Ctx> {
 public:
     remove_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
     virtual ~remove_obj_trail() {}
-    virtual void undo(Ctx & ctx) { m_table.insert(m_obj); } 
+    virtual void undo(Ctx & ctx) { m_table.insert(m_obj); }
 };
 
 
@@ -326,13 +327,13 @@ public:
     trail_stack(Ctx & c):m_ctx(c) {}
 
     ~trail_stack() {}
-    
+
     region & get_region() { return m_region; }
-    
+
-    void reset() { 
+    void reset() {
-        pop_scope(m_scopes.size()); 
+        pop_scope(m_scopes.size());
         // Undo trail objects stored at lvl 0 (avoid memory leaks if lvl 0 contains new_obj_trail objects).
-        undo_trail_stack(m_ctx, m_trail_stack, 0); 
+        undo_trail_stack(m_ctx, m_trail_stack, 0);
     }
 
     void push_ptr(trail<Ctx> * t) { m_trail_stack.push_back(t); }
@@ -357,4 +358,3 @@ public:
 };
 
 #endif /* TRAIL_H_ */
-