model refactor (#4723)

* refactor model fixing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* missing cond macro

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add macros dependency

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* deps and debug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add dependency to normal forms

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* build issues

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* compile

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix leal regression

* complete model fixer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fold back private functionality to model_finder

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* avoid duplicate fixed callbacks

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

scripts/mk_project.py

@@ -32,7 +32,7 @@ def init_project_def():
     add_lib('rewriter', ['ast', 'polynomial', 'automata', 'params'], 'ast/rewriter')
     add_lib('macros', ['rewriter'], 'ast/macros')
     add_lib('normal_forms', ['rewriter'], 'ast/normal_forms')
-    add_lib('model', ['rewriter'])
+    add_lib('model', ['rewriter', 'macros'])
     add_lib('tactic', ['ast', 'model'])
     add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution')
     add_lib('parser_util', ['ast'], 'parsers/util')
@@ -49,7 +49,7 @@ def init_project_def():
     add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core')
     add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
 
-    add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa'], 'sat/smt')
+    add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'normal_forms'], 'sat/smt')
     add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic')
     add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')
     add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')

src/CMakeLists.txt

@@ -47,6 +47,7 @@ add_subdirectory(ast)
 add_subdirectory(params)
 add_subdirectory(ast/rewriter)
 add_subdirectory(ast/normal_forms)
+add_subdirectory(ast/macros)
 add_subdirectory(model)
 add_subdirectory(tactic)
 add_subdirectory(ast/substitution)
@@ -64,7 +65,6 @@ add_subdirectory(solver)
 add_subdirectory(cmd_context)
 add_subdirectory(cmd_context/extra_cmds)
 add_subdirectory(parsers/smt2)
-add_subdirectory(ast/macros)
 add_subdirectory(ast/pattern)
 add_subdirectory(ast/rewriter/bit_blaster)
 add_subdirectory(smt/params)

src/ast/euf/euf_egraph.cpp

@@ -107,6 +107,11 @@ namespace euf {
         enode* n = enode::mk(m_region, f, num_args, args);
         m_nodes.push_back(n);
         m_exprs.push_back(f);
+        if (is_app(f) && num_args > 0) {
+           unsigned id = to_app(f)->get_decl()->get_decl_id();
+           m_decl2enodes.reserve(id+1);
+           m_decl2enodes[id].push_back(n);
+        }
         m_expr2enode.setx(f->get_id(), n, nullptr);
         push_node(n);
         for (unsigned i = 0; i < num_args; ++i)
@@ -114,9 +119,15 @@ namespace euf {
         return n;
     }
 
+    enode_vector const& egraph::enodes_of(func_decl* f) {
+        unsigned id = f->get_decl_id();
+        if (id < m_decl2enodes.size())
+            return m_decl2enodes[id];
+        return m_empty_enodes;
+    }
+
     enode_bool_pair egraph::insert_table(enode* p) {
         auto rc = m_table.insert(p);
-        enode* p_other = rc.first;
         p->m_cg = rc.first;
         return rc;
     }
@@ -338,6 +349,8 @@ namespace euf {
             
             m_expr2enode[e->get_id()] = nullptr;
             n->~enode();
+            if (is_app(e) && n->num_args() > 0)
+               m_decl2enodes[to_app(e)->get_decl()->get_decl_id()].pop_back();
             m_nodes.pop_back();
             m_exprs.pop_back();
         };

src/ast/euf/euf_egraph.h

@@ -141,7 +141,7 @@ namespace euf {
                 tag(tag_t::is_value_assignment), r1(n), n1(nullptr), qhead(0) {}
         };
         ast_manager&           m;
-        svector<to_merge>     m_to_merge;
+        svector<to_merge>      m_to_merge;
         etable                 m_table;
         region                 m_region;
         svector<update_record> m_updates;
@@ -150,6 +150,8 @@ namespace euf {
         enode*                 m_tmp_eq { nullptr };
         enode_vector           m_nodes;
         expr_ref_vector        m_exprs;
+        vector<enode_vector>   m_decl2enodes;
+        enode_vector           m_empty_enodes;
         unsigned               m_num_scopes { 0 };
         bool                   m_inconsistent { false };
         enode                  *m_n1 { nullptr };
@@ -214,6 +216,7 @@ namespace euf {
         ~egraph();
         enode* find(expr* f) { return m_expr2enode.get(f->get_id(), nullptr); }
         enode* mk(expr* f, unsigned n, enode *const* args);
+        enode_vector const& enodes_of(func_decl* f);
         void push() { ++m_num_scopes; }
         void pop(unsigned num_scopes);
 

src/ast/euf/euf_etable.cpp

@@ -22,7 +22,7 @@ namespace euf {
 
     // one table per func_decl implementation
     unsigned etable::cg_hash::operator()(enode * n) const {
-        SASSERT(decl(n)->is_flat_associative() || n->num_args() >= 3);
+        SASSERT(n->get_decl()->is_flat_associative() || n->num_args() >= 3);
         unsigned a, b, c;
         a = b = 0x9e3779b9;
         c = 11;    
@@ -50,7 +50,7 @@ namespace euf {
     }
 
     bool etable::cg_eq::operator()(enode * n1, enode * n2) const {
-        SASSERT(decl(n1) == decl(n2));
+        SASSERT(n1->get_decl() == n2->get_decl());
         unsigned num = n1->num_args();
         if (num != n2->num_args()) {
             return false;
@@ -96,7 +96,7 @@ namespace euf {
     }
 
     unsigned etable::set_table_id(enode * n) {
-        func_decl * f = decl(n);
+        func_decl * f = n->get_decl();
         unsigned tid;
         decl_info d(f, n->num_args());
         if (!m_func_decl2id.find(d, tid)) {

src/ast/euf/euf_etable.h

@@ -24,8 +24,6 @@ namespace euf {
     
     // one table per function symbol
 
-    static func_decl* decl(enode* n) { return n->get_decl(); }
-
 
     /**
        \brief Congruence table.
@@ -45,7 +43,7 @@ namespace euf {
             bool operator()(enode * n1, enode * n2) const {
                 SASSERT(n1->num_args() == 1);
                 SASSERT(n2->num_args() == 1);
-                SASSERT(decl(n1) == decl(n2));
+                SASSERT(n1->get_decl() == n2->get_decl());
                 return get_root(n1, 0) == get_root(n2, 0);
             }
         };
@@ -63,7 +61,7 @@ namespace euf {
             bool operator()(enode * n1, enode * n2) const {
                 SASSERT(n1->num_args() == 2);
                 SASSERT(n2->num_args() == 2);
-                SASSERT(decl(n1) == decl(n2));
+                SASSERT(n1->get_decl() == n2->get_decl());
                 return
                     get_root(n1, 0) == get_root(n2, 0) &&
                     get_root(n1, 1) == get_root(n2, 1);
@@ -90,7 +88,7 @@ namespace euf {
                 SASSERT(n1->num_args() == 2);
                 SASSERT(n2->num_args() == 2);
 
-                SASSERT(decl(n1) == decl(n2));
+                SASSERT(n1->get_decl() == n2->get_decl());
                 enode* c1_1 = get_root(n1, 0);  
                 enode* c1_2 = get_root(n1, 1); 
                 enode* c2_1 = get_root(n2, 0); 

src/ast/fpa/bv2fpa_converter.h

@@ -70,21 +70,4 @@ public:
     array_model convert_array_func_interp(model_core * mc, func_decl * f, func_decl * bv_f);
 };
 
-template <typename T>
-class fpa2bv_conversion_trail_elem : public trail<T> {
-    ast_manager& m;
-    obj_map<expr, expr*>& m_map;
-    expr_ref key;
-public:
-    fpa2bv_conversion_trail_elem(ast_manager& m, obj_map<expr, expr*>& map, expr* e) :
-        m(m), m_map(map), key(e, m) { }
-    ~fpa2bv_conversion_trail_elem() override { }
-    void undo(T& s) override {
-        expr* val = m_map.find(key);
-        m_map.remove(key);
-        m.dec_ref(key);
-        m.dec_ref(val);
-        key = nullptr;
-    }
-};
 

src/ast/fpa/fpa2bv_converter.cpp

@@ -32,11 +32,11 @@ Notes:
 fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
     m(m),
     m_simp(m),
-    m_util(m),
     m_bv_util(m),
     m_arith_util(m),
     m_dt_util(m),
     m_seq_util(m),
+    m_util(m),
     m_mpf_manager(m_util.fm()),
     m_mpz_manager(m_mpf_manager.mpz_manager()),
     m_hi_fp_unspecified(true),

src/ast/macros/CMakeLists.txt

@@ -2,6 +2,7 @@ z3_add_component(macros
   SOURCES
     macro_finder.cpp
     macro_manager.cpp
+    quantifier_macro_info.cpp
     macro_util.cpp
     quasi_macros.cpp
   COMPONENT_DEPENDENCIES

src/ast/macros/cond_macro.h

@@ -0,0 +1,72 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    cond_macro.h
+
+Abstract:
+
+    Class for maintaining conditional macros
+
+Author:
+
+    Leonardo de Moura (leonardo) 2010-12-17.
+
+Revision History:
+
+--*/
+#pragma once
+#include "ast/ast_ll_pp.h"
+
+class cond_macro {
+protected:
+    func_decl *           m_f;
+    expr_ref              m_def;
+    expr_ref              m_cond;
+    bool                  m_ineq;
+    bool                  m_satisfy_atom;
+    bool                  m_hint;
+    unsigned              m_weight;
+public:
+    cond_macro(ast_manager & m, func_decl * f, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, unsigned weight):
+        m_f(f),
+        m_def(def,m),
+        m_cond(cond, m),
+        m_ineq(ineq),
+        m_satisfy_atom(satisfy_atom),
+        m_hint(hint),
+        m_weight(weight) {
+        SASSERT(!m_hint || !m_cond);
+    }
+    
+    ~cond_macro() {
+    }
+    
+    func_decl * get_f() const { return m_f; }
+    
+    expr * get_def() const { return m_def; }
+    
+    expr * get_cond() const { return m_cond; }
+    
+    bool is_unconditional() const { return !m_cond || m_cond.m().is_true(m_cond); }
+    
+    bool satisfy_atom() const { return m_satisfy_atom; }
+    
+    bool is_hint() const { return m_hint; }
+    
+    bool is_equal(cond_macro const * other) const {
+        return m_f == other->m_f && m_def == other->m_def && m_cond == other->m_cond;
+    }
+    
+    std::ostream& display(std::ostream & out) const {
+        out << "[" << m_f->get_name() << " -> " << mk_bounded_pp(m_def, m_def.m(), 6);
+        if (m_hint)
+            out << " *hint*";
+        else
+            out << " when " << mk_bounded_pp(m_cond, m_cond.m(), 6);
+        return out << "] weight: " << m_weight;
+    }
+    
+    unsigned get_weight() const { return m_weight; }
+};

src/ast/macros/quantifier_macro_info.cpp

@@ -0,0 +1,66 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    quantifier_macro_info.cpp
+
+Abstract:
+
+    Macro solving utilities
+
+Author:
+
+    Leonardo de Moura (leonardo) 2010-12-17.
+
+Revision History:
+
+--*/
+#include "ast/ast_pp.h"
+#include "ast/macros/quantifier_macro_info.h"
+
+quantifier_macro_info::quantifier_macro_info(ast_manager& m, quantifier* q) :
+    m(m),
+    m_flat_q(q, m),
+    m_is_auf(true),
+    m_has_x_eq_y(false),
+    m_the_one(m) {
+    SASSERT(is_forall(q));
+    collect_macro_candidates(q);
+}
+
+void quantifier_macro_info::collect_macro_candidates(quantifier* q) {
+    macro_util mutil(m);
+    macro_util::macro_candidates candidates(m);
+    mutil.collect_macro_candidates(q, candidates);
+    unsigned num_candidates = candidates.size();
+    for (unsigned i = 0; i < num_candidates; i++) {
+        cond_macro* mc = alloc(cond_macro, m, candidates.get_f(i), candidates.get_def(i), candidates.get_cond(i),
+                               candidates.ineq(i), candidates.satisfy_atom(i), candidates.hint(i), q->get_weight());
+        insert_macro(mc);
+    }
+}
+
+
+bool quantifier_macro_info::unary_function_fragment() const {
+    unsigned sz = m_ng_decls.size();
+    if (sz > 1)
+        return false;
+    if (sz == 0)
+        return true;
+    func_decl* f = *(m_ng_decls.begin());
+    return f->get_arity() == 1;
+}
+
+std::ostream& quantifier_macro_info::display(std::ostream& out) const {
+    out << "info for quantifier:\n" << mk_pp(m_flat_q, m) << "\n";
+    out << "IS_AUF: " << m_is_auf << ", has x=y: " << m_has_x_eq_y << "\n";
+    out << "unary function fragment: " << unary_function_fragment() << "\n";
+    out << "ng decls: ";
+    for (func_decl* f : m_ng_decls)
+        out << f->get_name() << " ";
+    out << "\nmacros:\n";
+    for (cond_macro* cm : m_cond_macros)
+        cm->display(out << "  ") << "\n";
+    return out;
+}

src/ast/macros/quantifier_macro_info.h

@@ -0,0 +1,55 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    quantifier_macro_info.h
+
+Abstract:
+
+    Macro solving utilities
+
+Author:
+
+    Leonardo de Moura (leonardo) 2010-12-17.
+
+Revision History:
+
+--*/
+#pragma once
+#include "util/scoped_ptr_vector.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/macros/cond_macro.h"
+#include "ast/macros/macro_util.h"
+#include "ast/func_decl_dependencies.h"
+
+/**
+   \brief Store relevant information regarding a particular universal quantifier.
+   The information is used to (try to) build a model that satisfy the universal quantifier.
+*/
+class quantifier_macro_info {
+protected:
+    ast_manager& m;
+    quantifier_ref           m_flat_q;         // (flattened) quantifier
+    bool                     m_is_auf;
+    bool                     m_has_x_eq_y;
+    func_decl_set            m_ng_decls; // declarations used in non-ground applications (basic_family operators are ignored here).
+    scoped_ptr_vector<cond_macro>   m_cond_macros;
+    func_decl_ref            m_the_one; // the macro head used to satisfy the quantifier. this is useful for model checking
+    void collect_macro_candidates(quantifier* q);
+public:
+    quantifier_macro_info(ast_manager& m, quantifier* q);
+    virtual ~quantifier_macro_info() {}
+    bool is_auf() const { return m_is_auf; }
+    quantifier* get_flat_q() const { return m_flat_q; }
+    bool has_cond_macros() const { return !m_cond_macros.empty(); }
+    scoped_ptr_vector<cond_macro> const& macros() const { return m_cond_macros; }
+    void set_the_one(func_decl* f) { m_the_one = f; }
+    func_decl* get_the_one() const { return m_the_one; }
+    bool contains_ng_decl(func_decl* f) const { return m_ng_decls.contains(f); }
+    func_decl_set const& get_ng_decls() const { return m_ng_decls; }
+    virtual void reset_the_one() { m_the_one = nullptr; }
+    void insert_macro(cond_macro* m) { m_cond_macros.push_back(m); }
+    bool unary_function_fragment() const;
+    virtual std::ostream& display(std::ostream& out) const;
+};

src/model/CMakeLists.txt

@@ -8,6 +8,7 @@ z3_add_component(model
     model.cpp
     model_evaluator.cpp
     model_implicant.cpp
+    model_macro_solver.cpp
     model_pp.cpp
     model_smt2_pp.cpp
     model_v2_pp.cpp
@@ -16,6 +17,7 @@ z3_add_component(model
     value_factory.cpp
   COMPONENT_DEPENDENCIES
     rewriter
+    macros
   PYG_FILES
     model_evaluator_params.pyg
     model_params.pyg

src/model/model_core.cpp

@@ -74,9 +74,15 @@ void model_core::register_decl(func_decl * d, expr * v) {
 }
 
 void model_core::register_decl(func_decl * d, func_interp * fi) {
+    func_interp* old_fi = update_func_interp(d, fi);
+    dealloc(old_fi);
+}
+
+func_interp* model_core::update_func_interp(func_decl* d, func_interp* fi) {
     TRACE("model", tout << "register " << d->get_name() << "\n";);
     SASSERT(d->get_arity() > 0);
     SASSERT(&fi->m() == &m);
+    func_interp* old_fi = nullptr;
     auto& value = m_finterp.insert_if_not_there(d, nullptr);
     if (value == nullptr) {
         // new entry
@@ -87,10 +93,10 @@ void model_core::register_decl(func_decl * d, func_interp * fi) {
     }
     else {
         // replacing entry
-        if (fi != value)
+        old_fi = value;
-            dealloc(value);
         value = fi;
     }
+    return old_fi;
 }
 
 void model_core::unregister_decl(func_decl * d) {

src/model/model_core.h

@@ -68,6 +68,7 @@ public:
     void register_decl(func_decl * d, expr * v);
     void register_decl(func_decl * f, func_interp * fi);
     void unregister_decl(func_decl * d);
+    func_interp* update_func_interp(func_decl* f, func_interp* fi);
 
     virtual expr * get_some_value(sort * s) = 0;
     virtual expr * get_fresh_value(sort * s) = 0;

src/model/model_macro_solver.cpp

@@ -0,0 +1,593 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Abstract:
+
+    Macro solving utilities
+
+Author:
+
+    Leonardo de Moura (leonardo) 2010-12-17.
+
+--*/
+
+#include "ast/for_each_expr.h"
+#include "ast/ast_pp.h"
+#include "model/model_macro_solver.h"
+#include "model/model_core.h"
+
+void base_macro_solver::set_else_interp(func_decl* f, expr* f_else) {
+    SASSERT(f_else != nullptr);
+    func_interp* fi = m_model->get_func_interp(f);
+    if (fi == nullptr) {
+        fi = alloc(func_interp, m, f->get_arity());
+        m_model->register_decl(f, fi);
+    }
+    fi->set_else(f_else);
+    TRACE("model_finder", tout << f->get_name() << " " << mk_pp(f_else, m) << "\n";);
+}
+
+void base_macro_solver::operator()(model_core& m, ptr_vector<quantifier>& qs, ptr_vector<quantifier>& residue) {
+    m_model = &m;
+    ptr_vector<quantifier> curr_qs(qs), new_qs;
+    while (process(curr_qs, new_qs, residue)) {
+        curr_qs.swap(new_qs);
+        new_qs.reset();
+    }
+    std::swap(qs, new_qs);
+}
+
+/**
+   \brief Return true if \c f is in (qs\{q})
+*/
+bool simple_macro_solver::contains(func_decl* f, ptr_vector<quantifier> const& qs, quantifier* q) {
+    for (quantifier* other : qs) {
+        if (q == other)
+            continue;
+        quantifier_macro_info* other_qi = get_qinfo(other);
+        if (other_qi->contains_ng_decl(f))
+            return true;
+    }
+    return false;
+}
+
+bool simple_macro_solver::process(quantifier* q, ptr_vector<quantifier> const& qs) {
+    quantifier_macro_info* qi = get_qinfo(q);
+    for (cond_macro* m : qi->macros()) {
+        if (!m->satisfy_atom())
+            continue;
+        func_decl* f = m->get_f();
+        if (!contains(f, qs, q)) {
+            qi->set_the_one(f);
+            expr* f_else = m->get_def();
+            SASSERT(f_else != nullptr);
+            // Remark: I can ignore the conditions of m because
+            // I know the (partial) interpretation of f satisfied the ground part.
+            // MBQI will force extra instantiations if the (partial) interpretation of f
+            // does not satisfy the quantifier.
+            // In all other cases the "else" of f will satisfy the quantifier.
+            set_else_interp(f, f_else);
+            TRACE("model_finder", tout << "satisfying the quantifier using simple macro:\n";
+            m->display(tout); tout << "\n";);
+            return true; // satisfied quantifier
+        }
+    }
+    return false;
+}
+
+bool simple_macro_solver::process(ptr_vector<quantifier> const& qs, ptr_vector<quantifier>& new_qs, ptr_vector<quantifier>& residue) {
+    bool removed = false;
+    for (quantifier* q : qs) {
+        if (process(q, qs))
+            removed = true;
+        else
+            new_qs.push_back(q);
+    }
+    return removed;
+}
+
+
+
+void hint_macro_solver::insert_q_f(quantifier* q, func_decl* f) {
+    SASSERT(!m_forbidden.contains(f));
+    quantifier_set* s = nullptr;
+    if (!m_q_f.find(f, s)) {
+        s = alloc(quantifier_set);
+        m_q_f.insert(f, s);
+        m_qsets.push_back(s);
+    }
+    SASSERT(s != nullptr);
+    s->insert(q);
+}
+
+void hint_macro_solver::insert_f2def(func_decl* f, expr* def) {
+    expr_set* s = nullptr;
+    if (!m_f2defs.find(f, s)) {
+        s = alloc(expr_set);
+        m_f2defs.insert(f, s);
+        m_esets.push_back(s);
+    }
+    SASSERT(s != nullptr);
+    s->insert(def);
+}
+
+void hint_macro_solver::insert_q_f_def(quantifier* q, func_decl* f, expr* def) {
+    SASSERT(!m_forbidden.contains(f));
+    quantifier_set* s = nullptr;
+    if (!m_q_f_def.find(f, def, s)) {
+        s = alloc(quantifier_set);
+        m_q_f_def.insert(f, def, s);
+        insert_f2def(f, def);
+        m_qsets.push_back(s);
+    }
+    SASSERT(s != nullptr);
+    s->insert(q);
+}
+
+
+hint_macro_solver::quantifier_set* hint_macro_solver::get_q_f_def(func_decl* f, expr* def) {
+    quantifier_set* s = nullptr;
+    m_q_f_def.find(f, def, s);
+    SASSERT(s != nullptr);
+    return s;
+}
+
+
+void hint_macro_solver::reset_q_fs() {
+    std::for_each(m_qsets.begin(), m_qsets.end(), delete_proc<quantifier_set>());
+    std::for_each(m_esets.begin(), m_esets.end(), delete_proc<expr_set>());
+    m_q_f.reset();
+    m_q_f_def.reset();
+    m_qsets.reset();
+    m_f2defs.reset();
+    m_esets.reset();
+}
+
+
+bool hint_macro_solver::is_candidate(quantifier* q) const {
+    quantifier_macro_info* qi = get_qinfo(q);
+    for (cond_macro* m : qi->macros()) {
+        if (m->satisfy_atom() && !m_forbidden.contains(m->get_f()))
+            return true;
+    }
+    return false;
+}
+
+void hint_macro_solver::register_decls_as_forbidden(quantifier* q) {
+    quantifier_macro_info* qi = get_qinfo(q);
+    func_decl_set const& ng_decls = qi->get_ng_decls();
+    for (func_decl* f : ng_decls) {
+        m_forbidden.insert(f);
+    }
+}
+
+void hint_macro_solver::preprocess(ptr_vector<quantifier> const& qs, ptr_vector<quantifier>& qcandidates, ptr_vector<quantifier>& non_qcandidates) {
+    ptr_vector<quantifier> curr(qs);
+    while (true) {
+        for (quantifier* q : curr) {
+            if (is_candidate(q)) {
+                qcandidates.push_back(q);
+            }
+            else {
+                register_decls_as_forbidden(q);
+                non_qcandidates.push_back(q);
+            }
+        }
+        if (curr.size() == qcandidates.size())
+            return;
+        SASSERT(qcandidates.size() < curr.size());
+        curr.swap(qcandidates);
+        qcandidates.reset();
+    }
+}
+
+void hint_macro_solver::mk_q_f_defs(ptr_vector<quantifier> const& qs) {
+    for (quantifier* q : qs) {
+        quantifier_macro_info* qi = get_qinfo(q);
+        func_decl_set const& ng_decls = qi->get_ng_decls();
+        for (func_decl* f : ng_decls) {
+            if (!m_forbidden.contains(f))
+                insert_q_f(q, f);
+        }
+        for (cond_macro* m : qi->macros()) {
+            if (m->satisfy_atom() && !m_forbidden.contains(m->get_f())) {
+                insert_q_f_def(q, m->get_f(), m->get_def());
+                m_candidates.insert(m->get_f());
+            }
+        }
+    }
+}
+
+void hint_macro_solver::display_quantifier_set(std::ostream& out, quantifier_set const* s) {
+    for (quantifier* q : *s) {
+        out << q->get_qid() << " ";
+    }
+    out << "\n";
+}
+
+void hint_macro_solver::display_qcandidates(std::ostream& out, ptr_vector<quantifier> const& qcandidates) const {
+    for (quantifier* q : qcandidates) {
+        out << q->get_qid() << " ->\n" << mk_pp(q, m) << "\n";
+        quantifier_macro_info* qi = get_qinfo(q);
+        qi->display(out);
+        out << "------\n";
+    }
+    out << "Sets Q_f\n";
+    for (auto const& kv : m_q_f) {
+        func_decl* f = kv.m_key;
+        quantifier_set* s = kv.m_value;
+        out << f->get_name() << " -> "; display_quantifier_set(out, s);
+    }
+    out << "Sets Q_{f = def}\n";
+    for (auto const& kv : m_q_f_def) {
+        func_decl* f = kv.get_key1();
+        expr* def = kv.get_key2();
+        quantifier_set* s = kv.get_value();
+        out << f->get_name() << " " << mk_pp(def, m) << " ->\n"; display_quantifier_set(out, s);
+    }
+}
+
+
+void hint_macro_solver::display_search_state(std::ostream& out) const {
+    out << "fs:\n";
+    for (auto const& kv : m_fs) {
+        out << kv.m_key->get_name() << " ";
+    }
+    out << "\nsatisfied:\n";
+    for (auto q : m_satisfied) {
+        out << q->get_qid() << " ";
+    }
+    out << "\nresidue:\n";
+    for (auto q : m_residue) {
+        out << q->get_qid() << " ";
+    }
+    out << "\n";
+}
+
+bool hint_macro_solver::check_satisfied_residue_invariant() {
+    DEBUG_CODE(
+        for (quantifier* q : m_satisfied) {
+            SASSERT(!m_residue.contains(q));
+            auto* qi = get_qinfo(q);
+            SASSERT(qi != nullptr);
+            SASSERT(qi->get_the_one() != nullptr);
+        });
+    return true;
+}
+
+
+bool hint_macro_solver::update_satisfied_residue(func_decl* f, expr* def) {
+    bool useful = false;
+    SASSERT(check_satisfied_residue_invariant());
+    quantifier_set* q_f = get_q_f(f);
+    quantifier_set* q_f_def = get_q_f_def(f, def);
+    for (quantifier* q : *q_f_def) {
+        if (!m_satisfied.contains(q)) {
+            useful = true;
+            m_residue.erase(q);
+            m_satisfied.insert(q);
+            quantifier_macro_info* qi = get_qinfo(q);
+            SASSERT(qi->get_the_one() == 0);
+            qi->set_the_one(f); // remark... event handler will reset it during backtracking.
+        }
+    }
+    if (!useful)
+        return false;
+    for (quantifier* q : *q_f) {
+        if (!m_satisfied.contains(q)) {
+            m_residue.insert(q);
+        }
+    }
+    SASSERT(check_satisfied_residue_invariant());
+    return true;
+}
+
+/**
+   \brief Extract from m_residue, func_decls that can be used as macros to satisfy it.
+   The candidates must not be elements of m_fs.
+*/
+void hint_macro_solver::get_candidates_from_residue(func_decl_set& candidates) {
+    for (quantifier* q : m_residue) {
+        quantifier_macro_info* qi = get_qinfo(q);
+        for (cond_macro* m : qi->macros()) {
+            func_decl* f = m->get_f();
+            if (m->satisfy_atom() && !m_forbidden.contains(f) && !m_fs.contains(f)) {
+                candidates.insert(f);
+            }
+        }
+    }
+}
+
+#define GREEDY_MAX_DEPTH 10 /* to avoid too expensive search spaces */
+
+/**
+  \brief Try to reduce m_residue using the macros of f.
+*/
+void hint_macro_solver::greedy(func_decl* f, unsigned depth) {
+    if (depth >= GREEDY_MAX_DEPTH)
+        return; // failed
+
+    TRACE("model_finder_hint",
+        tout << "greedy depth: " << depth << ", f: " << f->get_name() << "\n";
+    display_search_state(tout););
+
+    expr_set* s = get_f_defs(f);
+    for (expr* def : *s) {
+
+        SASSERT(!m_fs.contains(f));
+
+        m_satisfied.push_scope();
+        m_residue.push_scope();
+        TRACE("model_finder", tout << f->get_name() << " " << mk_pp(def, m) << "\n";);
+        m_fs.insert(f, def);
+
+        if (update_satisfied_residue(f, def)) {
+            // update was useful
+            greedy(depth + 1); // greedy throws exception in case of success
+            // reachable iff greedy failed.
+        }
+
+        m_satisfied.pop_scope();
+        m_residue.pop_scope();
+        m_fs.erase(f);
+    }
+}
+
+/**
+   \brief check if satisfied subset introduces a cyclic dependency.
+
+   f_1 = def_1(f_2), ..., f_n = def_n(f_1)
+ */
+
+bool hint_macro_solver::is_cyclic() {
+    m_acyclic.reset();
+    while (true) {
+        unsigned sz = m_acyclic.size();
+        if (sz == m_fs.size()) return false; // there are no cyclic dependencies
+        for (auto const& kv : m_fs) {
+            func_decl* f = kv.m_key;
+            if (m_acyclic.contains(f)) continue;
+            if (is_acyclic(kv.m_value))
+                m_acyclic.insert(f);
+        }
+        if (sz == m_acyclic.size()) return true; // no progress, so dependency cycle found.                    
+    }
+}
+
+bool hint_macro_solver::is_acyclic(expr* def) {
+    m_visited.reset();
+    occurs_check oc(*this);
+    try {
+        for_each_expr(oc, m_visited, def);
+    }
+    catch (const occurs&) {
+        return false;
+    }
+    return true;
+}
+
+/**
+   \brief Try to reduce m_residue (if not empty) by selecting a function f
+   that is a macro in the residue.
+*/
+void hint_macro_solver::greedy(unsigned depth) {
+    if (m_residue.empty()) {
+        if (is_cyclic()) return;
+        TRACE("model_finder_hint",
+            tout << "found subset that is satisfied by macros\n";
+        display_search_state(tout););
+        throw found_satisfied_subset();
+    }
+    func_decl_set candidates;
+    get_candidates_from_residue(candidates);
+
+    TRACE("model_finder_hint", tout << "candidates from residue:\n";
+    for (func_decl* f : candidates) {
+        tout << f->get_name() << " ";
+    }
+    tout << "\n";);
+
+    for (func_decl* f : candidates) {
+        greedy(f, depth);
+    }
+}
+
+/**
+   \brief Try to find a set of quantifiers by starting to use the macros of f.
+   This is the "find" procedure in the comments above.
+   The set of satisfied quantifiers is in m_satisfied, and the remaining to be
+   satisfied in m_residue. When the residue becomes empty we throw the exception found_satisfied_subset.
+*/
+void hint_macro_solver::process(func_decl* f) {
+    SASSERT(m_satisfied.empty());
+    SASSERT(m_residue.empty());
+    greedy(f, 0);
+}
+
+/**
+   \brief Copy the quantifiers from qcandidates to new_qs that are not in m_satisfied.
+*/
+void hint_macro_solver::copy_non_satisfied(ptr_vector<quantifier> const& qcandidates, ptr_vector<quantifier>& new_qs) {
+    for (quantifier* q : qcandidates) {
+        if (!m_satisfied.contains(q))
+            new_qs.push_back(q);
+    }
+}
+
+/**
+   \brief Use m_fs to set the interpretation of the function symbols that were used to satisfy the
+   quantifiers in m_satisfied.
+*/
+void hint_macro_solver::set_interp() {
+    for (auto const& kv : m_fs) {
+        func_decl* f = kv.m_key;
+        expr* def = kv.m_value;
+        set_else_interp(f, def);
+    }
+}
+
+void hint_macro_solver::reset() {
+    reset_q_fs();
+    m_forbidden.reset();
+    m_candidates.reset();
+    m_satisfied.reset();
+    m_residue.reset();
+    m_fs.reset();
+}
+
+bool hint_macro_solver::process(ptr_vector<quantifier> const& qs, ptr_vector<quantifier>& new_qs, ptr_vector<quantifier>& residue) {
+    reset();
+    ptr_vector<quantifier> qcandidates;
+    preprocess(qs, qcandidates, new_qs);
+    if (qcandidates.empty()) {
+        SASSERT(new_qs.size() == qs.size());
+        return false;
+    }
+    mk_q_f_defs(qcandidates);
+    TRACE("model_finder_hint", tout << "starting hint-solver search using:\n"; display_qcandidates(tout, qcandidates););
+    for (func_decl* f : m_candidates) {
+        try {
+            process(f);
+        }
+        catch (const found_satisfied_subset&) {
+            set_interp();
+            copy_non_satisfied(qcandidates, new_qs);
+            return true;
+        }
+    }
+    // failed... copy everything to new_qs
+    new_qs.append(qcandidates);
+    return false;
+}
+
+/**
+\brief Satisfy clauses that are not in the AUF fragment but define conditional macros.
+These clauses are eliminated even if the symbol being defined occurs in other quantifiers.
+The auf_solver is ineffective in these clauses.
+
+\remark Full macros are used even if they are in the AUF fragment.
+*/
+
+bool non_auf_macro_solver::add_macro(func_decl* f, expr* f_else) {
+    TRACE("model_finder", tout << "trying to add macro for " << f->get_name() << "\n" << mk_pp(f_else, m) << "\n";);
+    func_decl_set* s = m_dependencies.mk_func_decl_set();
+    m_dependencies.collect_ng_func_decls(f_else, s);
+    if (!m_dependencies.insert(f, s)) {
+        TRACE("model_finder", tout << "failed to add macro\n";);
+        return false; // cyclic dependency
+    }
+    set_else_interp(f, f_else);
+    return true;
+}
+
+// Return true if r1 is a better macro than r2.
+bool non_auf_macro_solver::is_better_macro(cond_macro* r1, cond_macro* r2) {
+    if (r2 == nullptr || !r1->is_hint())
+        return true;
+    if (!r2->is_hint())
+        return false;
+    SASSERT(r1->is_hint() && r2->is_hint());
+    if (is_ground(r1->get_def()) && !is_ground(r2->get_def()))
+        return true;
+    return false;
+}
+
+cond_macro* non_auf_macro_solver::get_macro_for(func_decl* f, quantifier* q) {
+    cond_macro* r = nullptr;
+    quantifier_macro_info* qi = get_qinfo(q);
+    for (cond_macro* m : qi->macros()) {
+        if (m->get_f() == f && !m->is_hint() && is_better_macro(m, r))
+            r = m;
+    }
+    return r;
+}
+
+typedef std::pair<cond_macro*, quantifier*> mq_pair;
+
+void non_auf_macro_solver::collect_candidates(ptr_vector<quantifier> const& qs, obj_map<func_decl, mq_pair>& full_macros, func_decl_set& cond_macros) {
+    for (quantifier* q : qs) {
+        quantifier_macro_info* qi = get_qinfo(q);
+        for (cond_macro* m : qi->macros()) {
+            if (!m->is_hint()) {
+                func_decl* f = m->get_f();
+                TRACE("model_finder", tout << "considering macro for: " << f->get_name() << "\n";
+                m->display(tout); tout << "\n";);
+                if (m->is_unconditional() && (!qi->is_auf() || m->get_weight() >= m_mbqi_force_template)) {
+                    full_macros.insert(f, std::make_pair(m, q));
+                    cond_macros.erase(f);
+                }
+                else if (!full_macros.contains(f) && !qi->is_auf())
+                    cond_macros.insert(f);
+            }
+        }
+    }
+}
+
+void non_auf_macro_solver::process_full_macros(obj_map<func_decl, mq_pair> const& full_macros, obj_hashtable<quantifier>& removed) {
+    for (auto const& kv : full_macros) {
+        func_decl* f = kv.m_key;
+        cond_macro* m = kv.m_value.first;
+        quantifier* q = kv.m_value.second;
+        SASSERT(m->is_unconditional());
+        if (add_macro(f, m->get_def())) {
+            get_qinfo(q)->set_the_one(f);
+            removed.insert(q);
+        }
+    }
+}
+
+void non_auf_macro_solver::process(func_decl* f, ptr_vector<quantifier> const& qs, obj_hashtable<quantifier>& removed) {
+    expr_ref fi_else(m);
+    ptr_buffer<quantifier> to_remove;
+    for (quantifier* q : qs) {
+        if (removed.contains(q))
+            continue;
+        cond_macro* cm = get_macro_for(f, q);
+        if (!cm)
+            continue;
+        SASSERT(!cm->is_hint());
+        if (cm->is_unconditional())
+            return; // f is part of a full macro... ignoring it.
+        to_remove.push_back(q);
+        if (fi_else.get() == nullptr) {
+            fi_else = cm->get_def();
+        }
+        else {
+            fi_else = m.mk_ite(cm->get_cond(), cm->get_def(), fi_else);
+        }
+    }
+    if (fi_else.get() != nullptr && add_macro(f, fi_else)) {
+        for (quantifier* q : to_remove) {
+            get_qinfo(q)->set_the_one(f);
+            removed.insert(q);
+        }
+    }
+}
+
+void non_auf_macro_solver::process_cond_macros(func_decl_set const& cond_macros, ptr_vector<quantifier> const& qs, obj_hashtable<quantifier>& removed) {
+    for (func_decl* f : cond_macros) {
+        process(f, qs, removed);
+    }
+}
+
+bool non_auf_macro_solver::process(ptr_vector<quantifier> const& qs, ptr_vector<quantifier>& new_qs, ptr_vector<quantifier>& residue) {
+    obj_map<func_decl, mq_pair> full_macros;
+    func_decl_set cond_macros;
+    obj_hashtable<quantifier> removed;
+
+    // Possible improvement: sort full_macros & cond_macros using an user provided precedence function.
+
+    collect_candidates(qs, full_macros, cond_macros);
+    process_full_macros(full_macros, removed);
+    process_cond_macros(cond_macros, qs, removed);
+
+    for (quantifier* q : qs) {
+        if (removed.contains(q))
+            continue;
+        new_qs.push_back(q);
+        residue.push_back(q);
+    }
+    return !removed.empty();
+}
+
+

src/model/model_macro_solver.h

@@ -0,0 +1,308 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Abstract:
+
+    Macro solving utilities
+
+Author:
+
+    Leonardo de Moura (leonardo) 2010-12-17.
+
+--*/
+
+#pragma once
+#include "util/obj_pair_hashtable.h"
+#include "util/backtrackable_set.h"
+#include "ast/macros/quantifier_macro_info.h"
+#include "model/model_core.h"
+
+
+class quantifier2macro_infos {
+public:
+    virtual ~quantifier2macro_infos() {}
+    virtual quantifier_macro_info* operator()(quantifier* q) = 0;
+};
+
+/**
+   \brief Base class for macro solvers.
+*/
+class base_macro_solver {
+protected:
+    ast_manager& m;
+    quantifier2macro_infos& m_q2info;
+    model_core* m_model;
+
+    quantifier_macro_info* get_qinfo(quantifier* q) const {
+        return m_q2info(q);
+    }
+
+    void set_else_interp(func_decl* f, expr* f_else);
+
+    virtual bool process(ptr_vector<quantifier> const& qs, ptr_vector<quantifier>& new_qs, ptr_vector<quantifier>& residue) = 0;
+
+public:
+    base_macro_solver(ast_manager& m, quantifier2macro_infos& q2i) :
+        m(m),
+        m_q2info(q2i),
+        m_model(nullptr) {
+    }
+
+    virtual ~base_macro_solver() {}
+
+    /**
+       \brief Try to satisfy quantifiers in qs by using macro definitions.
+       Store in new_qs the quantifiers that were not satisfied.
+       Store in residue a subset of the quantifiers that were satisfied but contain information useful for the auf_solver.
+    */
+    void operator()(model_core& m, ptr_vector<quantifier>& qs, ptr_vector<quantifier>& residue);
+};
+
+/**
+   \brief The simple macro solver satisfies quantifiers that contain
+   (conditional) macros for a function f that does not occur in any other quantifier.
+
+   Since f does not occur in any other quantifier, I don't need to track the dependencies
+   of f. That is, recursive definition cannot be created.
+*/
+class simple_macro_solver : public base_macro_solver {
+protected:
+    /**
+       \brief Return true if \c f is in (qs\{q})
+    */
+    bool contains(func_decl* f, ptr_vector<quantifier> const& qs, quantifier* q);
+
+    bool process(quantifier* q, ptr_vector<quantifier> const& qs);
+
+    bool process(ptr_vector<quantifier> const& qs, ptr_vector<quantifier>& new_qs, ptr_vector<quantifier>& residue) override;
+
+public:
+    simple_macro_solver(ast_manager& m, quantifier2macro_infos& q2i) :
+        base_macro_solver(m, q2i) {}
+};
+
+
+class hint_macro_solver : public base_macro_solver {
+    /*
+      This solver tries to satisfy quantifiers by using macros, cond_macros and hints.
+      The idea is to satisfy a set of quantifiers Q = Q_{f_1} union ... union Q_{f_n}
+      where Q_{f_i} is the set of quantifiers that contain the function f_i.
+      Let f_i = def_i be macros (in this solver conditions are ignored).
+      Let Q_{f_i = def_i} be the set of quantifiers where f_i = def_i is a macro.
+      Then, the set Q can be satisfied using f_1 = def_1 ... f_n = def_n
+      when
+
+      Q_{f_1} union ... union Q_{f_n} = Q_{f_1 = def_1} ... Q_{f_n = def_n} (*)
+
+      So, given a set of macros f_1 = def_1, ..., f_n = d_n, it is very easy to check
+      whether they can be used to satisfy all quantifiers that use f_1, ..., f_n in
+      non ground terms.
+
+      We can find the sets of f_1 = def_1, ..., f_n = def_n that satisfy Q using
+      the following search procedure
+            find(Q)
+              for each f_i = def_i in Q
+                  R = greedy(Q_{f_i = def_1}, Q_f_i \ Q_{f_i = def_i}, {f_i}, {f_i = def_i})
+                  if (R != empty-set)
+                    return R
+            greedy(Satisfied, Residue, F, F_DEF)
+              if Residue = empty-set return F_DEF
+              for each f_j = def_j in Residue such that f_j not in F
+                  New-Satisfied = Satisfied union Q_{f_j = def_j}
+                  New-Residue = (Residue union Q_{f_j}) \ New-Satisfied
+                  R = greedy(New-Satisfied, New-Residue, F \union {f_j}, F_DEF union {f_j = def_j})
+                  if (R != empty-set)
+                     return R
+
+      This search may be too expensive, and is exponential on the number of different function
+      symbols.
+      Some observations to prune the search space.
+      1) If f_i occurs in a quantifier without macros, then f_i and any macro using it can be ignored during the search.
+      2) If f_i = def_i is not a macro in a quantifier q, and there is no other f_j = def_j (i != j) in q,
+         then f_i = def_i can be ignored during the search.
+    */
+
+    typedef obj_hashtable<quantifier> quantifier_set;
+    typedef obj_map<func_decl, quantifier_set*> q_f;
+    typedef obj_pair_map<func_decl, expr, quantifier_set*> q_f_def;
+    typedef obj_pair_hashtable<func_decl, expr> f_def_set;
+    typedef obj_hashtable<expr> expr_set;
+    typedef obj_map<func_decl, expr_set*> f2defs;
+
+    q_f                        m_q_f;
+    q_f_def                    m_q_f_def;
+    ptr_vector<quantifier_set> m_qsets;
+    f2defs                     m_f2defs;
+    ptr_vector<expr_set>       m_esets;
+
+    void insert_q_f(quantifier* q, func_decl* f);
+
+    void insert_f2def(func_decl* f, expr* def);
+    void insert_q_f_def(quantifier* q, func_decl* f, expr* def);
+
+    quantifier_set* get_q_f_def(func_decl* f, expr* def);
+
+    expr_set* get_f_defs(func_decl* f) { return m_f2defs[f]; }
+    quantifier_set* get_q_f(func_decl* f) { return m_q_f[f]; }
+
+    void reset_q_fs();
+
+    func_decl_set              m_forbidden;
+    func_decl_set              m_candidates;
+
+    bool is_candidate(quantifier* q) const;
+    void register_decls_as_forbidden(quantifier* q);
+
+    void preprocess(ptr_vector<quantifier> const& qs, ptr_vector<quantifier>& qcandidates, ptr_vector<quantifier>& non_qcandidates);
+
+    void mk_q_f_defs(ptr_vector<quantifier> const& qs);
+
+    static void display_quantifier_set(std::ostream& out, quantifier_set const* s);
+
+    void display_qcandidates(std::ostream& out, ptr_vector<quantifier> const& qcandidates) const;
+
+    //
+    // Search: main procedures
+    //
+
+    struct ev_handler {
+        hint_macro_solver* m_owner;
+
+        void operator()(quantifier* q, bool ins) {
+            quantifier_macro_info* qi = m_owner->get_qinfo(q);
+            qi->set_the_one(nullptr);
+        }
+
+        ev_handler(hint_macro_solver* o) :
+            m_owner(o) {
+        }
+    };
+
+
+    typedef backtrackable_set<quantifier_set, quantifier*> qset;
+    typedef backtrackable_set<quantifier_set, quantifier*, ev_handler> qsset;
+    typedef obj_map<func_decl, expr*> f2def;
+
+    qset         m_residue;
+    qsset        m_satisfied;
+    f2def        m_fs; // set of function symbols (and associated interpretation) that were used to satisfy the quantifiers in m_satisfied.
+
+    struct found_satisfied_subset {};
+
+    void display_search_state(std::ostream& out) const;
+    bool check_satisfied_residue_invariant();
+
+
+    bool update_satisfied_residue(func_decl* f, expr* def);
+
+    /**
+       \brief Extract from m_residue, func_decls that can be used as macros to satisfy it.
+       The candidates must not be elements of m_fs.
+    */
+    void get_candidates_from_residue(func_decl_set& candidates);
+
+    /**
+      \brief Try to reduce m_residue using the macros of f.
+    */
+    void greedy(func_decl* f, unsigned depth);
+
+    /**
+       \brief check if satisfied subset introduces a cyclic dependency.
+
+       f_1 = def_1(f_2), ..., f_n = def_n(f_1)
+     */
+
+    expr_mark               m_visited;
+    obj_hashtable<func_decl> m_acyclic;
+    bool is_cyclic();
+    struct occurs {};
+    struct occurs_check {
+        hint_macro_solver& m_cls;
+        occurs_check(hint_macro_solver& hs) : m_cls(hs) {}
+        void operator()(app* n) { if (m_cls.m_fs.contains(n->get_decl()) && !m_cls.m_acyclic.contains(n->get_decl())) throw occurs(); }
+        void operator()(var* n) {}
+        void operator()(quantifier* n) {}
+    };
+    bool is_acyclic(expr* def);
+
+    /**
+       \brief Try to reduce m_residue (if not empty) by selecting a function f
+       that is a macro in the residue.
+    */
+    void greedy(unsigned depth);
+
+    /**
+       \brief Try to find a set of quantifiers by starting to use the macros of f.
+       This is the "find" procedure in the comments above.
+       The set of satisfied quantifiers is in m_satisfied, and the remaining to be
+       satisfied in m_residue. When the residue becomes empty we throw the exception found_satisfied_subset.
+    */
+    void process(func_decl* f);
+
+    /**
+       \brief Copy the quantifiers from qcandidates to new_qs that are not in m_satisfied.
+    */
+    void copy_non_satisfied(ptr_vector<quantifier> const& qcandidates, ptr_vector<quantifier>& new_qs);
+    /**
+       \brief Use m_fs to set the interpretation of the function symbols that were used to satisfy the
+       quantifiers in m_satisfied.
+    */
+    void set_interp();
+
+    void reset();
+
+    bool process(ptr_vector<quantifier> const& qs, ptr_vector<quantifier>& new_qs, ptr_vector<quantifier>& residue) override;
+
+public:
+    hint_macro_solver(ast_manager& m, quantifier2macro_infos& q2i) :
+        base_macro_solver(m, q2i),
+        m_satisfied(ev_handler(this)) {
+    }
+
+    ~hint_macro_solver() override {
+        reset();
+    }
+
+};
+
+/**
+\brief Satisfy clauses that are not in the AUF fragment but define conditional macros.
+These clauses are eliminated even if the symbol being defined occurs in other quantifiers.
+The auf_solver is ineffective in these clauses.
+
+\remark Full macros are used even if they are in the AUF fragment.
+*/
+
+class non_auf_macro_solver : public base_macro_solver {
+    func_decl_dependencies& m_dependencies;
+    unsigned m_mbqi_force_template{ 0 };
+
+    bool add_macro(func_decl* f, expr* f_else);
+
+    // Return true if r1 is a better macro than r2.
+    bool is_better_macro(cond_macro* r1, cond_macro* r2);
+
+    cond_macro* get_macro_for(func_decl* f, quantifier* q);
+
+    typedef std::pair<cond_macro*, quantifier*> mq_pair;
+
+    void collect_candidates(ptr_vector<quantifier> const& qs, obj_map<func_decl, mq_pair>& full_macros, func_decl_set& cond_macros);
+
+    void process_full_macros(obj_map<func_decl, mq_pair> const& full_macros, obj_hashtable<quantifier>& removed);
+
+    void process(func_decl* f, ptr_vector<quantifier> const& qs, obj_hashtable<quantifier>& removed);
+
+    void process_cond_macros(func_decl_set const& cond_macros, ptr_vector<quantifier> const& qs, obj_hashtable<quantifier>& removed);
+
+    bool process(ptr_vector<quantifier> const& qs, ptr_vector<quantifier>& new_qs, ptr_vector<quantifier>& residue) override;
+
+public:
+    non_auf_macro_solver(ast_manager& m, quantifier2macro_infos& q2i, func_decl_dependencies& d) :
+        base_macro_solver(m, q2i),
+        m_dependencies(d) {
+    }
+
+    void set_mbqi_force_template(unsigned n) { m_mbqi_force_template = n; }
+};
+
+

src/sat/sat_extension.h

@@ -57,14 +57,16 @@ namespace sat {
     protected:
         bool m_drating { false };
         int  m_id { 0 };
+        symbol m_name;
         solver* m_solver { nullptr };
     public:        
-        extension(int id): m_id(id) {}
+        extension(symbol const& name, int id): m_id(id), m_name(name) {}
         virtual ~extension() {}
         int get_id() const { return m_id; }
         void set_solver(solver* s) { m_solver = s; }        
         solver& s() { return *m_solver; }
         solver const& s() const { return *m_solver; }
+        symbol const& name() const { return m_name;  }
 
         virtual void set_lookahead(lookahead* s) {};
         class scoped_drating {

src/sat/smt/CMakeLists.txt

@@ -26,6 +26,7 @@ z3_add_component(sat_smt
     fpa_solver.cpp
     q_mbi.cpp
     q_model_finder.cpp
+    q_model_fixer.cpp
     q_solver.cpp
     sat_dual_solver.cpp
     sat_th.cpp

src/sat/smt/array_solver.cpp

@@ -75,7 +75,7 @@ For example
 namespace array {
 
     solver::solver(euf::solver& ctx, theory_id id) :
-        th_euf_solver(ctx, id),
+        th_euf_solver(ctx, symbol("array"), id),
         a(m),
         m_sort2epsilon(m),
         m_sort2diag(m),

src/sat/smt/ba_solver.cpp

@@ -1363,7 +1363,7 @@ namespace sat {
         ba_solver(ctx.get_manager(), ctx.get_si(), id) {}
 
     ba_solver::ba_solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id)
-        : euf::th_solver(m, id),
+        : euf::th_solver(m, symbol("ba"), id),
           si(si), m_pb(m),
           m_lookahead(nullptr), 
           m_constraint_id(0), m_ba(*this), m_sort(m_ba) {

src/sat/smt/bv_solver.cpp

@@ -50,7 +50,7 @@ namespace bv {
     };
 
     solver::solver(euf::solver& ctx, theory_id id) :
-        euf::th_euf_solver(ctx, id),
+        euf::th_euf_solver(ctx, symbol("bv"), id),
         bv(m),
         m_autil(m),
         m_ackerman(*this),

src/sat/smt/euf_solver.cpp

@@ -29,7 +29,7 @@ Author:
 namespace euf {
 
     solver::solver(ast_manager& m, sat::sat_internalizer& si, params_ref const& p) :
-        extension(m.mk_family_id("euf")),
+        extension(symbol("euf"), m.mk_family_id("euf")),
         m(m),
         si(si),
         m_egraph(m),
@@ -76,7 +76,7 @@ namespace euf {
     }
 
     th_solver* solver::quantifier2solver() {
-        family_id fid = m.mk_family_id(q::solver::name());
+        family_id fid = m.mk_family_id(symbol("quant"));
         auto* ext = m_id2solver.get(fid, nullptr);
         if (ext)
             return ext;
@@ -99,27 +99,18 @@ namespace euf {
         bv_util bvu(m);
         array_util au(m);
         fpa_util fpa(m);
-        if (pb.get_family_id() == fid) {
+        if (pb.get_family_id() == fid) 
             ext = alloc(sat::ba_solver, *this, fid);
-            if (use_drat())
+        else if (bvu.get_family_id() == fid) 
-                s().get_drat().add_theory(fid, symbol("ba"));
-        }
-        else if (bvu.get_family_id() == fid) {
             ext = alloc(bv::solver, *this, fid);
-            if (use_drat())
+        else if (au.get_family_id() == fid) 
-                s().get_drat().add_theory(fid, symbol("bv"));            
-        }
-        else if (au.get_family_id() == fid) {
             ext = alloc(array::solver, *this, fid);
-            if (use_drat())
+        else if (fpa.get_family_id() == fid) 
-                s().get_drat().add_theory(fid, symbol("array"));
-        }
-        else if (fpa.get_family_id() == fid) {
             ext = alloc(fpa::solver, *this);
-            if (use_drat())
+
-                s().get_drat().add_theory(fid, symbol("fpa"));
-        }
         if (ext) {
+            if (use_drat())
+                s().get_drat().add_theory(fid, ext->name());
             ext->set_solver(m_solver);
             ext->push_scopes(s().num_scopes());
             add_solver(fid, ext);

src/sat/smt/fpa_solver.cpp

@@ -23,7 +23,7 @@ Revision History:
 namespace fpa {
 
     solver::solver(euf::solver& ctx) :
-        euf::th_euf_solver(ctx, ctx.get_manager().mk_family_id("fpa")),
+        euf::th_euf_solver(ctx, symbol("fpa"), ctx.get_manager().mk_family_id("fpa")),
         m_th_rw(ctx.get_manager()),
         m_converter(ctx.get_manager(), m_th_rw),
         m_rw(ctx.get_manager(), m_converter, params_ref()),
@@ -65,7 +65,7 @@ namespace fpa {
             m.inc_ref(e);
             m.inc_ref(res);
 
-            ctx.push(fpa2bv_conversion_trail_elem<euf::solver>(m, m_conversions, e));
+            ctx.push(insert_ref2_map<euf::solver, ast_manager, expr, expr>(m, m_conversions, e, res.get()));
         }
         return res;
     }

src/sat/smt/q_mbi.cpp

@@ -26,8 +26,13 @@ Author:
 namespace q {
 
     mbqi::mbqi(euf::solver& ctx, solver& s): 
-        ctx(ctx), qs(s), m(s.get_manager()), m_model_finder(ctx), m_fresh_trail(m)  {}
+        ctx(ctx), 
-
+        qs(s), 
+        m(s.get_manager()), 
+        m_model_fixer(ctx, qs),
+        m_model_finder(ctx), 
+        m_fresh_trail(m) 
+    {}
 
     void mbqi::restrict_to_universe(expr * sk, ptr_vector<expr> const & universe) {
         SASSERT(!universe.empty());
@@ -222,4 +227,8 @@ namespace q {
         m_max_cex = ctx.get_config().m_mbqi_max_cexs;
     }
 
+    void mbqi::finalize_model(model& mdl) {
+        m_model_fixer(mdl);
+    }
+
 }

src/sat/smt/q_mbi.h

@@ -19,7 +19,7 @@ Author:
 #include "solver/solver.h"
 #include "sat/smt/sat_th.h"
 #include "sat/smt/q_model_finder.h"
-
+#include "sat/smt/q_model_fixer.h"
 
 namespace euf {
     class solver;
@@ -33,13 +33,14 @@ namespace q {
         euf::solver&                           ctx;
         solver&                                qs;
         ast_manager&                           m;
+        model_fixer                            m_model_fixer;
         model_finder                           m_model_finder;
         model_ref                              m_model;
         ref<::solver>                          m_solver;
         obj_map<sort, obj_hashtable<expr>*>    m_fresh;
         scoped_ptr_vector<obj_hashtable<expr>> m_values;
         expr_ref_vector                        m_fresh_trail;
-        unsigned                               m_max_cex{ 10 };
+        unsigned                               m_max_cex{ 1 };
 
         void restrict_to_universe(expr * sk, ptr_vector<expr> const & universe);
         void register_value(expr* e);
@@ -58,6 +59,8 @@ namespace q {
         lbool operator()();
 
         void init_search();
+
+        void finalize_model(model& mdl);
     };
 
 }

src/sat/smt/q_model_finder.cpp

@@ -36,4 +36,8 @@ namespace q {
         
     }
 
+    void model_finder::adjust_model(model& mdl) {
+
+    }
+
 }

src/sat/smt/q_model_finder.h

@@ -37,10 +37,24 @@ namespace q {
 
         model_finder(euf::solver& ctx);
 
+        /**
+         * Compute an instantiation terms for the i'th bound variable in quantifier q.
+         */
         expr_ref inv_term(model& mdl, quantifier* q, unsigned idx, expr* value, unsigned& generation);
 
+        /**
+         * Pre-restrict instantiations of vars, by adding constraints to solver s
+         */
         void restrict_instantiations(::solver& s, model& mdl, quantifier* q, expr_ref_vector const& vars);
 
+        /**
+         * Update model in order to best satisfy quantifiers.
+         * For the array property fragment, update the model
+         * such that the range of functions behaves monotonically 
+         * based on regions over the inputs.
+         */
+        void adjust_model(model& mdl);
+        
     };
 
 }

src/sat/smt/q_model_fixer.cpp

@@ -0,0 +1,198 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    q_model_fixer.cpp
+
+Abstract:
+
+    Model-based quantifier instantiation model-finder plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-10-02
+
+Notes:
+   
+    Derives from smt/smt_model_finder.cpp
+
+--*/
+
+
+#include "ast/for_each_expr.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/bv_decl_plugin.h"
+#include "model/model_macro_solver.h"
+#include "sat/smt/q_model_fixer.h"
+#include "sat/smt/q_solver.h"
+#include "sat/smt/euf_solver.h"
+
+
+namespace q {
+
+    template<typename U>
+    static bool lt(U const& u, expr* x, expr* y) {
+        rational v1, v2;
+        if (u.is_numeral(x, v1) && u.is_numeral(y, v2)) 
+            return v1 < v2;
+        else 
+            return x->get_id() < y->get_id();                            
+    }
+
+    class arith_projection : public projection_function {
+        ast_manager& m;
+        arith_util   a;
+    public:
+        bool operator()(expr* e1, expr* e2) const { return lt(a, e1, e2); }
+        arith_projection(ast_manager& m): m(m), a(m) {}
+        ~arith_projection() override {}
+        void sort(ptr_buffer<expr>& values) override { std::sort(values.begin(), values.end(), *this); }
+        expr* mk_lt(expr* x, expr* y) override { return a.mk_lt(x, y); }
+    };
+
+    class ubv_projection : public projection_function {
+        ast_manager& m;
+        bv_util bvu;
+    public:
+        bool operator()(expr* e1, expr* e2) const { return lt(bvu, e1, e2); }
+        ubv_projection(ast_manager& m): m(m), bvu(m) {}
+        ~ubv_projection() override {}
+        void sort(ptr_buffer<expr>& values) override { std::sort(values.begin(), values.end(), *this); }
+        expr* mk_lt(expr* x, expr* y) override { return m.mk_not(bvu.mk_ule(y, x)); }        
+    };
+
+    model_fixer::model_fixer(euf::solver& ctx, q::solver& qs) :
+        ctx(ctx), m_qs(qs), m(ctx.get_manager()), m_dependencies(m) {}
+
+    void model_fixer::operator()(model& mdl) {
+        ptr_vector<quantifier> univ;
+        for (sat::literal lit : m_qs.universal()) {
+            quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var()));
+            if (ctx.is_relevant(q))
+                univ.push_back(q);
+        }
+        if (univ.empty())
+            return;
+
+        m_dependencies.reset();
+        ptr_vector<quantifier> residue;               
+        
+        simple_macro_solver sms(m, *this);
+        sms(mdl, univ, residue);
+
+        hint_macro_solver hms(m, *this);
+        hms(mdl, univ, residue);
+
+        non_auf_macro_solver nas(m, *this, m_dependencies);
+        nas.set_mbqi_force_template(ctx.get_config().m_mbqi_force_template);
+        nas(mdl, univ, residue);
+
+        univ.append(residue);
+        add_projection_functions(mdl, univ);
+    }
+
+    quantifier_macro_info* model_fixer::operator()(quantifier* q) {
+        quantifier_macro_info* info = nullptr;
+        if (!m_q2info.find(q, info)) {
+            info = alloc(quantifier_macro_info, m, m_qs.flatten(q));
+            m_q2info.insert(q, info);
+            ctx.push(new_obj_trail<euf::solver, quantifier_macro_info>(info));
+            ctx.push(insert_obj_map<euf::solver, quantifier, quantifier_macro_info*>(m_q2info, q));
+        }
+        return info;
+    }
+
+    void model_fixer::add_projection_functions(model& mdl, ptr_vector<quantifier> const& qs) {
+        func_decl_set fns;
+        collect_partial_functions(qs, fns);
+        for (func_decl* f : fns)
+            add_projection_functions(mdl, f);
+    }
+
+    void model_fixer::add_projection_functions(model& mdl, func_decl* f) {
+        // update interpretation of f so that the graph of f is fully determined by the
+        // ground values of its arguments.
+        func_interp* fi = mdl.get_func_interp(f);
+        if (!fi) 
+            return;
+        if (fi->is_constant())
+            return;
+        expr_ref_vector args(m);
+        for (unsigned i = 0; i < f->get_arity(); ++i) 
+            args.push_back(add_projection_function(mdl, f, i));
+        if (!fi->get_else() && fi->num_entries() > 0)
+            fi->set_else(fi->get_entry(ctx.s().rand()(fi->num_entries()))->get_result());
+        bool has_projection = false;
+        for (expr* arg : args)
+            has_projection |= !is_var(arg);
+        if (!has_projection)
+            return;
+        func_interp* new_fi = alloc(func_interp, m, f->get_arity());
+        func_decl* f_new = m.mk_fresh_func_decl(f->get_name(), symbol("aux"), f->get_arity(), f->get_domain(), f->get_range());
+        new_fi->set_else(m.mk_app(f_new, args));
+        mdl.update_func_interp(f, new_fi);
+        mdl.register_decl(f_new, fi);
+    }
+
+    expr_ref model_fixer::add_projection_function(model& mdl, func_decl* f, unsigned idx) {
+        sort* srt = f->get_domain(idx);
+        projection_function* proj = get_projection(srt);
+        if (!proj)
+            return expr_ref(m.mk_var(idx, srt), m);
+        ptr_buffer<expr> values;
+        for (euf::enode* n : ctx.get_egraph().enodes_of(f)) 
+            values.push_back(mdl(n->get_arg(idx)->get_expr()));
+        if (values.empty())
+            return expr_ref(m.mk_var(idx, srt), m);
+        proj->sort(values);
+        unsigned j = 0;
+        for (unsigned i = 0; i < values.size(); ++i) 
+            if (i == 0 || values[i-1] != values[i])
+                values[j++] = values[i];
+        values.shrink(j);
+
+        unsigned sz = values.size();
+        expr_ref var(m.mk_var(0, srt), m);
+        expr_ref pi(values.get(sz-1), m);
+        for (unsigned i = sz - 1; i >= 1; i--) {
+            expr* c = proj->mk_lt(var, values[i]);
+            pi = m.mk_ite(c, values[i - 1], pi);
+        }
+        func_interp* rpi = alloc(func_interp, m, 1);
+        rpi->set_else(pi);
+        func_decl * p = m.mk_fresh_func_decl(1, &srt, srt);
+        mdl.register_decl(p, rpi);       
+        return expr_ref(m.mk_app(p, m.mk_var(idx, srt)), m);
+    }
+
+    projection_function* model_fixer::get_projection(sort* srt) {
+        projection_function* proj = nullptr;
+        if (m_projections.find(srt, proj))
+            return proj;
+        arith_util autil(m);
+        bv_util butil(m);
+        if (autil.is_real(srt) || autil.is_int(srt))
+            proj = alloc(arith_projection, m);
+        else if (butil.is_bv_sort(srt))
+            proj = alloc(ubv_projection, m);
+        // TBD: sbv_projection? FP, ADT projection?
+        if (!proj)
+            return nullptr;
+        m_projections.insert(srt, proj);
+        ctx.push(new_obj_trail<euf::solver, projection_function>(proj));
+        ctx.push(insert_obj_map<euf::solver, sort, projection_function*>(m_projections, srt));
+        return proj;
+    }
+
+    void model_fixer::collect_partial_functions(ptr_vector<quantifier> const& qs, func_decl_set& fns) {
+        for (quantifier* q : qs) {
+            auto* info = (*this)(q);
+            quantifier* flat_q = info->get_flat_q();
+            expr_ref body(flat_q->get_expr(), m);
+            for (expr* t : subterms(body)) 
+                if (is_uninterp(t) && !to_app(t)->is_ground())
+                    fns.insert(to_app(t)->get_decl());           
+        }
+    }
+}

src/sat/smt/q_model_fixer.h

@@ -0,0 +1,78 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    q_model_fixer.h
+
+Abstract:
+
+    Model-based quantifier instantiation model-finder plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-10-02
+
+Notes:
+   
+    Derives from smt/smt_model_finder.cpp
+
+    Contains exclusively functionality that adjusts a model to make it
+    easier to satisfy relevant universally quantified literals.
+
+--*/
+#pragma once
+
+#include "sat/smt/sat_th.h"
+#include "solver/solver.h"
+#include "model/model_macro_solver.h"
+
+namespace euf {
+    class solver;
+}
+
+namespace q {
+
+    class solver;
+
+    typedef obj_hashtable<func_decl> func_decl_set;
+
+    class projection_function {
+    public:
+        virtual ~projection_function() {}
+        virtual void sort(ptr_buffer<expr>& values) = 0;
+        virtual expr* mk_lt(expr* a, expr* b) = 0;
+    };
+
+    class model_fixer : public quantifier2macro_infos {
+        euf::solver&        ctx;      
+        solver&             m_qs;
+        ast_manager&        m;
+        obj_map<quantifier, quantifier_macro_info*> m_q2info;
+        func_decl_dependencies                      m_dependencies;
+        obj_map<sort, projection_function*>         m_projections;
+
+        void add_projection_functions(model& mdl, ptr_vector<quantifier> const& qs);
+        void add_projection_functions(model& mdl, func_decl* f);
+        expr_ref add_projection_function(model& mdl, func_decl* f, unsigned idx);
+        void collect_partial_functions(ptr_vector<quantifier> const& qs, func_decl_set& fns);
+        projection_function* get_projection(sort* srt);
+
+    public:
+
+        model_fixer(euf::solver& ctx, solver& qs);
+        ~model_fixer() override {}
+
+        /**
+         * Update model in order to best satisfy quantifiers.
+         * For the array property fragment, update the model
+         * such that the range of functions behaves monotonically 
+         * based on regions over the inputs.
+         */
+        void operator()(model& mdl);
+
+        quantifier_macro_info* operator()(quantifier* q);
+        
+    };
+
+}

src/sat/smt/q_solver.cpp

@@ -19,13 +19,14 @@ Author:
 #include "sat/smt/q_solver.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/sat_th.h"
-
+#include "ast/normal_forms/pull_quant.h"
+#include "ast/well_sorted.h"
 
 namespace q {
 
     solver::solver(euf::solver& ctx):
-        th_euf_solver(ctx, ctx.get_manager().get_family_id(name())),
+        th_euf_solver(ctx, symbol("quant"), ctx.get_manager().get_family_id(symbol("quant"))),
-        m_mbqi(ctx, *this)
+        m_mbqi(ctx,  *this)
     {}
 
     void solver::asserted(sat::literal l) {
@@ -43,10 +44,12 @@ namespace q {
     }
 
     sat::check_result solver::check() {
-        switch (m_mbqi()) {
+        if (ctx.get_config().m_mbqi) {
-        case l_true: return sat::check_result::CR_DONE;
+            switch (m_mbqi()) {
-        case l_false: return sat::check_result::CR_CONTINUE;
+            case l_true: return sat::check_result::CR_DONE;
-        case l_undef: return sat::check_result::CR_GIVEUP;
+            case l_false: return sat::check_result::CR_CONTINUE;
+            case l_undef: return sat::check_result::CR_GIVEUP;
+            }
         }
         return sat::check_result::CR_GIVEUP;
     }
@@ -117,4 +120,27 @@ namespace q {
         mk_var(ctx.get_egraph().find(e));
         return lit;
     }
+
+    void solver::finalize_model(model& mdl) {
+        m_mbqi.finalize_model(mdl);
+    }
+
+    quantifier* solver::flatten(quantifier* q) {
+        quantifier* q_flat = nullptr;
+        if (!has_quantifiers(q->get_expr())) 
+            return q;
+        if (m_flat.find(q, q_flat))
+            return q_flat;
+        proof_ref pr(m);
+        expr_ref  new_q(m);
+        pull_quant pull(m);
+        pull(q, new_q, pr);
+        SASSERT(is_well_sorted(m, new_q));
+        q_flat = to_quantifier(new_q);
+        m.inc_ref(q_flat);
+        m.inc_ref(q);
+        m_flat.insert(q, q_flat);
+        ctx.push(insert_ref2_map<euf::solver, ast_manager, quantifier, quantifier>(m, m_flat, q, q_flat));
+        return q_flat;
+    }
 }

src/sat/smt/q_solver.h

@@ -30,6 +30,7 @@ namespace q {
     class solver : public euf::th_euf_solver {
 
         typedef obj_map<quantifier, sat::literal> skolem_table;
+        typedef obj_map<quantifier, quantifier*> flat_table;
         friend class mbqi;
 
         struct stats {
@@ -42,6 +43,7 @@ namespace q {
         mbqi                   m_mbqi;
 
         skolem_table           m_skolems;
+        flat_table             m_flat;
         sat::literal_vector    m_universal;
 
         sat::literal skolemize(quantifier* q);
@@ -51,7 +53,6 @@ namespace q {
 
         solver(euf::solver& ctx);
         ~solver() override {}
-        static char const* name() { return "quant"; }
         bool is_external(sat::bool_var v) override { return false; }
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override {}
         void asserted(sat::literal l) override;
@@ -67,7 +68,10 @@ namespace q {
         void internalize(expr* e, bool redundant) override { UNREACHABLE(); }
         euf::theory_var mk_var(euf::enode* n) override;
         void init_search() override;
+        void finalize_model(model& mdl) override;
 
         ast_manager& get_manager() { return m; }
+        sat::literal_vector const& universal() const { return m_universal; }
+        quantifier* flatten(quantifier* q);
     };
 }

src/sat/smt/sat_th.cpp

@@ -52,8 +52,8 @@ namespace euf {
         return true;
     }
 
-    th_euf_solver::th_euf_solver(euf::solver& ctx, euf::theory_id id):
+    th_euf_solver::th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id):
-        th_solver(ctx.get_manager(), id),
+        th_solver(ctx.get_manager(), name, id),
         ctx(ctx)
     {}
 

src/sat/smt/sat_th.h

@@ -97,7 +97,7 @@ namespace euf {
     protected:
         ast_manager &       m;
     public:
-        th_solver(ast_manager& m, euf::theory_id id): extension(id), m(m) {}
+        th_solver(ast_manager& m, symbol const& name, euf::theory_id id): extension(name, id), m(m) {}
 
         virtual th_solver* clone(sat::solver* s, euf::solver& ctx) = 0;  
 
@@ -158,7 +158,7 @@ namespace euf {
         }
 
     public:
-        th_euf_solver(euf::solver& ctx, euf::theory_id id);
+        th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id);
         virtual ~th_euf_solver() {}
         virtual theory_var mk_var(enode * n);
         unsigned get_num_vars() const { return m_var2enode.size();}

src/sat/smt/user_solver.cpp

@@ -21,7 +21,7 @@ Author:
 namespace user {
 
     solver::solver(euf::solver& ctx) :
-        th_euf_solver(ctx, ctx.get_manager().mk_family_id("user"))
+        th_euf_solver(ctx, symbol("user"), ctx.get_manager().mk_family_id("user"))
     {}
 
     solver::~solver() {

src/smt/smt_model_checker.h

@@ -54,7 +54,7 @@ namespace smt {
         obj_map<expr, expr *>                       m_value2expr;
         expr_ref_vector                             m_fresh_exprs;
 
-        friend class instantiation_set;
+        friend class model_instantiation_set;
 
         void init_aux_context();
         void init_value2expr();

src/smt/smt_model_finder.h

@@ -47,9 +47,12 @@ Revision History:
 
 #include "ast/ast.h"
 #include "ast/func_decl_dependencies.h"
+#include "model/model_macro_solver.h"
 #include "smt/proto_model/proto_model.h"
 #include "tactic/tactic_exception.h"
 
+class model_instantiation_set;
+
 namespace smt {
     class context;
     
@@ -63,13 +66,10 @@ namespace smt {
         class instantiation_set;
     };
         
-    class model_finder {
+    class model_finder : public quantifier2macro_infos {
         typedef mf::quantifier_analyzer        quantifier_analyzer;
         typedef mf::quantifier_info            quantifier_info;
         typedef mf::auf_solver                 auf_solver;
-        typedef mf::simple_macro_solver        simple_macro_solver;
-        typedef mf::hint_solver                hint_solver;
-        typedef mf::non_auf_macro_solver       non_auf_macro_solver;
         typedef mf::instantiation_set          instantiation_set;
 
         ast_manager &                          m;
@@ -79,9 +79,6 @@ namespace smt {
         obj_map<quantifier, quantifier_info *> m_q2info;
         ptr_vector<quantifier>                 m_quantifiers;
         func_decl_dependencies                 m_dependencies;
-        scoped_ptr<simple_macro_solver>        m_sm_solver;
-        scoped_ptr<hint_solver>                m_hint_solver;
-        scoped_ptr<non_auf_macro_solver>       m_nm_solver;
         
         struct scope {
             unsigned                           m_quantifiers_lim;
@@ -105,7 +102,7 @@ namespace smt {
 
     public:
         model_finder(ast_manager & m);
-        ~model_finder();
+        ~model_finder() override;
         void set_context(context * ctx);
         
         void register_quantifier(quantifier * q);
@@ -122,6 +119,9 @@ namespace smt {
         void restart_eh();
 
         void checkpoint(char const* component);
+
+        quantifier_macro_info* operator()(quantifier* q);
+
     };
 };
 

src/smt/theory_fpa.cpp

@@ -188,7 +188,7 @@ namespace smt {
             m_conversions.insert(e, res);
             m.inc_ref(e);
             m.inc_ref(res);
-            m_trail_stack.push(fpa2bv_conversion_trail_elem<theory_fpa>(m, m_conversions, e));
+            m_trail_stack.push(insert_ref2_map<theory_fpa, ast_manager, expr, expr>(m, m_conversions, e, res.get()));
         }
 
         return res;

src/smt/user_propagator.cpp

@@ -78,6 +78,10 @@ void user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits,
     if (!m_fixed_eh)
         return;
     force_push();
+    if (m_fixed.contains(v))
+        return;
+    m_fixed.insert(v);
+    ctx.push_trail(insert_map<context, uint_set, unsigned>(m_fixed, v));
     m_id2justification.setx(v, literal_vector(num_lits, jlits), literal_vector());
     m_fixed_eh(m_user_context, this, v, value);
 }

src/smt/user_propagator.h

@@ -22,6 +22,7 @@ Notes:
 
 #pragma once
 
+#include "util/uint_set.h"
 #include "smt/smt_theory.h"
 #include "solver/solver.h"
 
@@ -57,6 +58,7 @@ namespace smt {
         solver::eq_eh_t        m_diseq_eh;
         solver::context_obj*   m_api_context { nullptr };
         unsigned               m_qhead { 0 };
+        uint_set               m_fixed;
         vector<prop_info>      m_prop;
         unsigned_vector        m_prop_lim;
         vector<literal_vector> m_id2justification;

src/util/trail.h

@@ -192,6 +192,18 @@ public:
     virtual void undo(Ctx & ctx) { m_map.remove(m_obj); m.dec_ref(m_obj); }
 };
 
+template<typename Ctx, typename Mgr, typename D, typename R>
+class insert_ref2_map : public trail<Ctx> {
+    Mgr&           m;
+    obj_map<D,R*>&  m_map;
+    D*             m_obj;
+    R*             m_val;
+public:
+    insert_ref2_map(Mgr& m, obj_map<D,R*>& t, D*o, R*r) : m(m), m_map(t), m_obj(o), m_val(r) {}
+    virtual ~insert_ref2_map() {}
+    virtual void undo(Ctx & ctx) { m_map.remove(m_obj); m.dec_ref(m_obj); m.dec_ref(m_val); }
+};
+
 
 template<typename Ctx, typename V>
 class push_back_vector : public trail<Ctx> {