wip - updated version of elim_uncstr_tactic

- remove reduce_invertible. It is subsumed by reduce_uncstr(2)
- introduce a simplifier for reduce_unconstrained. It uses reference counting to deal with inefficiency bug of legacy reduce_uncstr. It decomposes theory plugins into expr_inverter.

reduce_invertible is a tactic used in most built-in scenarios. It is useful for removing subterms that can be eliminated using "cheap" quantifier elimination. Specifically variables that occur only once can be removed in many cases by computing an expression that represents the effect computing a value for the eliminated occurrence.

The theory plugins for variable elimination are very partial and should be augmented by extensions, esp. for the case of bit-vectors where the invertibility conditions are thoroughly documented by Niemetz and Preiner.

src/ast/arith_decl_plugin.h

@@ -447,6 +447,8 @@ class arith_util : public arith_recognizers {
     app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(arith_family_id, OP_ADD, arg1, arg2, arg3); }
     app * mk_add(expr_ref_vector const& args) const { return mk_add(args.size(), args.data()); }
     app * mk_add(expr_ref_buffer const& args) const { return mk_add(args.size(), args.data()); }
+    app * mk_add(ptr_buffer<expr> const& args) const { return mk_add(args.size(), args.data()); }
+    app * mk_add(ptr_vector<expr> const& args) const { return mk_add(args.size(), args.data()); }
 
     app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_SUB, arg1, arg2); }
     app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(arith_family_id, OP_SUB, num_args, args); }

src/ast/array_decl_plugin.h

@@ -207,6 +207,10 @@ class array_util : public array_recognizers {
         return mk_store(args.size(), args.data());
     }
 
+    app* mk_store(ptr_buffer<expr> const& args) const {
+        return mk_store(args.size(), args.data());
+    }
+
     app * mk_select(unsigned num_args, expr * const * args) const {
         return m_manager.mk_app(m_fid, OP_SELECT, 0, nullptr, num_args, args);
     }

src/ast/bv_decl_plugin.h

@@ -448,9 +448,17 @@ class bv_util : public bv_recognizers {
     app * mk_bv_srem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSREM, arg1, arg2); }
     app * mk_bv_smod(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSMOD, arg1, arg2); }
     app * mk_bv_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); }
+    app * mk_bv_add(ptr_buffer<expr> const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); }
+    app * mk_bv_add(ptr_vector<expr> const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); }
+    app * mk_bv_add(expr_ref_vector const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); }
+    app * mk_bv_add(expr_ref_buffer const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); }
     app * mk_bv_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); }
     app * mk_bv_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); }
     app * mk_bv_mul(unsigned n, expr* const* args) const { return m_manager.mk_app(get_fid(), OP_BMUL, n, args); }
+    app* mk_bv_mul(ptr_buffer<expr> const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); }
+    app* mk_bv_mul(ptr_vector<expr> const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); }
+    app* mk_bv_mul(expr_ref_vector const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); }
+    app* mk_bv_mul(expr_ref_buffer const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); }
     app * mk_bv_udiv(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUDIV, arg1, arg2); }
     app * mk_bv_udiv_i(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUDIV_I, arg1, arg2); }
     app * mk_bv_udiv0(expr * arg) const { return m_manager.mk_app(get_fid(), OP_BUDIV0, arg); }

src/ast/converters/CMakeLists.txt

@@ -1,5 +1,6 @@
 z3_add_component(converters
   SOURCES
+    expr_inverter.cpp
     equiv_proof_converter.cpp
     generic_model_converter.cpp
     horn_subsume_model_converter.cpp