convert reduce-args to a simplifier

- convert reduce-args to a simplifier. Currently exposed as reduce-args2 tactic until the old tactic code gets removed.
- bug fixes in model_reconstruction trail
  - allow multiple defs to be added with same pool of removed formulas
  - fix tracking of function symbols instead of expressions to filter replay
- add nla_divisions to track (cheap) divisibility lemmas.
-

src/ast/ast_util.h

@@ -101,6 +101,8 @@ expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx);
  */
 expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
 app  * mk_and(ast_manager & m, unsigned num_args, app * const * args);
+inline expr * mk_and(ast_manager & m, ptr_vector<expr> const& args) { return mk_and(m, args.size(), args.data()); }
+inline expr * mk_and(ast_manager & m, ptr_buffer<expr> const& args) { return mk_and(m, args.size(), args.data()); }
 inline expr * mk_and(ast_manager & m, expr* a, expr* b) { expr* args[2] = { a, b }; return mk_and(m, 2, args); }
 inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.data()), args.get_manager()); }
 inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.data()), args.get_manager()); }

src/ast/converters/generic_model_converter.h

@@ -68,8 +68,6 @@ public:
     void get_units(obj_map<expr, bool>& units) override;
 
     vector<entry> const& entries() const { return m_entries; }
-
-    void shrink(unsigned j) { m_entries.shrink(j); }
 };
 
 typedef ref<generic_model_converter> generic_model_converter_ref;

src/ast/simplifiers/CMakeLists.txt

@@ -19,6 +19,7 @@ z3_add_component(simplifiers
     max_bv_sharing.cpp
     model_reconstruction_trail.cpp
     propagate_values.cpp
+    reduce_args_simplifier.cpp
     solve_context_eqs.cpp
     solve_eqs.cpp
   COMPONENT_DEPENDENCIES

src/ast/simplifiers/dependent_expr_state.cpp

@@ -31,8 +31,13 @@ void dependent_expr_state::freeze(func_decl* f) {
 }
 
 void dependent_expr_state::freeze(expr* term) {
-    if (is_app(term))
+    if (is_app(term) && to_app(term)->get_num_args() == 0)
         freeze(to_app(term)->get_decl());
+    else {
+        ast_mark visited;
+        freeze_terms(term, false, visited);
+    }
+    
 }
 
 /**

src/ast/simplifiers/model_reconstruction_trail.cpp

@@ -13,6 +13,7 @@ Author:
 
 
 #include "ast/for_each_expr.h"
+#include "ast/ast_ll_pp.h"
 #include "ast/rewriter/macro_replacer.h"
 #include "ast/simplifiers/model_reconstruction_trail.h"
 #include "ast/simplifiers/dependent_expr_state.h"
@@ -24,6 +25,10 @@ Author:
 // TODO: add filters to skip sections of the trail that do not touch the current free variables.
 
 void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumptions, dependent_expr_state& st) {
+    TRACE("simplifier",
+        for (unsigned i = qhead; i < st.qtail(); ++i)
+            tout << mk_bounded_pp(st[i].fml(), m) << "\n";
+    );
     ast_mark free_vars;
     scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
     for (unsigned i = qhead; i < st.qtail(); ++i)        
@@ -32,6 +37,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
         add_vars(a, free_vars);
 
     for (auto& t : m_trail) {
+        TRACE("simplifier", tout << " active " << t->m_active << " hide " << t->is_hide() << " intersects " << t->intersects(free_vars) << "\n");
         if (!t->m_active)
             continue;
 
@@ -56,15 +62,17 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
         
         if (t->is_def()) {
             macro_replacer mrp(m);
+            for (auto const& [d, def, dep] : t->m_defs) {
                 app_ref head(m);
-            func_decl* d = t->m_decl;
                 ptr_buffer<expr> args;
                 for (unsigned i = 0; i < d->get_arity(); ++i)
                     args.push_back(m.mk_var(i, d->get_domain(i)));
                 head = m.mk_app(d, args);
-            mrp.insert(head, t->m_def, t->m_dep);
+                mrp.insert(head, def, dep);
-            dependent_expr de(m, t->m_def, nullptr, t->m_dep);
+                TRACE("simplifier", tout << d << " " << def << " " << dep << "\n");
+                dependent_expr de(m, def, nullptr, dep);
                 add_vars(de, free_vars);
+            }
             
             for (unsigned i = qhead; i < st.qtail(); ++i) {
                 auto [f, p, dep1] = st[i]();
@@ -140,6 +148,7 @@ model_converter_ref model_reconstruction_trail::get_model_converter() {
 * Append model conversions starting at index i
 */
 void model_reconstruction_trail::append(generic_model_converter& mc, unsigned& i) {
+    TRACE("simplifier", display(tout));
     for (; i < m_trail.size(); ++i) {
         auto* t = m_trail[i];
         if (!t->m_active)
@@ -147,7 +156,8 @@ void model_reconstruction_trail::append(generic_model_converter& mc, unsigned& i
         else if (t->is_hide())
             mc.hide(t->m_decl);
         else if (t->is_def())
-            mc.add(t->m_decl, t->m_def);
+            for (auto const& [f, def, dep] : t->m_defs)
+                mc.add(f, def);
         else {
             for (auto const& [v, def] : t->m_subst->sub())
                 mc.add(v, def);
@@ -167,8 +177,10 @@ std::ostream& model_reconstruction_trail::display(std::ostream& out) const {
             continue;
         else if (t->is_hide())
             out << "hide " << t->m_decl->get_name() << "\n";
-        else if (t->is_def())
+        else if (t->is_def()) {
-            out << t->m_decl->get_name() << " <- " << mk_pp(t->m_def, m) << "\n";
+            for (auto const& [f, def, dep] : t->m_defs)
+                out << f->get_name() << " <- " << mk_pp(def, m) << "\n";
+        }            
         else {
             for (auto const& [v, def] : t->m_subst->sub())
                 out << mk_pp(v, m) << " <- " << mk_pp(def, m) << "\n";            

src/ast/simplifiers/model_reconstruction_trail.h

@@ -39,34 +39,46 @@ class model_reconstruction_trail {
         scoped_ptr<expr_substitution> m_subst;
         vector<dependent_expr>        m_removed;
         func_decl_ref                 m_decl;
-        expr_ref                      m_def;
+        vector<std::tuple<func_decl_ref, expr_ref, expr_dependency_ref>> m_defs;
-        expr_dependency_ref           m_dep;
+
         bool                          m_active = true;
 
         entry(ast_manager& m, expr_substitution* s, vector<dependent_expr> const& rem) :
-            m_subst(s), m_removed(rem), m_decl(m), m_def(m), m_dep(m) {}
+            m_subst(s), m_removed(rem), m_decl(m) {}
 
-        entry(ast_manager& m, func_decl* h) : m_decl(h, m), m_def(m), m_dep(m) {}
+        entry(ast_manager& m, func_decl* h) : m_decl(h, m) {}
 
         entry(ast_manager& m, func_decl* f, expr* def, expr_dependency* dep, vector<dependent_expr> const& rem) :
-            m_removed(rem), m_decl(f, m), m_def(def, m), m_dep(dep, m) {}
+            m_removed(rem),
+            m_decl(m){
+            m_defs.push_back({ func_decl_ref(f, m), expr_ref(def, m), expr_dependency_ref(dep, m) });
+        }
+
+        entry(ast_manager& m, vector<std::tuple<func_decl_ref, expr_ref, expr_dependency_ref>> const& defs, vector<dependent_expr> const& rem) :
+            m_removed(rem),
+            m_decl(m),
+            m_defs(defs) {
+        }
 
         bool is_loose() const { return !m_removed.empty(); }
 
         bool intersects(ast_mark const& free_vars) const {
             if (is_hide())
                 return false;
-            if (is_def())
+            for (auto const& [f, def, dep] : m_defs)
-                return free_vars.is_marked(m_decl);
+                if (free_vars.is_marked(f))
+                    return true;
+            if (m_subst) {
                 for (auto const& [k, v] : m_subst->sub())
                     if (free_vars.is_marked(k))
                         return true;
+            }
             return false;
         }
 
-        bool is_hide() const { return m_decl && !m_def; }
+        bool is_hide() const { return m_decl && m_defs.empty(); }
-        bool is_def() const { return m_decl && m_def; }
+        bool is_def() const { return !m_defs.empty(); }
-        bool is_subst() const { return !m_decl; }
+        bool is_subst() const { return m_subst && !m_subst->empty(); }
     };
 
     ast_manager&             m;
@@ -76,7 +88,8 @@ class model_reconstruction_trail {
 
     void add_vars(expr* e, ast_mark& free_vars) {
         for (expr* t : subterms::all(expr_ref(e, m)))
-            free_vars.mark(t, true);
+            if (is_app(t))
+                free_vars.mark(to_app(t)->get_decl(), true);
     }
     
     void add_vars(dependent_expr const& d, ast_mark& free_vars) {
@@ -86,7 +99,7 @@ class model_reconstruction_trail {
     bool intersects(ast_mark const& free_vars, dependent_expr const& d) {
         expr_ref term(d.fml(), m);
         auto iter = subterms::all(term);
-        return any_of(iter, [&](expr* t) { return free_vars.is_marked(t); });
+        return any_of(iter, [&](expr* t) { return is_app(t) && free_vars.is_marked(to_app(t)->get_decl()); });
     }
 
     bool intersects(ast_mark const& free_vars, vector<dependent_expr> const& added) {
@@ -126,6 +139,14 @@ public:
         m_trail_stack.push(push_back_vector(m_trail));
     }
 
+    /**
+     * add definitions
+     */
+    void push(vector<std::tuple<func_decl_ref, expr_ref, expr_dependency_ref>> const& defs, vector<dependent_expr> const& removed) {
+        m_trail.push_back(alloc(entry, m, defs, removed));
+        m_trail_stack.push(push_back_vector(m_trail));
+    }
+
     /**
     * register a new depedent expression, update the trail 
     * by removing substitutions that are not equivalence preserving.

src/ast/simplifiers/reduce_args_simplifier.cpp

@@ -0,0 +1,428 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    reduce_args_simplifier.cpp
+
+Abstract:
+
+    Reduce the number of arguments in function applications.
+
+Author:
+
+    Leonardo (leonardo) 2012-02-19
+
+Notes:
+
+--*/
+
+#include "util/map.h"
+#include "ast/ast_smt2_pp.h"
+#include "ast/ast_util.h"
+#include "ast/has_free_vars.h"
+#include "ast/rewriter/rewriter_def.h"
+#include "ast/simplifiers/dependent_expr_state.h"
+
+/**
+   \brief Reduce the number of arguments in function applications.
+
+   Example, suppose we have a function f with 2 arguments. 
+   There are 1000 applications of this function, but the first argument is always "a", "b" or "c".
+   Thus, we replace the f(t1, t2)
+   with 
+      f_a(t2)   if   t1 = a
+      f_b(t2)   if   t2 = b
+      f_c(t2)   if   t2 = c
+
+   Since f_a, f_b, f_c are new symbols, satisfiability is preserved.
+   
+   This transformation is very similar in spirit to the Ackermman's reduction. 
+
+   This transformation should work in the following way:
+
+   1- Create a mapping decl2arg_map from declarations to tuples of booleans, an entry [f -> (true, false, true)]
+       means that f is a declaration with 3 arguments where the first and third arguments are always values.
+   2- Traverse the formula and populate the mapping. 
+        For each function application f(t1, ..., tn) do
+          a) Create a boolean tuple (is_value(t1), ..., is_value(tn)) and do
+             the logical-and with the tuple that is already in the mapping. If there is no such tuple
+             in the mapping, we just add a new entry.
+
+   If all entries are false-tuples, then there is nothing to be done. The transformation is not applicable.
+
+   Now, we create a mapping decl2new_decl from (decl, val_1, ..., val_n) to decls. Note that, n may be different for each entry,
+   but it is the same for the same declaration.
+   For example, suppose we have [f -> (true, false, true)] in decl2arg_map, and applications f(1, a, 2), f(1, b, 2), f(1, b, 3), f(2, b, 3), f(2, c, 3) in the formula.
+   Then, decl2arg_map would contain
+        (f, 1, 2) -> f_1_2
+        (f, 1, 3) -> f_1_3
+        (f, 2, 3) -> f_2_3
+   where f_1_2, f_1_3 and f_2_3 are new function symbols.
+   Using the new map, we can replace the occurrences of f.
+*/
+
+class reduce_args_simplifier : public dependent_expr_simplifier {
+    bv_util                  m_bv;
+    
+    static bool is_var_plus_offset(ast_manager& m, bv_util& bv, expr* e, expr*& base) {
+        expr *lhs, *rhs;
+        if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) 
+            base = rhs;
+        else
+            base = e;        
+        return !has_free_vars(base);
+    }
+
+    static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) {
+        base = nullptr;
+        return m.is_unique_value(e) || is_var_plus_offset(m, bv, e, base);
+    }
+
+    static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e) {
+        expr* base;
+        return may_be_unique(m, bv, e, base);
+    }
+    
+    struct find_non_candidates_proc {
+        ast_manager &              m;
+        bv_util &                  m_bv;
+        obj_hashtable<func_decl> & m_non_candidates;
+        
+        find_non_candidates_proc(ast_manager & m, bv_util & bv, obj_hashtable<func_decl> & non_candidates):
+            m(m),
+            m_bv(bv),
+            m_non_candidates(non_candidates) {
+        }
+        
+        void operator()(var * n) {}
+        
+        void operator()(quantifier *n) {}
+        
+        void operator()(app * n) {
+            if (!is_uninterp(n))
+                return;
+            func_decl * d;
+            if (n->get_num_args() == 0)
+                return; // ignore constants
+            d = n->get_decl();
+            if (m_non_candidates.contains(d))
+                return; // it is already in the set.
+            for (expr* arg : *n)
+                if (may_be_unique(m, m_bv, arg))
+                    return;
+            m_non_candidates.insert(d);
+        }
+    };
+
+    /**
+       \brief Populate the table non_candidates with function declarations \c f
+       such that there is a function application (f t1 ... tn) where t1 ... tn are not values.
+    */
+    void find_non_candidates(obj_hashtable<func_decl> & non_candidates) {
+        non_candidates.reset();
+        find_non_candidates_proc proc(m, m_bv, non_candidates);
+        expr_fast_mark1 visited;
+        for (auto i : indices())
+            quick_for_each_expr(proc, visited, m_fmls[i].fml());
+
+        TRACE("reduce_args", tout << "non_candidates:\n"; for (func_decl* d : non_candidates) tout << d->get_name() << "\n";);
+    }
+
+    struct populate_decl2args_proc {
+        reduce_args_simplifier&           m_owner;
+        ast_manager &                     m;
+        bv_util &                         m_bv;
+        obj_hashtable<func_decl> &        m_non_candidates;
+        obj_map<func_decl, bit_vector> &  m_decl2args;    
+        obj_map<func_decl, svector<expr*> > m_decl2base; // for args = base + offset
+
+        populate_decl2args_proc(reduce_args_simplifier& o, ast_manager & m, bv_util & bv, obj_hashtable<func_decl> & nc, obj_map<func_decl, bit_vector> & d):
+            m_owner(o), m(m), m_bv(bv), m_non_candidates(nc), m_decl2args(d) {}
+        
+        void operator()(var * n) {}
+        void operator()(quantifier * n) {}
+        void operator()(app * n) {
+            if (n->get_num_args() == 0)
+                return; // ignore constants
+            func_decl * d = n->get_decl();
+            if (d->get_family_id() != null_family_id)
+                return; // ignore interpreted symbols
+            if (m_non_candidates.contains(d))
+                return; // declaration is not a candidate
+            if (m_owner.m_fmls.frozen(d))
+                return;
+            
+            unsigned j = n->get_num_args();
+            obj_map<func_decl, bit_vector>::iterator it = m_decl2args.find_iterator(d);
+            expr* base;
+            if (it == m_decl2args.end()) {
+                m_decl2args.insert(d, bit_vector());
+                svector<expr*>& bases = m_decl2base.insert_if_not_there(d, svector<expr*>());
+                bases.resize(j);
+                it = m_decl2args.find_iterator(d);
+                SASSERT(it != m_decl2args.end());
+                it->m_value.reserve(j);
+                while (j > 0) {
+                    --j;
+                    it->m_value.set(j, may_be_unique(m, m_bv, n->get_arg(j), base));
+                    bases[j] = base;
+                }
+            } else {
+                svector<expr*>& bases = m_decl2base[d];
+                SASSERT(j == it->m_value.size());                        
+                while (j > 0) {
+                    --j;
+                    it->m_value.set(j, it->m_value.get(j) && may_be_unique(m, m_bv, n->get_arg(j), base) && bases[j] == base);
+                }
+            }
+        }
+    };
+
+    void populate_decl2args(obj_hashtable<func_decl> & non_candidates, 
+                            obj_map<func_decl, bit_vector> & decl2args) {
+        expr_fast_mark1 visited;
+        decl2args.reset();
+        populate_decl2args_proc proc(*this, m, m_bv, non_candidates, decl2args);
+        for (auto i : indices()) 
+            quick_for_each_expr(proc, visited, m_fmls[i].fml());
+        
+        // Remove all cases where the simplification is not applicable.
+        ptr_buffer<func_decl> bad_decls;
+        for (auto const& [k, v] : decl2args) 
+            if (all_of(v, [&](auto b) { return !b;}))
+                bad_decls.push_back(k);                        
+    
+        for (func_decl* a : bad_decls)
+            decl2args.erase(a);
+
+        TRACE("reduce_args", tout << "decl2args:" << std::endl;
+              for (auto const& [k, v] : decl2args) {
+                  tout << k->get_name() << ": ";
+                  for (unsigned i = 0; i < v.size(); ++i)
+                      tout << (v.get(i) ? "1" : "0");
+                  tout << std::endl;
+              });
+    }
+
+    struct arg2func_hash_proc {
+        bit_vector const & m_bv;
+        
+        arg2func_hash_proc(bit_vector const & bv):m_bv(bv) {}
+        unsigned operator()(app const * n) const {
+            // compute the hash-code using only the arguments where m_bv is true.
+            unsigned a = 0x9e3779b9;
+            unsigned num_args = n->get_num_args();
+            for (unsigned i = 0; i < num_args; i++) {
+                if (!m_bv.get(i)) 
+                    continue; // ignore argument
+                a = hash_u_u(a, n->get_arg(i)->get_id());
+            }
+            return a;
+        }
+    };
+     
+    struct arg2func_eq_proc {
+        bit_vector const & m_bv;
+     
+        arg2func_eq_proc(bit_vector const & bv):m_bv(bv) {}
+        bool operator()(app const * n1, app const * n2) const {
+            // compare only the arguments where m_bv is true
+            SASSERT(n1->get_num_args() == n2->get_num_args());
+            unsigned num_args = n1->get_num_args();
+            for (unsigned i = 0; i < num_args; i++) {
+                if (!m_bv.get(i)) 
+                    continue; // ignore argument
+                if (n1->get_arg(i) != n2->get_arg(i))
+                    return false;
+            }
+            return true;
+        }
+    };
+
+    typedef map<app *, func_decl *, arg2func_hash_proc, arg2func_eq_proc> arg2func;
+    typedef obj_map<func_decl, arg2func *> decl2arg2func_map;
+
+    struct reduce_args_ctx { 
+        ast_manager &           m;
+        decl2arg2func_map       m_decl2arg2funcs;
+
+        reduce_args_ctx(ast_manager & m): m(m) {
+        }
+        
+        ~reduce_args_ctx() {
+            for (auto const& [_, map] : m_decl2arg2funcs) {
+                for (auto const& [k, v] : *map) {
+                    m.dec_ref(k);
+                    m.dec_ref(v);
+                }
+                dealloc(map);
+            }
+        }
+    };
+    
+    struct reduce_args_rw_cfg : public default_rewriter_cfg {
+        ast_manager &                    m;
+        reduce_args_simplifier&          m_owner;
+        obj_map<func_decl, bit_vector> & m_decl2args;
+        decl2arg2func_map &              m_decl2arg2funcs;
+        
+        reduce_args_rw_cfg(reduce_args_simplifier& owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
+            m(owner.m),
+            m_owner(owner),
+            m_decl2args(decl2args),
+            m_decl2arg2funcs(decl2arg2funcs) {
+        }
+        
+        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+            result_pr = nullptr;
+            if (f->get_arity() == 0)
+                return BR_FAILED; // ignore constants
+            if (f->get_family_id() != null_family_id)
+                return BR_FAILED; // ignore interpreted symbols
+            obj_map<func_decl, bit_vector>::iterator it = m_decl2args.find_iterator(f);
+            if (it == m_decl2args.end())
+                return BR_FAILED;
+
+            bit_vector & bv = it->m_value;
+            arg2func *& map = m_decl2arg2funcs.insert_if_not_there(f, 0);
+            if (!map) {
+                map = alloc(arg2func, arg2func_hash_proc(bv), arg2func_eq_proc(bv));
+            }
+
+            app_ref tmp(m.mk_app(f, num, args), m);
+            func_decl *& new_f = map->insert_if_not_there(tmp, nullptr);
+            if (!new_f) {
+                // create fresh symbol
+                ptr_buffer<sort> domain;
+                unsigned arity = f->get_arity();
+                for (unsigned i = 0; i < arity; ++i) {
+                    if (!bv.get(i))
+                        domain.push_back(f->get_domain(i));
+                }
+                new_f = m.mk_fresh_func_decl(f->get_name(), symbol::null, domain.size(), domain.data(), f->get_range());
+                m.inc_ref(tmp);
+                m.inc_ref(new_f);
+            }
+
+            ptr_buffer<expr> new_args;
+            for (unsigned i = 0; i < num; i++) {
+                if (!bv.get(i))
+                    new_args.push_back(args[i]);
+            }
+            result = m.mk_app(new_f, new_args.size(), new_args.data());
+            return BR_DONE;
+        }
+    };
+
+    struct reduce_args_rw : rewriter_tpl<reduce_args_rw_cfg> {
+        reduce_args_rw_cfg m_cfg;
+    public:
+        reduce_args_rw(reduce_args_simplifier & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
+            rewriter_tpl<reduce_args_rw_cfg>(owner.m, false, m_cfg),
+            m_cfg(owner, decl2args, decl2arg2funcs) {
+        }
+    };
+
+    void mk_mc(obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs, vector<dependent_expr> const& removed) {
+        ptr_buffer<expr> new_args;
+        var_ref_vector   new_vars(m);
+        ptr_buffer<expr> new_eqs;
+        generic_model_converter * f_mc = alloc(generic_model_converter, m, "reduce_args");
+        for (auto const& [f, map] : decl2arg2funcs)
+            for (auto const& [t, new_def] : *map)
+                m_fmls.model_trail().hide(new_def);
+               
+        vector<std::tuple<func_decl_ref, expr_ref, expr_dependency_ref>> defs;
+        for (auto const& [f, map] : decl2arg2funcs) {
+            expr * def     = nullptr;
+            SASSERT(decl2args.contains(f));
+            bit_vector & bv = decl2args.find(f);
+            new_vars.reset();
+            new_args.reset();
+            for (unsigned i = 0; i < f->get_arity(); i++) {
+                new_vars.push_back(m.mk_var(i, f->get_domain(i)));
+                if (!bv.get(i))
+                    new_args.push_back(new_vars.back());
+            }
+            for (auto const& [t, new_def] : *map) {
+                SASSERT(new_def->get_arity() == new_args.size());
+                app * new_t = m.mk_app(new_def, new_args);
+                if (def == nullptr) {
+                    def = new_t;
+                }
+                else {
+                    new_eqs.reset();
+                    for (unsigned i = 0; i < f->get_arity(); i++) 
+                        if (bv.get(i))
+                            new_eqs.push_back(m.mk_eq(new_vars.get(i), t->get_arg(i)));                    
+                    SASSERT(new_eqs.size() > 0);
+                    expr * cond = mk_and(m, new_eqs);
+                    def = m.mk_ite(cond, new_t, def);
+                }
+            }
+            SASSERT(def);
+            expr_dependency* dep = nullptr;
+            defs.push_back({ func_decl_ref(f,m), expr_ref(def, m), expr_dependency_ref(dep, m) });                 
+        }        
+        m_fmls.model_trail().push(defs, removed);
+    }
+
+    unsigned m_num_decls = 0;
+
+public:
+    reduce_args_simplifier(ast_manager& m, dependent_expr_state& st, params_ref const& p) :
+        dependent_expr_simplifier(m, st),
+        m_bv(m)
+    {}
+
+    ~reduce_args_simplifier() override {}
+
+    char const* name() const override { return "reduce-args"; }
+
+    void collect_statistics(statistics& st) const override {
+        st.update("reduced-funcs", m_num_decls);
+    }
+
+    void reset_statistics() override {
+        m_num_decls = 0;
+    }
+
+    void reduce() override {
+        m_fmls.freeze_suffix();
+        
+        obj_hashtable<func_decl> non_candidates;
+        obj_map<func_decl, bit_vector> decl2args;
+        find_non_candidates(non_candidates);
+        populate_decl2args(non_candidates, decl2args);
+
+        if (decl2args.empty())
+            return;
+
+        m_num_decls += decl2args.size();
+
+        reduce_args_ctx ctx(m);
+        reduce_args_rw rw(*this, decl2args, ctx.m_decl2arg2funcs);
+        vector<dependent_expr> removed;
+        // if not global scope then what?
+        // cannot just use in incremental mode.
+        for (auto i : indices()) {
+            auto [f, p, d] = m_fmls[i]();
+            if (p)
+                continue;
+            expr_ref new_f(m);
+            rw(f, new_f);
+            if (f != new_f) {
+                removed.push_back(m_fmls[i]);
+                m_fmls.update(i, dependent_expr(m, new_f, p, d));
+            }
+        }
+        mk_mc(decl2args, ctx.m_decl2arg2funcs, removed);
+    }
+
+};
+
+dependent_expr_simplifier* mk_reduce_args_simplifier(ast_manager & m, dependent_expr_state& st, params_ref const & p) {
+    return alloc(reduce_args_simplifier, m, st, p);
+}
+

src/ast/simplifiers/reduce_args_simplifier.h

@@ -0,0 +1,16 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    reduce_args_simplifier.h
+
+Abstract:
+
+    Reduce the number of arguments in function applications.
+
+--*/
+#pragma once
+
+dependent_expr_simplifier* mk_reduce_args_simplifier(ast_manager & m, dependent_expr_state& st, params_ref const & p);
+

src/math/lp/CMakeLists.txt

@@ -34,6 +34,7 @@ z3_add_component(lp
     nla_basics_lemmas.cpp
     nla_common.cpp
     nla_core.cpp
+    nla_divisions.cpp
     nla_grobner.cpp
     nla_intervals.cpp
     nla_monotone_lemmas.cpp

src/math/lp/nla_core.cpp

@@ -30,6 +30,7 @@ core::core(lp::lar_solver& s, reslimit & lim) :
     m_order(this),
     m_monotone(this),
     m_powers(*this),
+    m_divisions(*this),
     m_intervals(this, lim),
     m_monomial_bounds(this),
     m_horner(this),
@@ -137,6 +138,11 @@ void core::add_monic(lpvar v, unsigned sz, lpvar const* vs) {
     m_emons.add(v, m_add_buffer);
 }
 
+void core::add_idivision(lpvar r, lpvar x, lpvar y) {
+    m_divisions.add_idivision(r, x, y);
+}
+
+    
 void core::push() {
     TRACE("nla_solver_verbose", tout << "\n";);
     m_emons.push();
@@ -1519,6 +1525,9 @@ lbool core::check(vector<lemma>& l_vec) {
     if (l_vec.empty() && !done()) 
         m_basics.basic_lemma(false);
 
+    if (l_vec.empty() && !done())
+        m_divisions.check(l_vec);
+    
 #if 0
     if (l_vec.empty() && !done() && !run_horner) 
         m_horner.horner_lemmas();

src/math/lp/nla_core.h

@@ -20,6 +20,7 @@
 #include "math/lp/nla_monotone_lemmas.h"
 #include "math/lp/nla_grobner.h"
 #include "math/lp/nla_powers.h"
+#include "math/lp/nla_divisions.h"
 #include "math/lp/emonics.h"
 #include "math/lp/nla_settings.h"
 #include "math/lp/nex.h"
@@ -88,6 +89,7 @@ class core {
     order                    m_order;
     monotone                 m_monotone;
     powers                   m_powers;
+    divisions                m_divisions;
     intervals                m_intervals; 
     monomial_bounds          m_monomial_bounds;
     nla_settings             m_nla_settings;        
@@ -199,8 +201,10 @@ public:
     void deregister_monic_from_tables(const monic & m, unsigned i);
 
     void add_monic(lpvar v, unsigned sz, lpvar const* vs);   
+    void add_idivision(lpvar r, lpvar x, lpvar y);
     void push();     
     void pop(unsigned n);
+    trail_stack& trail() { return m_emons.get_trail_stack(); }
 
     rational mon_value_by_vars(unsigned i) const;
     rational product_value(const monic & m) const;

src/math/lp/nla_divisions.cpp

@@ -0,0 +1,65 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+  nla_divisions.cpp
+
+Author:
+  Lev Nachmanson (levnach)
+  Nikolaj Bjorner (nbjorner)
+
+Description:
+
+  Check divisions
+
+--*/
+#include "math/lp/nla_core.h"
+
+namespace nla {
+
+    void divisions::add_idivision(lpvar r, lpvar x, lpvar y) {
+        m_idivisions.push_back({r, x, y});
+        m_core.trail().push(push_back_vector(m_idivisions));
+    }
+
+    typedef lp::lar_term term;
+    
+    // y1 >= y2 > 0 & x1 <= x2 => x1/y1 <= x2/y2
+    // y2 <= y1 < 0 & x1 >= x2 => x1/y1 <= x2/y2
+    void divisions::check(vector<lemma>& lemmas) {
+        core& c = m_core;        
+        if (c.use_nra_model()) 
+            return;
+
+        for (auto const & [r, x, y] : m_idivisions) {
+            auto xval = c.val(x);
+            auto yval = c.val(y);
+            auto rval = c.val(r);
+            if (!c.var_is_int(x)) 
+                continue;
+            if (yval == 0)
+                continue;
+            // idiv semantics
+            if (rval == div(xval, yval))
+                continue;
+            for (auto const& [r2, x2, y2] : m_idivisions) {
+                if (r2 == r)
+                    continue;
+                auto x2val = c.val(x2);
+                auto y2val = c.val(y2);
+                auto r2val = c.val(r2);
+                if (yval >= y2val && y2val > 0 && xval <= x2val && rval > r2val) {
+                    new_lemma lemma(c, "y1 >= y2 > 0 & x1 <= x2 => x1/y1 <= x2/y2");
+                    lemma |= ineq(term(y, rational(-1), y2), llc::LT, rational::zero());
+                    lemma |= ineq(y2, llc::LE, rational::zero());
+                    lemma |= ineq(term(x, rational(-1), x2), llc::GT, rational::zero());
+                    lemma |= ineq(term(r, rational(-1), r2), llc::LE, rational::zero());
+                    return;
+                }
+            }
+        }
+        
+    }
+    
+}

src/math/lp/nla_divisions.h

@@ -0,0 +1,31 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+  nla_divisions.h
+
+Author:
+  Lev Nachmanson (levnach)
+  Nikolaj Bjorner (nbjorner)
+
+Description:
+  Check division constraints.
+  
+--*/
+
+#include "math/lp/nla_types.h"
+
+namespace nla {
+    
+    class core;
+    
+    class divisions {
+        core& m_core;
+        vector<std::tuple<lpvar, lpvar, lpvar>> m_idivisions;
+    public:
+        divisions(core& c):m_core(c) {}
+        void add_idivision(lpvar r, lpvar x, lpvar y);
+        void check(vector<lemma>&);
+    };
+}

src/math/lp/nla_solver.cpp

@@ -23,6 +23,10 @@ namespace nla {
         m_core->add_monic(v, sz, vs);
     }
 
+    void solver::add_idivision(lpvar r, lpvar x, lpvar y) {
+        m_core->add_idivision(r, x, y);
+    }
+    
     bool solver::is_monic_var(lpvar v) const {
         return m_core->is_monic_var(v);
     }

src/math/lp/nla_solver.h

@@ -25,6 +25,7 @@ namespace nla {
         core* m_core;
     public:
         void add_monic(lpvar v, unsigned sz, lpvar const* vs);    
+        void add_idivision(lpvar r, lpvar x, lpvar y);
         solver(lp::lar_solver& s, reslimit& limit);
         ~solver();
         nla_settings& settings();

src/math/lp/var_eqs.h

@@ -68,8 +68,7 @@ class var_eqs {
 
     T*                                m_merge_handler;    
     union_find<var_eqs>               m_uf;
-    lp::incremental_vector<std::pair<signed_var, signed_var>>    
+    lp::incremental_vector<std::pair<signed_var, signed_var>> m_trail;
-	                                  m_trail;
     vector<svector<eq_edge>>          m_eqs;    // signed_var.index() -> the edges adjacent to signed_var.index()
 
     trail_stack                       m_stack;

src/sat/sat_solver/sat_smt_solver.cpp

@@ -161,7 +161,6 @@ class sat_smt_solver : public solver {
     expr_ref_vector             m_assumptions, m_core, m_ors, m_aux_fmls, m_internalized_fmls;
     atom2bool_var               m_map;
     generic_model_converter_ref m_mc;
-    unsigned                    m_mc_size = 0;
     mutable model_converter_ref m_cached_mc;
     mutable ref<sat2goal::mc>   m_sat_mc;
     std::string                 m_unknown = "no reason given";
@@ -180,8 +179,7 @@ public:
         m_trail(m_preprocess_state.m_trail),
         m_dep(m, m_trail),
         m_assumptions(m), m_core(m), m_ors(m), m_aux_fmls(m), m_internalized_fmls(m),
-        m_map(m),
+        m_map(m) {
-        m_mc(alloc(generic_model_converter, m, "sat-smt-solver")) {
         updt_params(p);
         init_preprocess();
         m_solver.set_incremental(true);
@@ -211,7 +209,6 @@ public:
         for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f));
         if (m_mc) result->m_mc = dynamic_cast<generic_model_converter*>(m_mc->translate(tr));
         result->m_dep.copy(tr, m_dep);
-        result->m_mc_size = m_mc_size;
         if (m_sat_mc) result->m_sat_mc = dynamic_cast<sat2goal::mc*>(m_sat_mc->translate(tr));
         result->m_internalized_converted = m_internalized_converted;
         return result;
@@ -291,7 +288,6 @@ public:
         m_preprocess.push();
         m_trail.push(restore_vector(m_assumptions));
         m_trail.push(restore_vector(m_fmls));
-        m_trail.push(value_trail(m_mc_size));
     }
 
     void pop(unsigned n) override {
@@ -302,7 +298,6 @@ public:
         m_map.pop(n);
         m_goal2sat.user_pop(n);
         m_solver.user_pop(n);
-        m_mc->shrink(m_mc_size);
     }
 
     void set_phase(expr* e) override { 
@@ -549,6 +544,7 @@ public:
 
     model_converter_ref get_model_converter() const override {
         const_cast<sat_smt_solver*>(this)->convert_internalized();
+        verbose_stream() << "get model converter " << (m_cached_mc.get() != nullptr) << "\n";
         if (m_cached_mc)
             return m_cached_mc;
         if (is_internalized() && m_internalized_converted) {            
@@ -660,6 +656,7 @@ private:
         if (!m.inc())
             return l_undef;
         m_preprocess_state.advance_qhead();
+        m_mc = alloc(generic_model_converter, m, "sat-model-converter");
         m_preprocess_state.append(*m_mc);
         m_solver.pop_to_base_level();
         m_aux_fmls.reset();
@@ -754,13 +751,11 @@ private:
         if (m_sat_mc) 
             (*m_sat_mc)(mdl);
         m_goal2sat.update_model(mdl);
-        TRACE("sat", m_mc->display(tout););
+
-        (*m_mc)(mdl);
     
         TRACE("sat", model_smt2_pp(tout, m, *mdl, 0););        
 
-        if (!gparams::get_ref().get_bool("model_validate", false)) 
+        if (gparams::get_ref().get_bool("model_validate", false)) {
-            return;        
             IF_VERBOSE(1, verbose_stream() << "Verifying solution\n";);
             model_evaluator eval(*mdl);
             eval.set_model_completion(true);
@@ -791,6 +786,9 @@ private:
                 IF_VERBOSE(1, verbose_stream() << "solution verified\n");
             }
         }
+        TRACE("sat", m_mc->display(tout););
+        (*m_mc)(mdl);        
+    }
 };
 
 

src/smt/theory_lra.cpp

@@ -435,6 +435,13 @@ class theory_lra::imp {
                     app_ref mod(a.mk_mod(n1, n2), m);
                     ctx().internalize(mod, false);
                     if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod);
+#if 0
+                    // shortcut to create non-linear division axioms.
+                    theory_var r = mk_var(n);
+                    theory_var x = mk_var(n1);
+                    theory_var y = mk_var(n2);
+                    m_nla->add_idivision(get_lpvar(n), get_lpvar(n1), get_lpvar(n2));
+#endif
                 }
                 else if (a.is_mod(n, n1, n2)) {
                     if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);

src/tactic/core/reduce_args_tactic.cpp

@@ -18,6 +18,7 @@ Notes:
 --*/
 #include "tactic/tactical.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_util.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/has_free_vars.h"
 #include "util/map.h"
@@ -414,7 +415,6 @@ struct reduce_args_tactic::imp {
                     new_args.push_back(new_vars.back());
             }
             for (auto const& [t, new_def] : *map) {
-                // f_mc->hide(new_def);
                 SASSERT(new_def->get_arity() == new_args.size());
                 app * new_t = m.mk_app(new_def, new_args);
                 if (def == nullptr) {
@@ -427,11 +427,7 @@ struct reduce_args_tactic::imp {
                             new_eqs.push_back(m.mk_eq(new_vars.get(i), t->get_arg(i)));
                     }
                     SASSERT(new_eqs.size() > 0);
-                    expr * cond;
+                    expr * cond = mk_and(m, new_eqs);
-                    if (new_eqs.size() == 1)
-                        cond = new_eqs[0];
-                    else
-                        cond = m.mk_and(new_eqs);
                     def = m.mk_ite(cond, new_t, def);
                 }
             }

src/tactic/core/reduce_args_tactic.h

@@ -63,6 +63,8 @@ It creates a fresh function for each of the different values at position `i`.
 #pragma once
 
 #include "util/params.h"
+#include "ast/simplifiers/reduce_args_simplifier.h"
+#include "tactic/dependent_expr_state_tactic.h"
 class ast_manager;
 class tactic;
 
@@ -71,3 +73,11 @@ tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p = params_re
   ADD_TACTIC("reduce-args", "reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.", "mk_reduce_args_tactic(m, p)")
 */
 
+inline tactic* mk_reduce_args_tactic2(ast_manager& m, params_ref const& p = params_ref()) {
+    return alloc(dependent_expr_state_tactic, m, p, 
+        [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { return mk_reduce_args_simplifier(m, s, p); });
+}
+/*
+  ADD_TACTIC("reduce-args2", "reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.", "mk_reduce_args_tactic2(m, p)")
+*/
+

src/tactic/dependent_expr_state_tactic.h

@@ -30,6 +30,7 @@ private:
     dependent_expr  m_dep;
     statistics      m_st;
     factoryTy       m_factory;
+    expr_ref_vector m_frozen;
     scoped_ptr<dependent_expr_simplifier>   m_simp;
     scoped_ptr<model_reconstruction_trail>  m_model_trail;
 
@@ -37,6 +38,9 @@ private:
         if (!m_simp) {
             m_simp = m_factory(m, m_params, *this);
             m_st.reset();
+            push();
+            for (expr* e : m_frozen)
+                freeze(e);
         }
         if (!m_model_trail)
             m_model_trail = alloc(model_reconstruction_trail, m, m_trail);
@@ -49,9 +53,15 @@ public:
         m(m),
         m_params(p),
         m_dep(m, m.mk_true(), nullptr, nullptr),
-        m_factory(f)
+        m_factory(f),
+        m_frozen(m)
     {}
 
+    ~dependent_expr_state_tactic() override {
+        if (m_simp)
+            pop(1);
+    }
+
     /**
     * size(), [](), update() and inconsisent() implement the abstract interface of dependent_expr_state
     */
@@ -124,8 +134,10 @@ public:
     }
 
     void cleanup() override {
-        if (m_simp) 
+        if (m_simp) {
             m_simp->collect_statistics(m_st);
+            pop(1);
+        }
         m_simp = nullptr;
         m_model_trail = nullptr;
         m_goal = nullptr;
@@ -144,5 +156,17 @@ public:
             m_simp->reset_statistics();
         m_st.reset();
     }
-};
 
+    void user_propagate_register_expr(expr* e) override {
+        freeze(e);
+        m_frozen.push_back(e);
+    }
+
+    void user_propagate_clear() override {
+        if (m_simp) {
+            pop(1);
+            push();
+        }
+        m_frozen.reset();
+    }
+};

src/util/bit_vector.h

@@ -211,6 +211,22 @@ public:
 
     bool contains(const bit_vector & other) const;
 
+    class iterator {
+        bit_vector const& b;
+        unsigned m_curr;
+    public:
+        iterator(bit_vector const& b, unsigned i) : b(b), m_curr(i) {}
+        bool operator*(unsigned i) const { return b.get(m_curr); }
+        bool operator*() const { return b.get(m_curr); }
+        iterator& operator++() { ++m_curr; return *this; }
+        iterator operator++(int) { iterator tmp = *this; ++* this; return tmp; }
+        bool operator==(iterator const& it) const { return m_curr == it.m_curr; }
+        bool operator!=(iterator const& it) const { return m_curr != it.m_curr; }        
+    };
+
+    iterator begin() const { return iterator(*this, 0); }
+    iterator end() const { return iterator(*this, size()); }
+
 };
 
 inline std::ostream & operator<<(std::ostream & out, bit_vector const & b) {