From 88a35119b969668869b17fb015c6b5a4d7c6ef0d Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 1 Aug 2017 14:17:27 -0400 Subject: [PATCH] moved obj_equiv_class to ast --- src/ast/CMakeLists.txt | 1 + src/ast/factor_equivs.cpp | 111 ++++++++++++++++++ .../obj_equiv_class.h => ast/factor_equivs.h} | 89 ++------------ src/muz/spacer/spacer_context.cpp | 3 +- src/muz/spacer/spacer_generalizers.cpp | 2 +- src/muz/spacer/spacer_legacy_frames.cpp | 2 +- src/muz/spacer/spacer_util.cpp | 2 +- src/muz/transforms/dl_mk_array_eq_rewrite.cpp | 8 +- src/muz/transforms/dl_mk_array_eq_rewrite.h | 7 +- .../transforms/dl_mk_array_instantiation.cpp | 3 +- .../transforms/dl_mk_array_instantiation.h | 4 +- src/util/trail.h | 60 +++++----- 12 files changed, 164 insertions(+), 128 deletions(-) create mode 100644 src/ast/factor_equivs.cpp rename src/{muz/spacer/obj_equiv_class.h => ast/factor_equivs.h} (66%) diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index de0e4bdaf..0a14d9473 100644 --- a/src/ast/CMakeLists.txt +++ b/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 diff --git a/src/ast/factor_equivs.cpp b/src/ast/factor_equivs.cpp new file mode 100644 index 000000000..853f52921 --- /dev/null +++ b/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; +} diff --git a/src/muz/spacer/obj_equiv_class.h b/src/ast/factor_equivs.h similarity index 66% rename from src/muz/spacer/obj_equiv_class.h rename to src/ast/factor_equivs.h index 7f58efa7d..f0ce1608d 100644 --- a/src/muz/spacer/obj_equiv_class.h +++ b/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_ -#define OBJ_EQUIV_CLASS_H_ +#ifndef FACTOR_EQUIVS_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 class obj_equiv_class { basic_union_find m_uf; @@ -164,87 +166,18 @@ typedef obj_equiv_class 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) { - 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); -} - +void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv); /** * converts equivalence classes to equalities */ -inline 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));} - } - } -} +void equiv_to_expr(expr_equiv_class &equiv, expr_ref_vector &out); /** * expands equivalence classes to all derivable equalities */ -inline 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; -} +bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out); -} #endif diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 8d0a4f627..f549205c3 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/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()), diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp index 40e5c2c4d..f16fb10e1 100644 --- a/src/muz/spacer/spacer_generalizers.cpp +++ b/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 { diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp index d3e01a585..9c302e5fd 100644 --- a/src/muz/spacer/spacer_legacy_frames.cpp +++ b/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 { diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index be6b12cd0..a277c9ed6 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/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 { diff --git a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp b/src/muz/transforms/dl_mk_array_eq_rewrite.cpp index 85dc1eee4..c33cecda9 100644 --- a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp +++ b/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" - -// 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". +#include "ast/factor_equivs.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; diff --git a/src/muz/transforms/dl_mk_array_eq_rewrite.h b/src/muz/transforms/dl_mk_array_eq_rewrite.h index cfdca990f..166c01142 100644 --- a/src/muz/transforms/dl_mk_array_eq_rewrite.h +++ b/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_ */ - diff --git a/src/muz/transforms/dl_mk_array_instantiation.cpp b/src/muz/transforms/dl_mk_array_instantiation.cpp index 9d983abd2..362d83865 100644 --- a/src/muz/transforms/dl_mk_array_instantiation.cpp +++ b/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()); diff --git a/src/muz/transforms/dl_mk_array_instantiation.h b/src/muz/transforms/dl_mk_array_instantiation.h index 2ef9873f4..b87f679fc 100644 --- a/src/muz/transforms/dl_mk_array_instantiation.h +++ b/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 > selects; - spacer::expr_equiv_class eq_classes; + expr_equiv_class eq_classes; unsigned cnt;//Index for new variables obj_map done_selects; expr_ref_vector ownership; diff --git a/src/util/trail.h b/src/util/trail.h index 1b8f36206..bba71fb00 100644 --- a/src/util/trail.h +++ b/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 class trail { @@ -35,16 +36,16 @@ template class value_trail : public trail { 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 class vector_value_trail : public trail { vector & 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 class pop_back_trail : public trail { vector & 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 & v): m_vector(v) { } - + virtual void undo(Ctx & ctx) { m_vector.pop_back(); } @@ -228,11 +229,11 @@ class push_back2_trail : public trail { 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 class new_obj_trail : public trail { 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& obj): m_obj(obj) { } - + virtual void undo(Ctx & ctx) { m_obj.reset(); } @@ -300,7 +301,7 @@ class remove_obj_trail : public trail { public: remove_obj_trail(obj_hashtable& 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() { - pop_scope(m_scopes.size()); + + void reset() { + 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 * t) { m_trail_stack.push_back(t); } @@ -357,4 +358,3 @@ public: }; #endif /* TRAIL_H_ */ -