Merge branch 'master' of https://github.com/Z3Prover/z3

src/api/api_model.cpp

@@ -30,6 +30,17 @@ Revision History:
 
 extern "C" {
 
+    Z3_model Z3_API Z3_mk_model(Z3_context c) {
+        Z3_TRY;
+        LOG_Z3_mk_model(c);
+        RESET_ERROR_CODE();
+        Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 
+        m_ref->m_model = alloc(model, mk_c(c)->m());
+        mk_c(c)->save_object(m_ref);
+        RETURN_Z3(of_model(m_ref));
+        Z3_CATCH_RETURN(0);
+    }
+
     void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m) {
         Z3_TRY;
         LOG_Z3_model_inc_ref(c, m);
@@ -224,6 +235,31 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast else_val) {
+        Z3_TRY;
+        LOG_Z3_add_func_interp(c, m, f, else_val);
+        RESET_ERROR_CODE();
+        func_decl* d = to_func_decl(f);
+        model* mdl = to_model_ref(m);
+        Z3_func_interp_ref * f_ref = alloc(Z3_func_interp_ref, *mk_c(c), mdl); 
+        f_ref->m_func_interp = alloc(func_interp, mk_c(c)->m(), d->get_arity());
+        mk_c(c)->save_object(f_ref);
+        mdl->register_decl(d, f_ref->m_func_interp);
+        f_ref->m_func_interp->set_else(to_expr(else_val));
+        RETURN_Z3(of_func_interp(f_ref));
+        Z3_CATCH_RETURN(0);        
+    }
+
+    void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_add_const_interp(c, m, f, a);
+        RESET_ERROR_CODE();
+        func_decl* d = to_func_decl(f);
+        model* mdl = to_model_ref(m);
+        mdl->register_decl(d, to_expr(a));
+        Z3_CATCH;
+    }
+
     void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f) {
         Z3_TRY;
         LOG_Z3_func_interp_inc_ref(c, f);
@@ -283,6 +319,15 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value) {
+        Z3_TRY;
+        LOG_Z3_func_interp_set_else(c, f, else_value);
+        RESET_ERROR_CODE();
+        // CHECK_NON_NULL(f, 0);
+        to_func_interp_ref(f)->set_else(to_expr(else_value));
+        Z3_CATCH;
+    }
+
     unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f) {
         Z3_TRY;
         LOG_Z3_func_interp_get_arity(c, f);
@@ -292,6 +337,24 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value) {
+        Z3_TRY;
+        LOG_Z3_func_interp_add_entry(c, fi, args, value);
+        //CHECK_NON_NULL(fi, void);
+        //CHECK_NON_NULL(args, void);
+        //CHECK_NON_NULL(value, void);
+        func_interp* _fi = to_func_interp_ref(fi);
+        expr* _value = to_expr(value);
+        if (to_ast_vector_ref(args).size() != _fi->get_arity()) {
+            SET_ERROR_CODE(Z3_IOB);
+            return;
+        }
+        // check sorts of value
+        expr* const* _args = (expr* const*) to_ast_vector_ref(args).c_ptr();
+        _fi->insert_entry(_args, _value);
+        Z3_CATCH;
+    }
+
     void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e) {
         Z3_TRY;
         LOG_Z3_func_entry_inc_ref(c, e);

src/api/c++/z3++.h

@@ -1731,6 +1731,14 @@ namespace z3 {
         expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
         unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
         func_entry entry(unsigned i) const { Z3_func_entry e = Z3_func_interp_get_entry(ctx(), m_interp, i); check_error(); return func_entry(ctx(), e); }
+        void add_entry(expr_vector const& args, expr& value) {
+            Z3_func_interp_add_entry(ctx(), m_interp, args, value);
+            check_error();
+        }
+        void set_else(expr& value) {
+            Z3_func_interp_set_else(ctx(), m_interp, value);
+            check_error();
+        }
     };
 
     class model : public object {
@@ -1740,6 +1748,7 @@ namespace z3 {
             Z3_model_inc_ref(ctx(), m);
         }
     public:
+        model(context & c):object(c) { init(Z3_mk_model(c)); }
         model(context & c, Z3_model m):object(c) { init(m); }
         model(model const & s):object(s) { init(s.m_model); }
         ~model() { Z3_model_dec_ref(ctx(), m_model); }
@@ -1795,6 +1804,17 @@ namespace z3 {
             return 0 != Z3_model_has_interp(ctx(), m_model, f);
         }
 
+        func_interp add_func_interp(func_decl& f, expr& else_val) {
+            Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
+            check_error();
+            return func_interp(ctx(), r);
+        }
+
+        void add_const_interp(func_decl& f, expr& value) {
+            Z3_add_const_interp(ctx(), m_model, f, value);
+            check_error();
+        }
+
         friend std::ostream & operator<<(std::ostream & out, model const & m);
     };
     inline std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }

src/api/z3_api.h

@@ -4680,6 +4680,14 @@ extern "C" {
 
     /** @name Models */
     /*@{*/
+
+    /**
+       \brief Create a fresh model object. It has reference count 0.
+
+       def_API('Z3_mk_model', MODEL, (_in(CONTEXT),))
+    */
+    Z3_model Z3_API Z3_mk_model(Z3_context c);
+
     /**
        \brief Increment the reference counter of the given model.
 
@@ -4850,6 +4858,26 @@ extern "C" {
     */
     Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a);
 
+    /**
+       \brief Create a fresh func_interp object, add it to a model for a specified function. 
+       It has reference count 0.       
+
+       \param c context
+       \param m model
+       \param f function declaration 
+       \param default_value default value for function interpretation
+
+       def_API('Z3_add_func_interp', FUNC_INTERP, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(AST)))
+    */
+    Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value);
+
+    /**
+       \brief Add a constant interpretation.
+
+       def_API('Z3_add_const_interp', VOID, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(AST)))
+     */
+    void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a);
+
     /**
        \brief Increment the reference counter of the given Z3_func_interp object.
 
@@ -4897,6 +4925,16 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f);
 
+    /**
+       \brief Return the 'else' value of the given function interpretation.
+
+       A function interpretation is represented as a finite map and an 'else' value.
+       This procedure can be used to update the 'else' value.
+
+       def_API('Z3_func_interp_set_else', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST)))
+    */
+    void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value);
+
     /**
        \brief Return the arity (number of arguments) of the given function interpretation.
 
@@ -4904,6 +4942,22 @@ extern "C" {
     */
     unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f);
 
+    /**
+       \brief add a function entry to a function interpretation.
+
+       \param c logical context
+       \param fi a function interpregation to be updated.
+       \param args list of arguments. They should be constant values (such as integers) and be of the same types as the domain of the function.
+       \param value value of the function when the parameters match args.
+
+       It is assumed that entries added to a function cover disjoint arguments. 
+       If an two entries are added with the same arguments, only the second insertion survives and the
+       first inserted entry is removed.
+
+       def_API('Z3_func_interp_add_entry', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST_VECTOR), _in(AST)))
+     */
+    void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value);
+
     /**
        \brief Increment the reference counter of the given Z3_func_entry object.
 

src/ast/arith_decl_plugin.cpp

@@ -215,18 +215,8 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m_e = m->mk_const(e_decl);
     m->inc_ref(m_e);
 
-    func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT));
-    m_0_pw_0_int = m->mk_const(z_pw_z_int);
-    m->inc_ref(m_0_pw_0_int);
-
-    func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL));
-    m_0_pw_0_real = m->mk_const(z_pw_z_real);
-    m->inc_ref(m_0_pw_0_real);
 
     MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r);
-    MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r);
-    MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i);
-    MK_UNARY(m_mod_0_decl, "mod0", OP_MOD_0, i);
     MK_UNARY(m_u_asin_decl, "asin-u", OP_U_ASIN, r);
     MK_UNARY(m_u_acos_decl, "acos-u", OP_U_ACOS, r);
 }
@@ -279,12 +269,7 @@ arith_decl_plugin::arith_decl_plugin():
     m_atanh_decl(0),
     m_pi(0),
     m_e(0),
-    m_0_pw_0_int(0),
-    m_0_pw_0_real(0),
     m_neg_root_decl(0),
-    m_div_0_decl(0),
-    m_idiv_0_decl(0),
-    m_mod_0_decl(0),
     m_u_asin_decl(0),
     m_u_acos_decl(0),
     m_convert_int_numerals_to_real(false) {
@@ -339,12 +324,7 @@ void arith_decl_plugin::finalize() {
     DEC_REF(m_atanh_decl);
     DEC_REF(m_pi);
     DEC_REF(m_e);
-    DEC_REF(m_0_pw_0_int);
-    DEC_REF(m_0_pw_0_real);
     DEC_REF(m_neg_root_decl);
-    DEC_REF(m_div_0_decl);
-    DEC_REF(m_idiv_0_decl);
-    DEC_REF(m_mod_0_decl);
     DEC_REF(m_u_asin_decl);
     DEC_REF(m_u_acos_decl);
     m_manager->dec_array_ref(m_small_ints.size(), m_small_ints.c_ptr());
@@ -392,12 +372,12 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
     case OP_ATANH:     return m_atanh_decl;
     case OP_PI:        return m_pi->get_decl();
     case OP_E:         return m_e->get_decl();
-    case OP_0_PW_0_INT:  return m_0_pw_0_int->get_decl();
+    //case OP_0_PW_0_INT:  return m_0_pw_0_int->get_decl();
-    case OP_0_PW_0_REAL: return m_0_pw_0_real->get_decl();
+    //case OP_0_PW_0_REAL: return m_0_pw_0_real->get_decl();
     case OP_NEG_ROOT:    return m_neg_root_decl;
-    case OP_DIV_0:       return m_div_0_decl;
+    //case OP_DIV_0:       return m_div_0_decl;
-    case OP_IDIV_0:      return m_idiv_0_decl;
+    //case OP_IDIV_0:      return m_idiv_0_decl;
-    case OP_MOD_0:       return m_mod_0_decl;
+    //case OP_MOD_0:       return m_mod_0_decl;
     case OP_U_ASIN:      return m_u_asin_decl;
     case OP_U_ACOS:      return m_u_acos_decl;
     default: return 0;
@@ -489,9 +469,9 @@ static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args
 static bool is_const_op(decl_kind k) {
     return
         k == OP_PI ||
-        k == OP_E  ||
+        k == OP_E;
-        k == OP_0_PW_0_INT ||
+        //k == OP_0_PW_0_INT ||
-        k == OP_0_PW_0_REAL;
+        //k == OP_0_PW_0_REAL;
 }
 
 func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,

src/ast/arith_decl_plugin.h

@@ -70,12 +70,7 @@ enum arith_op_kind {
     OP_PI,
     OP_E,
     // under-specified symbols
-    OP_0_PW_0_INT,    // 0^0 for integers
-    OP_0_PW_0_REAL,   // 0^0 for reals
     OP_NEG_ROOT,      // x^n when n is even and x is negative
-    OP_DIV_0,         // x/0
-    OP_IDIV_0,        // x div 0
-    OP_MOD_0,         // x mod 0
     OP_U_ASIN,        // asin(x) for x < -1 or x > 1
     OP_U_ACOS,        // acos(x) for x < -1 or x > 1
     LAST_ARITH_OP
@@ -141,12 +136,7 @@ protected:
     app       * m_pi;
     app       * m_e;
 
-    app       * m_0_pw_0_int;
-    app       * m_0_pw_0_real;
     func_decl * m_neg_root_decl;
-    func_decl * m_div_0_decl;
-    func_decl * m_idiv_0_decl;
-    func_decl * m_mod_0_decl;
     func_decl * m_u_asin_decl;
     func_decl * m_u_acos_decl;
     ptr_vector<app> m_small_ints;
@@ -207,10 +197,6 @@ public:
 
     app * mk_e() const { return m_e; }
 
-    app * mk_0_pw_0_int() const { return m_0_pw_0_int; }
-
-    app * mk_0_pw_0_real() const { return m_0_pw_0_real; }
-
     virtual expr * get_some_value(sort * s);
 
     virtual bool is_considered_uninterpreted(func_decl * f) {
@@ -218,12 +204,7 @@ public:
             return false;
         switch (f->get_decl_kind())
         {
-        case OP_0_PW_0_INT:
-        case OP_0_PW_0_REAL:
         case OP_NEG_ROOT:
-        case OP_DIV_0:
-        case OP_IDIV_0:
-        case OP_MOD_0:
         case OP_U_ASIN:
         case OP_U_ACOS:
             return true;
@@ -276,9 +257,9 @@ public:
     bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); }
     bool is_mul(expr const * n) const { return is_app_of(n, m_afid, OP_MUL); }
     bool is_div(expr const * n) const { return is_app_of(n, m_afid, OP_DIV); }
-    bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); }
+    //bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); }
     bool is_idiv(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV); }
-    bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); }
+    //bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); }
     bool is_mod(expr const * n) const { return is_app_of(n, m_afid, OP_MOD); }
     bool is_rem(expr const * n) const { return is_app_of(n, m_afid, OP_REM); }
     bool is_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); }
@@ -389,16 +370,16 @@ public:
     app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); }
     app * mk_gt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GT, arg1, arg2); }
 
-    app * mk_add(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_ADD, num_args, args); }
+    app * mk_add(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_ADD, num_args, args); }
-    app * mk_add(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); }
+    app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); }
-    app * mk_add(expr * arg1, expr * arg2, expr* arg3) { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); }
+    app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); }
 
-    app * mk_sub(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); }
+    app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); }
-    app * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); }
+    app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); }
-    app * mk_mul(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); }
+    app * mk_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); }
-    app * mk_mul(expr * arg1, expr * arg2, expr* arg3) { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); }
+    app * mk_mul(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); }
-    app * mk_mul(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_MUL, num_args, args); }
+    app * mk_mul(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_MUL, num_args, args); }
-    app * mk_uminus(expr * arg) { return m_manager.mk_app(m_afid, OP_UMINUS, arg); }
+    app * mk_uminus(expr * arg) const { return m_manager.mk_app(m_afid, OP_UMINUS, arg); }
     app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_DIV, arg1, arg2); }
     app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV, arg1, arg2); }
     app * mk_rem(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_REM, arg1, arg2); }
@@ -425,11 +406,6 @@ public:
     app * mk_pi() { return plugin().mk_pi(); }
     app * mk_e()  { return plugin().mk_e(); }
 
-    app * mk_0_pw_0_int() { return plugin().mk_0_pw_0_int(); }
-    app * mk_0_pw_0_real() { return plugin().mk_0_pw_0_real(); }
-    app * mk_div0(expr * arg) { return m_manager.mk_app(m_afid, OP_DIV_0, arg); }
-    app * mk_idiv0(expr * arg) { return m_manager.mk_app(m_afid, OP_IDIV_0, arg); }
-    app * mk_mod0(expr * arg) { return m_manager.mk_app(m_afid, OP_MOD_0, arg); }
     app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); }
     app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); }
     app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); }

src/ast/ast.cpp

@@ -1727,7 +1727,6 @@ ast * ast_manager::register_node_core(ast * n) {
 
     n->m_id   = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
 
-
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
     // increment reference counters

src/ast/macros/macro_finder.cpp

@@ -45,7 +45,7 @@ bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
 
    For case 2 & 3, the new quantifiers are stored in new_exprs and new_prs.
 */
-bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
+bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_dependency * dep, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
     if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
         return false;
     arith_simplifier_plugin * as = get_arith_simp();
@@ -78,8 +78,9 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
         proof * rw  = m_manager.mk_rewrite(n, new_q);
         new_pr      = m_manager.mk_modus_ponens(pr, rw);
     }
+    expr_dependency * new_dep = dep;
     if (m_manager.is_eq(body)) {
-        return m_macro_manager.insert(head->get_decl(), new_q, new_pr);
+        return m_macro_manager.insert(head->get_decl(), new_q, new_pr, new_dep);
     }
     // is ge or le
     //
@@ -111,6 +112,10 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
         new_prs.push_back(pr1);
         new_prs.push_back(pr2);
     }
+    if (dep) {
+        new_deps.push_back(new_dep);
+        new_deps.push_back(new_dep);
+    }
     return true;
 }
 
@@ -126,8 +131,8 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
 
    The new quantifiers and proofs are stored in new_exprs and new_prs
 */
-static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, 
+static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, expr_dependency * dep,
-                                         expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
+                                         expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps ) {
     func_decl * f = head->get_decl();
     func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
     app * k_app   = m.mk_app(k, head->get_num_args(), head->get_args());
@@ -153,6 +158,8 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e
         new_prs.push_back(pr1);
         new_prs.push_back(pr2);
     }
+    new_deps.push_back(dep);
+    new_deps.push_back(dep);
 }
 
 macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
@@ -164,57 +171,67 @@ macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
 macro_finder::~macro_finder() {
 }
 
-bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
+bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps,  expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
     TRACE("macro_finder", tout << "starting expand_macros:\n";
           m_macro_manager.display(tout););
     bool found_new_macro = false;
     for (unsigned i = 0; i < num; i++) {
         expr * n       = exprs[i];
         proof * pr     = m_manager.proofs_enabled() ? prs[i] : 0;
+        expr_dependency * depi = deps != 0 ? deps[i] : 0;
         expr_ref new_n(m_manager), def(m_manager);
         proof_ref new_pr(m_manager);
-        m_macro_manager.expand_macros(n, pr, new_n, new_pr);
+        expr_dependency_ref new_dep(m_manager);
+        m_macro_manager.expand_macros(n, pr, depi, new_n, new_pr, new_dep);
         app_ref head(m_manager), t(m_manager);
-        if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) {
+        if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr, new_dep)) {
             TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";);
             found_new_macro = true;
         }
-        else if (is_arith_macro(new_n, new_pr, new_exprs, new_prs)) {
+        else if (is_arith_macro(new_n, new_pr, new_dep, new_exprs, new_prs, new_deps)) {
             TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";);
             found_new_macro = true;
         }
         else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) {
             TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";);
-            pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_exprs, new_prs);
+            pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_dep, new_exprs, new_prs, new_deps);
             found_new_macro = true;
         }
         else {
             new_exprs.push_back(new_n);
             if (m_manager.proofs_enabled())
                 new_prs.push_back(new_pr);
+            if (deps != 0)
+                new_deps.push_back(new_dep);
         }
     }
     return found_new_macro;
 }
 
-void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
+void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
     TRACE("macro_finder", tout << "processing macros...\n";);
     expr_ref_vector   _new_exprs(m_manager);
     proof_ref_vector  _new_prs(m_manager);
-    if (expand_macros(num, exprs, prs, _new_exprs, _new_prs)) {
+    expr_dependency_ref_vector _new_deps(m_manager);
+    if (expand_macros(num, exprs, prs, deps, _new_exprs, _new_prs, _new_deps)) {
         while (true) {
             expr_ref_vector  old_exprs(m_manager);
             proof_ref_vector old_prs(m_manager);
+            expr_dependency_ref_vector old_deps(m_manager);
             _new_exprs.swap(old_exprs);
             _new_prs.swap(old_prs);
+            _new_deps.swap(old_deps);
             SASSERT(_new_exprs.empty());
             SASSERT(_new_prs.empty());
-            if (!expand_macros(old_exprs.size(), old_exprs.c_ptr(), old_prs.c_ptr(), _new_exprs, _new_prs))
+            SASSERT(_new_deps.empty());
+            if (!expand_macros(old_exprs.size(), old_exprs.c_ptr(), old_prs.c_ptr(), old_deps.c_ptr(),
+                               _new_exprs, _new_prs, _new_deps))
                 break;
         }
     }
     new_exprs.append(_new_exprs);
     new_prs.append(_new_prs);
+    new_deps.append(_new_deps);
 }
 
 

src/ast/macros/macro_finder.h

@@ -23,12 +23,6 @@ Revision History:
 #include "ast/simplifier/arith_simplifier_plugin.h"
 
 
-bool is_macro_head(expr * n, unsigned num_decls);
-bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, obj_hashtable<func_decl> const * forbidden_set, app * & head, expr * & def);
-inline bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, app * & head, expr * & def) {
-    return is_simple_macro(m, n, num_decls, 0, head, def);
-}
-
 /**
    \brief Macro finder is responsible for finding universally quantified sub-formulas that can be used
    as macros.
@@ -38,17 +32,14 @@ class macro_finder {
     macro_manager &             m_macro_manager;
     macro_util &                m_util;
     arith_simplifier_plugin * get_arith_simp() { return m_util.get_arith_simp(); }
-    bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
-    bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    bool is_arith_macro(expr * n, proof * pr, expr_dependency * dep, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
-
     bool is_macro(expr * n, app_ref & head, expr_ref & def);
-    bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t);
-    bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def);
 
 public:
     macro_finder(ast_manager & m, macro_manager & mm);
     ~macro_finder();
-    void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    void operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
 };
 
 #endif /* MACRO_FINDER_H_ */

src/ast/macros/macro_manager.cpp

@@ -32,6 +32,7 @@ macro_manager::macro_manager(ast_manager & m, simplifier & s):
     m_decls(m),
     m_macros(m),
     m_macro_prs(m),
+    m_macro_deps(m),
     m_forbidden(m),
     m_deps(m) {
     m_util.set_forbidden_set(&m_forbidden_set);
@@ -60,13 +61,16 @@ void macro_manager::restore_decls(unsigned old_sz) {
     for (unsigned i = old_sz; i < sz; i++) {
         m_decl2macro.erase(m_decls.get(i));
         m_deps.erase(m_decls.get(i));
-        if (m_manager.proofs_enabled())
+        if (m_manager.proofs_enabled()) {
             m_decl2macro_pr.erase(m_decls.get(i));
+            m_decl2macro_dep.erase(m_decls.get(i));
+        }
     }
     m_decls.shrink(old_sz);
     m_macros.shrink(old_sz);
     if (m_manager.proofs_enabled())
         m_macro_prs.shrink(old_sz);
+    m_macro_deps.shrink(old_sz);
 }
 
 void macro_manager::restore_forbidden(unsigned old_sz) {
@@ -79,16 +83,18 @@ void macro_manager::restore_forbidden(unsigned old_sz) {
 void macro_manager::reset() {
     m_decl2macro.reset();
     m_decl2macro_pr.reset();
+    m_decl2macro_dep.reset();
     m_decls.reset();
     m_macros.reset();
     m_macro_prs.reset();
+    m_macro_deps.reset();
     m_scopes.reset();
     m_forbidden_set.reset();
     m_forbidden.reset();
     m_deps.reset();
 }
 
-bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) {
+bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) {
     TRACE("macro_insert", tout << "trying to create macro: " << f->get_name() << "\n" << mk_pp(m, m_manager) << "\n";);
 
     // if we already have a macro for f then return false;
@@ -115,6 +121,8 @@ bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) {
         m_macro_prs.push_back(pr);
         m_decl2macro_pr.insert(f, pr);
     }
+    m_macro_deps.push_back(dep);
+    m_decl2macro_dep.insert(f, dep);
 
     TRACE("macro_insert", tout << "A macro was successfully created for: " << f->get_name() << "\n";);
 
@@ -195,7 +203,8 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
 
 macro_manager::macro_expander::macro_expander(ast_manager & m, macro_manager & mm, simplifier & s):
     simplifier(m),
-    m_macro_manager(mm) {
+    m_macro_manager(mm),
+    m_used_macro_dependencies(m) {
     // REMARK: theory simplifier should not be used by macro_expander...
     // is_arith_macro rewrites a quantifer such as:
     //   forall (x Int) (= (+ x (+ (f x) 1)) 2)
@@ -286,34 +295,41 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref
         }
         else {
             p = 0;
+            expr_dependency * ed = m_macro_manager.m_decl2macro_dep.find(d);
+            m_used_macro_dependencies = m.mk_join(m_used_macro_dependencies, ed);
         }
         return true;
     }
     return false;
 }
 
-void macro_manager::expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref & new_pr) {
+void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep) {
     if (has_macros()) {
         // Expand macros with "real" proof production support (NO rewrite*)
         expr_ref old_n(m_manager);
         proof_ref old_pr(m_manager);
+        expr_dependency_ref old_dep(m_manager);
         old_n  = n;
         old_pr = pr;
+        old_dep = dep;
         for (;;) {
             macro_expander proc(m_manager, *this, m_simplifier);
             proof_ref n_eq_r_pr(m_manager);
             TRACE("macro_manager_bug", tout << "expand_macros:\n" << mk_pp(n, m_manager) << "\n";);
             proc(old_n, r, n_eq_r_pr);
             new_pr = m_manager.mk_modus_ponens(old_pr, n_eq_r_pr);
+            new_dep = m_manager.mk_join(old_dep, proc.m_used_macro_dependencies);
             if (r.get() == old_n.get())
                 return;
             old_n  = r;
             old_pr = new_pr;
+            old_dep = new_dep;
         }
     }
     else {
         r      = n;
         new_pr = pr;
+        new_dep = dep;
     }
 }
 

src/ast/macros/macro_manager.h

@@ -42,9 +42,11 @@ class macro_manager {
 
     obj_map<func_decl, quantifier *> m_decl2macro;    // func-decl -> quantifier
     obj_map<func_decl, proof *>      m_decl2macro_pr; // func-decl -> quantifier_proof
+    obj_map<func_decl, expr_dependency *> m_decl2macro_dep; // func-decl -> unsat core dependency
     func_decl_ref_vector             m_decls;
     quantifier_ref_vector            m_macros;
     proof_ref_vector                 m_macro_prs;
+    expr_dependency_ref_vector       m_macro_deps;
     obj_hashtable<func_decl>         m_forbidden_set;
     func_decl_ref_vector             m_forbidden;
     struct scope {
@@ -64,6 +66,7 @@ class macro_manager {
         virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p);
         virtual void reduce1_quantifier(quantifier * q);
     public:
+        expr_dependency_ref m_used_macro_dependencies;
         macro_expander(ast_manager & m, macro_manager & mm, simplifier & s);
         ~macro_expander();
     };
@@ -74,7 +77,7 @@ public:
     ~macro_manager();
     ast_manager & get_manager() const { return m_manager; }
     macro_util & get_util() { return m_util; }
-    bool insert(func_decl * f, quantifier * m, proof * pr);
+    bool insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep);
     bool has_macros() const { return !m_macros.empty(); }
     void push_scope();
     void pop_scope(unsigned num_scopes);
@@ -90,7 +93,7 @@ public:
     func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const;
     quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = 0; m_decl2macro.find(f, q); return q; }
     void get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const;
-    void expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref & new_pr);
+    void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep);
 
 
 };

src/ast/macros/quasi_macros.cpp

@@ -267,11 +267,10 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
     for (unsigned i = 0 ; i < n ; i++)
         find_occurrences(exprs[i]);
 
-    TRACE("quasi_macros", tout << "Occurrences: " << std::endl;
+    TRACE("quasi_macros",
-    for (occurrences_map::iterator it = m_occurrences.begin(); 
+        tout << "Occurrences: " << std::endl;
-         it != m_occurrences.end(); 
+        for (auto & kd : m_occurrences)
-         it++)
+            tout << kd.m_key->get_name() << ": " << kd.m_value << std::endl; );
-        tout << it->m_key->get_name() << ": " << it->m_value << std::endl; );
 
     // Find all macros
     for (unsigned i = 0 ; i < n ; i++) {
@@ -285,7 +284,8 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
             proof * pr = 0;
             if (m_manager.proofs_enabled())
                 pr = m_manager.mk_def_axiom(macro);
-            if (m_macro_manager.insert(a->get_decl(), macro, pr))
+            expr_dependency * dep = 0;
+            if (m_macro_manager.insert(a->get_decl(), macro, pr, dep))
                 res = true;
         }
     }
@@ -293,21 +293,24 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
     return res;
 }
 
-void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {     
+void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
     for (unsigned i = 0 ; i < n ; i++) {
         expr_ref r(m_manager), rs(m_manager);
         proof_ref pr(m_manager), ps(m_manager);
         proof * p = m_manager.proofs_enabled() ? prs[i] : 0;
-        m_macro_manager.expand_macros(exprs[i], p, r, pr);
+        expr_dependency * dep = deps[i];
+        expr_dependency_ref new_dep(m_manager);
+        m_macro_manager.expand_macros(exprs[i], p, dep, r, pr, new_dep);
         m_simplifier(r, rs, ps);
         new_exprs.push_back(rs);
         new_prs.push_back(ps);
+        new_deps.push_back(new_dep);
     }
 }
 
-bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
+bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
     if (find_macros(n, exprs)) {
-        apply_macros(n, exprs, prs, new_exprs, new_prs);
+        apply_macros(n, exprs, prs, deps, new_exprs, new_prs, new_deps);
         return true;
     } else {
         // just copy them over

src/ast/macros/quasi_macros.h

@@ -54,7 +54,7 @@ class quasi_macros {
 
     void find_occurrences(expr * e);
     bool find_macros(unsigned n, expr * const * exprs);
-    void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
 
 public:
     quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s);
@@ -63,7 +63,7 @@ public:
     /**
        \brief Find pure function macros and apply them.
     */
-    bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);    
+    bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
 };
 
 #endif

src/ast/rewriter/arith_rewriter.cpp

@@ -680,8 +680,7 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul
     if (m_util.is_numeral(arg2, v2, is_int)) {
         SASSERT(!is_int);
         if (v2.is_zero()) {
-            result = m_util.mk_div0(arg1);
+            return BR_FAILED;
-            return BR_REWRITE1;
         }
         else if (m_util.is_numeral(arg1, v1, is_int)) {
             result = m_util.mk_numeral(v1/v2, false);
@@ -734,10 +733,6 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
         result = m_util.mk_numeral(div(v1, v2), is_int);
         return BR_DONE;
     }
-    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) {
-        result = m_util.mk_idiv0(arg1);
-        return BR_REWRITE1;
-    }
     return BR_FAILED;
 }
 

src/ast/simplifier/arith_simplifier_plugin.cpp

@@ -402,11 +402,9 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co
     case OP_TO_REAL:  SASSERT(num_args == 1); mk_to_real(args[0], result); break;
     case OP_TO_INT:   SASSERT(num_args == 1); mk_to_int(args[0], result); break;
     case OP_IS_INT:   SASSERT(num_args == 1); mk_is_int(args[0], result); break;
-    case OP_POWER:                    return false;
+    case OP_POWER:    SASSERT(num_args == 2); mk_power(args[0], args[1], result); break;
     case OP_ABS:      SASSERT(num_args == 1); mk_abs(args[0], result); break;
     case OP_IRRATIONAL_ALGEBRAIC_NUM: return false;
-    case OP_DIV_0: return false;
-    case OP_IDIV_0: return false;
     default:
         return false;
     }
@@ -414,6 +412,25 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co
     return true;
 }
 
+void arith_simplifier_plugin::mk_power(expr* x, expr* y, expr_ref& result) {
+    rational a, b;
+    if (is_numeral(y, b) && b.is_one()) {
+        result = x;
+        return;
+    }
+    if (is_numeral(x, a) && is_numeral(y, b) && b.is_unsigned()) {
+        if (b.is_zero() && !a.is_zero()) {
+            result = m_util.mk_numeral(rational(1), m_manager.get_sort(x));
+            return;
+        }
+        if (!b.is_zero()) {
+            result = m_util.mk_numeral(power(a, b.get_unsigned()), m_manager.get_sort(x));
+            return;
+        }
+    }
+    result = m_util.mk_power(x, y);
+}
+
 void arith_simplifier_plugin::mk_abs(expr * arg, expr_ref & result) {
     expr_ref c(m_manager);
     expr_ref m_arg(m_manager);

src/ast/simplifier/arith_simplifier_plugin.h

@@ -82,6 +82,7 @@ public:
     void mk_to_real(expr * arg, expr_ref & result);
     void mk_to_int(expr * arg, expr_ref & result);
     void mk_is_int(expr * arg, expr_ref & result);
+    void mk_power(expr* x, expr* y, expr_ref& result);
     void mk_abs(expr * arg, expr_ref & result);
 
     virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);

src/ast/simplifier/base_simplifier.h

@@ -37,6 +37,7 @@ protected:
                tout << mk_pp(n, m) << "\n";
                tout << mk_pp(r, m) << "\n";
                tout << mk_pp(p, m) << "\n";);
+        TRACE("cache", tout << mk_pp(n, m) << " -> " << mk_pp(r, m) << "\n";);
         SASSERT(is_rewrite_proof(n, r, p));
     }
     void reset_cache() { m_cache.reset(); }

src/ast/simplifier/simplifier.cpp

@@ -591,8 +591,10 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
                 if (m_ac_cache.find(to_app(arg), new_arg)) {
                     SASSERT(new_arg != 0);
                     new_args.push_back(new_arg);
-                    if (arg != new_arg)
+                    if (arg != new_arg) {
+                        TRACE("ac", tout << mk_pp(arg, m) << " -> " << mk_pp(new_arg, m) << "\n";);
                         has_new_arg = true;
+                    }
                     if (m.fine_grain_proofs()) {
                         proof * pr = 0;
                         m_ac_pr_cache.find(to_app(arg), pr);
@@ -610,8 +612,10 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
                 proof * pr;
                 get_cached(arg, new_arg, pr);
                 new_args.push_back(new_arg);
-                if (arg != new_arg)
+                if (arg != new_arg) {
+                    TRACE("ac", tout << "cached: " << mk_pp(arg, m) << " -> " << mk_pp(new_arg, m) << "\n";);
                     has_new_arg = true;
+                }
                 if (m.fine_grain_proofs() && pr != 0)
                     new_arg_prs.push_back(pr);
             }
@@ -627,6 +631,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
             else {
                 app * new_curr = m.mk_app(f, new_args.size(), new_args.c_ptr());
                 m_ac_cache.insert(curr, new_curr);
+                TRACE("ac", tout << mk_pp(curr, m) << " -> " << mk_pp(new_curr, m) << "\n";);
                 if (m.fine_grain_proofs()) {
                     proof * p = m.mk_congruence(curr, new_curr, new_arg_prs.size(), new_arg_prs.c_ptr());
                     m_ac_pr_cache.insert(curr, p);

src/cmd_context/cmd_context.cpp

@@ -229,6 +229,28 @@ func_decl * func_decls::find(ast_manager & m, unsigned num_args, expr * const *
     return find(num_args, sorts.c_ptr(), range);
 }
 
+unsigned func_decls::get_num_entries() const {
+    if (!more_than_one())
+        return 1;
+
+    func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
+    return fs->size();
+}
+
+func_decl * func_decls::get_entry(unsigned inx) {
+    if (!more_than_one()) {
+        SASSERT(inx == 0);
+        return first();
+    }
+    else {
+        func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
+        auto b = fs->begin();
+        for (unsigned i = 0; i < inx; i++)
+            b++;
+        return *b;
+    }
+}
+
 void macro_decls::finalize(ast_manager& m) {
     for (auto v : *m_decls) m.dec_ref(v.m_body);
     dealloc(m_decls);
@@ -1488,6 +1510,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     }
     display_sat_result(r);
     if (r == l_true) {
+        complete_model();
         validate_model();
     }
     validate_check_sat_result(r);
@@ -1632,6 +1655,65 @@ struct contains_array_op_proc {
     void operator()(quantifier * n) {}
 };
 
+/**
+    \brief Complete the model if necessary.
+*/
+void cmd_context::complete_model() {
+    if (!is_model_available() ||
+        gparams::get_value("model.completion") != "true")
+        return;
+
+    model_ref md;
+    get_check_sat_result()->get_model(md);
+    SASSERT(md.get() != 0);
+    params_ref p;
+    p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
+    p.set_uint("sort_store", true);
+    p.set_bool("completion", true);
+    model_evaluator evaluator(*(md.get()), p);
+    evaluator.set_expand_array_equalities(false);
+
+    scoped_rlimit _rlimit(m().limit(), 0);
+    cancel_eh<reslimit> eh(m().limit());
+    expr_ref r(m());
+    scoped_ctrl_c ctrlc(eh);
+
+    for (auto kd : m_psort_decls) {
+        symbol const & k = kd.m_key;
+        psort_decl * v = kd.m_value;
+        if (v->is_user_decl()) {
+            SASSERT(!v->has_var_params());
+            IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; );
+            ptr_vector<sort> param_sorts(v->get_num_params(), m().mk_bool_sort());
+            sort * srt = v->instantiate(*m_pmanager, param_sorts.size(), param_sorts.c_ptr());
+            if (!md->has_uninterpreted_sort(srt)) {
+                expr * singleton = m().get_some_value(srt);
+                md->register_usort(srt, 1, &singleton);
+            }
+        }
+    }
+
+    for (auto kd : m_func_decls) {
+        symbol const & k = kd.m_key;
+        func_decls & v = kd.m_value;
+        IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; );
+        for (unsigned i = 0; i < v.get_num_entries(); i++) {
+            func_decl * f = v.get_entry(i);
+            if (!md->has_interpretation(f)) {
+                sort * range = f->get_range();
+                expr * some_val = m().get_some_value(range);
+                if (f->get_arity() > 0) {
+                    func_interp * fi = alloc(func_interp, m(), f->get_arity());
+                    fi->set_else(some_val);
+                    md->register_decl(f, fi);
+                }
+                else
+                    md->register_decl(f, some_val);
+            }
+        }
+    }
+}
+
 /**
    \brief Check if the current model satisfies the quantifier free formulas.
 */

src/cmd_context/cmd_context.h

@@ -58,6 +58,8 @@ public:
     func_decl * first() const;
     func_decl * find(unsigned arity, sort * const * domain, sort * range) const;
     func_decl * find(ast_manager & m, unsigned num_args, expr * const * args, sort * range) const;
+    unsigned get_num_entries() const;
+    func_decl * get_entry(unsigned inx);
 };
 
 struct macro_decl {
@@ -360,6 +362,7 @@ public:
     void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
     check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
     check_sat_state cs_state() const;
+    void complete_model();
     void validate_model();
     void display_model(model_ref& mdl);
 

src/cmd_context/pdecl.cpp

@@ -268,6 +268,7 @@ public:
 
 psort_decl::psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n):
     pdecl(id, num_params),
+    m_psort_kind(PSORT_BASE),
     m_name(n),
     m_inst_cache(0) {
 }
@@ -317,6 +318,7 @@ void psort_dt_decl::display(std::ostream & out) const {
 psort_user_decl::psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p) :
     psort_decl(id, num_params, m, n),
     m_def(p) {
+    m_psort_kind = PSORT_USER;
     m.inc_ref(p);
     SASSERT(p == 0 || num_params == p->get_num_params());
 }
@@ -369,6 +371,7 @@ psort_builtin_decl::psort_builtin_decl(unsigned id, pdecl_manager & m, symbol co
     psort_decl(id, PSORT_DECL_VAR_PARAMS, m, n),
     m_fid(fid),
     m_kind(k) {
+    m_psort_kind = PSORT_BUILTIN;
 }
 
 sort * psort_builtin_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {

src/cmd_context/pdecl.h

@@ -86,10 +86,13 @@ typedef ptr_hashtable<psort, psort_hash_proc, psort_eq_proc> psort_table;
 
 #define PSORT_DECL_VAR_PARAMS UINT_MAX
 
+typedef enum { PSORT_BASE = 0, PSORT_USER, PSORT_BUILTIN } psort_decl_kind;
+
 class psort_decl : public pdecl {
 protected:
     friend class pdecl_manager;
     symbol                        m_name;
+    psort_decl_kind               m_psort_kind;
     psort_inst_cache *            m_inst_cache;
     void cache(pdecl_manager & m, sort * const * s, sort * r);
     sort * find(sort * const * s);
@@ -105,6 +108,8 @@ public:
     bool has_var_params() const { return m_num_params == PSORT_DECL_VAR_PARAMS; }
     symbol const & get_name() const { return m_name; }
     virtual void reset_cache(pdecl_manager& m);
+    bool is_user_decl() const { return m_psort_kind == PSORT_USER; }
+    bool is_builtin_decl() const { return m_psort_kind == PSORT_BUILTIN; }
 };
 
 class psort_user_decl : public psort_decl {

src/math/automata/automaton.h

@@ -25,6 +25,7 @@ Revision History:
 #include "util/util.h"
 #include "util/vector.h"
 #include "util/uint_set.h"
+#include "util/trace.h"
 
 template<class T>
 class default_value_manager {
@@ -107,11 +108,10 @@ public:
         m_init = init;
         m_delta.push_back(moves());
         m_delta_inv.push_back(moves());
-        for (unsigned i = 0; i < final.size(); ++i) {
+        for (unsigned f : final) {
-            add_to_final_states(final[i]);
+            add_to_final_states(f);
         }
-        for (unsigned i = 0; i < mvs.size(); ++i) {
+        for (move const& mv : mvs) {
-            move const& mv = mvs[i];
             unsigned n = std::max(mv.src(), mv.dst());
             if (n >= m_delta.size()) {
                 m_delta.resize(n+1, moves());
@@ -280,8 +280,8 @@ public:
         }
         else {
             init = a.num_states();
-            for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
+            for (unsigned st : a.m_final_states) {
-                mvs.push_back(move(m, init, a.m_final_states[i]));
+                mvs.push_back(move(m, init, st));
             }
         }
         return alloc(automaton, m, init, final, mvs);        
@@ -301,6 +301,16 @@ public:
         }
     }
 
+    bool is_sink_state(unsigned s) const {
+        if (is_final_state(s)) return false;
+        moves mvs;
+        get_moves_from(s, mvs);
+        for (move const& m : mvs) {
+            if (s != m.dst()) return false;
+        }
+        return true;
+    }
+
     void add_init_to_final_states() {
         add_to_final_states(init());
     }
@@ -374,12 +384,12 @@ public:
                     else if (1 == in_degree(dst) && (!is_final_state(dst) || is_final_state(src)) && init() != dst) {
                         moves const& mvs = m_delta[dst];
                         moves mvs1;
-                        for (unsigned k = 0; k < mvs.size(); ++k) {
+                        for (move const& mv : mvs) {
-                            mvs1.push_back(move(m, src, mvs[k].dst(), mvs[k].t()));
+                            mvs1.push_back(move(m, src, mv.dst(), mv.t()));
                         }
-                        for (unsigned k = 0; k < mvs1.size(); ++k) {
+                        for (move const& mv : mvs1) {
-                            remove(dst, mvs1[k].dst(), mvs1[k].t());
+                            remove(dst, mv.dst(), mv.t());
-                            add(mvs1[k]);
+                            add(mv);
                         }
                     }
                     //
@@ -392,13 +402,13 @@ public:
                         unsigned_vector src0s;
                         moves const& mvs = m_delta_inv[dst];
                         moves mvs1;
-                        for (unsigned k = 0; k < mvs.size(); ++k) {
+                        for (move const& mv1 : mvs) {
-                            SASSERT(mvs[k].is_epsilon());
+                            SASSERT(mv1.is_epsilon());
-                            mvs1.push_back(move(m, mvs[k].src(), dst1, t));
+                            mvs1.push_back(move(m, mv1.src(), dst1, t));
                         }
-                        for (unsigned k = 0; k < mvs1.size(); ++k) {
+                        for (move const& mv1 : mvs1) {
-                            remove(mvs1[k].src(), dst, 0);
+                            remove(mv1.src(), dst, 0);
-                            add(mvs1[k]);
+                            add(mv1);
                         }
                         remove(dst, dst1, t);    
                         --j;
@@ -410,12 +420,12 @@ public:
                     else if (1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
                         moves const& mvs = m_delta_inv[src];
                         moves mvs1;
-                        for (unsigned k = 0; k < mvs.size(); ++k) {
+                        for (move const& mv : mvs) {
-                            mvs1.push_back(move(m, mvs[k].src(), dst, mvs[k].t()));
+                            mvs1.push_back(move(m, mv.src(), dst, mv.t()));
                         }
-                        for (unsigned k = 0; k < mvs1.size(); ++k) {
+                        for (move const& mv : mvs1) {
-                            remove(mvs1[k].src(), src, mvs1[k].t());
+                            remove(mv.src(), src, mv.t());
-                            add(mvs1[k]);
+                            add(mv);
                         }
                     }
                     else {
@@ -438,6 +448,7 @@ public:
                 break;
             }
         }
+        sinkify_dead_states();
     }
 
     bool is_sequence(unsigned& length) const {
@@ -472,17 +483,16 @@ public:
     bool initial_state_is_source() const { return m_delta_inv[m_init].empty(); }
     bool is_final_state(unsigned s) const { return m_final_set.contains(s); }
     bool is_final_configuration(uint_set s) const {
-		for (uint_set::iterator it = s.begin(), end = s.end(); it != end; ++it) {
+        for (unsigned i : s) {
-			if (is_final_state(*it))
+            if (is_final_state(i))
                 return true;
         }
         return false; 
     }
     bool is_epsilon_free() const {
-        for (unsigned i = 0; i < m_delta.size(); ++i) {
+        for (moves const& mvs : m_delta) {
-            moves const& mvs = m_delta[i];
+            for (move const & m : mvs) {
-            for (unsigned j = 0; j < mvs.size(); ++j) {
+                if (!m.t()) return false;
-                if (!mvs[j].t()) return false;
             }
         }
         return true;
@@ -490,8 +500,8 @@ public:
 
     bool all_epsilon_in(unsigned s) {
         moves const& mvs = m_delta_inv[s];
-        for (unsigned j = 0; j < mvs.size(); ++j) {
+        for (move const& m : mvs) {
-            if (mvs[j].t()) return false;
+            if (m.t()) return false;
         }
         return true;
     }
@@ -504,15 +514,15 @@ public:
     bool is_loop_state(unsigned s) const {
         moves mvs;
         get_moves_from(s, mvs);
-        for (unsigned i = 0; i < mvs.size(); ++i) {
+        for (move const& m : mvs) {
-            if (s == mvs[i].dst()) return true;
+            if (s == m.dst()) return true;
         }
         return false;
     }
 
     unsigned move_count() const {
         unsigned result = 0;
-        for (unsigned i = 0; i < m_delta.size(); result += m_delta[i].size(), ++i) {}
+        for (moves const& mvs : m_delta) result += mvs.size();
         return result;
     }
     void get_epsilon_closure(unsigned state, unsigned_vector& states) {
@@ -525,9 +535,9 @@ public:
         get_moves(state, m_delta, mvs, epsilon_closure);
     }
     void get_moves_from_states(uint_set states, moves& mvs, bool epsilon_closure = true) const {
-		for (uint_set::iterator it = states.begin(), end = states.end(); it != end; ++it) {
+        for (unsigned i : states) {
             moves curr;
-			get_moves(*it, m_delta, curr, epsilon_closure);
+            get_moves(i, m_delta, curr, epsilon_closure);
             mvs.append(curr);
         }
     }
@@ -543,8 +553,7 @@ public:
         out << "\n";
         for (unsigned i = 0; i < m_delta.size(); ++i) {
             moves const& mvs = m_delta[i];
-            for (unsigned j = 0; j < mvs.size(); ++j) {
+            for (move const& mv : mvs) {
-                move const& mv = mvs[j];
                 out << i << " -> " << mv.dst() << " ";
                 if (mv.t()) {
                     out << "if "; 
@@ -557,6 +566,40 @@ public:
     }
 private:
 
+    void sinkify_dead_states() {
+        uint_set dead_states;
+        for (unsigned i = 0; i < m_delta.size(); ++i) {
+            if (!m_final_states.contains(i)) {
+                dead_states.insert(i);
+            }
+        }
+        bool change = true;
+        unsigned_vector to_remove;
+        while (change) {
+            change = false;
+            to_remove.reset();
+            for (unsigned s : dead_states) {
+                moves const& mvs = m_delta[s];
+                for (move const& mv : mvs) {
+                    if (!dead_states.contains(mv.dst())) {
+                        to_remove.push_back(s);
+                        break;
+                    }
+                }
+            }
+            change = !to_remove.empty();
+            for (unsigned s : to_remove) {
+                dead_states.remove(s);
+            }
+            to_remove.reset();
+        }
+        TRACE("seq", tout << "remove: " << dead_states << "\n";);
+        for (unsigned s : dead_states) {
+            CTRACE("seq", !m_delta[s].empty(), tout << "live state " << s << "\n";); 
+            m_delta[s].reset();
+        }
+    }
+
     void remove_dead_states() {
         unsigned_vector remap;
         for (unsigned i = 0; i < m_delta.size(); ++i) {
@@ -662,8 +705,8 @@ private:
     }
 
     static void append_final(unsigned offset, automaton const& a, unsigned_vector& final) {
-        for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
+        for (unsigned s : a.m_final_states) {
-            final.push_back(a.m_final_states[i]+offset);
+            final.push_back(s+offset);
         }
     }
  

src/math/automata/symbolic_automata.h

@@ -136,7 +136,8 @@ private:
             
             //false case
             curr_bv.push_back(false);
-            ref_t new_pred_neg(m_ba.mk_and(curr_pred, m_ba.mk_not(constraints[i])), m);
+            ref_t neg(m_ba.mk_not(constraints[i]), m);
+            ref_t new_pred_neg(m_ba.mk_and(curr_pred, neg), m);
             generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_neg);
             curr_bv.pop_back();
         }

src/math/automata/symbolic_automata_def.h

@@ -297,12 +297,17 @@ symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_accepta
     unsigned_vector new_final_states;                // new final states
     unsigned p_state_id = 0;                         // next state identifier
 
-    // adds non-final states of a to final if flipping and and final otherwise
+    TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";);    
+    // adds non-final states of a to final if flipping and final otherwise
+    unsigned_vector init_states;
+    a.get_epsilon_closure(a.init(), init_states);    
+    for (unsigned s : init_states) {
+        set.insert(s);
+    }
     if (a.is_final_configuration(set) != flip_acceptance) {
         new_final_states.push_back(p_state_id);
     }
     
-    set.insert(a.init());                         // Initial state as aset
     s2id.insert(set, p_state_id++);               // the index to the initial state is 0
     id2s.push_back(set);
     
@@ -342,6 +347,7 @@ symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_accepta
             
             bool is_new = !s2id.contains(set);
             if (is_new) {
+                TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";);    
                 if (a.is_final_configuration(set) != flip_acceptance) {
                     new_final_states.push_back(p_state_id);
                 }

src/model/model_params.pyg

@@ -4,5 +4,6 @@ def_module_params('model',
                           ('v1', BOOL, False, 'use Z3 version 1.x pretty printer'),
                           ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
                           ('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
+                          ('completion', BOOL, False, 'enable/disable model completion'),
                           ))
 

src/qe/nlqsat.cpp

@@ -444,16 +444,12 @@ namespace qe {
             div_rewriter_cfg(nlqsat& s): m(s.m), a(s.m), m_zero(a.mk_real(0), m) {}
             ~div_rewriter_cfg() {}
             br_status reduce_app(func_decl* f, unsigned sz, expr* const* args, expr_ref& result, proof_ref& pr) {
-                if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && !a.is_numeral(args[1])) {                    
+                rational r;
+                if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && (!a.is_numeral(args[1], r) || r.is_zero())) {                    
                     result = m.mk_fresh_const("div", a.mk_real());
                     m_divs.push_back(div(m, args[0], args[1], to_app(result)));
                     return BR_DONE;
                 }
-                if (is_decl_of(f, a.get_family_id(), OP_DIV_0) && sz == 1 && !a.is_numeral(args[0])) {                    
-                    result = m.mk_fresh_const("div", a.mk_real());
-                    m_divs.push_back(div(m, args[0], m_zero, to_app(result)));
-                    return BR_DONE;
-                }
                 return BR_FAILED;
             }
             vector<div> const& divs() const { return m_divs; }
@@ -507,10 +503,6 @@ namespace qe {
                     m_has_divs = true;
                     return;
                 }
-                if (a.is_div0(n) && s.m_mode == qsat_t) {
-                    m_has_divs = true;
-                    return;
-                }
                 TRACE("qe", tout << "not NRA: " << mk_pp(n, s.m) << "\n";);
                 throw tactic_exception("not NRA");
             }

src/sat/sat_solver/inc_sat_solver.cpp

@@ -388,6 +388,9 @@ private:
         m_subgoals.reset();
         init_preprocess();
         SASSERT(g->models_enabled());
+        if (g->proofs_enabled()) {
+            throw default_exception("generation of proof objects is not supported in this mode");
+        }
         SASSERT(!g->proofs_enabled());
         TRACE("sat", g->display(tout););
         try {

src/smt/asserted_formulas.cpp

@@ -387,8 +387,12 @@ void asserted_formulas::find_macros_core() {
     expr_ref_vector  new_exprs(m);
     proof_ref_vector new_prs(m);
     unsigned sz = m_asserted_formulas.size();
-    m_macro_finder->operator()(sz - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead, 
+    expr_dependency_ref_vector new_deps(m);
-                               m_asserted_formula_prs.c_ptr() + m_asserted_qhead, new_exprs, new_prs);
+    m_macro_finder->operator()(sz - m_asserted_qhead,
+                               m_asserted_formulas.c_ptr() + m_asserted_qhead,
+                               m_asserted_formula_prs.c_ptr() + m_asserted_qhead,
+                               0, // 0 == No dependency tracking
+                               new_exprs, new_prs, new_deps);
     swap_asserted_formulas(new_exprs, new_prs);
     reduce_and_solve();
 }
@@ -411,10 +415,12 @@ void asserted_formulas::apply_quasi_macros() {
     expr_ref_vector  new_exprs(m);
     proof_ref_vector new_prs(m);
     quasi_macros proc(m, m_macro_manager, m_simplifier);
+    expr_dependency_ref_vector new_deps(m);
     while (proc(m_asserted_formulas.size() - m_asserted_qhead,
                 m_asserted_formulas.c_ptr() + m_asserted_qhead,
                 m_asserted_formula_prs.c_ptr() + m_asserted_qhead,
-                new_exprs, new_prs)) {
+                0, // 0 == No dependency tracking
+                new_exprs, new_prs, new_deps)) {
         swap_asserted_formulas(new_exprs, new_prs);
         new_exprs.reset();
         new_prs.reset();
@@ -639,7 +645,7 @@ void asserted_formulas::propagate_values() {
                 new_prs2.push_back(pr);
         }
     }
-    TRACE("propagate_values", tout << "found: " << found << "\n";);
+    TRACE("propagate_values", tout << "found: " << found << "\n" << new_exprs2 << "\n";);
     // If C is not empty, then reduce R using the updated simplifier cache with entries
     // x -> n for each constraint 'x = n' in C.
     if (found) {
@@ -650,6 +656,7 @@ void asserted_formulas::propagate_values() {
             expr_ref new_n(m);
             proof_ref new_pr(m);
             m_simplifier(n, new_n, new_pr);
+            TRACE("propagate_values", tout << mk_pp(n, m) << " -> " << new_n << "\n";);
             if (n == new_n.get()) {
                 push_assertion(n, pr, new_exprs1, new_prs1);
             }

src/smt/asserted_formulas.h

@@ -141,9 +141,7 @@ public:
     func_decl * get_macro_func_decl(unsigned i) const { return m_macro_manager.get_macro_func_decl(i); }
     func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_macro_manager.get_macro_interpretation(i, interp); }
     quantifier * get_macro_quantifier(func_decl * f) const { return m_macro_manager.get_macro_quantifier(f); }
-    // auxiliary function used to create a logic context based on a model.
+    void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_macro_manager.insert(f, m, pr, dep); }
-    void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_macro_manager.insert(f, m, pr); }
-
 };
 
 #endif /* ASSERTED_FORMULAS_H_ */

src/smt/params/preprocessor_params.cpp

@@ -22,6 +22,8 @@ Revision History:
 void preprocessor_params::updt_local_params(params_ref const & _p) {
     smt_params_helper p(_p);
     m_macro_finder            = p.macro_finder();
+    m_quasi_macros            = p.quasi_macros();
+    m_restricted_quasi_macros = p.restricted_quasi_macros();
     m_pull_nested_quantifiers = p.pull_nested_quantifiers();
     m_refine_inj_axiom        = p.refine_inj_axioms();
 }

src/smt/params/smt_params_helper.pyg

@@ -7,6 +7,8 @@ def_module_params(module_name='smt',
                           ('random_seed', UINT, 0, 'random seed for the smt solver'),
                           ('relevancy', UINT, 2, 'relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant'),
                           ('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
+                          ('quasi_macros', BOOL, False, 'try to find universally quantified formulas that are quasi-macros'),
+                          ('restricted_quasi_macros', BOOL, False, 'try to find universally quantified formulas that are restricted quasi-macros'),
                           ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
                           ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
                           ('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),

src/smt/smt_context.h

@@ -1568,7 +1568,7 @@ namespace smt {
         func_decl * get_macro_func_decl(unsigned i) const { return m_asserted_formulas.get_macro_func_decl(i); }
         func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_asserted_formulas.get_macro_interpretation(i, interp); }
         quantifier * get_macro_quantifier(func_decl * f) const { return m_asserted_formulas.get_macro_quantifier(f); }
-        void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_asserted_formulas.insert_macro(f, m, pr); }
+        void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); }
     };
 
 };

src/smt/smt_quantifier.cpp

@@ -492,6 +492,7 @@ namespace smt {
 
         virtual void assign_eh(quantifier * q) {
             m_active = true;
+            ast_manager& m = m_context->get_manager();
             if (!m_fparams->m_ematching) {
                 return;
             }
@@ -514,7 +515,11 @@ namespace smt {
                 app * mp = to_app(q->get_pattern(i));
                 SASSERT(m_context->get_manager().is_pattern(mp));
                 bool unary = (mp->get_num_args() == 1);
-                if (!unary && j >= num_eager_multi_patterns) {
+                if (m.is_rec_fun_def(q) && i > 0) {
+                    // add only the first pattern
+                    TRACE("quantifier", tout << "skip recursive function body " << mk_ismt2_pp(mp, m) << "\n";);
+                }
+                else if (!unary && j >= num_eager_multi_patterns) {
                     TRACE("quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n"
                           << "j: " << j << " unary: " << unary << " m_params.m_qi_max_eager_multipatterns: " << m_fparams->m_qi_max_eager_multipatterns
                           << " num_eager_multi_patterns: " << num_eager_multi_patterns << "\n";);

src/smt/theory_arith_core.h

@@ -395,7 +395,8 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_div(app * n) {
-        if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
+        rational r;
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
@@ -406,7 +407,8 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_idiv(app * n) {
-        found_underspecified_op(n);
+        rational r;
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
         app * mod         = m_util.mk_mod(n->get_arg(0), n->get_arg(1));
@@ -419,7 +421,8 @@ namespace smt {
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_mod(app * n) {
         TRACE("arith_mod", tout << "internalizing...\n" << mk_pp(n, get_manager()) << "\n";);
-        if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
+        rational r;
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
         if (!ctx.relevancy())
@@ -429,7 +432,8 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_rem(app * n) {
-        if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
+        rational r;
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s  = mk_binary_op(n);
         context & ctx = get_context();
         if (!ctx.relevancy()) {
@@ -734,11 +738,6 @@ namespace smt {
             return internalize_div(n);
         else if (m_util.is_idiv(n))
             return internalize_idiv(n);
-        else if (is_app_of(n, get_id(), OP_IDIV_0) || is_app_of(n, get_id(), OP_DIV_0)) {
-            ctx.internalize(n->get_arg(0), false);
-            enode * e = mk_enode(n);
-            return mk_var(e);
-        }
         else if (m_util.is_mod(n)) 
             return internalize_mod(n);
         else if (m_util.is_rem(n)) 

src/smt/theory_lra.cpp

@@ -292,9 +292,6 @@ namespace smt {
         }
 
         void found_not_handled(expr* n) {
-            if (a.is_div0(n)) {
-                return;
-            }
             m_not_handled = n;
             if (is_app(n) && is_underspecified(to_app(n))) {
                 m_underspecified.push_back(to_app(n));
@@ -379,7 +376,12 @@ namespace smt {
                 }
                 else if (is_app(n) && a.get_family_id() == to_app(n)->get_family_id()) {
                     app* t = to_app(n);
+                    if (a.is_div(n, n1, n2) && is_numeral(n2, r)) {
+                        // skip
+                    }
+                    else {
                         found_not_handled(n);
+                    }
                     internalize_args(t);
                     mk_enode(t);
                     theory_var v = mk_var(n);

src/smt/theory_seq.cpp

@@ -19,11 +19,12 @@ Revision History:
 --*/
 
 #include <typeinfo>
+#include "ast/ast_pp.h"
+#include "ast/ast_trail.h"
 #include "smt/proto_model/value_factory.h"
 #include "smt/smt_context.h"
 #include "smt/smt_model_generator.h"
 #include "smt/theory_seq.h"
-#include "ast/ast_trail.h"
 #include "smt/theory_arith.h"
 #include "smt/smt_kernel.h"
 
@@ -150,9 +151,8 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) {
 }
 
 void theory_seq::solution_map::display(std::ostream& out) const {
-    eqdep_map_t::iterator it = m_map.begin(), end = m_map.end();
+    for (auto const& kv : m_map) {
-    for (; it != end; ++it) {
+        out << mk_pp(kv.m_key, m) << " |-> " << mk_pp(kv.m_value.first, m) << "\n";
-        out << mk_pp(it->m_key, m) << " |-> " << mk_pp(it->m_value.first, m) << "\n";
     }
 }
 
@@ -186,9 +186,8 @@ void theory_seq::exclusion_table::pop_scope(unsigned num_scopes) {
 }
 
 void theory_seq::exclusion_table::display(std::ostream& out) const {
-    table_t::iterator it = m_table.begin(), end = m_table.end();
+    for (auto const& kv : m_table) {
-    for (; it != end; ++it) {
+        out << mk_pp(kv.first, m) << " != " << mk_pp(kv.second, m) << "\n";
-        out << mk_pp(it->first, m) << " != " << mk_pp(it->second, m) << "\n";
     }
 }
 
@@ -213,6 +212,7 @@ theory_seq::theory_seq(ast_manager& m):
     m_trail_stack(*this),
     m_ls(m), m_rs(m),
     m_lhs(m), m_rhs(m),
+    m_res(m),
     m_atoms_qhead(0),
     m_new_solution(false),
     m_new_propagation(false),
@@ -936,18 +936,14 @@ bool theory_seq::check_length_coherence0(expr* e) {
 
 bool theory_seq::check_length_coherence() {
 
-    obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
 #if 1
-    for (; it != end; ++it) {
+    for (expr* e : m_length) {
-        expr* e = *it;
         if (check_length_coherence0(e)) {
             return true;
         }
     }
-    it = m_length.begin();
 #endif
-    for (; it != end; ++it) {
+    for (expr* e : m_length) {
-        expr* e = *it;
         if (check_length_coherence(e)) {
             return true;
         }
@@ -956,10 +952,9 @@ bool theory_seq::check_length_coherence() {
 }
 
 bool theory_seq::fixed_length() {
-    obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
     bool found = false;
-    for (; it != end; ++it) {
+    for (expr* e : m_length) {
-        if (fixed_length(*it)) {
+        if (fixed_length(e)) {
             found = true;
         }
     }
@@ -2501,12 +2496,11 @@ void theory_seq::display(std::ostream & out) const {
     }
     if (!m_re2aut.empty()) {
         out << "Regex\n";
-        obj_map<expr, eautomaton*>::iterator it = m_re2aut.begin(), end = m_re2aut.end();
+        for (auto const& kv : m_re2aut) {
-        for (; it != end; ++it) {
+            out << mk_pp(kv.m_key, m) << "\n";
-            out << mk_pp(it->m_key, m) << "\n";
             display_expr disp(m);
-            if (it->m_value) {
+            if (kv.m_value) {
-                it->m_value->display(out, disp);
+                kv.m_value->display(out, disp);
             }
         }
     }
@@ -2520,9 +2514,7 @@ void theory_seq::display(std::ostream & out) const {
     }
 
     if (!m_length.empty()) {
-        obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
+        for (expr* e : m_length) {
-        for (; it != end; ++it) {
-            expr* e = *it;
             rational lo(-1), hi(-1);
             lower_bound(e, lo);
             upper_bound(e, hi);
@@ -2635,6 +2627,12 @@ void theory_seq::collect_statistics(::statistics & st) const {
     st.update("seq int.to.str", m_stats.m_int_string);
 }
 
+void theory_seq::init_search_eh() {
+    m_re2aut.reset();
+    m_res.reset();
+    m_automata.reset();
+}
+
 void theory_seq::init_model(expr_ref_vector const& es) {
     expr_ref new_s(m);
     for (expr* e : es) {
@@ -3391,15 +3389,21 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
         return;
     }
 
-    eautomaton* a = get_automaton(e2);
+    expr_ref e3(e2, m);
+    context& ctx = get_context();
+    literal lit = ctx.get_literal(n);
+    if (!is_true) {
+        e3 = m_util.re.mk_complement(e2);
+        lit.neg();
+    }
+    eautomaton* a = get_automaton(e3);
     if (!a) return;
 
-    context& ctx = get_context();
 
     expr_ref len(m_util.str.mk_length(e1), m);
     for (unsigned i = 0; i < a->num_states(); ++i) {
-        literal acc = mk_accept(e1, len, e2, i);
+        literal acc = mk_accept(e1, len, e3, i);
-        literal rej = mk_reject(e1, len, e2, i);
+        literal rej = mk_reject(e1, len, e3, i);
         add_axiom(a->is_final_state(i)?acc:~acc);
         add_axiom(a->is_final_state(i)?~rej:rej);
     }
@@ -3408,20 +3412,11 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
     unsigned_vector states;
     a->get_epsilon_closure(a->init(), states);
     literal_vector lits;
-    literal lit = ctx.get_literal(n);
-    if (is_true) {
     lits.push_back(~lit);
-    }
+    
     for (unsigned i = 0; i < states.size(); ++i) {
-        if (is_true) {
+        lits.push_back(mk_accept(e1, zero, e3, states[i]));
-            lits.push_back(mk_accept(e1, zero, e2, states[i]));
     }
-        else {
-            literal nlit = ~lit;
-            propagate_lit(0, 1, &nlit, mk_reject(e1, zero, e2, states[i]));
-        }
-    }
-    if (is_true) {
     if (lits.size() == 2) {
         propagate_lit(0, 1, &lit, lits[1]);
     }
@@ -3430,7 +3425,6 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
         ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
     }
 }
-}
 
 
 expr_ref theory_seq::mk_sub(expr* a, expr* b) {
@@ -4173,10 +4167,8 @@ eautomaton* theory_seq::get_automaton(expr* re) {
         TRACE("seq", result->display(tout, disp););
     }
     m_automata.push_back(result);
-    m_trail_stack.push(push_back_vector<theory_seq, scoped_ptr_vector<eautomaton> >(m_automata));
-
     m_re2aut.insert(re, result);
-    m_trail_stack.push(insert_obj_map<theory_seq, expr, eautomaton*>(m_re2aut, re));
+    m_res.push_back(re);
     return result;
 }
 
@@ -4257,6 +4249,10 @@ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) {
     if (m_util.str.is_length(idx)) return;
     SASSERT(m_autil.is_numeral(idx));
     SASSERT(get_context().get_assignment(lit) == l_true);
+    if (aut->is_sink_state(src)) {
+        propagate_lit(0, 1, &lit, false_literal);
+        return;
+    }
     bool is_final = aut->is_final_state(src);
     if (is_final == is_acc) {
         propagate_lit(0, 1, &lit, mk_literal(m_autil.mk_ge(m_util.str.mk_length(s), idx)));

src/smt/theory_seq.h

@@ -328,6 +328,7 @@ namespace smt {
         // maintain automata with regular expressions.
         scoped_ptr_vector<eautomaton>  m_automata;
         obj_map<expr, eautomaton*>     m_re2aut;
+        expr_ref_vector                m_res;
 
         // queue of asserted atoms
         ptr_vector<expr>               m_atoms;
@@ -361,6 +362,7 @@ namespace smt {
         virtual void collect_statistics(::statistics & st) const;
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);
         virtual void init_model(model_generator & mg);
+        virtual void init_search_eh();
 
         void init_model(expr_ref_vector const& es);
         // final check 

src/tactic/arith/purify_arith_tactic.cpp

@@ -297,11 +297,11 @@ struct purify_arith_proc {
             push_cnstr(OR(EQ(y, mk_real_zero()),
                           EQ(u().mk_mul(y, k), x)));
             push_cnstr_pr(result_pr);
-
+            rational r;
-            if (complete()) {
+            if (complete() && (!u().is_numeral(y, r) || r.is_zero())) {
                 // y != 0 \/ k = div-0(x)
                 push_cnstr(OR(NOT(EQ(y, mk_real_zero())),
-                              EQ(k, u().mk_div0(x))));
+                              EQ(k, u().mk_div(x, mk_real_zero()))));
                 push_cnstr_pr(result_pr);
             }
         }
@@ -348,11 +348,12 @@ struct purify_arith_proc {
             push_cnstr(OR(u().mk_ge(y, zero), u().mk_lt(k2, u().mk_mul(u().mk_numeral(rational(-1), true), y))));
             push_cnstr_pr(mod_pr);
 
-            if (complete()) {
+            rational r;
-                push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv0(x))));
+            if (complete() && (!u().is_numeral(y, r) || r.is_zero())) {
+                push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv(x, zero))));
                 push_cnstr_pr(result_pr);
 
-                push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod0(x))));
+                push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod(x, zero))));
                 push_cnstr_pr(mod_pr);
             }
         }
@@ -414,7 +415,7 @@ struct purify_arith_proc {
                 // (^ x 0) --> k  |  x != 0 implies k = 1,   x = 0 implies k = 0^0 
                 push_cnstr(OR(EQ(x, zero), EQ(k, one)));
                 push_cnstr_pr(result_pr);
-                push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real())));
+                push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, u().mk_power(zero, zero))));
                 push_cnstr_pr(result_pr);
             }
             else if (!is_int) {

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -93,7 +93,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
         return mk_qffpbv_tactic(m, p);
     else if (logic=="HORN")
         return mk_horn_tactic(m, p);
-    else if (logic == "QF_FD" || logic == "SAT")
+    else if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled())
         return mk_solver2tactic(mk_fd_solver(m, p));
     //else if (logic=="QF_UFNRA")
     //    return mk_qfufnra_tactic(m, p);
@@ -102,7 +102,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
 }
 
 static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
-    if (logic == "QF_FD" || logic == "SAT") 
+    if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled())
         return mk_fd_solver(m, p);
     return 0;
 }

src/tactic/ufbv/macro_finder_tactic.cpp

@@ -49,9 +49,9 @@ class macro_finder_tactic : public tactic {
             SASSERT(g->is_well_sorted());
             mc = 0; pc = 0; core = 0;
             tactic_report report("macro-finder", *g);
-            fail_if_unsat_core_generation("macro-finder", g);
 
             bool produce_proofs = g->proofs_enabled();
+            bool unsat_core_enabled = g->unsat_core_enabled();
 
             simplifier simp(m_manager);
             basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager);
@@ -69,17 +69,21 @@ class macro_finder_tactic : public tactic {
 
             expr_ref_vector forms(m_manager), new_forms(m_manager);
             proof_ref_vector proofs(m_manager), new_proofs(m_manager);
+            expr_dependency_ref_vector deps(m_manager), new_deps(m_manager);
             unsigned size = g->size();
             for (unsigned idx = 0; idx < size; idx++) {
                 forms.push_back(g->form(idx));
                 proofs.push_back(g->pr(idx));
+                deps.push_back(g->dep(idx));
             }
 
-            mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);
+            mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), deps.c_ptr(), new_forms, new_proofs, new_deps);
 
             g->reset();
             for (unsigned i = 0; i < new_forms.size(); i++)
-                g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
+                g->assert_expr(new_forms.get(i),
+                               produce_proofs ? new_proofs.get(i) : 0,
+                               unsat_core_enabled ? new_deps.get(i) : 0);
 
             extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager());
             unsigned num = mm.get_num_macros();

src/tactic/ufbv/quasi_macros_tactic.cpp

@@ -47,9 +47,9 @@ class quasi_macros_tactic : public tactic {
             SASSERT(g->is_well_sorted());
             mc = 0; pc = 0; core = 0;
             tactic_report report("quasi-macros", *g);
-            fail_if_unsat_core_generation("quasi-macros", g);
 
             bool produce_proofs = g->proofs_enabled();
+            bool produce_unsat_cores = g->unsat_core_enabled();
 
             simplifier simp(m_manager);
             basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager);
@@ -68,11 +68,13 @@ class quasi_macros_tactic : public tactic {
 
             expr_ref_vector forms(m_manager), new_forms(m_manager);
             proof_ref_vector proofs(m_manager), new_proofs(m_manager);
+            expr_dependency_ref_vector deps(m_manager), new_deps(m_manager);
 
             unsigned size = g->size();
             for (unsigned i = 0; i < size; i++) {
                 forms.push_back(g->form(i));
                 proofs.push_back(g->pr(i));
+                deps.push_back(g->dep(i));
             }
 
             while (more) { // CMW: use repeat(...) ?
@@ -81,14 +83,18 @@ class quasi_macros_tactic : public tactic {
 
                 new_forms.reset();
                 new_proofs.reset();
-                more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);            
+                new_deps.reset();
+                more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), deps.c_ptr(), new_forms, new_proofs, new_deps);
                 forms.swap(new_forms);
                 proofs.swap(new_proofs);
+                deps.swap(new_deps);
             }
 
             g->reset();
             for (unsigned i = 0; i < new_forms.size(); i++)
-                g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
+                g->assert_expr(forms.get(i),
+                               produce_proofs ? proofs.get(i) : 0,
+                               produce_unsat_cores ? deps.get(i) : 0);
 
             extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager());
             unsigned num = mm.get_num_macros();