Reorganizing the code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/model/func_interp.cpp

@@ -0,0 +1,360 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    func_interp.cpp
+
+Abstract:
+    See func_interp.h
+
+Author:
+
+    Leonardo de Moura (leonardo) 2010-12-30.
+
+Revision History:
+
+--*/
+#include"func_interp.h"
+#include"simplifier.h"
+#include"basic_simplifier_plugin.h"
+#include"var_subst.h"
+#include"obj_hashtable.h"
+#include"ast_pp.h"
+#include"ast_smt2_pp.h"
+
+func_entry::func_entry(ast_manager & m, unsigned arity, expr * const * args, expr * result):
+    m_args_are_values(true),
+    m_result(result) {
+    SASSERT(is_ground(result));
+    m.inc_ref(result);
+    for (unsigned i = 0; i < arity; i++) {
+        expr * arg = args[i];
+        SASSERT(is_ground(arg));
+        if (!m.is_value(arg))
+            m_args_are_values = false;
+        m.inc_ref(arg);
+        m_args[i] = arg;
+    }
+}
+
+func_entry * func_entry::mk(ast_manager & m, unsigned arity, expr * const * args, expr * result) {
+    small_object_allocator & allocator = m.get_allocator();
+    unsigned sz = get_obj_size(arity);
+    void * mem  = allocator.allocate(sz);
+    return new (mem) func_entry(m, arity, args, result);
+}
+
+void func_entry::set_result(ast_manager & m, expr * r) {
+    m.inc_ref(r);
+    m.dec_ref(m_result);
+    m_result = r;
+}
+
+bool func_entry::eq_args(unsigned arity, expr * const * args) const {
+    unsigned i = 0;
+    for (; i < arity; i++) {
+        if (m_args[i] != args[i])
+            return false;
+    }
+    return true;
+}
+
+void func_entry::deallocate(ast_manager & m, unsigned arity) {
+    for (unsigned i = 0; i < arity; i++) {
+        m.dec_ref(m_args[i]);
+    }
+    m.dec_ref(m_result);
+    small_object_allocator & allocator = m.get_allocator();
+    unsigned sz = get_obj_size(arity);
+    allocator.deallocate(sz, this);
+}
+
+func_interp::func_interp(ast_manager & m, unsigned arity):
+    m_manager(m),
+    m_arity(arity),
+    m_else(0),
+    m_args_are_values(true),
+    m_interp(0) {
+}
+
+func_interp::~func_interp() {
+    ptr_vector<func_entry>::iterator it  = m_entries.begin();
+    ptr_vector<func_entry>::iterator end = m_entries.end();
+    for (; it != end; ++it) {
+        func_entry * curr = *it;
+        curr->deallocate(m_manager, m_arity);
+    }
+    m_manager.dec_ref(m_else);
+    m_manager.dec_ref(m_interp);
+}
+
+func_interp * func_interp::copy() const {
+    func_interp * new_fi = alloc(func_interp, m_manager, m_arity);
+
+    ptr_vector<func_entry>::const_iterator it  = m_entries.begin();
+    ptr_vector<func_entry>::const_iterator end = m_entries.end();
+    for (; it != end; ++it) {
+        func_entry * curr = *it;
+        new_fi->insert_new_entry(curr->get_args(), curr->get_result());
+    }
+    new_fi->set_else(m_else);
+    return new_fi;
+}
+
+void func_interp::reset_interp_cache() {
+    m_manager.dec_ref(m_interp);
+    m_interp = 0;
+}
+    
+void func_interp::set_else(expr * e) {
+    reset_interp_cache();
+    m_manager.inc_ref(e);
+    m_manager.dec_ref(m_else);
+    m_else = e;
+}
+
+/**
+   \brief Return true if the interpretation represents the constant function.
+*/
+bool func_interp::is_constant() const {
+    if (is_partial())
+        return false;
+    if (!is_ground(m_else))
+        return false;
+    ptr_vector<func_entry>::const_iterator it  = m_entries.begin();
+    ptr_vector<func_entry>::const_iterator end = m_entries.end();
+    for (; it != end; ++it) {
+        func_entry * curr = *it;
+        if (curr->get_result() != m_else)
+            return false;
+    }
+    return true;
+}
+
+/**
+   \brief Return a func_entry e such that e.m_args[i] == args[i] for all i in [0, m_arity).
+   If such entry does not exist then return 0, and store set
+   args_are_values to true if for all entries e e.args_are_values() is true.
+*/
+func_entry * func_interp::get_entry(expr * const * args) const {
+    ptr_vector<func_entry>::const_iterator it  = m_entries.begin();
+    ptr_vector<func_entry>::const_iterator end = m_entries.end();
+    for (; it != end; ++it) {
+        func_entry * curr = *it;
+        if (curr->eq_args(m_arity, args))
+            return curr;
+    }
+    return 0;
+}
+
+void func_interp::insert_entry(expr * const * args, expr * r) {
+    reset_interp_cache();
+    func_entry * entry = get_entry(args); 
+    if (entry != 0) {
+        entry->set_result(m_manager, r);
+        return;
+    }
+    insert_new_entry(args, r);
+}
+
+void func_interp::insert_new_entry(expr * const * args, expr * r) {
+    reset_interp_cache();
+    CTRACE("func_interp_bug", get_entry(args) != 0,
+           for (unsigned i = 0; i < m_arity; i++) {
+               tout << mk_ismt2_pp(args[i], m_manager) << "\n";
+           }
+           tout << "Old: " << mk_ismt2_pp(get_entry(args)->m_result, m_manager) << "\n";
+           tout << "New: " << mk_ismt2_pp(r, m_manager) << "\n";);
+    SASSERT(get_entry(args) == 0);
+    func_entry * new_entry = func_entry::mk(m_manager, m_arity, args, r);
+    if (!new_entry->args_are_values())
+        m_args_are_values = false;
+    m_entries.push_back(new_entry);
+}
+
+bool func_interp::eval_else(expr * const * args, expr_ref & result) const {
+    if (m_else == 0)
+        return false;
+    var_subst s(m_manager, false);
+    SASSERT(!s.std_order()); // (VAR 0) <- args[0], (VAR 1) <- args[1], ...
+    s(m_else, m_arity, args, result);
+    return true;
+}
+
+/**
+   \brief Store in r the result of applying args to this function.
+   Return true in case of success.
+   The function may fail if m_else == 0.
+*/
+bool func_interp::eval(simplifier & s, expr * const * args, expr_ref & result) {
+    bool actuals_are_values = true;
+    
+    if (!m_entries.empty()) {
+        for (unsigned i = 0; actuals_are_values && i < m_arity; i++) {
+            actuals_are_values = m_manager.is_value(args[i]);
+        }
+    }
+
+    func_entry * entry = get_entry(args);
+    if (entry != 0) {
+        result = entry->get_result();
+        TRACE("func_interp", tout << "found entry for: "; 
+              for(unsigned i = 0; i < m_arity; i++) 
+                 tout << mk_pp(args[i], m_manager) << " "; 
+              tout << "\nresult: " << mk_pp(result, m_manager) << "\n";);
+        return true;
+    }
+    
+    TRACE("func_interp", tout << "failed to find entry for: "; 
+          for(unsigned i = 0; i < m_arity; i++) 
+             tout << mk_pp(args[i], m_manager) << " "; 
+          tout << "\nis partial: " << is_partial() << "\n";);
+    
+    if (!eval_else(args, result)) {
+        TRACE("func_interp", tout << "function is partial, failed to evaluate\n";);
+        return false;
+    }
+    
+    if (actuals_are_values && m_args_are_values) {
+        // cheap case... we are done
+        return true;
+    }
+
+
+    // build symbolic result... the actuals may be equal to the args of one of the entries.
+    basic_simplifier_plugin * bs = static_cast<basic_simplifier_plugin*>(s.get_plugin(m_manager.get_basic_family_id()));
+    ptr_vector<func_entry>::iterator it  = m_entries.begin();
+    ptr_vector<func_entry>::iterator end = m_entries.end();
+    for (; it != end; ++it) {
+        func_entry * curr = *it;
+        SASSERT(!curr->eq_args(m_arity, args));
+        if (!actuals_are_values || !curr->args_are_values()) {
+            expr_ref_buffer eqs(m_manager);
+            unsigned i = m_arity;
+            while (i > 0) {
+                --i;
+                expr_ref new_eq(m_manager);
+                bs->mk_eq(curr->get_arg(i), args[i], new_eq);
+                eqs.push_back(new_eq);
+            }
+            SASSERT(eqs.size() == m_arity);
+            expr_ref new_cond(m_manager);
+            bs->mk_and(eqs.size(), eqs.c_ptr(), new_cond);
+            bs->mk_ite(new_cond, curr->get_result(), result, result);
+        }
+    }
+    return true;
+}
+
+/**
+   \brief Return the result with the maximal number of occurrencies in m_entries.
+*/
+expr * func_interp::get_max_occ_result() const {
+    if (m_entries.empty())
+        return 0;
+    obj_map<expr, unsigned> num_occs;
+    expr *   r_max = 0;
+    unsigned max   = 0;
+    ptr_vector<func_entry>::const_iterator it  = m_entries.begin();
+    ptr_vector<func_entry>::const_iterator end = m_entries.end();
+    for (; it != end; ++it) {
+        func_entry * curr = *it;
+        expr * r = curr->get_result();
+        unsigned occs = 0; 
+        num_occs.find(r, occs);
+        occs++;
+        num_occs.insert(r, occs);
+        if (occs > max) {
+            max   = occs;
+            r_max = r;
+        }
+    }
+    return r_max;
+}
+
+/**
+   \brief Remove entries e such that e.get_result() == m_else.
+*/
+void func_interp::compress() {
+    if (m_else == 0 || m_entries.empty())
+        return; // nothing to be done
+    if (!is_ground(m_else))
+        return; // forall entries e in m_entries e.get_result() is ground
+    unsigned i = 0;
+    unsigned j = 0;
+    unsigned sz = m_entries.size();
+    m_args_are_values = true;
+    for (; i < sz; i++) {
+        func_entry * curr = m_entries[i];
+        if (curr->get_result() != m_else) {
+            m_entries[j] = curr;
+            j++;
+            if (!curr->args_are_values())
+                m_args_are_values = false;
+        }
+        else {
+            curr->deallocate(m_manager, m_arity);
+        }
+    }
+    if (j < sz) {
+        reset_interp_cache();
+        m_entries.shrink(j);
+    }
+}
+
+expr * func_interp::get_interp_core() const {
+    if (m_else == 0)
+        return 0;
+    expr * r = m_else;
+    ptr_buffer<expr> vars;
+    ptr_vector<func_entry>::const_iterator it  = m_entries.begin();
+    ptr_vector<func_entry>::const_iterator end = m_entries.end();
+    for (; it != end; ++it) {
+        func_entry * curr = *it;
+        if (vars.empty()) {
+            for (unsigned i = 0; i < m_arity; i++) {
+                vars.push_back(m_manager.mk_var(i, m_manager.get_sort(curr->get_arg(i))));
+            }
+        }
+        ptr_buffer<expr> eqs;
+        for (unsigned i = 0; i < m_arity; i++) {
+            eqs.push_back(m_manager.mk_eq(vars[i], curr->get_arg(i)));
+        }
+        SASSERT(eqs.size() == m_arity);
+        expr * cond;
+        if (m_arity == 1)
+            cond = eqs.get(0);
+        else
+            cond = m_manager.mk_and(eqs.size(), eqs.c_ptr());
+        r = m_manager.mk_ite(cond, curr->get_result(), r);
+    }
+    return r;
+}
+
+expr * func_interp::get_interp() const {
+    if (m_interp != 0)
+        return m_interp;
+    expr * r = get_interp_core();
+    if (r != 0) {
+        const_cast<func_interp*>(this)->m_interp = r;
+        m_manager.inc_ref(m_interp);
+    }
+    return r;
+}
+
+func_interp * func_interp::translate(ast_translation & translator) const {
+    func_interp * new_fi = alloc(func_interp, m_manager, m_arity);
+
+    ptr_vector<func_entry>::const_iterator it  = m_entries.begin();
+    ptr_vector<func_entry>::const_iterator end = m_entries.end();
+    for (; it != end; ++it) {
+        func_entry * curr = *it;        
+        ptr_buffer<expr> new_args;
+        for (unsigned i=0; i<m_arity; i++)
+            new_args.push_back(translator(curr->get_arg(i)));
+        new_fi->insert_new_entry(new_args.c_ptr(), translator(curr->get_result()));
+    }
+    new_fi->set_else(translator(m_else));
+    return new_fi;
+}

src/model/func_interp.h

@@ -0,0 +1,114 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    func_interp.h
+
+Abstract:
+
+    Support for function graphs (aka interpretations for functions).
+    They are used during model construction, and for evaluating expressions
+    modulo a model.
+
+    Main goal: Remove some code duplication and make the evaluator more efficient.
+    
+    Example of code duplication that existed in Z3:
+      - smt_model_generator was creating func_values that were essentially partial func_interps
+      - smt_model_generator was creating if-then-else (lambda) exprs representing func_values
+      - the model object was converting these lambdas back into func_graphs (a limited version of func_interps).
+      - the smt_model_finder needs to manipulate func_interps, but the func_values in smt_model_generator
+        were private and too restrictive.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2010-12-30.
+
+Revision History:
+
+--*/
+#ifndef _FUNC_INTERP_H
+#define _FUNC_INTERP_H
+
+#include"ast.h"
+#include"ast_translation.h"
+
+class func_interp;
+class simplifier;
+
+class func_entry {
+    bool   m_args_are_values; //!< true if is_value(m_args[i]) is true for all i in [0, arity)
+
+    // m_result and m_args[i] must be ground terms.
+    
+    expr * m_result;
+    expr * m_args[];
+
+    static unsigned get_obj_size(unsigned arity) { return sizeof(func_entry) + arity * sizeof(expr*); }
+    func_entry(ast_manager & m, unsigned arity, expr * const * args, expr * result);
+    
+    friend class func_interp;
+    
+    void set_result(ast_manager & m, expr * r);
+    bool args_are_values() const { return m_args_are_values; }
+    
+public:
+    static func_entry * mk(ast_manager & m, unsigned arity, expr * const * args, expr * result);
+    void deallocate(ast_manager & m, unsigned arity);
+    expr * get_result() const { return m_result; }
+    expr * get_arg(unsigned idx) const { return m_args[idx]; }
+    expr * const * get_args() const { return m_args; }
+    /**
+       \brief Return true if m_args[i] == args[i] for all i in [0, arity)
+    */
+    bool eq_args(unsigned arity, expr * const * args) const;
+};
+
+class func_interp {
+    ast_manager &          m_manager;
+    unsigned               m_arity;
+    ptr_vector<func_entry> m_entries;
+    expr *                 m_else;
+    bool                   m_args_are_values; //!< true if forall e in m_entries e.args_are_values() == true
+    
+    expr *                 m_interp; //!< cache for representing the whole interpretation as a single expression (it uses ite terms).
+
+    void reset_interp_cache();
+
+    expr * get_interp_core() const;
+
+public:
+    func_interp(ast_manager & m, unsigned arity);
+    ~func_interp();
+
+    func_interp * copy() const;
+    
+    unsigned get_arity() const { return m_arity; }
+
+    bool is_partial() const { return m_else == 0; }
+    // A function interpretation is said to be simple if m_else is ground.
+    bool is_simple() const { return is_partial() || is_ground(m_else); }
+
+    bool is_constant() const;
+
+    expr * get_else() const { return m_else; }
+    void set_else(expr * e);
+    
+    void insert_entry(expr * const * args, expr * r);
+    void insert_new_entry(expr * const * args, expr * r);
+    func_entry * get_entry(expr * const * args) const;
+    bool eval_else(expr * const * args, expr_ref & result) const;
+    bool eval(simplifier & s, expr * const * args, expr_ref & result);
+    unsigned num_entries() const { return m_entries.size(); }
+    func_entry const * const * get_entries() const { return m_entries.c_ptr(); }
+    func_entry const * get_entry(unsigned idx) const { return m_entries[idx]; }
+
+    expr * get_max_occ_result() const;
+    void compress();
+
+    expr * get_interp() const;
+
+    func_interp * translate(ast_translation & translator) const;
+};
+
+#endif

src/model/model.cpp

@@ -0,0 +1,234 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-04-30.
+
+Revision History:
+
+--*/
+#include"model.h"
+#include"ast_pp.h"
+#include"ast_ll_pp.h"
+#include"var_subst.h"
+#include"front_end_params.h"
+#include"array_decl_plugin.h"
+#include"well_sorted.h"
+#include"used_symbols.h"
+#include"model_evaluator.h"
+
+model::model(ast_manager & m): 
+    model_core(m) {
+}
+
+model::~model() {
+    decl2expr::iterator it1  = m_interp.begin();
+    decl2expr::iterator end1 = m_interp.end();
+    for (; it1 != end1; ++it1) {
+        m_manager.dec_ref(it1->m_key);
+        m_manager.dec_ref(it1->m_value);
+    }
+
+    decl2finterp::iterator it2  = m_finterp.begin();
+    decl2finterp::iterator end2 = m_finterp.end();
+    for (; it2 != end2; ++it2) {
+        m_manager.dec_ref(it2->m_key);
+        dealloc(it2->m_value);
+    }
+    
+    sort2universe::iterator it3  = m_usort2universe.begin();
+    sort2universe::iterator end3 = m_usort2universe.end();
+    for (; it3 != end3; ++it3) {
+        m_manager.dec_ref(it3->m_key);
+        m_manager.dec_array_ref(it3->m_value->size(), it3->m_value->c_ptr());
+        dealloc(it3->m_value);
+    }
+}
+
+void model::register_decl(func_decl * d, expr * v) {
+    SASSERT(d->get_arity() == 0);
+    decl2expr::obj_map_entry * entry = m_interp.insert_if_not_there2(d, 0);
+    if (entry->get_data().m_value == 0) {
+        // new entry
+        m_decls.push_back(d);
+        m_const_decls.push_back(d);
+        m_manager.inc_ref(d);
+        m_manager.inc_ref(v);
+        entry->get_data().m_value = v;
+    }
+    else {
+        // replacing entry
+        m_manager.inc_ref(v);
+        m_manager.dec_ref(entry->get_data().m_value);
+        entry->get_data().m_value = v;
+    }
+}
+
+void model::register_decl(func_decl * d, func_interp * fi) {
+    SASSERT(d->get_arity() > 0);
+    decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0);
+    if (entry->get_data().m_value == 0) {
+        // new entry
+        m_decls.push_back(d);
+        m_func_decls.push_back(d);
+        m_manager.inc_ref(d);
+        entry->get_data().m_value = fi;
+    }
+    else {
+        // replacing entry
+        if (fi != entry->get_data().m_value)
+            dealloc(entry->get_data().m_value);
+        entry->get_data().m_value = fi;
+    }
+}
+
+
+void model::copy_const_interps(model const & source) {
+    decl2expr::iterator it1  = source.m_interp.begin();
+    decl2expr::iterator end1 = source.m_interp.end();
+    for (; it1 != end1; ++it1) {
+        register_decl(it1->m_key, it1->m_value);
+    }
+}
+
+void model::copy_func_interps(model const & source) {
+    decl2finterp::iterator it2  = source.m_finterp.begin();
+    decl2finterp::iterator end2 = source.m_finterp.end();
+    for (; it2 != end2; ++it2) {
+        register_decl(it2->m_key, it2->m_value->copy());
+    }
+}
+ 
+void model::copy_usort_interps(model const & source) {
+    sort2universe::iterator it3  = source.m_usort2universe.begin();
+    sort2universe::iterator end3 = source.m_usort2universe.end();
+    for (; it3 != end3; ++it3) {
+        register_usort(it3->m_key, it3->m_value->size(), it3->m_value->c_ptr());
+    }
+}
+
+model * model::copy() const {
+    model * m = alloc(model, m_manager);
+    
+    m->copy_const_interps(*this);
+    m->copy_func_interps(*this);
+    m->copy_usort_interps(*this);
+
+    return m;
+}
+
+// Remark: eval is for backward compatibility. We should use model_evaluator.
+bool model::eval(expr * e, expr_ref & result, bool model_completion) {
+    model_evaluator ev(*this);
+    ev.set_model_completion(model_completion);
+    try {
+        ev(e, result);
+        return true;
+    }
+    catch (model_evaluator_exception &) {
+        return false;
+    }
+}
+
+struct model::value_proc : public some_value_proc {
+    model & m_model;
+    value_proc(model & m):m_model(m) {}
+    virtual expr * operator()(sort * s) {
+        ptr_vector<expr> * u = 0;
+        if (m_model.m_usort2universe.find(s, u)) {
+            if (u->size() > 0)
+                return u->get(0);
+        }
+        return 0;
+    }
+};
+
+expr * model::get_some_value(sort * s) {
+    value_proc p(*this);
+    return m_manager.get_some_value(s, &p);
+}
+
+ptr_vector<expr> const & model::get_universe(sort * s) const {
+    ptr_vector<expr> * u = 0;
+    m_usort2universe.find(s, u);
+    SASSERT(u != 0);
+    return *u;
+}
+
+bool model::has_uninterpreted_sort(sort * s) const {
+    ptr_vector<expr> * u = 0;
+    m_usort2universe.find(s, u);
+    return u != 0;
+}
+
+unsigned model::get_num_uninterpreted_sorts() const { 
+    return m_usorts.size(); 
+}
+
+sort * model::get_uninterpreted_sort(unsigned idx) const { 
+    return m_usorts[idx]; 
+}
+
+void model::register_usort(sort * s, unsigned usize, expr * const * universe) {
+    SASSERT(m_manager.is_uninterp(s));
+    sort2universe::obj_map_entry * entry = m_usort2universe.insert_if_not_there2(s, 0);
+    m_manager.inc_array_ref(usize, universe);
+    if (entry->get_data().m_value == 0) {
+        // new entry
+        m_usorts.push_back(s);
+        m_manager.inc_ref(s);
+        ptr_vector<expr> * new_u = alloc(ptr_vector<expr>);
+        new_u->append(usize, universe);
+        entry->get_data().m_value = new_u;
+    }
+    else {
+        // updating
+        ptr_vector<expr> * u = entry->get_data().m_value;
+        SASSERT(u);
+        m_manager.dec_array_ref(u->size(), u->c_ptr());
+        u->append(usize, universe);
+    }
+}
+
+model * model::translate(ast_translation & translator) const {
+    model * res = alloc(model, translator.to());    
+
+    // Translate const interps
+    decl2expr::iterator it1  = m_interp.begin();
+    decl2expr::iterator end1 = m_interp.end();
+    for (; it1 != end1; ++it1) {
+        res->register_decl(translator(it1->m_key), translator(it1->m_value));
+    }
+
+    // Translate func interps
+    decl2finterp::iterator it2  = m_finterp.begin();
+    decl2finterp::iterator end2 = m_finterp.end();
+    for (; it2 != end2; ++it2) {
+        func_interp * fi = it2->m_value;
+        res->register_decl(translator(it2->m_key), fi->translate(translator));
+    }
+    
+    // Translate usort interps
+    sort2universe::iterator it3  = m_usort2universe.begin();
+    sort2universe::iterator end3 = m_usort2universe.end();
+    for (; it3 != end3; ++it3) {
+        ptr_vector<expr> new_universe;
+        for (unsigned i=0; i<it3->m_value->size(); i++)
+            new_universe.push_back(translator(it3->m_value->get(i)));
+        res->register_usort(translator(it3->m_key), 
+                            new_universe.size(), 
+                            new_universe.c_ptr());
+    }
+
+    return res;
+}
+

src/model/model.h

@@ -0,0 +1,69 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model.h
+
+Abstract:
+
+    Model for satisfiable formulas
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-04-30.
+
+Revision History:
+
+--*/
+#ifndef _MODEL_H_
+#define _MODEL_H_
+
+#include"model_core.h"
+#include"ref.h"
+#include"ast_translation.h"
+
+class model : public model_core {
+protected:
+    typedef obj_map<sort, ptr_vector<expr>*> sort2universe;
+    
+    ptr_vector<sort>              m_usorts;
+    sort2universe                 m_usort2universe;
+    struct value_proc;
+
+public:
+    model(ast_manager & m);
+    virtual ~model(); 
+
+    void copy_func_interps(model const & source);
+    void copy_const_interps(model const & source);
+    void copy_usort_interps(model const & source);
+
+    model * copy() const;
+    
+    bool eval(func_decl * f, expr_ref & r) const { return model_core::eval(f, r); }
+    bool eval(expr * e, expr_ref & result, bool model_completion = false);
+    
+    expr * get_some_value(sort * s);
+
+    virtual ptr_vector<expr> const & get_universe(sort * s) const;
+    virtual unsigned get_num_uninterpreted_sorts() const;
+    virtual sort * get_uninterpreted_sort(unsigned idx) const;
+    bool has_uninterpreted_sort(sort * s) const; 
+
+    //
+    // Primitives for building models
+    //
+    void register_decl(func_decl * d, expr * v);
+    void register_decl(func_decl * f, func_interp * fi);
+    void register_usort(sort * s, unsigned usize, expr * const * universe);
+
+    // Model translation
+    //
+    model * translate(ast_translation & translator) const;
+};
+
+typedef ref<model> model_ref;
+
+#endif /* _MODEL_H_ */
+

src/model/model_core.cpp

@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_core.cpp
+
+Abstract:
+
+    Base class for models.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-04-30.
+
+Revision History:
+
+--*/
+#include"model_core.h"
+
+bool model_core::eval(func_decl* f, expr_ref & r) const {
+    if (f->get_arity() == 0) {
+        r = get_const_interp(f);
+        return r != 0;
+    }
+    else {
+        func_interp * fi = get_func_interp(f);
+        if (fi != 0) {
+            r = fi->get_interp();
+            return r != 0;
+        }
+        return false;
+    }
+}

src/model/model_core.h

@@ -0,0 +1,73 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_core.h
+
+Abstract:
+
+    Base class for models.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-04-30.
+
+Revision History:
+
+--*/
+#ifndef _MODEL_CORE_H
+#define _MODEL_CORE_H
+
+#include"ast.h"
+#include"obj_hashtable.h"
+#include"func_interp.h"
+
+class model_core {
+protected:
+    typedef obj_map<func_decl, expr *>       decl2expr;
+    typedef obj_map<func_decl, func_interp*> decl2finterp;
+    ast_manager &                 m_manager;
+    unsigned                      m_ref_count;
+    decl2expr                     m_interp;      //!< interpretation for uninterpreted constants
+    decl2finterp                  m_finterp;     //!< interpretation for uninterpreted functions
+    ptr_vector<func_decl>         m_decls;       //!< domain of m_interp
+    ptr_vector<func_decl>         m_const_decls; 
+    ptr_vector<func_decl>         m_func_decls;  
+    
+public:
+    model_core(ast_manager & m):m_manager(m), m_ref_count(0) {}
+    virtual ~model_core() {}
+
+    ast_manager & get_manager() const { return m_manager; }
+
+    unsigned get_num_decls() const { return m_decls.size(); }
+    func_decl * get_decl(unsigned i) const { return m_decls[i]; }
+    bool has_interpretation(func_decl * d) const { return m_interp.contains(d) || m_finterp.contains(d); }
+    expr * get_const_interp(func_decl * d) const { expr * v; return m_interp.find(d, v) ? v : 0; }
+    func_interp * get_func_interp(func_decl * d) const { func_interp * fi; return m_finterp.find(d, fi) ? fi : 0; }
+
+    bool eval(func_decl * f, expr_ref & r) const;
+
+    unsigned get_num_constants() const { return m_const_decls.size(); }
+    unsigned get_num_functions() const { return m_func_decls.size(); }
+    func_decl * get_constant(unsigned i) const { return m_const_decls[i]; }
+    func_decl * get_function(unsigned i) const { return m_func_decls[i]; }
+
+    virtual ptr_vector<expr> const & get_universe(sort * s) const = 0;
+    virtual unsigned get_num_uninterpreted_sorts() const = 0;
+    virtual sort * get_uninterpreted_sort(unsigned idx) const = 0;
+
+    //
+    // Reference counting
+    //
+    void inc_ref() { ++m_ref_count; }
+    void dec_ref() { 
+        --m_ref_count;
+        if (m_ref_count == 0) {
+            dealloc(this);
+        }
+    }
+};
+
+#endif

src/model/model_evaluator.cpp

@@ -0,0 +1,274 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_evaluator.cpp
+
+Abstract:
+
+    Evaluate expressions in a given model.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-04-30.
+
+Revision History:
+
+--*/
+#include"model.h"
+#include"rewriter_types.h"
+#include"model_evaluator.h"
+#include"bool_rewriter.h"
+#include"arith_rewriter.h"
+#include"bv_rewriter.h"
+#include"datatype_rewriter.h"
+#include"array_rewriter.h"
+#include"float_rewriter.h"
+#include"rewriter_def.h"
+#include"cooperate.h"
+
+struct evaluator_cfg : public default_rewriter_cfg {
+    model &                         m_model;
+    bool_rewriter                   m_b_rw;
+    arith_rewriter                  m_a_rw;
+    bv_rewriter                     m_bv_rw;
+    array_rewriter                  m_ar_rw;
+    datatype_rewriter               m_dt_rw;
+    float_rewriter                  m_f_rw;
+    unsigned long long              m_max_memory;
+    unsigned                        m_max_steps;
+    bool                            m_model_completion;
+    bool                            m_cache;
+
+    evaluator_cfg(ast_manager & m, model & md, params_ref const & p):
+        m_model(md),
+        m_b_rw(m),
+        // We must allow customers to set parameters for arithmetic rewriter/evaluator. 
+        // In particular, the maximum degree of algebraic numbers that will be evaluated.
+        m_a_rw(m, p), 
+        m_bv_rw(m),
+        // See comment above. We want to allow customers to set :sort-store
+        m_ar_rw(m, p),
+        m_dt_rw(m),
+        m_f_rw(m) {
+        m_b_rw.set_flat(false);
+        m_a_rw.set_flat(false);
+        m_bv_rw.set_flat(false);
+        m_bv_rw.set_mkbv2num(true);
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & p) {
+        m_max_memory       = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
+        m_max_steps        = p.get_uint(":max-steps", UINT_MAX);
+        m_model_completion = p.get_bool(":model-completion", false);
+        m_cache            = p.get_bool(":cache", true);
+    }
+        
+    ast_manager & m() const { return m_model.get_manager(); }
+
+    // Try to use the entries to quickly evaluate the fi
+    bool eval_fi(func_interp * fi, unsigned num, expr * const * args, expr_ref & result) {
+        if (fi->num_entries() == 0)
+            return false; // let get_macro handle it.
+
+        SASSERT(fi->get_arity() == num);
+
+        bool actuals_are_values = true;
+    
+        for (unsigned i = 0; actuals_are_values && i < num; i++) {
+            actuals_are_values = m().is_value(args[i]);
+        }
+        
+        if (!actuals_are_values)
+            return false; // let get_macro handle it
+
+        func_entry * entry = fi->get_entry(args);
+        if (entry != 0) {
+            result = entry->get_result();
+            return true;
+        }
+
+        return false;
+    }
+
+    br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+        result_pr = 0;
+        family_id fid = f->get_family_id();
+        if (fid == null_family_id) {
+            if (num == 0) {
+                expr * val = m_model.get_const_interp(f);
+                if (val != 0) {
+                    result = val;
+                    return BR_DONE;
+                }
+                
+                if (m_model_completion) {
+                    sort * s   = f->get_range();
+                    expr * val = m_model.get_some_value(s);
+                    m_model.register_decl(f, val);
+                    result = val;
+                    return BR_DONE;
+                }
+                return BR_FAILED;
+            }
+            SASSERT(num > 0);
+            func_interp * fi = m_model.get_func_interp(f);
+            if (fi != 0 && eval_fi(fi, num, args, result)) {
+                TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
+                      for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
+                      tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";);
+                return BR_DONE;
+            }
+        }
+
+        if (fid == m_b_rw.get_fid()) {
+            decl_kind k = f->get_decl_kind();
+            if (k == OP_EQ) {
+                // theory dispatch for =
+                SASSERT(num == 2);
+                family_id s_fid = m().get_sort(args[0])->get_family_id();
+                br_status st = BR_FAILED;
+                if (s_fid == m_a_rw.get_fid())
+                    st = m_a_rw.mk_eq_core(args[0], args[1], result);
+                else if (s_fid == m_bv_rw.get_fid())
+                    st = m_bv_rw.mk_eq_core(args[0], args[1], result);
+                else if (s_fid == m_dt_rw.get_fid())
+                    st = m_dt_rw.mk_eq_core(args[0], args[1], result);
+                else if (s_fid == m_f_rw.get_fid())
+                    st = m_f_rw.mk_eq_core(args[0], args[1], result);
+                if (st != BR_FAILED)
+                    return st;
+            }
+            return m_b_rw.mk_app_core(f, num, args, result);
+        }
+        if (fid == m_a_rw.get_fid())
+            return m_a_rw.mk_app_core(f, num, args, result);
+        if (fid == m_bv_rw.get_fid())
+            return m_bv_rw.mk_app_core(f, num, args, result);
+        if (fid == m_ar_rw.get_fid())
+            return m_ar_rw.mk_app_core(f, num, args, result);
+        if (fid == m_dt_rw.get_fid())
+            return m_dt_rw.mk_app_core(f, num, args, result);
+        if (fid == m_f_rw.get_fid())
+            return m_f_rw.mk_app_core(f, num, args, result);
+        return BR_FAILED;
+    }
+
+    bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { 
+        if (f->get_family_id() == null_family_id) {
+            func_interp * fi = m_model.get_func_interp(f);
+            
+            if (fi != 0) {
+                if (fi->is_partial()) {
+                    if (m_model_completion) {
+                        sort * s   = f->get_range();
+                        expr * val = m_model.get_some_value(s);
+                        fi->set_else(val);
+                    }
+                    else {
+                        return false;
+                    }
+                }
+                
+                def    = fi->get_interp();
+                SASSERT(def != 0);
+                return true;
+            }
+            
+            if (m_model_completion) {
+                sort * s   = f->get_range();
+                expr * val = m_model.get_some_value(s);
+                func_interp * new_fi = alloc(func_interp, m(), f->get_arity());
+                new_fi->set_else(val);
+                m_model.register_decl(f, new_fi);
+                def = val;
+                return true;
+            }
+        }
+        return false;
+    }
+    
+    bool max_steps_exceeded(unsigned num_steps) const { 
+        cooperate("model evaluator");
+        if (memory::get_allocation_size() > m_max_memory)
+            throw rewriter_exception(TACTIC_MAX_MEMORY_MSG);
+        return num_steps > m_max_steps;
+    }
+
+    bool cache_results() const { return m_cache; }
+
+};
+
+template class rewriter_tpl<evaluator_cfg>;
+
+struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
+    evaluator_cfg m_cfg;
+    imp(model & md, params_ref const & p):
+        rewriter_tpl<evaluator_cfg>(md.get_manager(), 
+                                    false, // no proofs for evaluator
+                                    m_cfg),
+        m_cfg(md.get_manager(), md, p) {
+    }
+};
+
+model_evaluator::model_evaluator(model & md, params_ref const & p) {
+    m_imp = alloc(imp, md, p);
+}
+
+ast_manager & model_evaluator::m() const {
+    return m_imp->m();
+}
+
+model_evaluator::~model_evaluator() {
+    dealloc(m_imp);
+}
+
+void model_evaluator::updt_params(params_ref const & p) {
+    m_imp->cfg().updt_params(p);
+}
+
+void model_evaluator::get_param_descrs(param_descrs & r) {
+    insert_max_memory(r);
+    insert_max_steps(r);
+    r.insert(":model-completion", CPK_BOOL, "(default: false) assigns an interpretation to symbols that are not intepreted by the model.");
+    r.insert(":cache", CPK_BOOL, "(default: true) cache intermediate results.");
+}
+
+void model_evaluator::set_model_completion(bool f) {
+    m_imp->cfg().m_model_completion = f;
+}
+
+unsigned model_evaluator::get_num_steps() const {
+    return m_imp->get_num_steps();
+}
+
+void model_evaluator::cancel() {
+    #pragma omp critical (model_evaluator)
+    {
+        m_imp->cancel();
+    }
+}
+
+void model_evaluator::cleanup(params_ref const & p) {
+    model & md = m_imp->cfg().m_model;
+    #pragma omp critical (model_evaluator)
+    {
+        dealloc(m_imp);
+        m_imp = alloc(imp, md, p);
+    }
+}
+
+void model_evaluator::reset(params_ref const & p) {
+    m_imp->reset();
+    updt_params(p);
+}
+
+void model_evaluator::operator()(expr * t, expr_ref & result) {
+    TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
+    m_imp->operator()(t, result);
+}
+
+
+

src/model/model_evaluator.h

@@ -0,0 +1,51 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_evaluator.h
+
+Abstract:
+
+    Evaluate expressions in a given model.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-04-30.
+
+Revision History:
+
+--*/
+#ifndef _MODEL_EVALUATOR_H_
+#define _MODEL_EVALUATOR_H_
+
+#include"ast.h"
+#include"rewriter_types.h"
+#include"params.h"
+class model;
+
+typedef rewriter_exception model_evaluator_exception;
+
+class model_evaluator {
+    struct imp;
+    imp *  m_imp;
+public:
+    model_evaluator(model & m, params_ref const & p = params_ref());
+    ~model_evaluator();
+
+    ast_manager & m () const;
+    void set_model_completion(bool f);
+
+    void updt_params(params_ref const & p);
+    static void get_param_descrs(param_descrs & r);
+
+    void operator()(expr * t, expr_ref & r);
+
+    void cancel();
+    void cleanup(params_ref const & p = params_ref());
+    void reset(params_ref const & p = params_ref());
+    
+    unsigned get_num_steps() const;
+};
+
+#endif

src/model/model_evaluator_params.cpp

@@ -0,0 +1,76 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_evaluator_params.cpp
+
+Abstract:
+
+    New parameter setting support for rewriter. 
+
+Author:
+
+    Leonardo (leonardo) 2011-04-22
+
+Notes:
+
+--*/
+#include"model_evaluator_params.h"
+
+model_evaluator_params::model_evaluator_params() {
+    reset();
+}
+
+void model_evaluator_params::reset() {
+    m_model_completion = false;
+    m_cache            = true;
+    m_max_steps        = UINT_MAX;
+    m_max_memory       = UINT_MAX;
+}
+
+#define PARAM(name) param_names.push_back(name)
+
+void model_evaluator_params::get_params(svector<char const *> & param_names) const {
+    PARAM(":model-completion");
+    PARAM(":cache");
+    PARAM(":max-steps");
+    PARAM(":max-memory");
+}
+
+#define DESCR(NAME, DR) if (strcmp(name, NAME) == 0) return DR 
+
+char const * model_evaluator_params::get_param_descr(char const * name) const {
+    DESCR(":model-completion", "(default: false) assigns an interpretation to symbols that are not intepreted by the model.");
+    DESCR(":cache", "(default: true) cache intermediate results.");
+    DESCR(":max-steps", "(default: infty) maximum number of steps.");
+    DESCR(":max-memory", "(default: infty) maximum amount of memory in megabytes.");
+    return 0;
+}
+
+#define RBOOL(NAME) if (strcmp(name, NAME) == 0) return CPK_BOOL
+#define RUINT(NAME) if (strcmp(name, NAME) == 0) return CPK_UINT
+
+param_kind model_evaluator_params::get_param_kind(char const * name) const {
+    RBOOL(":model-completion");
+    RBOOL(":cache");
+    RUINT(":max-steps");
+    RUINT(":max-memory");
+    return CPK_INVALID;
+}
+
+#define SET(NAME, FIELD) if (strcmp(name, NAME) == 0) { FIELD = value; return true; }
+
+bool model_evaluator_params::set_bool_param(char const * name, bool value) {
+    SET(":model-completion", m_model_completion);
+    SET(":cache", m_cache);
+    return false;
+}
+
+bool model_evaluator_params::set_uint_param(char const * name, unsigned value) {
+    SET(":max-steps", m_max_steps);
+    SET(":max-memory", m_max_memory);
+    return false;
+}
+
+

src/model/model_params.cpp

@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    model_params.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2007-08-23.
+
+Revision History:
+
+--*/
+
+#include"model_params.h"
+
+void model_params::register_params(ini_params & p) {
+    p.register_bool_param("MODEL_PARTIAL", m_model_partial, "enable/disable partial function interpretations", true);
+    p.register_bool_param("MODEL_HIDE_UNUSED_PARTITIONS", m_model_hide_unused_partitions, "hide unused partitions, some partitions are associated with internal terms/formulas created by Z3", true);
+    p.register_bool_param("MODEL_V1", m_model_v1_pp, 
+                          "use Z3 version 1.x pretty printer", true);
+    p.register_bool_param("MODEL_V2", m_model_v2_pp, 
+                          "use Z3 version 2.x (x <= 16) pretty printer", true);
+    p.register_bool_param("MODEL_COMPACT", m_model_compact, 
+                          "try to compact function graph (i.e., function interpretations that are lookup tables", true);
+    p.register_bool_param("MODEL_COMPLETION", m_model_completion, 
+                          "assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model", true);
+    p.register_bool_param("MODEL_DISPLAY_ARG_SORT", m_model_display_arg_sort, 
+                          "display the sort of each argument when printing function interpretations", true);
+}
+
+

src/model/model_params.h

@@ -0,0 +1,47 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    model_params.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2007-08-23.
+
+Revision History:
+
+--*/
+#ifndef _MODEL_PARAMS_H_
+#define _MODEL_PARAMS_H_
+
+#include"ini_file.h"
+
+struct model_params {
+    bool m_model_partial;
+    bool m_model_hide_unused_partitions;
+    bool m_model_compact;
+    bool m_model_v1_pp;
+    bool m_model_v2_pp;
+    bool m_model_completion;
+    bool m_model_display_arg_sort;
+
+    model_params():
+        m_model_partial(false),
+        m_model_hide_unused_partitions(true),
+        m_model_compact(false),
+        m_model_v1_pp(false),
+        m_model_v2_pp(false),
+        m_model_completion(false),
+        m_model_display_arg_sort(true) {
+    }
+
+    void register_params(ini_params & p);
+};
+
+#endif /* _MODEL_PARAMS_H_ */
+

src/model/model_pp.cpp

@@ -0,0 +1,102 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_pp.cpp
+
+Abstract:
+
+    Pretty printer for models for debugging purposes.
+
+Author:
+
+    Leonardo de Moura (leonardo)
+
+Revision History:
+
+
+--*/
+#include"model_pp.h"
+#include"model_core.h"
+#include"ast_pp.h"
+#include"ast_smt2_pp.h"
+#include"used_symbols.h"
+#include"pp.h"
+
+static void display_uninterp_sorts(std::ostream & out, model_core const & md) {
+    ast_manager & m = md.get_manager();
+    unsigned sz = md.get_num_uninterpreted_sorts();
+    for (unsigned i = 0; i < sz; i++) {
+        sort * s = md.get_uninterpreted_sort(i);
+        out << "(define-sort " << mk_pp(s, m); 
+        ptr_vector<expr> const & univ  = md.get_universe(s);
+        ptr_vector<expr>::const_iterator it  = univ.begin();
+        ptr_vector<expr>::const_iterator end = univ.end();
+        for (; it != end; ++it) {
+            out << " " << mk_ismt2_pp(*it, m);
+        }
+        out << ")\n";
+    }
+}
+
+static void display_constants(std::ostream & out, model_core const & md) {
+    ast_manager & m = md.get_manager();
+    unsigned sz = md.get_num_constants();
+    for (unsigned i = 0; i < sz; i++) {
+        func_decl * c = md.get_constant(i);
+        char const * d = "(define ";
+        std::string n  = c->get_name().str();
+        unsigned indent = static_cast<unsigned>(n.length() + strlen(d) + 1);
+        out << d << n << " " << mk_ismt2_pp(md.get_const_interp(c), m, indent) << ")\n";
+    }
+}
+
+static void display_functions(std::ostream & out, model_core const & md) {
+    ast_manager & m = md.get_manager();
+    unsigned sz = md.get_num_functions();
+    for (unsigned i = 0; i < sz; i++) {
+        func_decl * f = md.get_function(i);
+        out << "(define (" << f->get_name();
+        unsigned arity = f->get_arity();
+        func_interp * fi = md.get_func_interp(f);
+        for (unsigned j = 0; j < arity; j++) {
+            out << " " << "x!" << j;
+        }
+        out << ")\n";
+        
+        unsigned num_entries = fi->num_entries();
+        for (unsigned j = 0; j < num_entries; j++) {
+            func_entry const * curr = fi->get_entry(j);
+            out << "  (if ";
+            if (arity > 1)
+                out << "(and ";
+            for (unsigned j = 0; j < arity; j++) {
+                out << "(= x!" << j << " " << mk_ismt2_pp(curr->get_arg(j), m) << ")";
+                if (j + 1 < arity)
+                    out << " ";
+            }
+            if (arity > 1)
+                out << ")";
+            out << " " << mk_ismt2_pp(curr->get_result(), m) << "\n";
+        }
+        if (num_entries > 0)
+            out << "  ";
+        if (fi->is_partial())
+            out << "  #unspecified";
+        else {
+            pp_params const & params = get_pp_default_params();
+            out << "  " << mk_ismt2_pp(fi->get_else(), m, params, 5, arity, "x");
+        }
+        for (unsigned j = 0; j < num_entries; j++)
+            out << ")";
+        out << ")\n";
+    }
+}
+
+
+void model_pp(std::ostream & out, model_core const & md) {
+    display_uninterp_sorts(out, md);
+    display_constants(out, md);
+    display_functions(out, md);
+}

src/model/model_pp.h

@@ -0,0 +1,28 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_pp.h
+
+Abstract:
+
+    Pretty printer for models for debugging purposes.
+
+Author:
+
+    Leonardo de Moura (leonardo)
+
+Revision History:
+
+
+--*/
+#ifndef _MODEL_PP_H_
+#define _MODEL_PP_H_
+
+#include<iostream>
+class model_core;
+
+void model_pp(std::ostream & out, model_core const & m);
+
+#endif

src/model/model_smt2_pp.cpp

@@ -0,0 +1,348 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_smt2_pp.cpp
+
+Abstract:
+
+    Pretty printer for models using SMT2 format.
+
+Author:
+
+    Leonardo de Moura (leonardo)
+
+Revision History:
+
+
+--*/
+#include"model_smt2_pp.h"
+#include"ast_smt2_pp.h"
+#include"func_decl_dependencies.h"
+#include"pp.h"
+using namespace format_ns;
+
+static void pp_indent(std::ostream & out, unsigned indent) {
+    for (unsigned i = 0; i < indent; i++) 
+        out << " ";
+}
+
+static unsigned pp_symbol(std::ostream & out, symbol const & s) {
+    if (is_smt2_quoted_symbol(s)) {
+        std::string str = mk_smt2_quoted_symbol(s);
+        out << str;
+        return static_cast<unsigned>(str.length());
+    }
+    else if (s.is_numerical()) {
+        std::string str = s.str();
+        out << str;
+        return static_cast<unsigned>(str.length());
+    }
+    else {
+        out << s.bare_str();
+        return static_cast<unsigned>(strlen(s.bare_str()));
+    }
+}
+
+#define TAB_SZ 2
+
+class model_smt2_pp_ctx {
+public:
+    virtual ast_manager & m() const = 0;
+    virtual void display(std::ostream & out, sort * s, unsigned indent = 0) = 0;
+    virtual void display(std::ostream & out, expr * n, unsigned indent = 0) = 0;
+    virtual void pp(sort * s, format_ns::format_ref & r) = 0;
+    virtual void pp(func_decl * f, format_ns::format_ref & r) = 0;
+    virtual void pp(expr * n, format_ns::format_ref & r) = 0;
+    virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) = 0;
+};
+
+class model_smt2_pp_cmd_ctx : public model_smt2_pp_ctx {
+    cmd_context & m_ctx;
+public:
+    model_smt2_pp_cmd_ctx(cmd_context & ctx):m_ctx(ctx) {}
+    virtual ast_manager & m() const { return m_ctx.m(); }
+    virtual void display(std::ostream & out, sort * s, unsigned indent = 0) { m_ctx.display(out, s, indent); }
+    virtual void display(std::ostream & out, expr * n, unsigned indent = 0) { m_ctx.display(out, n, indent); }
+    virtual void pp(sort * s, format_ns::format_ref & r) { r = m_ctx.pp(s); }
+    virtual void pp(func_decl * f, format_ns::format_ref & r) { return m_ctx.pp(f, r); }
+    virtual void pp(expr * n, format_ns::format_ref & r) { return m_ctx.pp(n, r); }
+    virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) {
+        return m_ctx.pp(n, num_vars, var_prefix, r, var_names);
+    }
+};
+
+class model_smt2_pp_simple_ctx : public model_smt2_pp_ctx {
+    ast_manager & m_manager;
+    smt2_pp_environment_dbg m_env;
+public:
+    model_smt2_pp_simple_ctx(ast_manager & m):m_manager(m), m_env(m) {}
+    virtual ast_manager & m() const { return m_manager; }
+    virtual void display(std::ostream & out, sort * s, unsigned indent = 0) { out << mk_ismt2_pp(s, m(), indent); }
+    virtual void display(std::ostream & out, expr * n, unsigned indent = 0) { out << mk_ismt2_pp(n, m(), indent); }
+    virtual void pp(sort * s, format_ns::format_ref & r) { mk_smt2_format(s, m_env, get_pp_default_params(), r); }
+    virtual void pp(func_decl * f, format_ns::format_ref & r) { mk_smt2_format(f, m_env, get_pp_default_params(), r); }
+    virtual void pp(expr * n, format_ns::format_ref & r) { 
+        sbuffer<symbol> buf;
+        mk_smt2_format(n, m_env, get_pp_default_params(), 0, 0, r, buf); 
+    }
+    virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) {
+        mk_smt2_format(n, m_env, get_pp_default_params(), num_vars, var_prefix, r, var_names);
+    }
+};
+
+static void pp_uninterp_sorts(std::ostream & out, model_smt2_pp_ctx & ctx, model_core const & md, unsigned indent) {
+    ast_manager & m = ctx.m();
+    ptr_buffer<format> f_conds;
+    unsigned num = md.get_num_uninterpreted_sorts();
+    for (unsigned i = 0; i < num; i++) {
+        sort * s = md.get_uninterpreted_sort(i);
+        ptr_vector<expr> const & u = md.get_universe(s);
+        std::ostringstream buffer;
+        buffer << "universe for ";
+        ctx.display(buffer, s, 13);
+        buffer << ":\n";
+        pp_indent(buffer, TAB_SZ);
+        ptr_vector<expr>::const_iterator it  = u.begin();
+        ptr_vector<expr>::const_iterator end = u.end();
+        for (; it != end; ++it) {
+            SASSERT(is_app(*it));
+            app * c = to_app(*it);
+            pp_symbol(buffer, c->get_decl()->get_name());
+            buffer << " ";
+        }
+        buffer << "\n-----------";
+        std::string buffer_str = buffer.str();
+        unsigned len = static_cast<unsigned>(buffer_str.length());
+        pp_indent(out, indent);
+        out << ";; ";
+        for (unsigned i = 0; i < len; i++) {
+            char c = buffer_str[i];
+            if (c == '\n') {
+                out << "\n";
+                pp_indent(out, indent);
+                out << ";; ";
+            }
+            else {
+                out << c;
+            }
+        }
+        out << "\n";
+        pp_indent(out, indent);
+        out << ";; definitions for universe elements:\n";
+        it  = u.begin();
+        for (; it != end; ++it) {
+            app * c = to_app(*it);
+            pp_indent(out, indent);
+            out << "(declare-fun ";
+            unsigned len  = pp_symbol(out, c->get_decl()->get_name());
+            out << " () ";
+            ctx.display(out, c->get_decl()->get_range(), indent + len + 16);
+            out << ")\n";
+        }
+        pp_indent(out, indent);
+        out << ";; cardinality constraint:\n";
+        f_conds.reset();
+        format * var = mk_string(m, "x");
+        it  = u.begin();
+        for (; it != end; ++it) {
+            app * c = to_app(*it);
+            symbol csym = c->get_decl()->get_name();
+            std::string cname;
+            if (is_smt2_quoted_symbol(csym))
+                cname = mk_smt2_quoted_symbol(csym);
+            else
+                cname = csym.str();
+            format * c_args[2] = { var, mk_string(m, cname.c_str()) };
+            f_conds.push_back(mk_seq1<format**, f2f>(m, c_args, c_args+2, f2f(), "="));
+        }
+        SASSERT(!f_conds.empty());
+        format * f_cond;
+        if (f_conds.size() > 1)
+            f_cond = mk_seq1(m, f_conds.begin(), f_conds.end(), f2f(), "or");
+        else
+            f_cond = f_conds[0];
+        format_ref f_s(fm(m));
+        ctx.pp(s, f_s);
+        format * f_args[2] = { mk_compose(m, 
+                                          mk_string(m, "((x "),
+                                          mk_indent(m, 4, mk_compose(m, f_s.get(), mk_string(m, "))")))),
+                               f_cond };
+        format_ref f_card(fm(m));
+        f_card = mk_indent(m, indent, mk_seq1<format**, f2f>(m, f_args, f_args+2, f2f(), "forall"));
+        pp_indent(out, indent);
+        pp(out, f_card, m, get_pp_default_params());
+        out << "\n";
+        pp_indent(out, indent);
+        out << ";; -----------\n";
+    }
+}
+
+static void pp_consts(std::ostream & out, model_smt2_pp_ctx & ctx, model_core const & md, unsigned indent) {
+    unsigned num = md.get_num_constants();
+    for (unsigned i = 0; i < num; i++) {
+        func_decl * c = md.get_constant(i);
+        expr * c_i    = md.get_const_interp(c);
+        pp_indent(out, indent);
+        out << "(define-fun ";
+        unsigned len  = pp_symbol(out, c->get_name());
+        out << " () ";
+        ctx.display(out, c->get_range(), indent + len + 16);
+        out << "\n";
+        pp_indent(out, indent + TAB_SZ);
+        ctx.display(out, c_i);
+        out << ")\n";
+    }
+}
+
+void sort_fun_decls(ast_manager & m, model_core const & md, ptr_buffer<func_decl> & result) {
+    func_decl_set         visited;
+    ptr_vector<func_decl> todo;
+    unsigned sz = md.get_num_functions();
+    for (unsigned i = 0; i < sz; i++) {
+        func_decl * f = md.get_function(i);
+        if (visited.contains(f))
+            continue;
+        visited.insert(f);
+        todo.push_back(f);
+        while (!todo.empty()) {
+            func_decl * curr = todo.back();
+            func_interp * curr_i = md.get_func_interp(curr);
+            SASSERT(curr_i != 0);
+            if (!curr_i->is_partial()) {
+                func_decl_set deps;
+                bool all_visited = true;
+                collect_func_decls(m, curr_i->get_else(), deps);
+                func_decl_set::iterator it2  = deps.begin();
+                func_decl_set::iterator end2 = deps.end();
+                for (; it2 != end2; ++it2) {
+                    func_decl * d = *it2;
+                    if (d->get_arity() > 0 && md.has_interpretation(d) && !visited.contains(d)) {
+                        todo.push_back(d);
+                        visited.insert(d);
+                        all_visited = false;
+                    }
+                }
+                if (!all_visited)
+                    continue;
+            }
+            todo.pop_back();
+            result.push_back(curr);
+        }
+    }
+}
+
+static void pp_funs(std::ostream & out, model_smt2_pp_ctx & ctx, model_core const & md, unsigned indent) {
+    ast_manager & m = ctx.m();
+    sbuffer<symbol>    var_names;
+    ptr_buffer<format> f_var_names;
+    ptr_buffer<format> f_arg_decls;
+    ptr_buffer<format> f_entries;
+    ptr_buffer<format> f_entry_conds;
+    ptr_buffer<func_decl> func_decls;
+    sort_fun_decls(m, md, func_decls);
+    for (unsigned i = 0; i < func_decls.size(); i++) {
+        func_decl * f     = func_decls[i]; 
+        func_interp * f_i = md.get_func_interp(f);
+        SASSERT(f->get_arity() == f_i->get_arity());
+        format_ref body(fm(m));
+        var_names.reset();
+        if (f_i->is_partial()) {
+            body = mk_string(m, "#unspecified");
+            for (unsigned j = 0; j < f->get_arity(); j++) {
+                std::stringstream strm;
+                strm << "x!" << (j+1);
+                var_names.push_back(symbol(strm.str().c_str()));
+            }
+        }
+        else {
+            ctx.pp(f_i->get_else(), f->get_arity(), "x", body, var_names);  
+        }
+        TRACE("model_smt2_pp", for (unsigned i = 0; i < var_names.size(); i++) tout << var_names[i] << "\n";);
+        f_var_names.reset();
+        for (unsigned i = 0; i < f->get_arity(); i++)
+            f_var_names.push_back(mk_string(m, var_names[i].bare_str()));
+        f_arg_decls.reset();
+        for (unsigned i = 0; i < f->get_arity(); i++) {
+            format_ref f_domain(fm(m));
+            ctx.pp(f->get_domain(i), f_domain);
+            format * args[2] = { f_var_names[i], f_domain.get() };
+            f_arg_decls.push_back(mk_seq5<format**, f2f>(m, args, args+2, f2f()));
+        }
+        format * f_domain = mk_seq5(m, f_arg_decls.begin(), f_arg_decls.end(), f2f());
+        format_ref f_range(fm(m));
+        ctx.pp(f->get_range(), f_range);
+        if (f_i->num_entries() > 0) {
+            f_entries.reset();
+            for (unsigned i = 0; i < f_i->num_entries(); i++) {
+                func_entry const * e = f_i->get_entry(i);
+                f_entry_conds.reset();
+                for (unsigned j = 0; j < f->get_arity(); j++) {
+                    format_ref f_arg(fm(m));
+                    ctx.pp(e->get_arg(j), f_arg);
+                    format * eq_args[2] = { f_var_names[j], f_arg.get() };
+                    f_entry_conds.push_back(mk_seq1<format**, f2f>(m, eq_args, eq_args+2, f2f(), "="));
+                }
+                format * f_entry_cond;
+                SASSERT(!f_entry_conds.empty());
+                if (f_entry_conds.size() > 1)
+                    f_entry_cond = mk_seq1(m, f_entry_conds.begin(), f_entry_conds.end(), f2f(), "and");
+                else
+                    f_entry_cond = f_entry_conds[0];
+                format_ref f_result(fm(m));
+                ctx.pp(e->get_result(), f_result);
+                if (i > 0)
+                    f_entries.push_back(mk_line_break(m));
+                f_entries.push_back(mk_group(m, mk_compose(m, 
+                                                           mk_string(m, "(ite "),
+                                                           mk_indent(m, 5, f_entry_cond),
+                                                           mk_indent(m, TAB_SZ, mk_compose(m, 
+                                                                                           mk_line_break(m),
+                                                                                           f_result.get())))));
+            }
+            f_entries.push_back(mk_indent(m, TAB_SZ, mk_compose(m,
+                                                                mk_line_break(m),
+                                                                body.get())));
+            for (unsigned i = 0; i < f_i->num_entries(); i++)
+                f_entries.push_back(mk_string(m, ")"));
+            body = mk_compose(m, f_entries.size(), f_entries.c_ptr());
+        }
+        format_ref def(fm(m));
+        std::string fname;
+        if (is_smt2_quoted_symbol(f->get_name()))
+            fname = mk_smt2_quoted_symbol(f->get_name());
+        else
+            fname = f->get_name().str();
+        def = mk_indent(m, indent, mk_compose(m, 
+                                              mk_compose(m, 
+                                                         mk_string(m, "(define-fun "),
+                                                         mk_string(m, fname.c_str()),
+                                                         mk_string(m, " "),
+                                                         mk_compose(m, 
+                                                                    f_domain,
+                                                                    mk_string(m, " "),
+                                                                    f_range)),
+                                              mk_indent(m, TAB_SZ, mk_compose(m, 
+                                                                              mk_line_break(m),
+                                                                              body.get(),
+                                                                              mk_string(m, ")")))));
+        pp_indent(out, indent);
+        pp(out, def.get(), m, get_pp_default_params());
+        out << "\n";
+    }
+}
+
+void model_smt2_pp(std::ostream & out, cmd_context & ctx, model_core const & m, unsigned indent) {
+    model_smt2_pp_cmd_ctx _ctx(ctx);
+    pp_uninterp_sorts(out, _ctx, m, indent);
+    pp_consts(out, _ctx, m, indent);
+    pp_funs(out, _ctx, m, indent);
+}
+
+void model_smt2_pp(std::ostream & out, ast_manager & m, model_core const & md, unsigned indent) {
+    model_smt2_pp_simple_ctx _ctx(m);
+    pp_uninterp_sorts(out, _ctx, md, indent);
+    pp_consts(out, _ctx, md, indent);
+    pp_funs(out, _ctx, md, indent);
+}

src/model/model_smt2_pp.h

@@ -0,0 +1,28 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_smt2_pp.h
+
+Abstract:
+
+    Pretty printer for models using SMT2 format.
+
+Author:
+
+    Leonardo de Moura (leonardo)
+
+Revision History:
+
+
+--*/
+#ifndef _MODEL_SMT2_PP_H_
+#define _MODEL_SMT2_PP_H_
+
+#include"cmd_context.h"
+
+void model_smt2_pp(std::ostream & out, cmd_context & ctx, model_core const & m, unsigned indent);
+void model_smt2_pp(std::ostream & out, ast_manager & m, model_core const & md, unsigned indent);
+
+#endif

src/model/model_v2_pp.cpp

@@ -0,0 +1,82 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_v2_pp.cpp
+
+Abstract:
+
+    V2 Pretty printer for models. (backward compatibility)
+
+Author:
+
+    Leonardo de Moura (leonardo)
+
+Revision History:
+--*/
+#include"model_v2_pp.h"
+#include"model_core.h"
+#include"ast_pp.h"
+
+static void display_function(std::ostream & out, model_core const & md, func_decl * f, bool partial) {
+    ast_manager & m = md.get_manager();
+    func_interp * g = md.get_func_interp(f);
+    out << f->get_name() << " -> {\n";
+    unsigned num_entries = g->num_entries();
+    unsigned arity       = g->get_arity();
+    char const * else_str = num_entries == 0 ? "  " : "  else -> ";
+    unsigned else_indent  = static_cast<unsigned>(strlen(else_str));
+    for (unsigned i = 0; i < num_entries; i++) {
+        func_entry const * entry = g->get_entry(i);
+        out << "  ";
+        for (unsigned j = 0; j < arity; j++) {
+            expr * arg = entry->get_arg(j);
+            out << mk_pp(arg, m);
+            out << " ";
+        }
+        out << "-> "; 
+        out << mk_pp(entry->get_result(), m);
+        out << "\n";
+    }
+    if (partial) {
+        out << else_str << "#unspecified\n";
+    }
+    else {
+        expr * else_val = g->get_else();
+        out << else_str;
+        if (else_val)
+            out << mk_pp(else_val, m, else_indent);
+        else
+            out << "#unspecified";
+        out << "\n";
+    }
+    out << "}\n";
+}
+
+static void display_functions(std::ostream & out, model_core const & md, bool partial) {
+    unsigned sz = md.get_num_functions();
+    for (unsigned i = 0; i < sz; i++) {
+        func_decl * f = md.get_function(i);
+        display_function(out, md, f, partial);
+    }
+}
+
+static void display_constants(std::ostream & out, model_core const & md) {
+    ast_manager & m = md.get_manager();
+    unsigned sz = md.get_num_constants();
+    for (unsigned i = 0; i < sz; i++) {
+        func_decl * d = md.get_constant(i);
+
+        std::string name   = d->get_name().str();
+        const char * arrow = " -> "; 
+        out << name << arrow;
+        unsigned indent = static_cast<unsigned>(name.length() + strlen(arrow));
+        out << mk_pp(md.get_const_interp(d), m, indent) << "\n";
+    }
+}
+
+void model_v2_pp(std::ostream & out, model_core const & md, bool partial) {
+    display_constants(out, md);
+    display_functions(out, md, partial);
+}

src/model/model_v2_pp.h

@@ -0,0 +1,26 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_v2_pp.h
+
+Abstract:
+
+    V2 Pretty printer for models. (backward compatibility)
+
+Author:
+
+    Leonardo de Moura (leonardo)
+
+Revision History:
+--*/
+#ifndef _MODEL_V2_PP_H_
+#define _MODEL_V2_PP_H_
+
+#include<iostream>
+class model_core;
+
+void model_v2_pp(std::ostream & out, model_core const & m, bool partial = false);
+
+#endif

src/model/proto_model.cpp

@@ -0,0 +1,608 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    proto_model.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2007-03-08.
+
+Revision History:
+
+--*/
+#include"proto_model.h"
+#include"ast_pp.h"
+#include"ast_ll_pp.h"
+#include"var_subst.h"
+#include"front_end_params.h"
+#include"array_decl_plugin.h"
+#include"well_sorted.h"
+#include"used_symbols.h"
+#include"model_v2_pp.h"
+
+proto_model::proto_model(ast_manager & m, simplifier & s, model_params const & p):
+    model_core(m),
+    m_params(p),
+    m_asts(m),
+    m_simplifier(s),
+    m_afid(m.get_family_id(symbol("array"))) {
+    register_factory(alloc(basic_factory, m));
+    m_user_sort_factory = alloc(user_sort_factory, m);
+    register_factory(m_user_sort_factory);
+}
+
+void proto_model::reset_finterp() {
+     decl2finterp::iterator it  = m_finterp.begin();
+     decl2finterp::iterator end = m_finterp.end();
+     for (; it != end; ++it) {
+         dealloc(it->m_value);
+     }
+}
+
+proto_model::~proto_model() {
+    reset_finterp();
+}
+
+void proto_model::register_decl(func_decl * d, expr * v) {
+    SASSERT(d->get_arity() == 0);
+    if (m_interp.contains(d)) {
+        DEBUG_CODE({
+            expr * old_v = 0;
+            m_interp.find(d, old_v);
+            SASSERT(old_v == v);
+        });
+        return;
+    }
+    SASSERT(!m_interp.contains(d));
+    m_decls.push_back(d);
+    m_asts.push_back(d);
+    m_asts.push_back(v);
+    m_interp.insert(d, v);
+    m_const_decls.push_back(d);
+}
+
+void proto_model::register_decl(func_decl * d, func_interp * fi, bool aux) {
+    SASSERT(d->get_arity() > 0);
+    SASSERT(!m_finterp.contains(d));
+    m_decls.push_back(d);
+    m_asts.push_back(d);
+    m_finterp.insert(d, fi);
+    m_func_decls.push_back(d);
+    if (aux)
+        m_aux_decls.insert(d);
+}
+
+/**
+   \brief Set new_fi as the new interpretation for f.
+   If f_aux != 0, then assign the old interpretation of f to f_aux.
+   If f_aux == 0, then delete the old interpretation of f.
+
+   f_aux is marked as a auxiliary declaration.
+*/
+void proto_model::reregister_decl(func_decl * f, func_interp * new_fi, func_decl * f_aux) {
+    func_interp * fi = get_func_interp(f);
+    if (fi == 0) {
+        register_decl(f, new_fi);
+    }
+    else {
+        if (f_aux != 0) {
+            register_decl(f_aux, fi);
+            m_aux_decls.insert(f_aux);
+        }
+        else {
+            dealloc(fi);
+        }
+        m_finterp.insert(f, new_fi);
+    }
+}
+
+expr * proto_model::mk_some_interp_for(func_decl * d) {
+    SASSERT(!has_interpretation(d));
+    expr * r = get_some_value(d->get_range()); // if t is a function, then it will be the constant function.
+    if (d->get_arity() == 0) {
+        register_decl(d, r);
+    }
+    else {
+        func_interp * new_fi = alloc(func_interp, m_manager, d->get_arity());
+        new_fi->set_else(r);
+        register_decl(d, new_fi);
+    }
+    return r;
+}
+
+/**
+   \brief Evaluate the expression e in the current model, and store the result in \c result.
+   It returns \c true if succeeded, and false otherwise. If the evaluation fails,
+   then r contains a term that is simplified as much as possible using the interpretations
+   available in the model.
+   
+   When model_completion == true, if the model does not assign an interpretation to a
+   declaration it will build one for it. Moreover, partial functions will also be completed.
+   So, if model_completion == true, the evaluator never fails if it doesn't contain quantifiers.
+*/
+bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
+    bool is_ok = true;
+    SASSERT(is_well_sorted(m_manager, e));
+    TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n";
+          tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";);
+    
+    obj_map<expr, expr*> eval_cache;
+    expr_ref_vector trail(m_manager);
+    sbuffer<std::pair<expr*, expr*>, 128> todo;
+    ptr_buffer<expr> args;
+    expr * null = static_cast<expr*>(0);
+    todo.push_back(std::make_pair(e, null));
+
+    expr * a;
+    expr * expanded_a;
+    while (!todo.empty()) {
+        std::pair<expr *, expr *> & p = todo.back();
+        a          = p.first;
+        expanded_a = p.second;
+        if (expanded_a != 0) {
+            expr * r = 0;
+            eval_cache.find(expanded_a, r);
+            SASSERT(r != 0);
+            todo.pop_back();
+            eval_cache.insert(a, r);
+            TRACE("model_eval", 
+                  tout << "orig:\n" << mk_pp(a, m_manager) << "\n";
+                  tout << "after beta reduction:\n" << mk_pp(expanded_a, m_manager) << "\n";
+                  tout << "new:\n" << mk_pp(r, m_manager) << "\n";);
+        }
+        else {
+            switch(a->get_kind()) {
+            case AST_APP: {
+                app * t = to_app(a);
+                bool visited = true;
+                args.reset();
+                unsigned num_args = t->get_num_args();
+                for (unsigned i = 0; i < num_args; ++i) {
+                    expr * arg = 0;
+                    if (!eval_cache.find(t->get_arg(i), arg)) {
+                        visited = false;
+                        todo.push_back(std::make_pair(t->get_arg(i), null));
+                    }
+                    else {
+                        args.push_back(arg);
+                    }
+                }
+                if (!visited) {
+                    continue;
+                }
+                SASSERT(args.size() == t->get_num_args());
+                expr_ref new_t(m_manager);
+                func_decl * f   = t->get_decl();
+                
+                if (!has_interpretation(f)) {
+                    // the model does not assign an interpretation to f.
+                    SASSERT(new_t.get() == 0);
+                    if (f->get_family_id() == null_family_id) {
+                        if (model_completion) {
+                            // create an interpretation for f.
+                            new_t = mk_some_interp_for(f);
+                        }
+                        else {
+                            is_ok = false;
+                        }
+                    }
+                    if (new_t.get() == 0) {
+                        // t is interpreted or model completion is disabled.
+                        m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t);
+                        trail.push_back(new_t);
+                        if (!is_app(new_t) || to_app(new_t)->get_decl() != f) {
+                            // if the result is not of the form (f ...), then assume we must simplify it.
+                            expr * new_new_t = 0;
+                            if (!eval_cache.find(new_t.get(), new_new_t)) {
+                                todo.back().second = new_t;
+                                todo.push_back(std::make_pair(new_t, null));
+                                continue;
+                            }
+                            else {
+                                new_t = new_new_t;
+                            }
+                        }
+                    }
+                }
+                else {
+                    // the model has an interpretaion for f.
+                    if (num_args == 0) {
+                        // t is a constant
+                        new_t = get_const_interp(f);
+                    }
+                    else {
+                        // t is a function application
+                        SASSERT(new_t.get() == 0);
+                        // try to use function graph first
+                        func_interp * fi = get_func_interp(f);
+                        SASSERT(fi->get_arity() == num_args);
+                        expr_ref r1(m_manager);
+                        // fi may be partial...
+                        if (!fi->eval(m_simplifier, args.c_ptr(), r1)) {
+                            SASSERT(fi->is_partial()); // fi->eval only fails when fi is partial.
+                            if (model_completion) {
+                                expr * r = get_some_value(f->get_range()); 
+                                fi->set_else(r);
+                                SASSERT(!fi->is_partial());
+                                new_t = r;
+                            }
+                            else {
+                                // f is an uninterpreted function, there is no need to use m_simplifier.mk_app
+                                new_t = m_manager.mk_app(f, num_args, args.c_ptr());
+                                trail.push_back(new_t);
+                                is_ok = false;
+                            }
+                        }
+                        else {
+                            SASSERT(r1);
+                            trail.push_back(r1);
+                            expr * r2 = 0;
+                            if (!eval_cache.find(r1.get(), r2)) {
+                                todo.back().second = r1;
+                                todo.push_back(std::make_pair(r1, null));
+                                continue;
+                            }
+                            else {
+                                new_t = r2;
+                            }
+                        }
+                    }
+                }
+                TRACE("model_eval", 
+                      tout << "orig:\n" << mk_pp(t, m_manager) << "\n";
+                      tout << "new:\n" << mk_pp(new_t, m_manager) << "\n";);
+                todo.pop_back();
+                SASSERT(new_t.get() != 0);
+                eval_cache.insert(t, new_t);
+                break;
+            }
+            case AST_VAR:  
+                SASSERT(a != 0);
+                eval_cache.insert(a, a);
+                todo.pop_back();
+                break;
+            case AST_QUANTIFIER: 
+                is_ok = false; // evaluator does not handle quantifiers.
+                SASSERT(a != 0);
+                eval_cache.insert(a, a);
+                todo.pop_back();
+                break;
+            default:
+                UNREACHABLE();
+                break;
+            }
+        }
+    }
+
+    if (!eval_cache.find(e, a)) {
+        TRACE("model_eval", tout << "FAILED e: " << mk_bounded_pp(e, m_manager) << "\n";);
+        UNREACHABLE();
+    }
+
+    result = a;
+    TRACE("model_eval", 
+          ast_ll_pp(tout << "original:  ", m_manager, e);
+          ast_ll_pp(tout << "evaluated: ", m_manager, a);
+          ast_ll_pp(tout << "reduced:   ", m_manager, result.get());
+          tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";
+          ); 
+    SASSERT(is_well_sorted(m_manager, result.get()));
+    return is_ok;
+}
+
+/**
+   \brief Replace uninterpreted constants occurring in fi->get_else()
+   by their interpretations.
+*/
+void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs) {
+    if (fi->is_partial())
+        return;
+    expr * fi_else = fi->get_else();
+    TRACE("model_bug", tout << "cleaning up:\n" << mk_pp(fi_else, m_manager) << "\n";);
+
+    obj_map<expr, expr*> cache;
+    expr_ref_vector trail(m_manager);
+    ptr_buffer<expr, 128> todo;
+    ptr_buffer<expr> args;
+    todo.push_back(fi_else);
+
+    expr * a;
+    while (!todo.empty()) {
+        a = todo.back();
+        if (is_uninterp_const(a)) {
+            todo.pop_back();
+            func_decl * a_decl = to_app(a)->get_decl();
+            expr * ai = get_const_interp(a_decl);
+            if (ai == 0) {
+                ai = get_some_value(a_decl->get_range());
+                register_decl(a_decl, ai);
+            }
+            cache.insert(a, ai);
+        }
+        else {
+            switch(a->get_kind()) {
+            case AST_APP: {
+                app * t = to_app(a);
+                bool visited = true;
+                args.reset();
+                unsigned num_args = t->get_num_args();
+                for (unsigned i = 0; i < num_args; ++i) {
+                    expr * arg = 0;
+                    if (!cache.find(t->get_arg(i), arg)) {
+                        visited = false;
+                        todo.push_back(t->get_arg(i));
+                    }
+                    else {
+                        args.push_back(arg);
+                    }
+                }
+                if (!visited) {
+                    continue;
+                }
+                func_decl * f = t->get_decl();
+                if (m_aux_decls.contains(f))
+                    found_aux_fs.insert(f);
+                expr_ref new_t(m_manager);
+                m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t);
+                if (t != new_t.get())
+                    trail.push_back(new_t);
+                todo.pop_back();
+                cache.insert(t, new_t);
+                break;
+            }
+            default:
+                SASSERT(a != 0);
+                cache.insert(a, a);
+                todo.pop_back();
+                break;
+            }
+        }
+    }
+
+    if (!cache.find(fi_else, a)) {
+        UNREACHABLE();
+    }
+    
+    fi->set_else(a);
+}
+
+void proto_model::remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, func_decl_set const & s) {
+    unsigned sz = decls.size();
+    unsigned i  = 0;
+    unsigned j  = 0;
+    for (; i < sz; i++) {
+        func_decl * f = decls[i];
+        if (!m_aux_decls.contains(f) || s.contains(f)) {
+            decls[j] = f;
+            j++;
+        }
+    }
+    decls.shrink(j);
+}
+
+
+/**
+   \brief Replace uninterpreted constants occurring in the func_interp's get_else()
+   by their interpretations.
+*/
+void proto_model::cleanup() {
+    func_decl_set found_aux_fs;
+    decl2finterp::iterator it  = m_finterp.begin();
+    decl2finterp::iterator end = m_finterp.end();
+    for (; it != end; ++it) {
+        func_interp * fi = (*it).m_value;
+        cleanup_func_interp(fi, found_aux_fs);
+    }
+    
+    // remove auxiliary declarations that are not used.
+    if (found_aux_fs.size() != m_aux_decls.size()) {
+        remove_aux_decls_not_in_set(m_decls, found_aux_fs);
+        remove_aux_decls_not_in_set(m_func_decls, found_aux_fs);
+        
+        func_decl_set::iterator it2  = m_aux_decls.begin();
+        func_decl_set::iterator end2 = m_aux_decls.end();
+        for (; it2 != end2; ++it2) {
+            func_decl * faux = *it2;
+            if (!found_aux_fs.contains(faux)) {
+                TRACE("cleanup_bug", tout << "eliminating " << faux->get_name() << "\n";);
+                func_interp * fi = 0;
+                m_finterp.find(faux, fi);
+                SASSERT(fi != 0);
+                m_finterp.erase(faux);
+                dealloc(fi);
+            }
+        }
+        m_aux_decls.swap(found_aux_fs);
+    }
+}
+
+value_factory * proto_model::get_factory(family_id fid) {
+    return m_factories.get_plugin(fid);
+}
+
+void proto_model::freeze_universe(sort * s) {
+    SASSERT(m_manager.is_uninterp(s));
+    m_user_sort_factory->freeze_universe(s);
+}
+
+/**
+   \brief Return the known universe of an uninterpreted sort.
+*/
+obj_hashtable<expr> const & proto_model::get_known_universe(sort * s) const {
+    SASSERT(m_manager.is_uninterp(s));
+    return m_user_sort_factory->get_known_universe(s);
+}
+
+ptr_vector<expr> const & proto_model::get_universe(sort * s) const {
+    ptr_vector<expr> & tmp = const_cast<proto_model*>(this)->m_tmp;
+    tmp.reset();
+    obj_hashtable<expr> const & u = get_known_universe(s);
+    obj_hashtable<expr>::iterator it = u.begin();
+    obj_hashtable<expr>::iterator end = u.end();
+    for (; it != end; ++it)
+        tmp.push_back(*it);
+    return tmp;
+}
+
+unsigned proto_model::get_num_uninterpreted_sorts() const { 
+    return m_user_sort_factory->get_num_sorts(); 
+}
+
+sort * proto_model::get_uninterpreted_sort(unsigned idx) const { 
+    SASSERT(idx < get_num_uninterpreted_sorts()); 
+    return m_user_sort_factory->get_sort(idx); 
+}
+
+/**
+   \brief Return true if the given sort is uninterpreted and has a finite interpretation
+   in the model.
+*/
+bool proto_model::is_finite(sort * s) const {
+    return m_manager.is_uninterp(s) && m_user_sort_factory->is_finite(s);
+}
+
+expr * proto_model::get_some_value(sort * s) {
+    family_id fid = s->get_family_id();
+    if (fid == null_family_id) {
+        return m_user_sort_factory->get_some_value(s);
+    }
+    value_factory * f = get_factory(fid);
+    if (f) 
+        return f->get_some_value(s);
+    // there is no factory for the family id, then assume s is uninterpreted.
+    return m_user_sort_factory->get_some_value(s);
+}
+
+bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
+    family_id fid = s->get_family_id();
+    if (fid == null_family_id) {
+        return m_user_sort_factory->get_some_values(s, v1, v2);
+    }
+    value_factory * f = get_factory(fid);
+    if (f) 
+        return f->get_some_values(s, v1, v2);
+    else
+        return false;
+}
+
+expr * proto_model::get_fresh_value(sort * s) {
+    family_id fid = s->get_family_id();
+    if (fid == null_family_id)
+        return m_user_sort_factory->get_fresh_value(s);
+    value_factory * f = get_factory(fid);
+    if (f) 
+        return f->get_fresh_value(s);
+    else
+        // Use user_sort_factory if the theory has no support for model construnction.
+        // This is needed when dummy theories are used for arithmetic or arrays.
+        return m_user_sort_factory->get_fresh_value(s);
+}
+
+void proto_model::register_value(expr * n) {
+    sort * s = m_manager.get_sort(n);
+    family_id fid = s->get_family_id();
+    if (fid == null_family_id) {
+        m_user_sort_factory->register_value(n);
+    }
+    else {
+        value_factory * f = get_factory(fid);
+        if (f)
+            f->register_value(n);
+    }
+}
+
+bool proto_model::is_array_value(expr * v) const {
+    return is_app_of(v, m_afid, OP_AS_ARRAY);
+}
+
+void proto_model::compress() {
+    ptr_vector<func_decl>::iterator it  = m_func_decls.begin();
+    ptr_vector<func_decl>::iterator end = m_func_decls.end();
+    for (; it != end; ++it) {
+        func_decl * f = *it;
+        func_interp * fi = get_func_interp(f);
+        SASSERT(fi != 0);
+        fi->compress();
+    }
+}
+
+/**
+   \brief Complete the interpretation fi of f if it is partial.
+   If f does not have an interpretation in the given model, then this is a noop.
+*/
+void proto_model::complete_partial_func(func_decl * f) {
+    func_interp * fi = get_func_interp(f);
+    if (fi && fi->is_partial()) {
+        expr * else_value = 0;
+#if 0 
+        // For UFBV benchmarks, setting the "else" to false is not a good idea.
+        // TODO: find a permanent solution. A possibility is to add another option.
+        if (m_manager.is_bool(f->get_range())) {
+            else_value = m_manager.mk_false();
+        }
+        else {
+            else_value = fi->get_max_occ_result();
+            if (else_value == 0)
+                else_value = get_some_value(f->get_range());
+        }
+#else
+        else_value = fi->get_max_occ_result();
+        if (else_value == 0)
+            else_value = get_some_value(f->get_range());
+#endif
+        fi->set_else(else_value);
+    }
+}
+
+/**
+   \brief Set the (else) field of function interpretations... 
+*/
+void proto_model::complete_partial_funcs() {
+    if (m_params.m_model_partial)
+        return;
+
+    ptr_vector<func_decl>::iterator it  = m_func_decls.begin();
+    ptr_vector<func_decl>::iterator end = m_func_decls.end();
+    for (; it != end; ++it)
+        complete_partial_func(*it);
+}
+
+model * proto_model::mk_model() {
+    TRACE("proto_model", tout << "mk_model\n"; model_v2_pp(tout, *this););
+    model * m = alloc(model, m_manager);
+
+    decl2expr::iterator it1  = m_interp.begin();
+    decl2expr::iterator end1 = m_interp.end();
+    for (; it1 != end1; ++it1) {
+        m->register_decl(it1->m_key, it1->m_value);
+    }
+
+    decl2finterp::iterator it2  = m_finterp.begin();
+    decl2finterp::iterator end2 = m_finterp.end();
+    for (; it2 != end2; ++it2) {
+        m->register_decl(it2->m_key, it2->m_value);
+    }
+    m_finterp.reset(); // m took the ownership of the func_interp's
+
+    unsigned sz = get_num_uninterpreted_sorts();
+    for (unsigned i = 0; i < sz; i++) {
+        sort * s = get_uninterpreted_sort(i);
+        TRACE("proto_model", tout << "copying uninterpreted sorts...\n" << mk_pp(s, m_manager) << "\n";);
+        ptr_buffer<expr> buf;
+        obj_hashtable<expr> const & u = get_known_universe(s);
+        obj_hashtable<expr>::iterator it  = u.begin();
+        obj_hashtable<expr>::iterator end = u.end();
+        for (; it != end; ++it) {
+            buf.push_back(*it);
+        }
+        m->register_usort(s, buf.size(), buf.c_ptr());
+    }
+
+    return m;
+}

src/model/proto_model.h

@@ -0,0 +1,119 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    proto_model.h
+
+Abstract:
+
+    This is the old model object.
+    smt::context used it during model construction and for
+    reporting the model for external consumers. 
+    The whole value_factory "business" was due to model construction
+    and unnecessary for external consumers.
+    Future solvers will not use value_factory objects for 
+    helping during model construction. 
+    
+    After smt::context finishes building the model, it is converted
+    into a new (light) model object.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2007-03-08.
+
+Revision History:
+
+--*/
+#ifndef _PROTO_MODEL_H_
+#define _PROTO_MODEL_H_
+
+#include"model_core.h"
+#include"model_params.h"
+#include"value_factory.h"
+#include"plugin_manager.h"
+#include"simplifier.h"
+#include"arith_decl_plugin.h"
+#include"func_decl_dependencies.h"
+#include"model.h"
+
+class proto_model : public model_core {
+    model_params const &          m_params; 
+    ast_ref_vector                m_asts;
+    plugin_manager<value_factory> m_factories;
+    user_sort_factory *           m_user_sort_factory;
+    simplifier &                  m_simplifier;
+    family_id                     m_afid;        //!< array family id: hack for displaying models in V1.x style
+    func_decl_set                 m_aux_decls;
+    ptr_vector<expr>              m_tmp;
+
+    void reset_finterp();
+
+    expr * mk_some_interp_for(func_decl * d);
+
+    // Invariant: m_decls subset m_func_decls union m_const_decls union union m_value_decls
+    // Invariant: m_func_decls  subset m_decls
+    // Invariant: m_const_decls subset m_decls
+    
+    void remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, func_decl_set const & s);
+    void cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs);
+
+
+public:
+    proto_model(ast_manager & m, simplifier & s, model_params const & p);
+    virtual ~proto_model(); 
+
+    model_params const & get_model_params() const { return m_params; }
+
+    void register_factory(value_factory * f) { m_factories.register_plugin(f); }
+
+    bool eval(expr * e, expr_ref & result, bool model_completion = false);
+
+    bool is_array_value(expr * v) const;
+    
+    value_factory * get_factory(family_id fid);
+
+    expr * get_some_value(sort * s);
+
+    bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2);
+
+    expr * get_fresh_value(sort * s);
+
+    void register_value(expr * n);
+
+    //
+    // Primitives for building models
+    //
+    void register_decl(func_decl * d, expr * v);
+    void register_decl(func_decl * f, func_interp * fi, bool aux = false);
+    void reregister_decl(func_decl * f, func_interp * new_fi, func_decl * f_aux);
+    void compress();
+    void cleanup();
+
+    //
+    // Primitives for building finite interpretations for uninterpreted sorts,
+    // and retrieving the known universe.
+    //
+    void freeze_universe(sort * s);
+    bool is_finite(sort * s) const;
+    obj_hashtable<expr> const & get_known_universe(sort * s) const;
+    virtual ptr_vector<expr> const & get_universe(sort * s) const;
+    virtual unsigned get_num_uninterpreted_sorts() const;
+    virtual sort * get_uninterpreted_sort(unsigned idx) const;
+
+    //
+    // Complete partial function interps
+    //
+    void complete_partial_func(func_decl * f);
+    void complete_partial_funcs();
+
+    //
+    // Create final model object. 
+    // proto_model is corrupted after that.
+    model * mk_model();
+};
+
+typedef ref<proto_model> proto_model_ref;
+
+#endif /* _PROTO_MODEL_H_ */
+

src/model/value.cpp

@@ -0,0 +1,42 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    value.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2007-08-17.
+
+Revision History:
+
+--*/
+#include"value.h"
+
+void bool_value::display(std::ostream & out) const {
+    out << (m_value ? "true" : "false");
+}
+
+unsigned bool_value::hash() const {
+    return m_value ? 1 : 0;
+}
+
+bool bool_value::operator==(const value & other) const {
+    const bool_value * o = dynamic_cast<const bool_value*>(&other);
+    return o && m_value == o->m_value;
+}
+
+basic_factory::basic_factory(ast_manager & m):
+    value_factory(symbol("basic"), m),
+    m_bool(m) {
+    m_bool  = m.mk_type(m.get_basic_family_id(), BOOL_SORT);
+    m_true  = alloc(bool_value, true, m_bool.get());
+    m_false = alloc(bool_value, false, m_bool.get());
+}
+
+

src/model/value.h

@@ -0,0 +1,162 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    value.h
+
+Abstract:
+
+    Abstract class used to represent values in a model.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2007-08-14.
+
+Revision History:
+
+--*/
+#ifndef _VALUE_H_
+#define _VALUE_H_
+
+#include"core_model.h"
+#include"ast.h"
+#include"ref.h"
+
+class model;
+
+class value {
+    partition_id m_partition_id;
+    unsigned     m_ref_count;
+    type_ast *   m_type;
+
+    friend class model;
+
+    void set_partition_id(partition_id id) { 
+        m_partition_id = id;
+    }
+
+public:
+    value(type_ast * ty):
+        m_partition_id(null_partition_id),
+        m_ref_count(0),
+        m_type(ty) {
+    }
+
+    virtual ~value() {}
+
+    void inc_ref() { m_ref_count ++; }
+    
+    void dec_ref() { 
+        SASSERT(m_ref_count > 0);
+        m_ref_count--;
+        if (m_ref_count == 0) {
+            dealloc(this);
+        }
+    }
+
+    partition_id get_partition_id() { return m_partition_id; }
+
+    type_ast * get_type() const { return m_type; }
+
+    virtual void display(std::ostream & out) const = 0;
+
+    virtual unsigned hash() const = 0;
+
+    virtual bool operator==(const value & other) const = 0;
+
+    virtual void infer_types(ast_vector<type_ast> & result) { /* default: do nothing */ }
+    
+    virtual void collect_used_partitions(svector<bool> & result) { /* default: do nothing */ }
+};
+
+inline std::ostream & operator<<(std::ostream & target, const value & v) {
+    v.display(target);
+    return target;
+}
+
+class value_factory {
+    family_id     m_fid;
+public:
+    value_factory(symbol fname, ast_manager & m):
+        m_fid(m.get_family_id(fname)) {
+    }
+    
+    virtual ~value_factory() {}
+    
+    // Return some value of the given type
+    virtual value * get_some_value(type_ast * ty) = 0; 
+
+    // Return two distinct values of the given type
+    virtual bool get_some_values(type_ast * ty, ref<value> & v1, ref<value> & v2) = 0;
+    
+    // Return a fresh value of the given type
+    virtual value * get_fresh_value(type_ast * ty) = 0;
+
+    virtual value * update_value(value * source, const svector<partition_id> & pid2pid) {
+        return source;
+    }
+
+    family_id get_family_id() const { return m_fid; }
+};
+
+class bool_value : public value {
+    friend class basic_factory;
+    bool m_value;
+
+    bool_value(bool v, type_ast * ty):
+        value(ty),
+        m_value(v) {
+    }
+
+public:
+   
+    bool get_value() const { 
+        return m_value;
+    }
+
+    virtual void display(std::ostream & out) const;
+
+    virtual unsigned hash() const;
+
+    virtual bool operator==(const value & other) const;
+};
+
+class basic_factory : public value_factory {
+    ast_ref<type_ast> m_bool;
+    ref<bool_value> m_true;
+    ref<bool_value> m_false;
+public:
+    basic_factory(ast_manager & m);
+
+    virtual ~basic_factory() {}
+
+    bool_value * get_true() const { 
+        return m_true.get();
+    }
+
+    bool_value * get_false() const {
+        return m_false.get();
+    }
+
+    // Return some value of the given type
+    virtual value * get_some_value(type_ast * ty) {
+        return get_false();
+    }
+
+    // Return two distinct values of the given type
+    virtual bool get_some_values(type_ast * ty, ref<value> & v1, ref<value> & v2) {
+        v1 = get_false();
+        v2 = get_true();
+        return true;
+    }
+    
+    // Return a fresh value of the given type
+    virtual value * get_fresh_value(type_ast * ty) {
+        // it is not possible to create new fresh values... 
+        return 0;
+    }
+};
+
+#endif /* _VALUE_H_ */
+

src/model/value_factory.cpp

@@ -0,0 +1,117 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    value_factory.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-10-28.
+
+Revision History:
+
+--*/
+
+#include"value_factory.h"
+
+value_factory::value_factory(ast_manager & m, family_id fid):
+    m_manager(m), 
+    m_fid(fid) {
+}
+
+value_factory::~value_factory() {
+}
+
+basic_factory::basic_factory(ast_manager & m):
+    value_factory(m, m.get_basic_family_id()) {
+}
+
+expr * basic_factory::get_some_value(sort * s) {
+    if (m_manager.is_bool(s))
+        return m_manager.mk_false();
+    return 0;
+}
+
+bool basic_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
+    if (m_manager.is_bool(s)) {
+        v1 = m_manager.mk_false();
+        v2 = m_manager.mk_true();
+        return true;
+    }
+    return false;
+}
+    
+expr * basic_factory::get_fresh_value(sort * s) {
+    return 0;
+}
+
+user_sort_factory::user_sort_factory(ast_manager & m): 
+    simple_factory<unsigned>(m, m.get_family_id("user-sort")) {
+}
+
+void user_sort_factory::freeze_universe(sort * s) {
+    if (!m_finite.contains(s)) {
+        value_set * set = 0;
+        m_sort2value_set.find(s, set);
+        if (!m_sort2value_set.find(s, set) || set->m_values.empty()) {
+            // we cannot freeze an empty universe.
+            get_some_value(s); // add one element to the universe...
+        }
+        SASSERT(m_sort2value_set.find(s, set) && set != 0 && !set->m_values.empty());
+        m_finite.insert(s);
+    }
+}
+
+obj_hashtable<expr> const & user_sort_factory::get_known_universe(sort * s) const {
+    value_set * set = 0;
+    if (m_sort2value_set.find(s, set)) {
+        return set->m_values;
+    }
+    return m_empty_universe;
+}
+
+expr * user_sort_factory::get_some_value(sort * s) {
+    if (is_finite(s)) {
+        value_set * set = 0;
+        m_sort2value_set.find(s, set);
+        SASSERT(set != 0);
+        SASSERT(!set->m_values.empty());
+        return *(set->m_values.begin());
+    }
+    return simple_factory<unsigned>::get_some_value(s);
+}
+
+bool user_sort_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
+    if (is_finite(s)) {
+        value_set * set = 0;
+        if (m_sort2value_set.find(s, set) && set->m_values.size() >= 2) {
+            obj_hashtable<expr>::iterator it = set->m_values.begin();
+            v1 = *it;
+            ++it;
+            v2 = *it;
+            return true;
+        }
+        return false;
+    }
+    return simple_factory<unsigned>::get_some_values(s, v1, v2);
+}
+
+expr * user_sort_factory::get_fresh_value(sort * s) {
+    if (is_finite(s))
+        return 0;
+    return simple_factory<unsigned>::get_fresh_value(s);
+}
+
+void user_sort_factory::register_value(expr * n) {
+    SASSERT(!is_finite(m_manager.get_sort(n)));
+    simple_factory<unsigned>::register_value(n);
+}
+
+app * user_sort_factory::mk_value_core(unsigned const & val, sort * s) {
+    return m_manager.mk_model_value(val, s);
+}

src/model/value_factory.h

@@ -0,0 +1,257 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    value_factory.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-10-28.
+
+Revision History:
+
+--*/
+#ifndef _VALUE_FACTORY_H_
+#define _VALUE_FACTORY_H_
+
+#include"ast.h"
+#include"obj_hashtable.h"
+
+/**
+   \brief Auxiliary object used during model construction.
+*/
+class value_factory {
+protected:
+    ast_manager & m_manager;
+    family_id     m_fid;
+public:
+    value_factory(ast_manager & m, family_id fid);
+
+    virtual ~value_factory();
+
+    /**
+       \brief Return some value of the given sort. The result is always different from zero.
+    */
+    virtual expr * get_some_value(sort * s) = 0;
+
+    /**
+       \brief Return two distinct values of the given sort. The results are stored in v1 and v2.
+       Return false if the intended interpretation of the given sort has only one element. 
+    */
+    virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0;
+    
+    /**
+       \brief Return a fresh value of the given sort. 
+       Return 0 if it is not possible to do that (e.g., the sort is finite).
+    */
+    virtual expr * get_fresh_value(sort * s) = 0;
+
+    /**
+       \brief Used to register that the given value was used in model construction.
+       So, get_fresh_value cannot return this value anymore.
+    */
+    virtual void register_value(expr * n) = 0;
+
+    family_id get_family_id() const { return m_fid; }
+};
+
+class basic_factory : public value_factory {
+public:
+    basic_factory(ast_manager & m);
+    
+    virtual expr * get_some_value(sort * s);
+
+    virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2);
+    
+    virtual expr * get_fresh_value(sort * s);
+
+    virtual void register_value(expr * n) { }
+};
+
+/**
+   \brief Template for value factories for numeric (and enumeration-like) sorts
+*/
+template<typename Number>
+class simple_factory : public value_factory {
+protected:
+    struct value_set {
+        obj_hashtable<expr> m_values;
+        Number              m_next;
+        value_set():
+            m_next(0) {
+        }
+    };
+    
+    typedef obj_map<sort, value_set *> sort2value_set;
+    
+    sort2value_set         m_sort2value_set;
+    expr_ref_vector        m_values;
+    sort_ref_vector        m_sorts;
+    ptr_vector<value_set>  m_sets;
+
+    value_set * get_value_set(sort * s) {
+        value_set * set = 0;
+        if (!m_sort2value_set.find(s, set)) {
+            set = alloc(value_set);
+            m_sort2value_set.insert(s, set);
+            m_sorts.push_back(s);
+            m_sets.push_back(set);
+        }
+        SASSERT(set != 0);
+        DEBUG_CODE({
+            value_set * set2 = 0;
+            SASSERT(m_sort2value_set.find(s, set2));
+            SASSERT(set == set2);
+        });
+        return set;
+    }
+
+    virtual app * mk_value_core(Number const & val, sort * s) = 0;
+
+    app * mk_value(Number const & val, sort * s, bool & is_new) {
+        value_set * set = get_value_set(s);
+        app * new_val   = mk_value_core(val, s);
+        is_new          = false;
+        if (!set->m_values.contains(new_val)) {
+            m_values.push_back(new_val);
+            set->m_values.insert(new_val);
+            is_new = true;
+        }
+        SASSERT(set->m_values.contains(new_val));
+        return new_val;
+    }
+
+public:
+    simple_factory(ast_manager & m, family_id fid):
+        value_factory(m, fid),
+        m_values(m),
+        m_sorts(m) {
+    }
+
+    virtual ~simple_factory() {
+        std::for_each(m_sets.begin(), m_sets.end(), delete_proc<value_set>());
+    }
+    
+    virtual expr * get_some_value(sort * s) {
+        value_set * set = 0;
+        expr * result = 0;
+        if (m_sort2value_set.find(s, set) && !set->m_values.empty()) 
+            result = *(set->m_values.begin());
+        else
+            result = mk_value(Number(0), s);
+        return result;
+    }
+
+    virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
+        value_set * set = 0;
+        if (m_sort2value_set.find(s, set)) {
+            switch (set->m_values.size()) {
+            case 0:
+                v1 = mk_value(Number(0), s);
+                v2 = mk_value(Number(1), s);
+                break;
+            case 1:
+                v1 = *(set->m_values.begin());
+                v2 = mk_value(Number(0), s);
+                if (v1 == v2)
+                    v2 = mk_value(Number(1), s);
+                break;
+            default:
+                obj_hashtable<expr>::iterator it = set->m_values.begin();
+                v1 = *it;
+                ++it;
+                v2 = *it;
+                break;
+            }
+            SASSERT(v1 != v2);
+            return true;
+        }
+        v1 = mk_value(Number(0), s);
+        v2 = mk_value(Number(1), s);
+        return true;
+    }
+
+    virtual expr * get_fresh_value(sort * s) {
+        value_set * set  = get_value_set(s);
+        bool is_new      = false;
+        expr * result    = 0;
+        Number & next    = set->m_next;
+        while (!is_new) {
+            result = mk_value(next, s, is_new);
+            next++;
+        }
+        SASSERT(result != 0);
+        return result;
+    }
+
+    virtual void register_value(expr * n) {
+        sort * s = this->m_manager.get_sort(n);
+        value_set * set  = get_value_set(s);
+        if (!set->m_values.contains(n)) {
+            m_values.push_back(n);
+            set->m_values.insert(n);
+        }
+    }
+        
+    virtual app * mk_value(Number const & val, sort * s) {
+        bool is_new;
+        return mk_value(val, s, is_new);
+    }
+
+    unsigned get_num_sorts() const { return m_sorts.size(); }
+
+    sort * get_sort(unsigned idx) const { return m_sorts.get(idx); }
+};
+
+/**
+   \brief Factory for creating values for uninterpreted sorts and user
+   declared (uninterpreted) sorts.
+*/
+class user_sort_factory : public simple_factory<unsigned> {
+    obj_hashtable<sort>  m_finite;   //!< set of sorts that are marked as finite.
+    obj_hashtable<expr>  m_empty_universe;
+    virtual app * mk_value_core(unsigned const & val, sort * s);
+public:
+    user_sort_factory(ast_manager & m);
+    virtual ~user_sort_factory() {}
+
+    /**
+       \brief Make the universe of \c s finite, by preventing new
+       elements to be added to its universe.
+    */
+    void freeze_universe(sort * s);
+
+    /**
+       \brief Return true if the universe of \c s is frozen and finite.
+    */
+    bool is_finite(sort * s) const {
+        return m_finite.contains(s);
+    }
+
+    /**
+       \brief Return the "known" universe of \c s. It doesn't matter whether
+       s is finite or not. If \c s is finite, then it is the whole universe.
+    */
+    obj_hashtable<expr> const & get_known_universe(sort * s) const;
+
+    /**
+       \brief Return sorts with finite interpretations.
+    */
+    obj_hashtable<sort> const & get_finite_sorts() const { return m_finite; }
+
+    virtual expr * get_some_value(sort * s);
+
+    virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2);
+
+    virtual expr * get_fresh_value(sort * s);
+    
+    virtual void register_value(expr * n);
+};
+
+#endif /* _VALUE_FACTORY_H_ */
+