Reorganizing the code

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

src/ast/expr_map.cpp

@@ -0,0 +1,94 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    expr_map.cpp
+
+Abstract:
+
+    Mapping from expressions to expressions + proofs. This mapping
+    is used to cache simplification results. 
+    For every entry [e1->(e2, p)] we have that p is a proof that (= e1 e2).
+
+Author:
+
+    Leonardo (leonardo) 2008-01-03
+
+Notes:
+
+--*/
+#include"expr_map.h"
+#include"dec_ref_util.h"
+
+expr_map::expr_map(ast_manager & m):
+    m_manager(m),
+    m_store_proofs(m.proofs_enabled()) {
+}
+
+expr_map::expr_map(ast_manager & m, bool store_proofs):
+    m_manager(m),
+    m_store_proofs(store_proofs) {
+}
+
+expr_map::~expr_map() {
+    reset();
+}
+
+void expr_map::insert(expr * k, expr * d, proof * p) {  
+    m_manager.inc_ref(d);
+    obj_map<expr, expr*>::obj_map_entry * entry = m_expr2expr.find_core(k);
+    if (entry != 0) {
+        m_manager.dec_ref(entry->get_data().m_value);
+        entry->get_data().m_value = d;
+        if (m_store_proofs) {
+            m_manager.inc_ref(p);
+            obj_map<expr, proof*>::obj_map_entry * entry_pr = m_expr2pr.find_core(k);
+            SASSERT(entry_pr != 0);
+            m_manager.dec_ref(entry_pr->get_data().m_value);
+            entry_pr->get_data().m_value = p;
+        }
+    }
+    else {
+        m_manager.inc_ref(k);
+        m_expr2expr.insert(k, d);
+        if (m_store_proofs) {
+            m_manager.inc_ref(p);
+            m_expr2pr.insert(k, p);
+        }
+    }
+}
+
+void expr_map::get(expr * k, expr * & d, proof * & p) const {
+    if (m_expr2expr.find(k, d)) {
+        p = 0;
+        if (m_store_proofs)
+            m_expr2pr.find(k, p);
+    }
+}
+
+void expr_map::erase(expr * k) {
+    expr * v;
+    if (m_expr2expr.find(k, v)) {
+        m_expr2expr.erase(k);
+        m_manager.dec_ref(v);
+        if (m_store_proofs) {
+            proof * pr = 0;
+            m_expr2pr.find(k, pr);
+            m_expr2pr.erase(k);
+            m_manager.dec_ref(pr);
+        }
+        m_manager.dec_ref(k);
+    }
+}
+
+void expr_map::reset() {
+    dec_ref_values(m_manager, m_expr2pr);
+    dec_ref_key_values(m_manager, m_expr2expr);
+}
+
+void expr_map::flush() {
+    reset();
+    m_expr2expr.finalize();
+    m_expr2pr.finalize();
+}

src/ast/expr_map.h

@@ -0,0 +1,49 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    expr_map.h
+
+Abstract:
+
+    Mapping from expressions to expressions + proofs. This mapping
+    is used to cache simplification results. 
+    For every entry [e1->(e2, p)] we have that p is a proof that (= e1 e2).
+
+Author:
+
+    Leonardo (leonardo) 2008-01-03
+
+Notes:
+
+--*/
+#ifndef _EXPR_MAP_H_
+#define _EXPR_MAP_H_
+
+#include"ast.h"
+#include"obj_hashtable.h"
+
+/**
+   \brief Map from expressions to expressions+proofs.
+
+   When proof production is disabled, no extra space is used.
+*/
+class expr_map {
+    ast_manager &         m_manager;
+    bool                  m_store_proofs;
+    obj_map<expr, expr*>  m_expr2expr;
+    obj_map<expr, proof*> m_expr2pr;
+public:
+    expr_map(ast_manager & m);
+    expr_map(ast_manager & m, bool store_proofs);
+    ~expr_map();
+    void insert(expr * k, expr * d, proof * p);
+    bool contains(expr * k) const { return m_expr2expr.contains(k); }
+    void get(expr * k, expr * & d, proof * & p) const;
+    void erase(expr * k);
+    void reset();
+    void flush();
+};
+
+#endif

src/ast/func_decl_dependencies.cpp

@@ -0,0 +1,225 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    func_decl_dependencies.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2010-12-15.
+
+Revision History:
+
+--*/
+#include"func_decl_dependencies.h"
+#include"for_each_expr.h"
+#include"ast_util.h"
+
+struct collect_dependencies_proc {
+    ast_manager &     m_manager;
+    func_decl_set &   m_set;
+    bool              m_ng_only; // collect only declarations in non ground expressions
+   
+    collect_dependencies_proc(ast_manager & m, func_decl_set & s, bool ng_only):
+        m_manager(m),
+        m_set(s),
+        m_ng_only(ng_only) {}
+
+    void operator()(var * n) {}
+    
+    void operator()(quantifier * n) {}
+    
+    void operator()(app * n) {        
+        // We do not need to track dependencies on constants ...
+        if (n->get_num_args()==0) 
+            return;
+        if (m_ng_only && is_ground(n))
+            return;
+        // ... and interpreted function symbols
+        func_decl * d = n->get_decl();
+        if (d->get_family_id() == null_family_id) {
+            m_set.insert(d);
+        }
+    }
+};
+
+void collect_func_decls(ast_manager & m, expr * n, func_decl_set & r, bool ng_only) {
+    collect_dependencies_proc proc(m, r, ng_only);
+    for_each_expr(proc, n);
+}
+
+void func_decl_dependencies::reset() {
+    dependency_graph::iterator it  = m_deps.begin();
+    dependency_graph::iterator end = m_deps.end();
+    for (; it != end; ++it) {
+        func_decl * f  = (*it).m_key;
+        func_decl_set * s    = (*it).m_value;
+        m_manager.dec_ref(f);
+        dec_ref(m_manager, *s);
+        dealloc(s);
+    }
+    m_deps.reset();
+}
+
+void func_decl_dependencies::collect_func_decls(expr * n, func_decl_set * s) {
+    ::collect_func_decls(m_manager, n, *s, false);
+}
+
+void func_decl_dependencies::collect_ng_func_decls(expr * n, func_decl_set * s) {
+    ::collect_func_decls(m_manager, n, *s, true);
+}
+
+/**
+   \brief Functor for finding cycles in macro definitions
+*/
+class func_decl_dependencies::top_sort {
+    enum color { OPEN, IN_PROGRESS, CLOSED };
+    ast_manager &       m_manager;    
+    dependency_graph &  m_deps;
+
+    typedef obj_map<func_decl, color> color_map;
+    color_map               m_colors;
+    ptr_vector<func_decl>   m_todo;
+
+    func_decl_set * definition(func_decl * f) const {        
+        func_decl_set * r = 0;
+        m_deps.find(f, r);
+        return r;
+    }
+
+    color get_color(func_decl * f) const {
+        if (!f) 
+            return CLOSED;
+        color_map::iterator it = m_colors.find_iterator(f);
+        if (it != m_colors.end()) 
+            return it->m_value;
+        return OPEN;
+    }
+
+    void set_color(func_decl * f, color c) {        
+        m_colors.insert(f, c);
+    }
+
+    void visit(func_decl * f, bool & visited) {
+        if (get_color(f) != CLOSED) {
+            m_todo.push_back(f);
+            visited = false;
+        }
+    }
+
+    bool visit_children(func_decl * f) {              
+        func_decl_set * def = definition(f);
+        if (!def) 
+            return true;
+        bool visited = true;
+        func_decl_set::iterator it  = def->begin();
+        func_decl_set::iterator end = def->end();
+        for (; it != end; ++it) {
+            visit(*it, visited);
+        }
+        return visited;
+    }
+
+    bool all_children_closed(func_decl * f) const {
+        func_decl_set * def = definition(f);
+        if (!def) 
+            return true;
+        func_decl_set::iterator it  = def->begin();
+        func_decl_set::iterator end = def->end();
+        for (; it != end; ++it) {
+            if (get_color(*it) != CLOSED)
+                return false;
+        }
+        return true;
+    }
+
+    /**
+       \brief Return \c true if a cycle is detected.
+    */
+    bool main_loop(func_decl * f) {
+        if (get_color(f) == CLOSED) 
+            return false;
+        m_todo.push_back(f);
+        while (!m_todo.empty()) {
+            func_decl * f = m_todo.back();
+            
+            switch (get_color(f)) {
+            case CLOSED:                
+                m_todo.pop_back();
+                break;
+            case OPEN:
+                set_color(f, IN_PROGRESS);
+                if (visit_children(f)) {
+                    SASSERT(m_todo.back() == f);
+                    m_todo.pop_back();
+                    set_color(f, CLOSED);
+                }
+                break;
+            case IN_PROGRESS: 
+                if (all_children_closed(f)) {
+                    SASSERT(m_todo.back() == f);
+                    set_color(f, CLOSED);
+                } else {
+                    m_todo.reset();
+                    return true;
+                }
+                break;
+            default:
+                UNREACHABLE();
+            }
+        }
+        return false;
+    }
+
+public:
+    top_sort(ast_manager & m, dependency_graph & deps):m_manager(m), m_deps(deps) {}
+    
+    bool operator()(func_decl * new_decl) {
+
+        // [Leo]: It is not trivial to reuse m_colors between different calls since we are update the graph.
+        // To implement this optimization, we need an incremental topological sort algorithm.
+        // The trick of saving the dependencies will save a lot of time. So, I don't think we really
+        // need a incremental top-sort algo. 
+        m_colors.reset();
+        return main_loop(new_decl);
+    }
+};
+
+bool func_decl_dependencies::insert(func_decl * f, func_decl_set * s) {
+    if (m_deps.contains(f)) {
+        dealloc(s);
+        return false;
+    }
+
+    m_deps.insert(f, s);
+
+    top_sort cycle_detector(m_manager, m_deps);
+    if (cycle_detector(f)) {
+        m_deps.erase(f);
+        dealloc(s);
+        return false;
+    }
+
+    m_manager.inc_ref(f);
+    inc_ref(m_manager, *s);
+    return true;
+}
+
+void func_decl_dependencies::erase(func_decl * f) {
+    func_decl_set * s = 0;
+    if (m_deps.find(f, s)) {
+        m_manager.dec_ref(f);
+        dec_ref(m_manager, *s);
+        m_deps.erase(f);
+        dealloc(s);
+    }
+}
+
+void func_decl_dependencies::display(std::ostream & out) {
+    // TODO
+}

src/ast/func_decl_dependencies.h

@@ -0,0 +1,110 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    func_decl_dependencies.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2010-12-15.
+
+Revision History:
+
+--*/
+#ifndef _FUNC_DECL_DEPENDENCIES_H_
+#define _FUNC_DECL_DEPENDENCIES_H_
+
+#include"ast.h"
+#include"obj_hashtable.h"
+
+// Set of dependencies
+typedef obj_hashtable<func_decl> func_decl_set;
+
+/**
+   \brief Collect uninterpreted function declarations (with arity > 0) occurring in \c n.
+*/
+void collect_func_decls(ast_manager & m, expr * n, func_decl_set & r, bool ng_only = false);
+
+/**
+   \brief Auxiliary data-structure used for tracking dependencies between function declarations.
+
+   The following pattern of use is expected:
+   
+   func_decl_dependencies & dm;
+   func_decl_set * S = dm.mk_func_decl_set();
+   dm.collect_func_decls(t_1, S);
+   ...
+   dm.collect_func_decls(t_n, S);
+   dm.insert(f, S);
+*/
+class func_decl_dependencies {
+    typedef obj_map<func_decl, func_decl_set *> dependency_graph;
+    ast_manager &     m_manager;
+    dependency_graph  m_deps;
+
+    class top_sort;
+
+public:
+    func_decl_dependencies(ast_manager & m):m_manager(m) {}
+    ~func_decl_dependencies() {
+        reset();
+    }
+    
+    void reset();
+
+    /**
+       \brief Create a dependecy set.
+       This set should be populated using #collect_func_decls.
+       After populating the set, it must be used as an argument for the #insert method.
+
+       \remark The manager owns the set.
+
+       \warning Failure to call #insert will produce a memory leak.
+    */
+    func_decl_set * mk_func_decl_set() { return alloc(func_decl_set); }
+    
+    /**
+       \brief Store the uninterpreted function declarations used in \c n into \c s.
+    */
+    void collect_func_decls(expr * n, func_decl_set * s);
+    
+    /**
+       \brief Store the uninterpreted function declarations (in non ground terms) used in \c n into \c s.
+    */
+    void collect_ng_func_decls(expr * n, func_decl_set * s);
+
+    /**
+       \brief Insert \c f in the manager with the given set of dependencies.
+       The insertion succeeds iff 
+            1- no cycle is created between the new entry and
+            the already existing dependencies. 
+            2- \c f was not already inserted into the manager.
+       
+       Return false in case of failure. 
+
+       \remark The manager is the owner of the dependency sets.
+    */
+    bool insert(func_decl * f, func_decl_set * s);
+
+    /**
+       \brief Return true if \c f is registered in this manager.
+    */
+    bool contains(func_decl * f) const { return m_deps.contains(f); }
+
+    func_decl_set * get_dependencies(func_decl * f) const { func_decl_set * r = 0; m_deps.find(f, r); return r; }
+
+    /**
+       \brief Erase \c f (and its dependencies) from the manager.
+    */
+    void erase(func_decl * f);
+
+    void display(std::ostream & out);
+};
+
+
+#endif

src/ast/used_symbols.h

@@ -0,0 +1,105 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    used_symbols.h
+
+Abstract:
+
+    Collect the symbols used in an expression.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-01-11.
+
+Revision History:
+
+--*/
+#ifndef _USED_SYMBOLS_H_
+#define _USED_SYMBOLS_H_
+
+#include"ast.h"
+#include"hashtable.h"
+#include"obj_hashtable.h"
+
+struct do_nothing_rename_proc {
+    symbol operator()(symbol const & s) const { return s; }
+};
+
+/**
+   \brief Functor for collecting the symbols used in an expression.
+*/
+template<typename RENAME_PROC=do_nothing_rename_proc>
+class used_symbols : public RENAME_PROC { 
+    typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
+
+    symbol_set          m_used;
+    obj_hashtable<expr> m_visited;
+    ptr_vector<expr>    m_todo;
+
+    void found(symbol const & s) { m_used.insert(RENAME_PROC::operator()(s)); }
+
+    void visit(expr * n) {
+        if (!m_visited.contains(n)) {
+            m_visited.insert(n);
+            m_todo.push_back(n);
+        }
+    }
+
+public:
+    used_symbols(RENAME_PROC const & p = RENAME_PROC()):
+        RENAME_PROC(p) {
+    }
+    
+    void operator()(expr * n, bool ignore_quantifiers = false) {
+        m_visited.reset();
+        m_used.reset();
+        m_todo.reset();
+        visit(n);
+        while (!m_todo.empty()) {
+            n = m_todo.back();
+            m_todo.pop_back();
+            unsigned j;
+            switch (n->get_kind()) {
+            case AST_APP:
+                found(to_app(n)->get_decl()->get_name());
+                j = to_app(n)->get_num_args();
+                while (j > 0) {
+                    --j;
+                    visit(to_app(n)->get_arg(j));
+                }
+                break;
+            case AST_QUANTIFIER:
+                if (!ignore_quantifiers) {
+                    found(to_quantifier(n)->get_qid());
+                    unsigned num_decls = to_quantifier(n)->get_num_decls();
+                    for (unsigned i = 0; i < num_decls; i++)
+                        found(to_quantifier(n)->get_decl_name(i));
+                    unsigned num_pats = to_quantifier(n)->get_num_patterns();
+                    for (unsigned i = 0; i < num_pats; i++)
+                        visit(to_quantifier(n)->get_pattern(i));
+                    unsigned num_no_pats = to_quantifier(n)->get_num_no_patterns();
+                    for (unsigned i = 0; i < num_no_pats; i++)
+                        visit(to_quantifier(n)->get_no_pattern(i));
+                    visit(to_quantifier(n)->get_expr());
+                }
+                break;
+            default:
+                break;
+            }
+        }
+    }
+
+    bool contains(symbol const & s) const { return m_used.contains(RENAME_PROC::operator()(s)); }
+
+    bool contains_core(symbol const & s) const { return m_used.contains(s); }
+
+    void insert(symbol const & s) { m_used.insert(RENAME_PROC::operator()(s)); }
+    
+    void insert_core(symbol const & s) { m_used.insert(s); }
+
+    void erase_core(symbol const & s) { m_used.erase(s); }
+};
+
+#endif /* _USED_SYMBOLS_H_ */

src/model/model.cpp

@@ -20,7 +20,6 @@ Revision History:
 #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"

src/model/model_evaluator_params.cpp

@@ -1,76 +0,0 @@
-/*++
-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/proto_model.cpp

@@ -20,7 +20,6 @@ Revision History:
 #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"

src/model/value.cpp

@@ -1,42 +0,0 @@
-/*++
-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

@@ -1,162 +0,0 @@
-/*++
-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/muz/dl_simplifier_plugin.cpp

@@ -0,0 +1,64 @@
+/*++
+Copyright (c) 2010 Microsoft Corporation
+
+Module Name:
+
+    dl_simplifier_plugin.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2010-08-10
+
+Revision History:
+
+--*/
+
+#include"dl_simplifier_plugin.h"
+
+namespace datalog {
+
+    dl_simplifier_plugin::dl_simplifier_plugin(ast_manager& m) 
+        : simplifier_plugin(symbol("datalog_relation"), m),
+          m_util(m)
+    {}
+        
+    bool dl_simplifier_plugin::reduce(
+        func_decl * f, unsigned num_args, expr* const* args, expr_ref& result) {
+        uint64 v1, v2;
+        switch(f->get_decl_kind()) {
+        case OP_DL_LT:
+            if (m_util.try_get_constant(args[0], v1) &&
+                m_util.try_get_constant(args[1], v2)) {
+                result = (v1 < v2)?m_manager.mk_true():m_manager.mk_false();
+                return true;
+            }
+            // x < x <=> false
+            if (args[0] == args[1]) {
+                result = m_manager.mk_false();
+                return true;
+            }
+            // x < 0 <=> false
+            if (m_util.try_get_constant(args[1], v2) && v2 == 0) {
+                result = m_manager.mk_false();
+                return true;
+            }
+            // 0 < x <=> 0 != x
+            if (m_util.try_get_constant(args[1], v1) && v1 == 0) {
+                result = m_manager.mk_not(m_manager.mk_eq(args[0], args[1]));
+                return true;
+            }
+            break;
+
+        default:
+            break;
+        }
+        return false;
+    }
+    
+};
+
+

src/muz/dl_simplifier_plugin.h

@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2010 Microsoft Corporation
+
+Module Name:
+
+    dl_simplifier_plugin.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2010-08-10
+
+Revision History:
+
+--*/
+#ifndef _DL_SIMPLIFIER_PLUGIN_H_
+#define _DL_SIMPLIFIER_PLUGIN_H_
+
+#include"dl_decl_plugin.h"
+#include "simplifier_plugin.h"
+
+namespace datalog {
+
+    class dl_simplifier_plugin : public simplifier_plugin {
+        dl_decl_util  m_util;
+    public:
+        dl_simplifier_plugin(ast_manager& m);
+        
+        virtual bool reduce(func_decl * f, unsigned num_args, expr* const* args, expr_ref& result);
+        
+    };
+    
+};
+#endif /* _DL_SIMPLIFIER_PLUGIN_H_ */
+

src/simplifier/arith_simplifier_params.h

@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    arith_simplifier_params.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-05-09.
+
+Revision History:
+
+--*/
+#ifndef _ARITH_SIMPLIFIER_PARAMS_H_
+#define _ARITH_SIMPLIFIER_PARAMS_H_
+
+#include"ini_file.h"
+
+struct arith_simplifier_params {
+    bool    m_arith_expand_eqs;
+    bool    m_arith_process_all_eqs;
+
+    arith_simplifier_params():
+        m_arith_expand_eqs(false),
+        m_arith_process_all_eqs(false) {
+    }
+    
+    void register_params(ini_params & p);
+};
+    
+#endif /* _ARITH_SIMPLIFIER_PARAMS_H_ */
+

src/simplifier/arith_simplifier_plugin.cpp

@@ -0,0 +1,442 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    arith_simplifier_plugin.cpp
+
+Abstract:
+
+    Simplifier for the arithmetic family.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-08
+    
+--*/
+#include"arith_simplifier_plugin.h"
+#include"ast_pp.h"
+#include"ast_ll_pp.h"
+#include"ast_smt2_pp.h"
+
+arith_simplifier_plugin::~arith_simplifier_plugin() {
+}
+
+arith_simplifier_plugin::arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p):
+    poly_simplifier_plugin(symbol("arith"), m, OP_ADD, OP_MUL, OP_UMINUS, OP_SUB, OP_NUM),
+    m_params(p),
+    m_util(m),
+    m_bsimp(b),
+    m_int_zero(m),
+    m_real_zero(m) {
+    m_int_zero  = m_util.mk_numeral(rational(0), true);
+    m_real_zero = m_util.mk_numeral(rational(0), false);
+}
+
+/**
+   \brief Return true if the first monomial of t is negative.
+*/
+bool arith_simplifier_plugin::is_neg_poly(expr * t) const {
+    if (m_util.is_add(t)) {
+        t = to_app(t)->get_arg(0);
+    }
+    if (m_util.is_mul(t)) {
+        t = to_app(t)->get_arg(0);
+        rational r;
+        bool is_int;
+        if (m_util.is_numeral(t, r, is_int))
+            return r.is_neg();
+    }
+    return false;
+}
+
+void arith_simplifier_plugin::get_monomial_gcd(expr_ref_vector& monomials, numeral& g) {
+    g = numeral::zero();
+    numeral n;
+    for (unsigned  i = 0; !g.is_one() && i < monomials.size(); ++i) {
+        expr* e = monomials[i].get();
+        if (is_numeral(e, n)) {
+            g = gcd(abs(n), g);
+        }
+        else if (is_mul(e) && is_numeral(to_app(e)->get_arg(0), n)) {
+            g = gcd(abs(n), g);        
+        }
+        else {
+            g = numeral::one();
+            return;
+        }
+    }
+    if (g.is_zero()) {
+        g = numeral::one();
+    }
+}
+
+void arith_simplifier_plugin::div_monomial(expr_ref_vector& monomials, numeral const& g) {
+    numeral n;
+    for (unsigned  i = 0; i < monomials.size(); ++i) {
+        expr* e = monomials[i].get();
+        if (is_numeral(e, n)) {
+            SASSERT((n/g).is_int());
+            monomials[i] = mk_numeral(n/g);
+        }
+        else if (is_mul(e) && is_numeral(to_app(e)->get_arg(0), n)) {
+            SASSERT((n/g).is_int());
+            monomials[i] = mk_mul(n/g, to_app(e)->get_arg(1));
+        }
+        else {
+            UNREACHABLE();
+        }
+    }
+}
+
+void arith_simplifier_plugin::gcd_reduce_monomial(expr_ref_vector& monomials, numeral& k) {
+    numeral g, n;
+
+    get_monomial_gcd(monomials, g);
+    g = gcd(abs(k), g);
+
+    if (g.is_one()) {
+        return;
+    }
+    SASSERT(g.is_pos());
+
+    k = k / g;
+    div_monomial(monomials, g);
+    
+}
+
+template<arith_simplifier_plugin::op_kind Kind>
+void arith_simplifier_plugin::mk_le_ge_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
+    set_curr_sort(arg1);
+    bool is_int = m_curr_sort->get_decl_kind() == INT_SORT;
+    expr_ref_vector monomials(m_manager);
+    rational k;
+    TRACE("arith_eq_bug", tout << mk_ismt2_pp(arg1, m_manager) << "\n" << mk_ismt2_pp(arg2, m_manager) << "\n";);
+    process_sum_of_monomials(false, arg1, monomials, k);
+    process_sum_of_monomials(true,  arg2, monomials, k);
+    k.neg();
+    if (is_int) {
+        numeral g;
+        get_monomial_gcd(monomials, g);
+        if (!g.is_one()) {
+            div_monomial(monomials, g);
+            switch(Kind) {
+            case LE:
+                //
+                //   g*monmials' <= k
+                // <=> 
+                //   monomials' <= floor(k/g)
+                //
+                k = floor(k/g);
+                break;
+            case GE:
+                //
+                //   g*monmials' >= k
+                // <=> 
+                //   monomials' >= ceil(k/g)
+                //
+                k = ceil(k/g);
+                break;
+            case EQ:
+                k = k/g;
+                if (!k.is_int()) {
+                    result = m_manager.mk_false();
+                    return;
+                }
+                break;
+            }
+        }
+    }
+    expr_ref lhs(m_manager);
+    mk_sum_of_monomials(monomials, lhs);
+    if (m_util.is_numeral(lhs)) {
+        SASSERT(lhs == mk_zero());
+        if (( Kind == LE && numeral::zero() <= k) ||
+            ( Kind == GE && numeral::zero() >= k) ||
+            ( Kind == EQ && numeral::zero() == k))
+            result = m_manager.mk_true();
+        else
+            result = m_manager.mk_false();
+    }
+    else {
+        
+        if (is_neg_poly(lhs)) {
+            expr_ref neg_lhs(m_manager);
+            mk_uminus(lhs, neg_lhs);
+            lhs = neg_lhs;
+            k.neg();
+            expr * rhs = m_util.mk_numeral(k, is_int);
+            switch (Kind) {
+            case LE:
+                result = m_util.mk_ge(lhs, rhs); 
+                break;
+            case GE:
+                result = m_util.mk_le(lhs, rhs);
+                break;
+            case EQ:
+                result = m_manager.mk_eq(lhs, rhs);
+                break;
+            }
+        }
+        else {
+            expr * rhs = m_util.mk_numeral(k, is_int);
+            switch (Kind) {
+            case LE:
+                result = m_util.mk_le(lhs, rhs); 
+                break;
+            case GE:
+                result = m_util.mk_ge(lhs, rhs);
+                break;
+            case EQ:
+                result = m_manager.mk_eq(lhs, rhs);
+                break;
+            }
+        }
+    }
+}
+
+void arith_simplifier_plugin::mk_arith_eq(expr * arg1, expr * arg2, expr_ref & result) {
+    mk_le_ge_eq_core<EQ>(arg1, arg2, result);
+}
+
+void arith_simplifier_plugin::mk_le(expr * arg1, expr * arg2, expr_ref & result) {
+    mk_le_ge_eq_core<LE>(arg1, arg2, result);
+}
+
+void arith_simplifier_plugin::mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
+    mk_le_ge_eq_core<GE>(arg1, arg2, result);
+}
+
+void arith_simplifier_plugin::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
+    expr_ref tmp(m_manager);
+    mk_le(arg2, arg1, tmp);
+    m_bsimp.mk_not(tmp, result);
+}
+ 
+void arith_simplifier_plugin::mk_gt(expr * arg1, expr * arg2, expr_ref & result) {
+    expr_ref tmp(m_manager);
+    mk_le(arg1, arg2, tmp);
+    m_bsimp.mk_not(tmp, result);
+}
+
+void arith_simplifier_plugin::gcd_normalize(numeral & coeff, expr_ref& term) {
+    if (!abs(coeff).is_one()) {
+        set_curr_sort(term);
+        SASSERT(m_curr_sort->get_decl_kind() == INT_SORT);
+        expr_ref_vector monomials(m_manager);
+        rational k;
+        monomials.push_back(mk_numeral(numeral(coeff), true));
+        process_sum_of_monomials(false, term, monomials, k);
+        gcd_reduce_monomial(monomials, k);
+        numeral coeff1;
+        if (!is_numeral(monomials[0].get(), coeff1)) {
+            UNREACHABLE();
+        }
+        if (coeff1 == coeff) {
+            return;
+        }
+        monomials[0] = mk_numeral(k, true);
+        coeff = coeff1;        
+        mk_sum_of_monomials(monomials, term);        
+    }
+}
+
+
+void arith_simplifier_plugin::mk_div(expr * arg1, expr * arg2, expr_ref & result) {
+    set_curr_sort(arg1);
+    numeral v1, v2;
+    bool is_int;
+    if (m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
+        SASSERT(!is_int);
+        if (m_util.is_numeral(arg1, v1, is_int))
+            result = m_util.mk_numeral(v1/v2, false);
+        else {
+            numeral k(1);
+            k /= v2;
+            
+            expr_ref inv_arg2(m_util.mk_numeral(k, false), m_manager);
+            mk_mul(inv_arg2, arg1, result);
+        }
+    }
+    else
+        result = m_util.mk_div(arg1, arg2);
+}
+
+void arith_simplifier_plugin::mk_idiv(expr * arg1, expr * arg2, expr_ref & result) {
+    set_curr_sort(arg1);
+    numeral v1, v2;
+    bool is_int;
+    if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero())
+        result = m_util.mk_numeral(div(v1, v2), is_int);
+    else 
+        result = m_util.mk_idiv(arg1, arg2);
+}
+
+void arith_simplifier_plugin::prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result) {
+    SASSERT(m_util.is_int(e));
+    SASSERT(k.is_int() && k.is_pos());
+    numeral n;
+    bool is_int;
+
+    if (depth == 0) {
+        result = e;
+    }
+    else if (is_add(e) || is_mul(e)) {
+        expr_ref_vector args(m_manager);
+        expr_ref tmp(m_manager);
+        app* a = to_app(e);
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {
+            prop_mod_const(a->get_arg(i), depth - 1, k, tmp);
+            args.push_back(tmp);
+        }
+        reduce(a->get_decl(), args.size(), args.c_ptr(), result);
+    }
+    else if (m_util.is_numeral(e, n, is_int) && is_int) {
+        result = mk_numeral(mod(n, k), true);
+    }
+    else {
+        result = e;
+    }
+}
+
+void arith_simplifier_plugin::mk_mod(expr * arg1, expr * arg2, expr_ref & result) {
+    set_curr_sort(arg1);
+    numeral v1, v2;
+    bool is_int;
+    if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
+        result = m_util.mk_numeral(mod(v1, v2), is_int);
+    }
+    else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) {
+        result = m_util.mk_numeral(numeral(0), true);
+    }
+    else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos()) {
+        expr_ref tmp(m_manager);
+        prop_mod_const(arg1, 5, v2, tmp);
+        result = m_util.mk_mod(tmp, arg2);
+    }
+    else {
+        result = m_util.mk_mod(arg1, arg2);
+    }
+}
+
+void arith_simplifier_plugin::mk_rem(expr * arg1, expr * arg2, expr_ref & result) {
+    set_curr_sort(arg1);
+    numeral v1, v2;
+    bool is_int;
+    if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
+        numeral m = mod(v1, v2);
+        //
+        // rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2)
+        //
+        if (v2.is_neg()) {
+            m.neg();
+        }
+        result = m_util.mk_numeral(m, is_int);
+    }
+    else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) {
+        result = m_util.mk_numeral(numeral(0), true);
+    }
+    else if (m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) {
+        expr_ref tmp(m_manager);
+        prop_mod_const(arg1, 5, v2, tmp);
+        result = m_util.mk_mod(tmp, arg2);
+        if (v2.is_neg()) {
+            result = m_util.mk_uminus(result);
+        }
+    }
+    else {
+        result = m_util.mk_rem(arg1, arg2);
+    }
+}
+
+void arith_simplifier_plugin::mk_to_real(expr * arg, expr_ref & result) {
+    numeral v;
+    if (m_util.is_numeral(arg, v))
+        result = m_util.mk_numeral(v, false);
+    else
+        result = m_util.mk_to_real(arg);
+}
+
+void arith_simplifier_plugin::mk_to_int(expr * arg, expr_ref & result) {
+    numeral v;
+    if (m_util.is_numeral(arg, v))
+        result = m_util.mk_numeral(floor(v), true);
+    else if (m_util.is_to_real(arg)) 
+        result = to_app(arg)->get_arg(0);
+    else 
+        result = m_util.mk_to_int(arg);
+}
+
+void arith_simplifier_plugin::mk_is_int(expr * arg, expr_ref & result) {
+    numeral v;
+    if (m_util.is_numeral(arg, v))
+        result = v.is_int()?m_manager.mk_true():m_manager.mk_false();
+    else if (m_util.is_to_real(arg)) 
+        result = m_manager.mk_true();
+    else 
+        result = m_util.mk_is_int(arg);
+}
+
+bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    set_reduce_invoked();
+    SASSERT(f->get_family_id() == m_fid);
+    TRACE("arith_simplifier_plugin", tout << mk_pp(f, m_manager) << "\n"; 
+          for (unsigned i = 0; i < num_args; i++) tout << mk_pp(args[i], m_manager) << "\n";);
+    arith_op_kind k = static_cast<arith_op_kind>(f->get_decl_kind());
+    switch (k) {
+    case OP_NUM:      return false;
+    case OP_LE:       if (m_presimp) return false; SASSERT(num_args == 2); mk_le(args[0], args[1], result); break;
+    case OP_GE:       if (m_presimp) return false; SASSERT(num_args == 2); mk_ge(args[0], args[1], result); break;
+    case OP_LT:       if (m_presimp) return false; SASSERT(num_args == 2); mk_lt(args[0], args[1], result); break;
+    case OP_GT:       if (m_presimp) return false; SASSERT(num_args == 2); mk_gt(args[0], args[1], result); break;
+    case OP_ADD:      mk_add(num_args, args, result); break;
+    case OP_SUB:      mk_sub(num_args, args, result); break;
+    case OP_UMINUS:   SASSERT(num_args == 1); mk_uminus(args[0], result); break;
+    case OP_MUL:      
+        mk_mul(num_args, args, result); 
+        TRACE("arith_simplifier_plugin", tout << mk_pp(result, m_manager) << "\n";); 
+        break;
+    case OP_DIV:      SASSERT(num_args == 2); mk_div(args[0], args[1], result); break;
+    case OP_IDIV:     SASSERT(num_args == 2); mk_idiv(args[0], args[1], result); break;
+    case OP_REM:      SASSERT(num_args == 2); mk_rem(args[0], args[1], result); break;
+    case OP_MOD:      SASSERT(num_args == 2); mk_mod(args[0], args[1], result); break;
+    case OP_TO_REAL:  SASSERT(num_args == 1); mk_to_real(args[0], result); break;
+    case OP_TO_INT:   SASSERT(num_args == 1); mk_to_int(args[0], result); break;
+    case OP_IS_INT:   SASSERT(num_args == 1); mk_is_int(args[0], result); break;
+    case OP_POWER:                    return false;
+    case OP_IRRATIONAL_ALGEBRAIC_NUM: return false;
+    default:
+        UNREACHABLE();
+        return false;
+    }
+    TRACE("arith_simplifier_plugin", tout << mk_pp(result.get(), m_manager) << "\n";);
+    return true;
+}
+
+bool arith_simplifier_plugin::is_arith_term(expr * n) const {
+    return n->get_kind() == AST_APP && to_app(n)->get_family_id() == m_fid;
+}
+
+bool arith_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
+    TRACE("reduce_eq_bug", tout << mk_ismt2_pp(lhs, m_manager) << "\n" << mk_ismt2_pp(rhs, m_manager) << "\n";);
+    set_reduce_invoked();
+    if (m_presimp) {
+        return false;
+    }
+    if (m_params.m_arith_expand_eqs) {
+        expr_ref le(m_manager), ge(m_manager);
+        mk_le_ge_eq_core<LE>(lhs, rhs, le);
+        mk_le_ge_eq_core<GE>(lhs, rhs, ge);
+        m_bsimp.mk_and(le, ge, result);
+        return true;
+    }
+
+    if (m_params.m_arith_process_all_eqs || is_arith_term(lhs) || is_arith_term(rhs)) {
+        mk_arith_eq(lhs, rhs, result); 
+        return true;
+    }
+    return false;
+}
+
+
+

src/simplifier/arith_simplifier_plugin.h

@@ -0,0 +1,95 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    arith_simplifier_plugin.h
+
+Abstract:
+
+    Simplifier for the arithmetic family.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-08
+    
+--*/
+#ifndef _ARITH_SIMPLIFIER_PLUGIN_H_
+#define _ARITH_SIMPLIFIER_PLUGIN_H_
+
+#include"basic_simplifier_plugin.h"
+#include"poly_simplifier_plugin.h"
+#include"arith_decl_plugin.h"
+#include"arith_simplifier_params.h"
+
+/**
+   \brief Simplifier for the arith family.
+*/
+class arith_simplifier_plugin : public poly_simplifier_plugin {
+public:
+    enum op_kind {
+        LE, GE, EQ
+    };
+protected:
+    arith_simplifier_params & m_params;
+    arith_util                m_util;
+    basic_simplifier_plugin & m_bsimp;
+    expr_ref                  m_int_zero;
+    expr_ref                  m_real_zero;
+
+    bool is_neg_poly(expr * t) const;
+
+    template<op_kind k>
+    void mk_le_ge_eq_core(expr * arg1, expr * arg2, expr_ref & result);
+
+    void prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result);
+
+    void gcd_reduce_monomial(expr_ref_vector& monomials, numeral& k);
+
+    void div_monomial(expr_ref_vector& monomials, numeral const& g);
+    void get_monomial_gcd(expr_ref_vector& monomials, numeral& g);
+
+public:
+    arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p);
+    ~arith_simplifier_plugin();
+    arith_util & get_arith_util() { return m_util; }
+    virtual numeral norm(const numeral & n) { return n; }
+    virtual bool is_numeral(expr * n, rational & val) const { bool f; return m_util.is_numeral(n, val, f); }
+    bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
+    virtual bool is_minus_one(expr * n) const { numeral tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
+    virtual expr * get_zero(sort * s) const { return m_util.is_int(s) ? m_int_zero.get() : m_real_zero.get(); }
+
+    virtual app * mk_numeral(numeral const & n) { return m_util.mk_numeral(n, m_curr_sort->get_decl_kind() == INT_SORT); }
+    app * mk_numeral(numeral const & n, bool is_int) { return m_util.mk_numeral(n, is_int); }
+    bool is_int_sort(sort const * s) const { return m_util.is_int(s); }
+    bool is_real_sort(sort const * s) const { return m_util.is_real(s); }
+    bool is_arith_sort(sort const * s) const { return is_int_sort(s) || is_real_sort(s); }
+    bool is_int(expr const * n) const { return m_util.is_int(n); }
+    bool is_le(expr const * n) const { return m_util.is_le(n); }
+    bool is_ge(expr const * n) const { return m_util.is_ge(n); }
+
+    virtual bool is_le_ge(expr * n) const { return is_le(n) || is_ge(n); }
+    
+    void mk_le(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_ge(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_lt(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_gt(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_arith_eq(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_div(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_idiv(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_mod(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_rem(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_to_real(expr * arg, expr_ref & result);
+    void mk_to_int(expr * arg, expr_ref & result);
+    void mk_is_int(expr * arg, expr_ref & result);
+
+    virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+    virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);
+
+    bool is_arith_term(expr * n) const;
+
+    void gcd_normalize(numeral & coeff, expr_ref& term);
+
+};
+
+#endif /* _ARITH_SIMPLIFIER_PLUGIN_H_ */

src/simplifier/base_simplifier.h

@@ -0,0 +1,54 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    base_simplifier.h
+
+Abstract:
+
+    Base class for expression simplifier functors.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-11
+
+Notes:
+
+--*/
+#ifndef _BASE_SIMPLIFIER_H_
+#define _BASE_SIMPLIFIER_H_
+
+#include"expr_map.h"
+
+/**
+   \brief Implements basic functionality used by expression simplifiers.
+*/
+class base_simplifier {
+protected:
+    ast_manager &                  m_manager;
+    expr_map                       m_cache;
+    ptr_vector<expr>               m_todo;
+
+    void cache_result(expr * n, expr * r, proof * p) { m_cache.insert(n, r, p); }
+    void reset_cache() { m_cache.reset(); }
+    void flush_cache() { m_cache.flush(); }
+    void get_cached(expr * n, expr * & r, proof * & p) const { m_cache.get(n, r, p); }
+
+    void visit(expr * n, bool & visited) {
+        if (!is_cached(n)) {
+            m_todo.push_back(n);
+            visited = false;
+        }
+    }
+
+public:
+    base_simplifier(ast_manager & m):
+        m_manager(m),
+        m_cache(m, m.fine_grain_proofs()) {
+    }
+    bool is_cached(expr * n) const {  return m_cache.contains(n); }
+    ast_manager & get_manager() { return m_manager; }
+};
+
+#endif /* _BASE_SIMPLIFIER_H_ */

src/simplifier/basic_simplifier_plugin.cpp

@@ -0,0 +1,142 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    basic_simplifier_plugin.cpp
+
+Abstract:
+
+    Simplifier for the basic family.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-07
+    
+--*/
+#include"basic_simplifier_plugin.h"
+#include"ast_ll_pp.h"
+#include"bool_rewriter.h"
+
+basic_simplifier_plugin::basic_simplifier_plugin(ast_manager & m):
+    simplifier_plugin(symbol("basic"), m), 
+    m_rewriter(alloc(bool_rewriter, m)) {
+}
+
+basic_simplifier_plugin::~basic_simplifier_plugin() {
+    dealloc(m_rewriter);
+}
+    
+bool basic_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    set_reduce_invoked();
+    SASSERT(f->get_family_id() == m_manager.get_basic_family_id());
+    basic_op_kind k = static_cast<basic_op_kind>(f->get_decl_kind());
+    switch (k) {
+    case OP_FALSE:     
+    case OP_TRUE:      
+        return false;
+    case OP_EQ:        
+        SASSERT(num_args == 2); 
+        mk_eq(args[0], args[1], result); 
+        return true;
+    case OP_DISTINCT:
+        mk_distinct(num_args, args, result);
+        return true;
+    case OP_ITE: 
+        SASSERT(num_args == 3);
+        mk_ite(args[0], args[1], args[2], result);
+        return true;
+    case OP_AND:       
+        mk_and(num_args, args, result); 
+        return true;
+    case OP_OR:        
+        mk_or(num_args, args, result); 
+        return true;
+    case OP_IMPLIES:
+        mk_implies(args[0], args[1], result); 
+        return true;
+    case OP_IFF:      
+        mk_iff(args[0], args[1], result); 
+        return true;
+    case OP_XOR: 
+        mk_xor(args[0], args[1], result); 
+        return true;
+    case OP_NOT:      
+        SASSERT(num_args == 1);
+        mk_not(args[0], result); 
+        return true;
+    default:
+        UNREACHABLE();
+        return false;
+    }
+}
+
+/**
+   \brief Return true if \c rhs is of the form (ite c t1 t2) and are_distinct(lhs, t1) and are_distinct(lhs, t2).
+*/
+static bool is_lhs_diseq_rhs_ite_branches(ast_manager & m, expr * lhs, expr * rhs) {
+    return m.is_ite(rhs) && m.are_distinct(lhs, to_app(rhs)->get_arg(1)) && m.are_distinct(lhs, to_app(rhs)->get_arg(2));
+}
+
+/**
+   \brief Return true if \c rhs is of the form (ite c t1 t2) and lhs = t1 && are_distinct(lhs, t2)
+*/
+static bool is_lhs_eq_rhs_ite_then(ast_manager & m, expr * lhs, expr * rhs) {
+    return m.is_ite(rhs) && lhs == to_app(rhs)->get_arg(1) && m.are_distinct(lhs, to_app(rhs)->get_arg(2));
+}
+
+/**
+   \brief Return true if \c rhs is of the form (ite c t1 t2) and are_distinct(lhs,t1) && lhs = t2
+*/
+static bool is_lhs_eq_rhs_ite_else(ast_manager & m, expr * lhs, expr * rhs) {
+    return m.is_ite(rhs) && lhs == to_app(rhs)->get_arg(2) && m.are_distinct(lhs, to_app(rhs)->get_arg(1));
+}
+
+void basic_simplifier_plugin::mk_eq(expr * lhs, expr * rhs, expr_ref & result) {
+    // (= t1 (ite C t2 t3)) --> false if are_distinct(t1, t2) && are_distinct(t1, t3)
+    if (is_lhs_diseq_rhs_ite_branches(m_manager, lhs, rhs) || is_lhs_diseq_rhs_ite_branches(m_manager, rhs, lhs)) {
+        result = m_manager.mk_false();
+    }
+    // (= t1 (ite C t2 t3)) --> C if t1 = t2 && are_distinct(t1, t3)
+    else if (is_lhs_eq_rhs_ite_then(m_manager, lhs, rhs)) {
+        result = to_app(rhs)->get_arg(0);
+    }
+    // (= t1 (ite C t2 t3)) --> C if t1 = t2 && are_distinct(t1, t3)
+    else if (is_lhs_eq_rhs_ite_then(m_manager, rhs, lhs)) {
+        result = to_app(lhs)->get_arg(0);
+    }
+    // (= t1 (ite C t2 t3)) --> (not C)  if t1 = t3 && are_distinct(t1, t2)
+    else if (is_lhs_eq_rhs_ite_else(m_manager, lhs, rhs)) {
+        mk_not(to_app(rhs)->get_arg(0), result);
+    }
+    // (= t1 (ite C t2 t3)) --> (not C)  if t1 = t3 && are_distinct(t1, t2)
+    else if (is_lhs_eq_rhs_ite_else(m_manager, rhs, lhs)) {
+        mk_not(to_app(lhs)->get_arg(0), result);
+    }
+    else {
+        m_rewriter->mk_eq(lhs, rhs, result);
+    }
+}
+
+bool basic_simplifier_plugin::eliminate_and() const { return m_rewriter->elim_and(); }
+void basic_simplifier_plugin::set_eliminate_and(bool f) { m_rewriter->set_elim_and(f); }
+void basic_simplifier_plugin::mk_iff(expr * lhs, expr * rhs, expr_ref & result) { mk_eq(lhs, rhs, result); }
+void basic_simplifier_plugin::mk_xor(expr * lhs, expr * rhs, expr_ref & result) { m_rewriter->mk_xor(lhs, rhs, result); }
+void basic_simplifier_plugin::mk_implies(expr * lhs, expr * rhs, expr_ref & result) { m_rewriter->mk_implies(lhs, rhs, result); }
+void basic_simplifier_plugin::mk_ite(expr * c, expr * t, expr * e, expr_ref & result) { m_rewriter->mk_ite(c, t, e, result); }
+void basic_simplifier_plugin::mk_and(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_and(num_args, args, result); }
+void basic_simplifier_plugin::mk_or(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_or(num_args, args, result); }
+void basic_simplifier_plugin::mk_and(expr * arg1, expr * arg2, expr_ref & result) { m_rewriter->mk_and(arg1, arg2, result); }
+void basic_simplifier_plugin::mk_or(expr * arg1, expr * arg2, expr_ref & result) { m_rewriter->mk_or(arg1, arg2, result); }
+void basic_simplifier_plugin::mk_and(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { m_rewriter->mk_and(arg1, arg2, arg3, result); }
+void basic_simplifier_plugin::mk_or(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { m_rewriter->mk_or(arg1, arg2, arg3, result); }
+void basic_simplifier_plugin::mk_nand(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_nand(num_args, args, result); } 
+void basic_simplifier_plugin::mk_nor(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_nor(num_args, args, result); } 
+void basic_simplifier_plugin::mk_nand(expr * arg1, expr * arg2, expr_ref & result) { m_rewriter->mk_nand(arg1, arg2, result); }
+void basic_simplifier_plugin::mk_nor(expr * arg1, expr * arg2, expr_ref & result) { m_rewriter->mk_nor(arg1, arg2, result); }
+void basic_simplifier_plugin::mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_distinct(num_args, args, result); }
+void basic_simplifier_plugin::mk_not(expr * n, expr_ref & result) { m_rewriter->mk_not(n, result); }
+
+void basic_simplifier_plugin::enable_ac_support(bool flag) {
+    m_rewriter->set_flat(flag);
+}

src/simplifier/basic_simplifier_plugin.h

@@ -0,0 +1,78 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    basic_simplifier_plugin.h
+
+Abstract:
+
+    Simplifier for the basic family.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-07
+    
+--*/
+#ifndef _BASIC_SIMPLIFIER_PLUGIN_H_
+#define _BASIC_SIMPLIFIER_PLUGIN_H_
+
+#include"simplifier_plugin.h"
+
+class bool_rewriter;
+
+/**
+   \brief Simplifier for the basic family.
+*/
+class basic_simplifier_plugin : public simplifier_plugin {
+    bool_rewriter * m_rewriter;
+public:
+    basic_simplifier_plugin(ast_manager & m);
+    virtual ~basic_simplifier_plugin();
+    bool_rewriter & get_rewriter() { return *m_rewriter; }
+    bool eliminate_and() const;
+    void set_eliminate_and(bool f);
+    void mk_eq(expr * lhs, expr * rhs, expr_ref & result);
+    void mk_iff(expr * lhs, expr * rhs, expr_ref & result);
+    void mk_xor(expr * lhs, expr * rhs, expr_ref & result);
+    void mk_implies(expr * lhs, expr * rhs, expr_ref & result);
+    void mk_ite(expr * c, expr * t, expr * e, expr_ref & result);
+    void mk_and(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_or(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_and(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_or(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_and(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
+    void mk_or(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
+    void mk_nand(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_nor(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_nand(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_nor(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_distinct(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_not(expr * n, expr_ref & result);
+    virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+    virtual void enable_ac_support(bool flag);
+};
+
+/**
+   \brief Functor that compares expressions, but puts the expressions e and f(e) close to each other, where
+   f is in family m_fid, and has kind m_dkind;
+*/
+struct expr_lt_proc {
+    family_id  m_fid;
+    decl_kind  m_dkind;
+
+    expr_lt_proc(family_id fid = null_family_id, decl_kind k = null_decl_kind):m_fid(fid), m_dkind(k) {}
+
+    unsigned get_id(expr * n) const {
+        if (m_fid != null_family_id && is_app_of(n, m_fid, m_dkind))
+            return (to_app(n)->get_arg(0)->get_id() << 1) + 1;
+        else
+            return n->get_id() << 1;
+    }
+
+    bool operator()(expr * n1, expr * n2) const {
+        return get_id(n1) < get_id(n2);
+    }
+};
+
+#endif /* _BASIC_SIMPLIFIER_PLUGIN_H_ */

src/simplifier/bv_simplifier_params.h

@@ -0,0 +1,39 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    bv_simplifier_params.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-10-10.
+
+Revision History:
+
+--*/
+#ifndef _BV_SIMPLIFIER_PARAMS_H_
+#define _BV_SIMPLIFIER_PARAMS_H_
+
+#include"ini_file.h"
+
+struct bv_simplifier_params {
+    bool  m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted.
+    bool  m_bv2int_distribute; //!< if true allows downward propagation of bv2int.
+
+    bv_simplifier_params():
+        m_hi_div0(true),
+        m_bv2int_distribute(true) {
+    }
+    void register_params(ini_params & p) {
+        p.register_bool_param("HI_DIV0", m_hi_div0, "if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero. Otherwise, these operations are considered uninterpreted.");
+        p.register_bool_param("BV2INT_DISTRIBUTE", m_bv2int_distribute, "if true, then int2bv is distributed over arithmetical operators.");
+    }
+};
+
+#endif /* _BV_SIMPLIFIER_PARAMS_H_ */
+

src/simplifier/bv_simplifier_plugin.h

@@ -0,0 +1,187 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    bv_simplifier_plugin.h
+
+Abstract:
+
+    Simplifier for the bv family.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-08
+    
+--*/
+#ifndef _BV_SIMPLIFIER_PLUGIN_H_
+#define _BV_SIMPLIFIER_PLUGIN_H_
+
+#include"basic_simplifier_plugin.h"
+#include"poly_simplifier_plugin.h"
+#include"bv_decl_plugin.h"
+#include"map.h"
+#include"bv_simplifier_params.h"
+#include"arith_decl_plugin.h"
+
+/**
+   \brief Simplifier for the bv family.
+*/
+class bv_simplifier_plugin : public poly_simplifier_plugin {
+
+    typedef rational numeral;
+    struct extract_entry {
+        unsigned m_high;
+        unsigned m_low;
+        expr *    m_arg;
+        extract_entry():m_high(0), m_low(0), m_arg(0) {}
+        extract_entry(unsigned h, unsigned l, expr * n):m_high(h), m_low(l), m_arg(n) {}
+        unsigned hash() const {
+            unsigned a = m_high;
+            unsigned b = m_low;
+            unsigned c = m_arg->get_id();
+            mix(a,b,c);
+            return c;
+        }
+        bool operator==(const extract_entry & e) const {
+            return m_high == e.m_high && m_low == e.m_low && m_arg == e.m_arg;
+        }
+        struct hash_proc {
+            unsigned operator()(extract_entry const& e) const { return e.hash(); }
+        };
+        struct eq_proc {
+            bool operator()(extract_entry const& a, extract_entry const& b) const { return a == b; }
+        };
+    };
+    typedef map<extract_entry, expr *, extract_entry::hash_proc , extract_entry::eq_proc > extract_cache;
+
+protected:
+    ast_manager&              m_manager;
+    bv_util                   m_util;
+    arith_util                m_arith;
+    basic_simplifier_plugin & m_bsimp;
+    bv_simplifier_params &    m_params;
+    expr_ref_vector           m_zeros;
+    extract_cache             m_extract_cache;
+
+    unsigned_vector           m_lows, m_highs;
+    ptr_vector<expr>          m_extract_args;
+
+    rational mk_bv_and(numeral const& a0, numeral const& b0, unsigned sz);
+    rational mk_bv_or(numeral const& a0, numeral const& b0, unsigned sz);
+    rational mk_bv_xor(numeral const& a0, numeral const& b0, unsigned sz);
+    rational mk_bv_not(numeral const& a0, unsigned sz);
+    rational num(expr* e);
+    bool has_sign_bit(numeral const& n, unsigned bv_size) { return m_util.has_sign_bit(n, bv_size); }
+
+    bool shift_shift(bv_op_kind k, expr* arg1, expr* arg2, expr_ref& result);
+
+    void bit2bool_simplify(unsigned idx, expr* e, expr_ref& result);
+
+    void mk_add_concat(expr_ref& result);
+    bool is_zero_bit(expr* x, unsigned idx);
+
+    void mk_bv_rotate_left_core(unsigned shift, numeral r, unsigned bv_size, expr_ref& result);
+    void mk_bv_rotate_right_core(unsigned shift, numeral r, unsigned bv_size, expr_ref& result);
+
+public:
+    bv_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, bv_simplifier_params & p);
+    virtual ~bv_simplifier_plugin();
+
+
+    // simplifier_plugin:
+    virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+    virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);
+    virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result);
+    virtual void flush_caches();
+
+    // poly_simplifier_plugin
+    virtual rational norm(const rational & n);
+    virtual bool is_numeral(expr * n, rational & val) const;
+    bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
+    virtual bool is_minus_one(expr * n) const { return is_minus_one_core(n); }
+    virtual expr * get_zero(sort * s) const;
+    virtual app * mk_numeral(rational const & n);
+
+    bool is_bv(expr * n) const { return m_util.is_bv(n); }
+    bool is_bv_sort(sort * s) const { return m_util.is_bv_sort(s); }
+
+    bool is_le(expr * n) const { return m_util.is_bv_ule(n) || m_util.is_bv_sle(n); }
+    // REMARK: simplified bv expressions are never of the form a >= b.
+    virtual bool is_le_ge(expr * n) const { return is_le(n); }
+
+    uint64 to_uint64(const numeral & n, unsigned bv_size);
+    rational norm(rational const& n, unsigned bv_size, bool is_signed) { return m_util.norm(n, bv_size, is_signed); }
+    unsigned get_bv_size(expr const * n) { return get_bv_size(m_manager.get_sort(n)); }
+    unsigned get_bv_size(sort const * s) { return m_util.get_bv_size(s); }
+    void mk_leq_core(bool is_signed, expr * arg1, expr * arg2, expr_ref & result);
+    void mk_ule(expr* a, expr* b, expr_ref& result);
+    void mk_ult(expr* a, expr* b, expr_ref& result);
+    void mk_sle(expr* a, expr* b, expr_ref& result);
+    void mk_slt(expr* a, expr* b, expr_ref& result);
+    void mk_bv_and(unsigned num_args, expr * const* args, expr_ref & result);
+    void mk_bv_or(unsigned num_args, expr * const* args, expr_ref & result);
+    void mk_bv_xor(unsigned num_args, expr * const* args, expr_ref & result);
+    void mk_bv_not(expr * arg, expr_ref & result);
+    void mk_extract(unsigned hi,unsigned lo, expr* bv, expr_ref& result);
+    void mk_extract_core(unsigned high, unsigned low, expr * arg, expr_ref& result);
+    void cache_extract(unsigned h, unsigned l, expr * arg, expr * result);
+    expr* get_cached_extract(unsigned h, unsigned l, expr * arg);
+
+    bool lookup_mk_extract(unsigned high, unsigned low, expr * arg, expr_ref& result);
+    bool try_mk_extract(unsigned high, unsigned low, expr * arg, expr_ref& result);
+
+    void mk_bv_eq(expr* a1, expr* a2, expr_ref& result);
+    void mk_eq_core(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_args_eq_numeral(app * app, expr * n, expr_ref & result);
+
+    void mk_concat(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_concat(expr * arg1, expr * arg2, expr_ref & result) { 
+        expr * args[2] = { arg1, arg2 }; 
+        mk_concat(2, args, result); 
+    }
+    void mk_zeroext(unsigned n, expr * arg, expr_ref & result);
+    void mk_repeat(unsigned n, expr * arg, expr_ref & result);
+    void mk_sign_extend(unsigned n, expr * arg, expr_ref & result);
+    void mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_bv_ashr(expr* arg1, expr* arg2, expr_ref& result);
+    void mk_bv_smod(expr* arg1, expr* arg2, expr_ref& result);
+    void mk_bv_urem(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_bv_srem(expr* arg1, expr* arg2, expr_ref& result);
+    void mk_bv_udiv(expr* arg1, expr* arg2, expr_ref& result);
+    void mk_bv_sdiv(expr* arg1, expr* arg2, expr_ref& result);
+    void mk_bv_smod_i(expr* arg1, expr* arg2, expr_ref& result);
+    void mk_bv_urem_i(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_bv_srem_i(expr* arg1, expr* arg2, expr_ref& result);
+    void mk_bv_udiv_i(expr* arg1, expr* arg2, expr_ref& result);
+    void mk_bv_sdiv_i(expr* arg1, expr* arg2, expr_ref& result);
+    void mk_bv_nand(unsigned num_args, expr* const* args, expr_ref& result);
+    void mk_bv_nor(unsigned num_args, expr* const* args, expr_ref& result);
+    void mk_bv_xnor(unsigned num_args, expr* const* args, expr_ref& result);
+    void mk_bv_rotate_right(func_decl* f, expr* arg, expr_ref& result);
+    void mk_bv_rotate_left(func_decl* f, expr* arg, expr_ref& result);
+    void mk_bv_ext_rotate_right(expr* arg1, expr* arg2, expr_ref& result);
+    void mk_bv_ext_rotate_left(expr* arg1, expr* arg2, expr_ref& result);
+
+    void mk_bv_redor(expr* arg, expr_ref& result);
+    void mk_bv_redand(expr* arg, expr_ref& result);
+    void mk_bv_comp(expr* arg1, expr* arg2, expr_ref& result);
+
+    bool are_numerals(unsigned num_args, expr * const* args, unsigned& bv_size);
+    app * mk_numeral(rational const & n, unsigned bv_size);
+    app * mk_numeral(uint64 n, unsigned bv_size) { return mk_numeral(numeral(n, numeral::ui64()), bv_size); }
+    app* mk_bv0(unsigned bv_size) { return m_util.mk_numeral(numeral(0), bv_size); }
+    rational mk_allone(unsigned bv_size) { return m_util.power_of_two(bv_size) - numeral(1); }
+    bool is_minus_one_core(expr * arg) const;
+    bool is_x_minus_one(expr * arg, expr * & x);
+    void mk_int2bv(expr * arg, sort* range, expr_ref & result);
+    void mk_bv2int(expr * arg, sort* range, expr_ref & result);
+    uint64 n64(expr* e);
+    bool is_mul_no_overflow(expr* e);
+    bool is_add_no_overflow(expr* e);
+    unsigned num_leading_zero_bits(expr* e);
+
+};
+
+#endif /* _BV_SIMPLIFIER_PLUGIN_H_ */

src/simplifier/datatype_simplifier_plugin.cpp

@@ -0,0 +1,113 @@
+/*++
+Copyright (c) 2008 Microsoft Corporation
+
+Module Name:
+
+    datatype_simplifier_plugin.cpp
+
+Abstract:
+
+    Simplifier for algebraic datatypes.
+
+Author:
+
+    nbjorner 2008-11-6
+    
+--*/
+
+#include"datatype_simplifier_plugin.h"
+
+datatype_simplifier_plugin::datatype_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b):
+    simplifier_plugin(symbol("datatype"), m),
+    m_util(m),
+    m_bsimp(b) {
+}
+
+datatype_simplifier_plugin::~datatype_simplifier_plugin() {
+}
+
+bool datatype_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    set_reduce_invoked();
+
+    SASSERT(f->get_family_id() == get_family_id());
+    switch(f->get_decl_kind()) {
+    case OP_DT_CONSTRUCTOR: {
+        return false;
+    }
+    case OP_DT_RECOGNISER: {
+        //
+        // simplify is_cons(cons(x,y)) -> true
+        // simplify is_cons(nil) -> false
+        //
+        SASSERT(num_args == 1);
+        
+        if (!is_app_of(args[0], get_family_id(), OP_DT_CONSTRUCTOR)) {
+            return false;
+        }
+        app* a = to_app(args[0]);
+        func_decl* f1 = a->get_decl();
+        func_decl* f2 = m_util.get_recognizer_constructor(f);
+        if (f1 == f2) {
+            result = m_manager.mk_true();
+        }
+        else {
+            result = m_manager.mk_false();
+        }
+        return true;
+    }
+    case OP_DT_ACCESSOR: {
+        // 
+        // simplify head(cons(x,y)) -> x
+        // 
+        SASSERT(num_args == 1);
+        
+        if (!is_app_of(args[0], get_family_id(), OP_DT_CONSTRUCTOR)) {
+            return false;
+        }
+        app* a = to_app(args[0]);
+        func_decl* f1 = a->get_decl();
+        func_decl* f2 = m_util.get_accessor_constructor(f);
+        if (f1 != f2) {
+            return false;
+        }
+        ptr_vector<func_decl> const* acc = m_util.get_constructor_accessors(f1);
+        SASSERT(acc && acc->size() == a->get_num_args());
+        for (unsigned i = 0; i < acc->size(); ++i) {
+            if (f == (*acc)[i]) {
+                // found it.
+                result = a->get_arg(i);
+                return true;
+            }
+        }
+        UNREACHABLE();
+    }
+    default:
+        UNREACHABLE();
+    }
+    
+    return false;
+}
+
+bool datatype_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
+    set_reduce_invoked();
+    if (is_app_of(lhs, get_family_id(), OP_DT_CONSTRUCTOR) &&
+        is_app_of(rhs, get_family_id(), OP_DT_CONSTRUCTOR)) {
+        app* a = to_app(lhs);
+        app* b = to_app(rhs);
+        if (a->get_decl() != b->get_decl()) {
+            result = m_manager.mk_false();
+            return true;
+        }
+        expr_ref_vector eqs(m_manager);
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {            
+            m_bsimp.mk_eq(a->get_arg(i),b->get_arg(i), result);
+            eqs.push_back(result);                
+        }
+        m_bsimp.mk_and(eqs.size(), eqs.c_ptr(), result);
+        return true;
+    }
+    // TBD: occurs check, constructor check.
+
+    return false;
+}
+

src/simplifier/datatype_simplifier_plugin.h

@@ -0,0 +1,42 @@
+/*++
+Copyright (c) 2008 Microsoft Corporation
+
+Module Name:
+
+    datatype_simplifier_plugin.h
+
+Abstract:
+
+    Simplifier for algebraic datatypes.
+
+Author:
+
+    nbjorner 2008-11-6
+    
+--*/
+#ifndef _DATATYPE_SIMPLIFIER_PLUGIN_H_
+#define _DATATYPE_SIMPLIFIER_PLUGIN_H_
+
+#include"basic_simplifier_plugin.h"
+#include"datatype_decl_plugin.h"
+
+/**
+   \brief Simplifier for the arith family.
+*/
+class datatype_simplifier_plugin : public simplifier_plugin {
+    datatype_util             m_util;
+    basic_simplifier_plugin & m_bsimp;
+
+
+public:
+    datatype_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b);
+    ~datatype_simplifier_plugin();
+    
+
+    virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+
+    virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);
+
+};
+
+#endif /* _DATATYPE_SIMPLIFIER_PLUGIN_H_ */

src/simplifier/poly_simplifier_plugin.cpp

@@ -0,0 +1,812 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    poly_simplifier_plugin.cpp
+
+Abstract:
+
+    Abstract class for families that have polynomials.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-08
+    
+--*/
+#include"poly_simplifier_plugin.h"
+#include"ast_pp.h"
+#include"ast_util.h"
+#include"ast_smt2_pp.h"
+
+poly_simplifier_plugin::poly_simplifier_plugin(symbol const & fname, ast_manager & m, decl_kind add, decl_kind mul, decl_kind uminus, decl_kind sub,
+                                               decl_kind num):
+    simplifier_plugin(fname, m), 
+    m_ADD(add), 
+    m_MUL(mul),
+    m_SUB(sub),
+    m_UMINUS(uminus),
+    m_NUM(num),
+    m_curr_sort(0),
+    m_curr_sort_zero(0) {
+}
+
+expr * poly_simplifier_plugin::mk_add(unsigned num_args, expr * const * args) { 
+    SASSERT(num_args > 0);
+#ifdef Z3DEBUG
+    // check for incorrect use of mk_add
+    for (unsigned i = 0; i < num_args; i++) {
+        SASSERT(!is_zero(args[i]));
+    }
+#endif    
+    if (num_args == 1)
+        return args[0];
+    else
+        return m_manager.mk_app(m_fid, m_ADD, num_args, args); 
+}
+
+expr * poly_simplifier_plugin::mk_mul(unsigned num_args, expr * const * args) { 
+    SASSERT(num_args > 0);
+#ifdef Z3DEBUG
+    // check for incorrect use of mk_mul
+    set_curr_sort(args[0]);
+    SASSERT(!is_zero(args[0]));
+    numeral k;
+    for (unsigned i = 0; i < num_args; i++) {
+        SASSERT(!is_numeral(args[i], k) || !k.is_one());
+        SASSERT(i == 0 || !is_numeral(args[i]));
+    }
+#endif
+    if (num_args == 1) 
+        return args[0];
+    else if (num_args == 2)
+        return m_manager.mk_app(m_fid, m_MUL, args[0], args[1]);
+    else if (is_numeral(args[0]))
+        return m_manager.mk_app(m_fid, m_MUL, args[0], m_manager.mk_app(m_fid, m_MUL, num_args - 1, args+1));
+    else
+        return m_manager.mk_app(m_fid, m_MUL, num_args, args); 
+}
+
+expr * poly_simplifier_plugin::mk_mul(numeral const & c, expr * body) {
+    numeral c_prime;
+    c_prime = norm(c);
+    if (c_prime.is_zero())
+        return 0;
+    if (body == 0)
+        return mk_numeral(c_prime);
+    if (c_prime.is_one())
+        return body;
+    set_curr_sort(body);
+    expr * args[2] = { mk_numeral(c_prime), body };
+    return mk_mul(2, args);
+}
+
+/**
+   \brief Traverse args, and copy the non-numeral exprs to result, and accumulate the 
+   value of the numerals in k.
+*/
+void poly_simplifier_plugin::process_monomial(unsigned num_args, expr * const * args, numeral & k, ptr_buffer<expr> & result) {
+    rational v;
+    for (unsigned i = 0; i < num_args; i++) {
+        expr * arg = args[i];
+        if (is_numeral(arg, v))
+            k *= v;
+        else
+            result.push_back(arg);
+    }
+}
+
+#ifdef Z3DEBUG
+/**
+   \brief Return true if m is a wellformed monomial.
+*/
+bool poly_simplifier_plugin::wf_monomial(expr * m) const {
+    SASSERT(!is_add(m));
+    if (is_mul(m)) {
+        app * curr = to_app(m);
+        expr * pp  = 0;
+        if (is_numeral(curr->get_arg(0)))
+            pp = curr->get_arg(1);
+        else
+            pp = curr;
+        if (is_mul(pp)) {
+            for (unsigned i = 0; i < to_app(pp)->get_num_args(); i++) {
+                expr * arg = to_app(pp)->get_arg(i);
+                CTRACE("wf_monomial_bug", is_mul(arg), 
+                       tout << "m:  "  << mk_ismt2_pp(m, m_manager) << "\n";
+                       tout << "pp: "  << mk_ismt2_pp(pp, m_manager) << "\n";
+                       tout << "arg: " << mk_ismt2_pp(arg, m_manager) << "\n";
+                       tout << "i:  " << i << "\n";
+                       );
+                SASSERT(!is_mul(arg));
+                SASSERT(!is_numeral(arg));
+            }
+        }
+    }
+    return true;
+}
+
+/**
+   \brief Return true if m is a wellformed polynomial.
+*/
+bool poly_simplifier_plugin::wf_polynomial(expr * m) const {
+    if (is_add(m)) {
+        for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
+            expr * arg = to_app(m)->get_arg(i);
+            SASSERT(!is_add(arg));
+            SASSERT(wf_monomial(arg));
+        }
+    }
+    else if (is_mul(m)) {
+        SASSERT(wf_monomial(m));
+    }
+    return true;
+}
+#endif
+
+/**
+   \brief Functor used to sort the elements of a monomial.
+   Force numeric constants to be in the beginning.
+*/
+struct monomial_element_lt_proc {
+    poly_simplifier_plugin &  m_plugin;
+    monomial_element_lt_proc(poly_simplifier_plugin & p):m_plugin(p) {}
+    bool operator()(expr * m1, expr * m2) const {
+        SASSERT(!m_plugin.is_numeral(m1) || !m_plugin.is_numeral(m2));
+        if (m_plugin.is_numeral(m1))
+            return true;
+        if (m_plugin.is_numeral(m2))
+            return false;
+        return m1->get_id() < m2->get_id();
+    }
+};
+
+/**
+   \brief Create a monomial (* args). 
+*/
+void poly_simplifier_plugin::mk_monomial(unsigned num_args, expr * * args, expr_ref & result) {
+    switch(num_args) {
+    case 0:
+        result = mk_one();
+        break;
+    case 1:
+        result = args[0];
+        break;
+    default:
+        std::sort(args, args + num_args, monomial_element_lt_proc(*this));
+        result = mk_mul(num_args, args);
+        SASSERT(wf_monomial(result));
+        break;
+    }
+}
+
+/**
+   \brief Return the body of the monomial. That is, the monomial without a coefficient.
+   Examples: (* 2 (* x y)) ==> (* x y)
+             (* x x) ==> (* x x)
+             x       ==> x
+             10      ==> 10
+*/
+expr * poly_simplifier_plugin::get_monomial_body(expr * m) {
+    TRACE("get_monomial_body_bug", tout << mk_pp(m, m_manager) << "\n";);
+    SASSERT(wf_monomial(m));
+    if (!is_mul(m))
+       return m;
+    if (is_numeral(to_app(m)->get_arg(0)))
+        return to_app(m)->get_arg(1);
+    return m;
+}
+
+inline bool is_essentially_var(expr * n, family_id fid) {
+    SASSERT(is_var(n) || is_app(n));
+    return is_var(n) || to_app(n)->get_family_id() != fid;
+}
+
+/**
+   \brief Hack for ordering monomials.
+   We want an order << where
+      - (* c1 m1) << (* c2 m2)    when  m1->get_id() < m2->get_id(), and c1 and c2 are numerals.
+      - c << m                    when  c is a numeral, and m is not.
+
+   So, this method returns -1 for numerals, and the id of the body of the monomial   
+*/
+int poly_simplifier_plugin::get_monomial_body_order(expr * m) {
+    if (is_essentially_var(m, m_fid)) {
+        return m->get_id();
+    }
+    else if (is_mul(m)) {
+        if (is_numeral(to_app(m)->get_arg(0)))
+            return to_app(m)->get_arg(1)->get_id();
+        else
+            return m->get_id();
+    }
+    else if (is_numeral(m)) {
+        return -1;
+    }
+    else {
+        return m->get_id();
+    }
+}
+
+void poly_simplifier_plugin::get_monomial_coeff(expr * m, numeral & result) {
+    SASSERT(!is_numeral(m));
+    SASSERT(wf_monomial(m));
+    if (!is_mul(m))
+        result = numeral::one();
+    else if (is_numeral(to_app(m)->get_arg(0), result))
+        return;
+    else
+        result = numeral::one();
+}
+
+/**
+   \brief Return true if n1 and n2 can be written as k1 * t and k2 * t, where k1 and
+   k2 are numerals, or n1 and n2 are both numerals.
+*/
+bool poly_simplifier_plugin::eq_monomials_modulo_k(expr * n1, expr * n2) {
+    bool is_num1 = is_numeral(n1);
+    bool is_num2 = is_numeral(n2);
+    if (is_num1 != is_num2)
+        return false;
+    if (is_num1 && is_num2)
+        return true;
+    return get_monomial_body(n1) == get_monomial_body(n2);
+}
+
+/**
+   \brief Return (k1 + k2) * t (or (k1 - k2) * t when inv = true), where n1 = k1 * t, and n2 = k2 * t
+   Return false if the monomials cancel each other.
+*/
+bool poly_simplifier_plugin::merge_monomials(bool inv, expr * n1, expr * n2, expr_ref & result) {
+    numeral k1;
+    numeral k2;
+    bool is_num1 = is_numeral(n1, k1);
+    bool is_num2 = is_numeral(n2, k2);
+    SASSERT(is_num1 == is_num2);
+    if (!is_num1 && !is_num2) {
+        get_monomial_coeff(n1, k1);
+        get_monomial_coeff(n2, k2);        
+        SASSERT(eq_monomials_modulo_k(n1, n2));
+    }
+    if (inv)
+        k1 -= k2;
+    else 
+        k1 += k2;
+    if (k1.is_zero())
+        return false;
+    if (is_num1 && is_num2) {
+        result = mk_numeral(k1);
+    }
+    else {
+        expr * b = get_monomial_body(n1);
+        if (k1.is_one())
+            result = b;
+        else
+            result = m_manager.mk_app(m_fid, m_MUL, mk_numeral(k1), b);
+    }
+    return true;
+}
+
+/**
+   \brief Return a monomial equivalent to -n.
+*/
+void poly_simplifier_plugin::inv_monomial(expr * n, expr_ref & result) {
+    set_curr_sort(n);
+    SASSERT(wf_monomial(n));
+    rational v;
+    SASSERT(n != 0);
+    TRACE("inv_monomial_bug", tout << "n:\n" << mk_ismt2_pp(n, m_manager) << "\n";);
+    if (is_numeral(n, v)) {
+        TRACE("inv_monomial_bug", tout << "is numeral\n";);
+        v.neg();
+        result = mk_numeral(v);
+    }
+    else {
+        TRACE("inv_monomial_bug", tout << "is not numeral\n";);
+        numeral k;
+        get_monomial_coeff(n, k);
+        expr * b = get_monomial_body(n);
+        k.neg();
+        if (k.is_one())
+            result = b;
+        else
+            result = m_manager.mk_app(m_fid, m_MUL, mk_numeral(k), b);
+    }
+}
+
+/** 
+    \brief Add a monomial n to result. 
+*/
+template<bool Inv>
+void poly_simplifier_plugin::add_monomial_core(expr * n, expr_ref_vector & result) {
+    if (is_zero(n)) 
+        return;
+    if (Inv) {
+        expr_ref n_prime(m_manager);
+        inv_monomial(n, n_prime);
+        result.push_back(n_prime);
+    }
+    else { 
+        result.push_back(n);
+    }
+}
+
+void poly_simplifier_plugin::add_monomial(bool inv, expr * n, expr_ref_vector & result) {
+    if (inv)
+        add_monomial_core<true>(n, result);
+    else
+        add_monomial_core<false>(n, result);
+}
+
+/**
+   \brief Copy the monomials in n to result. The monomials are inverted if inv is true.
+   Equivalent monomials are merged. 
+*/
+template<bool Inv>
+void poly_simplifier_plugin::process_sum_of_monomials_core(expr * n, expr_ref_vector & result) {
+    SASSERT(wf_polynomial(n));
+    if (is_add(n)) {
+        for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) 
+            add_monomial_core<Inv>(to_app(n)->get_arg(i), result);
+    }
+    else {
+        add_monomial_core<Inv>(n, result);
+    }
+}
+
+void poly_simplifier_plugin::process_sum_of_monomials(bool inv, expr * n, expr_ref_vector & result) {
+    if (inv)
+        process_sum_of_monomials_core<true>(n, result);
+    else
+        process_sum_of_monomials_core<false>(n, result);
+}
+
+/**
+   \brief Copy the (non-numeral) monomials in n to result. The monomials are inverted if inv is true.
+   Equivalent monomials are merged. The constant (numeral) monomials are accumulated in k.
+*/
+void poly_simplifier_plugin::process_sum_of_monomials(bool inv, expr * n, expr_ref_vector & result, numeral & k) {
+    SASSERT(wf_polynomial(n));
+    numeral val;
+    if (is_add(n)) {
+        for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) {
+            expr * arg = to_app(n)->get_arg(i);
+            if (is_numeral(arg, val)) {
+                k += inv ? -val : val;
+            }
+            else {
+                add_monomial(inv, arg, result);
+            }
+        }
+    }
+    else if (is_numeral(n, val)) {
+        k += inv ? -val : val;
+    }
+    else {
+        add_monomial(inv, n, result);
+    }
+}
+
+/**
+   \brief Functor used to sort monomials.
+   Force numeric constants to be in the beginning of a polynomial.
+*/
+struct monomial_lt_proc {
+    poly_simplifier_plugin & m_plugin;
+    monomial_lt_proc(poly_simplifier_plugin & p):m_plugin(p) {}
+    bool operator()(expr * m1, expr * m2) const {
+        return m_plugin.get_monomial_body_order(m1) < m_plugin.get_monomial_body_order(m2);
+    }
+};
+
+void poly_simplifier_plugin::mk_sum_of_monomials_core(unsigned sz, expr ** ms, expr_ref & result) {
+    switch (sz) {
+    case 0:
+        result = mk_zero();
+        break;
+    case 1:
+        result = ms[0];
+        break;
+    default:
+        result = mk_add(sz, ms);
+        break;
+    }
+}
+
+/**
+   \brief Return true if m is essentially a variable, or is of the form (* c x),
+   where c is a numeral and x is essentially a variable.
+   Store the "variable" in x.
+*/
+bool poly_simplifier_plugin::is_simple_monomial(expr * m, expr * & x) {
+    if (is_essentially_var(m, m_fid)) {
+        x = m;
+        return true;
+    }
+    if (is_app(m) && to_app(m)->get_num_args() == 2) {
+        expr * arg1 = to_app(m)->get_arg(0);
+        expr * arg2 = to_app(m)->get_arg(1);
+        if (is_numeral(arg1) && is_essentially_var(arg2, m_fid)) {
+            x = arg2;
+            return true;
+        }
+    }
+    return false;
+}
+
+/**
+   \brief Return true if all monomials are simple, and each "variable" occurs only once.
+   The method assumes the monomials were sorted using monomial_lt_proc.
+*/
+bool poly_simplifier_plugin::is_simple_sum_of_monomials(expr_ref_vector & monomials) {
+    expr * last_var = 0;
+    expr * curr_var = 0;
+    unsigned size = monomials.size();
+    for (unsigned i = 0; i < size; i++) {
+        expr * m = monomials.get(i);
+        if (!is_simple_monomial(m, curr_var))
+            return false;
+        if (curr_var == last_var)
+            return false;
+        last_var = curr_var;
+    }
+    return true;
+}
+
+/**
+   \brief Store in result the sum of the given monomials.
+*/
+void poly_simplifier_plugin::mk_sum_of_monomials(expr_ref_vector & monomials, expr_ref & result) {
+    switch (monomials.size()) {
+    case 0:
+        result = mk_zero();
+        break;
+    case 1:
+        result = monomials.get(0);
+        break;
+    default: {
+        std::sort(monomials.c_ptr(), monomials.c_ptr() + monomials.size(), monomial_lt_proc(*this));
+        if (is_simple_sum_of_monomials(monomials)) {
+            mk_sum_of_monomials_core(monomials.size(), monomials.c_ptr(), result);
+            return;
+        }
+        ptr_buffer<expr> new_monomials;
+        expr * last_body = 0;
+        numeral last_coeff;
+        numeral coeff; 
+        unsigned sz = monomials.size();
+        for (unsigned i = 0; i < sz; i++) {
+            expr * m    = monomials.get(i);
+            expr * body = 0;
+            if (!is_numeral(m, coeff)) {
+                body = get_monomial_body(m);
+                get_monomial_coeff(m, coeff);
+            }
+            if (last_body == body) {
+                last_coeff += coeff;
+                continue;
+            }
+            expr * new_m = mk_mul(last_coeff, last_body);
+            if (new_m)
+                new_monomials.push_back(new_m);
+            last_body  = body;
+            last_coeff = coeff;
+        }
+        expr * new_m = mk_mul(last_coeff, last_body);
+        if (new_m)
+            new_monomials.push_back(new_m);
+        TRACE("mk_sum", for (unsigned i = 0; i < monomials.size(); i++) tout << mk_pp(monomials.get(i), m_manager) << "\n";
+              tout << "======>\n";
+              for (unsigned i = 0; i < new_monomials.size(); i++) tout << mk_pp(new_monomials.get(i), m_manager) << "\n";);
+        mk_sum_of_monomials_core(new_monomials.size(), new_monomials.c_ptr(), result);
+        break;
+    } }
+}
+
+/**
+   \brief Auxiliary template for mk_add_core
+*/
+template<bool Inv>
+void poly_simplifier_plugin::mk_add_core_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(num_args >= 2);
+    expr_ref_vector monomials(m_manager);
+    process_sum_of_monomials_core<false>(args[0], monomials);
+    for (unsigned i = 1; i < num_args; i++) {
+        process_sum_of_monomials_core<Inv>(args[i], monomials);
+    }
+    TRACE("mk_add_core_bug", 
+          for (unsigned i = 0; i < monomials.size(); i++) { 
+              SASSERT(monomials.get(i) != 0); 
+              tout << mk_ismt2_pp(monomials.get(i), m_manager) << "\n"; 
+          });
+    mk_sum_of_monomials(monomials, result);
+}
+
+/**
+   \brief Return a sum of monomials. The method assume that each arg in args is a sum of monomials.
+   If inv is true, then all but the first argument in args are inverted.
+*/
+void poly_simplifier_plugin::mk_add_core(bool inv, unsigned num_args, expr * const * args, expr_ref & result) {
+    TRACE("mk_add_core_bug", 
+          for (unsigned i = 0; i < num_args; i++) { 
+              SASSERT(args[i] != 0);
+              tout << mk_ismt2_pp(args[i], m_manager) << "\n";
+          });
+    switch (num_args) {
+    case 0:
+        result = mk_zero();
+        break;
+    case 1:
+        result = args[0];
+        break;
+    default:
+        if (inv)
+            mk_add_core_core<true>(num_args, args, result);
+        else
+            mk_add_core_core<false>(num_args, args, result);
+        break;
+    }
+}
+
+void poly_simplifier_plugin::mk_add(unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(num_args > 0);
+    set_curr_sort(args[0]);
+    mk_add_core(false, num_args, args, result);
+}
+
+void poly_simplifier_plugin::mk_add(expr * arg1, expr * arg2, expr_ref & result) {
+    expr * args[2] = { arg1, arg2 };
+    mk_add(2, args, result);
+}
+
+void poly_simplifier_plugin::mk_sub(unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(num_args > 0);
+    set_curr_sort(args[0]);
+    mk_add_core(true, num_args, args, result);
+}
+
+void poly_simplifier_plugin::mk_sub(expr * arg1, expr * arg2, expr_ref & result) {
+    expr * args[2] = { arg1, arg2 };
+    mk_sub(2, args, result);
+}
+
+void poly_simplifier_plugin::mk_uminus(expr * arg, expr_ref & result) {
+    set_curr_sort(arg);
+    rational v;
+    if (is_numeral(arg, v)) {
+        v.neg();
+        result = mk_numeral(v);
+    }
+    else {
+        expr_ref zero(mk_zero(), m_manager);
+        mk_sub(zero.get(), arg, result);
+    }
+}
+
+/**
+   \brief Add monomial n to result, the coeff of n is stored in k.
+*/
+void poly_simplifier_plugin::append_to_monomial(expr * n, numeral & k, ptr_buffer<expr> & result) {
+    SASSERT(wf_monomial(n));
+    rational val;
+    if (is_numeral(n, val)) {
+        k *= val;
+        return;
+    }
+    get_monomial_coeff(n, val);
+    k *= val;
+    n  = get_monomial_body(n);
+
+    if (is_mul(n)) {
+        for (unsigned i = 0; i < to_app(n)->get_num_args(); i++)
+            result.push_back(to_app(n)->get_arg(i));
+    }
+    else {
+        result.push_back(n);
+    }
+}
+
+/**
+   \brief Return a sum of monomials that is equivalent to (* args[0] ... args[num_args-1]).
+   This method assumes that each arg[i] is a sum of monomials.
+*/
+void poly_simplifier_plugin::mk_mul(unsigned num_args, expr * const * args, expr_ref & result) {
+    if (num_args == 1) {
+        result = args[0];
+        return;
+    }
+    rational val;
+    if (num_args == 2 && is_numeral(args[0], val) && is_essentially_var(args[1], m_fid)) {
+        if (val.is_one())
+            result = args[1];
+        else if (val.is_zero())
+            result = args[0];
+        else
+            result = mk_mul(num_args, args);
+        return;
+    }
+    if (num_args == 2 && is_essentially_var(args[0], m_fid) && is_numeral(args[1], val)) {
+        if (val.is_one())
+            result = args[0];
+        else if (val.is_zero())
+            result = args[1];
+        else {
+            expr * inv_args[2] = { args[1], args[0] };
+            result = mk_mul(2, inv_args);
+        }
+        return;
+    }
+
+    TRACE("mk_mul_bug", 
+          for (unsigned i = 0; i < num_args; i++) {
+              tout << mk_pp(args[i], m_manager) << "\n";
+          });
+    set_curr_sort(args[0]);
+    buffer<unsigned> szs;
+    buffer<unsigned> it;
+    vector<ptr_vector<expr> > sums;
+    for (unsigned i = 0; i < num_args; i ++) {
+        it.push_back(0);
+        expr * arg  = args[i];
+        SASSERT(wf_polynomial(arg));
+        sums.push_back(ptr_vector<expr>());
+        ptr_vector<expr> & v = sums.back();
+        if (is_add(arg)) {
+            v.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
+        }
+        else {
+            v.push_back(arg);
+        }
+        szs.push_back(v.size());
+    }
+    expr_ref_vector monomials(m_manager);
+    do {
+        rational k(1);
+        ptr_buffer<expr> m;
+        for (unsigned i = 0; i < num_args; i++) {
+            ptr_vector<expr> & v = sums[i];
+            expr * arg           = v[it[i]];
+            TRACE("mk_mul_bug", tout << "k: " << k << " arg: " << mk_pp(arg, m_manager) << "\n";);
+            append_to_monomial(arg, k, m);
+            TRACE("mk_mul_bug", tout << "after k: " << k << "\n";);
+        }
+        expr_ref num(m_manager);
+        if (!k.is_zero() && !k.is_one()) {
+            num = mk_numeral(k);
+            m.push_back(num);
+            // bit-vectors can normalize 
+            // to 1 during
+            // internalization.
+            if (is_numeral(num, k) && k.is_one()) {
+                m.pop_back();
+            }                
+        }
+        if (!k.is_zero()) {
+            expr_ref new_monomial(m_manager);
+            TRACE("mk_mul_bug", 
+                  for (unsigned i = 0; i < m.size(); i++) {
+                      tout << mk_pp(m[i], m_manager) << "\n";
+                  });
+            mk_monomial(m.size(), m.c_ptr(), new_monomial);
+            TRACE("mk_mul_bug", tout << "new_monomial:\n" << mk_pp(new_monomial, m_manager) << "\n";);
+            add_monomial_core<false>(new_monomial, monomials);
+        }
+    }
+    while (product_iterator_next(szs.size(), szs.c_ptr(), it.c_ptr()));
+    mk_sum_of_monomials(monomials, result);
+}
+
+void poly_simplifier_plugin::mk_mul(expr * arg1, expr * arg2, expr_ref & result) {
+    expr * args[2] = { arg1, arg2 };
+    mk_mul(2, args, result);
+}
+
+bool poly_simplifier_plugin::reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
+    set_reduce_invoked();
+    unsigned i = 0;
+    for (; i < num_args; i++)
+        if (!is_numeral(args[i]))
+            break;
+    if (i == num_args) {
+        // all arguments are numerals
+        // check if arguments are different...
+        ptr_buffer<expr> buffer;
+        buffer.append(num_args, args);
+        std::sort(buffer.begin(), buffer.end(), ast_lt_proc());
+        for (unsigned i = 0; i < num_args; i++) {
+            if (i > 0 && buffer[i] == buffer[i-1]) {
+                result = m_manager.mk_false();
+                return true;
+            }
+        }
+        result = m_manager.mk_true();
+        return true;
+    }
+    return false;
+}
+
+bool poly_simplifier_plugin::reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result) {
+    set_reduce_invoked();
+    if (is_decl_of(f, m_fid, m_ADD)) {
+        SASSERT(num_args > 0);
+        set_curr_sort(args[0]);
+        expr_ref_buffer args1(m_manager);
+        for (unsigned i = 0; i < num_args; ++i) {
+            expr * arg = args[i];
+            rational m = norm(mults[i]);
+            if (m.is_zero()) {
+                // skip
+            }
+            else if (m.is_one()) {
+                args1.push_back(arg);
+            }
+            else {
+                expr_ref k(m_manager);
+                k = mk_numeral(m);
+                expr_ref new_arg(m_manager);
+                mk_mul(k, args[i], new_arg);
+                args1.push_back(new_arg);
+            }
+        }
+        if (args1.empty()) {
+            result = mk_zero();
+        }
+        else {
+            mk_add(args1.size(), args1.c_ptr(), result);
+        }
+        return true;
+    }
+    else {
+        return simplifier_plugin::reduce(f, num_args, mults, args, result);
+    }
+}
+
+/**
+   \brief Return true if n is can be put into the form (+ v t) or (+ (- v) t)
+   \c inv = true will contain true if (- v) is found, and false otherwise.
+*/
+bool poly_simplifier_plugin::is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) {
+    if (!is_add(n) || is_ground(n))
+        return false;
+    
+    ptr_buffer<expr> args;
+    v = 0;
+    expr * curr = to_app(n);
+    bool stop = false;
+    inv = false;
+    while (!stop) {
+        expr * arg;
+        expr * neg_arg;
+        if (is_add(curr)) {
+            arg  = to_app(curr)->get_arg(0);
+            curr = to_app(curr)->get_arg(1);
+        }
+        else {
+            arg  = curr;
+            stop = true;
+        }
+        if (is_ground(arg)) {
+            TRACE("model_checker_bug", tout << "pushing:\n" << mk_pp(arg, m_manager) << "\n";);
+            args.push_back(arg);
+        }
+        else if (is_var(arg)) {
+            if (v != 0)
+                return false; // already found variable
+            v = to_var(arg);
+        }
+        else if (is_times_minus_one(arg, neg_arg) && is_var(neg_arg)) {
+            if (v != 0)
+                return false; // already found variable
+            v = to_var(neg_arg);
+            inv = true;
+        }
+        else {
+            return false; // non ground term.
+        }
+    }
+    if (v == 0)
+        return false; // did not find variable
+    SASSERT(!args.empty());
+    mk_add(args.size(), args.c_ptr(), t);
+    return true;
+}

src/simplifier/poly_simplifier_plugin.h

@@ -0,0 +1,151 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    poly_simplifier_plugin.h
+
+Abstract:
+
+    Abstract class for families that have polynomials.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-08
+    
+--*/
+#ifndef _POLY_SIMPLIFIER_PLUGIN_H_
+#define _POLY_SIMPLIFIER_PLUGIN_H_
+
+#include "simplifier_plugin.h"
+
+/**
+   \brief Abstract class that provides simplification functions for polynomials.
+*/
+class poly_simplifier_plugin : public simplifier_plugin {
+protected:
+    typedef rational numeral;
+    decl_kind          m_ADD;
+    decl_kind          m_MUL;
+    decl_kind          m_SUB;
+    decl_kind          m_UMINUS;
+    decl_kind          m_NUM;
+    sort *             m_curr_sort;
+    expr *             m_curr_sort_zero;
+
+    expr * mk_add(unsigned num_args, expr * const * args);
+    expr * mk_add(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_add(2, args); }
+    expr * mk_mul(unsigned num_args, expr * const * args);
+    expr * mk_mul(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_mul(2, args); }
+    expr * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_fid, m_SUB, num_args, args); }
+    expr * mk_uminus(expr * arg) { return m_manager.mk_app(m_fid, m_UMINUS, arg); }
+
+    void process_monomial(unsigned num_args, expr * const * args, numeral & k, ptr_buffer<expr> & result);
+    void mk_monomial(unsigned num_args, expr * * args, expr_ref & result);
+    bool eq_monomials_modulo_k(expr * n1, expr * n2);
+    bool merge_monomials(bool inv, expr * n1, expr * n2, expr_ref & result);
+    template<bool Inv>
+    void add_monomial_core(expr * n, expr_ref_vector & result);
+    void add_monomial(bool inv, expr * n, expr_ref_vector & result);
+    template<bool Inv>
+    void process_sum_of_monomials_core(expr * n, expr_ref_vector & result);
+    void process_sum_of_monomials(bool inv, expr * n, expr_ref_vector & result);
+    void process_sum_of_monomials(bool inv, expr * n, expr_ref_vector & result, numeral & k);
+    void mk_sum_of_monomials(expr_ref_vector & monomials, expr_ref & result);
+    template<bool Inv>
+    void mk_add_core_core(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_add_core(bool inv, unsigned num_args, expr * const * args, expr_ref & result);
+    void append_to_monomial(expr * n, numeral & k, ptr_buffer<expr> & result);
+    expr * mk_mul(numeral const & c, expr * body);
+    void mk_sum_of_monomials_core(unsigned sz, expr ** ms, expr_ref & result);
+    bool is_simple_sum_of_monomials(expr_ref_vector & monomials);
+    bool is_simple_monomial(expr * m, expr * & x);
+
+public:
+    poly_simplifier_plugin(symbol const & fname, ast_manager & m, decl_kind add, decl_kind mul, decl_kind uminus, decl_kind sub, decl_kind num);
+    virtual ~poly_simplifier_plugin() {}
+
+    /** 
+        \brief Return true if the given expression is a numeral, and store its value in \c val.
+    */
+    virtual bool is_numeral(expr * n, numeral & val) const = 0;
+    bool is_numeral(expr * n) const { return is_app_of(n, m_fid, m_NUM); }
+    bool is_zero(expr * n) const { 
+        SASSERT(m_curr_sort_zero != 0);
+        SASSERT(m_manager.get_sort(n) == m_manager.get_sort(m_curr_sort_zero)); 
+        return n == m_curr_sort_zero; 
+    }
+    bool is_zero_safe(expr * n) {
+        set_curr_sort(m_manager.get_sort(n));
+        return is_zero(n);
+    }
+    virtual bool is_minus_one(expr * n) const = 0;
+    virtual expr * get_zero(sort * s) const = 0;
+    
+
+    /**
+       \brief Return true if n is of the form (* -1 r)
+    */
+    bool is_times_minus_one(expr * n, expr * & r) const {
+        if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {
+            r = to_app(n)->get_arg(1);
+            return true;
+        }
+        return false;
+    }
+    
+    /**
+       \brief Return true if n is of the form: a <= b or a >= b.
+    */
+    virtual bool is_le_ge(expr * n) const = 0;
+    
+    /**
+       \brief Return a constant representing the giving numeral and sort m_curr_sort.
+    */
+    virtual app * mk_numeral(numeral const & n) = 0;
+    app * mk_zero() { return mk_numeral(numeral::zero()); }
+    app * mk_one() { return mk_numeral(numeral::one()); }
+    app * mk_minus_one() { return mk_numeral(numeral::minus_one()); }
+    
+    /**
+       \brief Normalize the given numeral with respect to m_curr_sort
+    */
+    virtual numeral norm(numeral const & n) = 0;
+
+    void set_curr_sort(sort * s) { 
+        if (s != m_curr_sort) { 
+            // avoid virtual function call
+            m_curr_sort = s; 
+            m_curr_sort_zero = get_zero(m_curr_sort); 
+        } 
+    }
+    void set_curr_sort(expr * n) { set_curr_sort(m_manager.get_sort(n)); }
+
+    bool is_add(expr const * n) const { return is_app_of(n, m_fid, m_ADD); }
+    bool is_mul(expr const * n) const { return is_app_of(n, m_fid, m_MUL); }
+    void mk_add(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_add(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_sub(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_sub(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_uminus(expr * arg, expr_ref & result);
+    void mk_mul(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_mul(expr * arg1, expr * arg2, expr_ref & result);
+    
+    virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result);
+
+    virtual bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result);
+
+    expr * get_monomial_body(expr * m);
+    int get_monomial_body_order(expr * m);
+    void get_monomial_coeff(expr * m, numeral & result);
+    void inv_monomial(expr * n, expr_ref & result);
+
+    bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t);
+
+#ifdef Z3DEBUG
+    bool wf_monomial(expr * m) const;
+    bool wf_polynomial(expr * m) const;
+#endif
+};
+
+#endif /* _POLY_SIMPLIFIER_PLUGIN_H_ */

src/simplifier/simplifier.cpp

@@ -0,0 +1,949 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    simplifier.cpp
+
+Abstract:
+
+    Expression simplifier.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-03
+
+Notes:
+
+--*/
+#include"simplifier.h"
+#include"var_subst.h"
+#include"ast_ll_pp.h"
+#include"ast_pp.h"
+#include"well_sorted.h"
+#include"ast_smt_pp.h"
+
+simplifier::simplifier(ast_manager & m):
+    base_simplifier(m),
+    m_proofs(m),
+    m_subst_proofs(m),
+    m_need_reset(false),
+    m_use_oeq(false),
+    m_visited_quantifier(false),
+    m_ac_support(true) {
+}
+
+void simplifier::register_plugin(plugin * p) { 
+    m_plugins.register_plugin(p); 
+}
+
+simplifier::~simplifier() {
+    flush_cache();
+}
+
+void simplifier::enable_ac_support(bool flag) {
+    m_ac_support = flag;
+    ptr_vector<plugin>::const_iterator it  = m_plugins.begin();
+    ptr_vector<plugin>::const_iterator end = m_plugins.end();
+    for (; it != end; ++it) {
+        if (*it != 0) 
+            (*it)->enable_ac_support(flag);
+    }
+}
+
+/**
+   \brief External interface for the simplifier. 
+   A client will invoke operator()(s, r, p) to simplify s.
+   The result is stored in r.
+   When proof generation is enabled, a proof for the equivalence (or equisatisfiability)
+   of s and r is stored in p.
+   When proof generation is disabled, this method stores the "undefined proof" object in p.
+*/
+void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) {
+    m_need_reset = true;
+    expr  * old_s;
+    expr  * result;
+    proof * result_proof;
+    switch (m_manager.proof_mode()) {
+    case PGM_DISABLED: // proof generation is disabled.
+        reduce_core(s); 
+        // after executing reduce_core, the result of the simplification is in the cache
+        get_cached(s, result, result_proof);
+        r = result;
+        p = m_manager.mk_undef_proof();
+        break;
+    case PGM_COARSE: // coarse proofs... in this case, we do not produce a step by step (fine grain) proof to show the equivalence (or equisatisfiability) of s an r.
+        m_subst_proofs.reset(); // m_subst_proofs is an auxiliary vector that is used to justify substitutions. See comment on method get_subst. 
+        reduce_core(s);
+        get_cached(s, result, result_proof);
+        r = result;
+        if (result == s)
+            p = m_manager.mk_reflexivity(s);
+        else {
+            remove_duplicates(m_subst_proofs);
+            p = m_manager.mk_rewrite_star(s, result, m_subst_proofs.size(), m_subst_proofs.c_ptr());
+        }
+        break;
+    case PGM_FINE: // fine grain proofs... in this mode, every proof step (or most of them) is described.
+        m_proofs.reset();
+        old_s = 0;
+        // keep simplyfing until no further simplifications are possible.
+        while (s != old_s) {
+            TRACE("simplifier", tout << "simplification pass... " << s->get_id() << "\n";);
+            TRACE("simplifier_loop", tout << mk_ll_pp(s, m_manager) << "\n";);
+            reduce_core(s);
+            get_cached(s, result, result_proof);
+            if (result_proof != 0)
+                m_proofs.push_back(result_proof);
+            old_s = s;
+            s     = result;
+        }
+        SASSERT(s != 0);
+        r = s;
+        p = m_proofs.empty() ? m_manager.mk_reflexivity(s) : m_manager.mk_transitivity(m_proofs.size(), m_proofs.c_ptr());
+        break;
+    default:
+        UNREACHABLE();
+    }
+}
+
+void simplifier::flush_cache() {
+    m_cache.flush();
+    ptr_vector<plugin>::const_iterator it  = m_plugins.begin();
+    ptr_vector<plugin>::const_iterator end = m_plugins.end();
+    for (; it != end; ++it) {
+        if (*it != 0) {
+            (*it)->flush_caches();
+        }
+    }
+}
+
+bool simplifier::get_subst(expr * n, expr_ref & r, proof_ref & p) {
+    return false;
+}
+
+void simplifier::reduce_core(expr * n) {
+    if (!is_cached(n)) {
+        // We do not assume m_todo is empty... So, we store the current size of the todo-stack.
+        unsigned sz = m_todo.size();
+        m_todo.push_back(n);
+        while (m_todo.size() != sz) {
+            expr * n = m_todo.back();
+            if (is_cached(n))
+                m_todo.pop_back();
+            else if (visit_children(n)) {
+                // if all children were already simplified, then remove n from the todo stack and apply a
+                // simplification step to it.
+                m_todo.pop_back();
+                reduce1(n);
+            }
+        }
+    }
+}
+
+/**
+   \brief Return true if all children of n have been already simplified.
+*/
+bool simplifier::visit_children(expr * n) {
+    switch(n->get_kind()) {
+    case AST_VAR:
+        return true;
+    case AST_APP:
+        // The simplifier has support for flattening AC (associative-commutative) operators.
+        // The method ast_manager::mk_app is used to create the flat version of an AC operator.
+        // In Z3 1.x, we used multi-ary operators. This creates problems for the superposition engine.
+        // So, starting at Z3 2.x, only boolean operators can be multi-ary.
+        // Example: 
+        //    (and (and a b) (and c d)) --> (and a b c d)
+        //    (+ (+ a b) (+ c d)) --> (+ a (+ b (+ c d)))
+        // Remark: The flattening is only applied if m_ac_support is true.
+        if (m_ac_support && to_app(n)->get_decl()->is_associative() && to_app(n)->get_decl()->is_commutative())
+            return visit_ac(to_app(n));
+        else {
+            bool visited = true;
+            unsigned j = to_app(n)->get_num_args();
+            while (j > 0) {
+                --j;
+                visit(to_app(n)->get_arg(j), visited);
+            }
+            return visited;
+        }
+    case AST_QUANTIFIER: 
+        return visit_quantifier(to_quantifier(n));
+    default:
+        UNREACHABLE();
+        return true;
+    }
+}
+
+/**
+   \brief Visit the children of n assuming it is an AC (associative-commutative) operator.
+   
+   For example, if n is of the form (+ (+ a b) (+ c d)), this method
+   will return true if the nodes a, b, c and d have been already simplified.
+   The nodes (+ a b) and (+ c d) are not really checked.
+*/
+bool simplifier::visit_ac(app * n) {
+    bool visited = true;
+    func_decl * decl = n->get_decl();
+    SASSERT(m_ac_support);
+    SASSERT(decl->is_associative());
+    SASSERT(decl->is_commutative());
+    m_ac_marked.reset();
+    ptr_buffer<app> todo;
+    todo.push_back(n);
+    while (!todo.empty()) {
+        app * n = todo.back();
+        todo.pop_back();
+        if (m_ac_mark.is_marked(n))
+            continue;
+        m_ac_mark.mark(n, true);
+        m_ac_marked.push_back(n);
+        SASSERT(n->get_decl() == decl);
+        unsigned i = n->get_num_args();
+        while (i > 0) {
+            --i;
+            expr * arg  = n->get_arg(i);
+            if (is_app_of(arg, decl))
+                todo.push_back(to_app(arg));
+            else 
+                visit(arg, visited);
+        }
+    }
+    ptr_vector<expr>::const_iterator it  = m_ac_marked.begin();
+    ptr_vector<expr>::const_iterator end = m_ac_marked.end();
+    for (; it != end; ++it)
+        m_ac_mark.mark(*it, false);
+    return visited;
+}
+
+bool simplifier::visit_quantifier(quantifier * n) {
+    m_visited_quantifier = true;
+    bool visited         = true;
+    unsigned j = to_quantifier(n)->get_num_patterns();
+    while (j > 0) {
+        --j;
+        visit(to_quantifier(n)->get_pattern(j), visited);
+    }
+    j = to_quantifier(n)->get_num_no_patterns();
+    while (j > 0) {
+        --j;
+        visit(to_quantifier(n)->get_no_pattern(j), visited);
+    }
+    visit(to_quantifier(n)->get_expr(), visited);
+    return visited;
+}
+
+/**
+   \brief Simplify n and store the result in the cache.
+*/
+void simplifier::reduce1(expr * n) {
+    switch (n->get_kind()) {
+    case AST_VAR:
+        cache_result(n, n, 0);
+        break;
+    case AST_APP:
+        reduce1_app(to_app(n));
+        break;
+    case AST_QUANTIFIER:
+        reduce1_quantifier(to_quantifier(n));
+        break;
+    default:
+        UNREACHABLE();
+    }
+}
+
+/**
+   \brief Simplify the given application using the cached values,
+   associativity flattening, the given substitution, and family/theory
+   specific simplifications via plugins.
+*/
+void simplifier::reduce1_app(app * n) {
+    expr_ref r(m_manager);
+    proof_ref p(m_manager);
+    TRACE("reduce", tout << "reducing...\n" << mk_pp(n, m_manager) << "\n";);
+    if (get_subst(n, r, p)) {
+        TRACE("reduce", tout << "applying substitution...\n";);
+        cache_result(n, r, p);
+        return;
+    }
+
+    func_decl * decl = n->get_decl();
+    if (m_ac_support && decl->is_associative() && decl->is_commutative())
+        reduce1_ac_app_core(n);
+    else
+        reduce1_app_core(n);
+}
+
+
+void simplifier::reduce1_app_core(app * n) {
+    m_args.reset();
+    func_decl * decl = n->get_decl();
+    proof_ref p1(m_manager);
+    // Stores the new arguments of n in m_args.
+    // Let n be of the form
+    // (decl arg_0 ... arg_{n-1})
+    // then
+    // m_args contains [arg_0', ..., arg_{n-1}'],
+    // where arg_i' is the simplification of arg_i
+    // and
+    // p1 is a proof for
+    // (decl arg_0 ... arg_{n-1}) is equivalente/equisatisfiable to (decl arg_0' ... arg_{n-1}')
+    // p1 is built using the congruence proof step and the proofs for arg_0' ... arg_{n-1}'.
+    // Of course, p1 is 0 if proofs are not enabled or coarse grain proofs are used.
+    bool has_new_args = get_args(n, m_args, p1);
+    // The following if implements a simple trick.
+    //   If none of the arguments have been simplified, and n is not a theory symbol,
+    //   Then no simplification is possible, and we can cache the result of the simplification of n as n.
+    if (has_new_args || decl->get_family_id() != null_family_id) {
+        expr_ref r(m_manager);
+        TRACE("reduce", tout << "reduce1_app\n"; for(unsigned i = 0; i < m_args.size(); i++) tout << mk_ll_pp(m_args[i], m_manager););
+        // the method mk_app invokes get_subst and plugins to simplify
+        // (decl arg_0' ... arg_{n-1}')
+        mk_app(decl, m_args.size(), m_args.c_ptr(), r);
+        if (!m_manager.fine_grain_proofs()) {
+            cache_result(n, r, 0);
+        }
+        else {
+            expr * s = m_manager.mk_app(decl, m_args.size(), m_args.c_ptr());
+            proof * p;
+            if (n == r)
+                p = 0;
+            else if (r != s) 
+                // we use a "theory rewrite generic proof" to justify the step
+                // s = (decl arg_0' ... arg_{n-1}') --> r
+                p = m_manager.mk_transitivity(p1, m_manager.mk_rewrite(s, r));
+            else
+                p = p1;
+            cache_result(n, r, p);
+        }
+    }
+    else {
+        cache_result(n, n, 0);
+    }
+}
+
+bool is_ac_list(app * n, ptr_vector<expr> & args) {
+    args.reset();
+    func_decl * f = n->get_decl();
+    app * curr    = n;
+    while (true) {
+        if (curr->get_num_args() != 2)
+            return false;
+        expr * arg1 = curr->get_arg(0);
+        if (is_app_of(arg1, f))
+            return false;
+        args.push_back(arg1);
+        expr * arg2 = curr->get_arg(1);
+        if (!is_app_of(arg2, f)) {
+            args.push_back(arg2);
+            return true;
+        }
+        curr = to_app(arg2);
+    }
+}
+
+bool is_ac_vector(app * n) {
+    func_decl * f     = n->get_decl();
+    unsigned num_args = n->get_num_args();
+    for (unsigned i = 0; i < num_args; i++) {
+        if (is_app_of(n->get_arg(i), f))
+            return false;
+    }
+    return true;
+}
+
+void simplifier::reduce1_ac_app_core(app * n) {
+    app_ref    n_c(m_manager);
+    proof_ref  p1(m_manager);
+    mk_ac_congruent_term(n, n_c, p1);
+    TRACE("ac", tout << "expr:\n" << mk_pp(n, m_manager) << "\ncongruent term:\n" << mk_pp(n_c, m_manager) << "\n";);
+    expr_ref r(m_manager); 
+    func_decl * decl = n->get_decl();
+    family_id fid    = decl->get_family_id();
+    plugin * p       = get_plugin(fid);
+    if (is_ac_vector(n_c)) {
+        if (p != 0 && p->reduce(decl, n_c->get_num_args(), n_c->get_args(), r)) {
+            // done...
+        }
+        else {
+            r = n_c;
+        }
+    }
+    else if (is_ac_list(n_c, m_args)) {
+        // m_args contains the arguments...
+        if (p != 0 && p->reduce(decl, m_args.size(), m_args.c_ptr(), r)) {
+            // done...
+        }
+        else {
+            r = m_manager.mk_app(decl, m_args.size(), m_args.c_ptr());
+        }
+    }
+    else {
+        m_args.reset();
+        m_mults.reset();
+        get_ac_args(n_c, m_args, m_mults);
+        TRACE("ac", tout << "AC args:\n";
+              for (unsigned i = 0; i < m_args.size(); i++) {
+                  tout << mk_pp(m_args[i], m_manager) << " * " << m_mults[i] << "\n";
+              });
+        if (p != 0 && p->reduce(decl, m_args.size(), m_mults.c_ptr(), m_args.c_ptr(), r)) {
+            // done...
+        }
+        else {
+            ptr_buffer<expr> new_args;
+            expand_args(m_args.size(), m_mults.c_ptr(), m_args.c_ptr(), new_args);
+            r = m_manager.mk_app(decl, new_args.size(), new_args.c_ptr());
+        }
+    }
+    TRACE("ac", tout << "AC result:\n" << mk_pp(r, m_manager) << "\n";);
+
+    if (!m_manager.fine_grain_proofs()) {
+        cache_result(n, r, 0);
+    }
+    else {
+        proof * p;
+        if (n == r.get())
+            p = 0;
+        else if (r.get() != n_c.get()) 
+            p = m_manager.mk_transitivity(p1, m_manager.mk_rewrite(n_c, r));
+        else
+            p = p1;
+        cache_result(n, r, p);
+    }
+}
+
+static unsigned g_rewrite_lemma_id = 0;
+
+void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr * const * args, expr* result) {
+    expr_ref arg(m_manager);
+    arg = m_manager.mk_app(decl, num_args, args);
+    if (arg.get() != result) {
+        char buffer[128];
+#ifdef _WINDOWS
+        sprintf_s(buffer, ARRAYSIZE(buffer), "lemma_%d.smt", g_rewrite_lemma_id);
+#else
+        sprintf(buffer, "rewrite_lemma_%d.smt", g_rewrite_lemma_id);
+#endif        
+        ast_smt_pp pp(m_manager);
+        pp.set_benchmark_name("rewrite_lemma");
+        pp.set_status("unsat");
+        expr_ref n(m_manager);
+        n = m_manager.mk_not(m_manager.mk_eq(arg.get(), result));
+        std::ofstream out(buffer);
+        pp.display(out, n);
+        out.close();
+        ++g_rewrite_lemma_id;
+    }
+}
+
+/**
+   \brief Return in \c result an expression \c e equivalent to <tt>(f args[0] ... args[num_args - 1])</tt>, and
+   store in \c pr a proof for <tt>(= (f args[0] ... args[num_args - 1]) e)</tt>
+   
+   If e is identical to (f args[0] ... args[num_args - 1]), then pr is set to 0.
+*/
+void simplifier::mk_app(func_decl * decl, unsigned num_args, expr * const * args, expr_ref & result) {
+    m_need_reset = true;
+    if (m_manager.is_eq(decl)) {
+        sort * s = m_manager.get_sort(args[0]);
+        plugin * p = get_plugin(s->get_family_id());
+        if (p != 0 && p->reduce_eq(args[0], args[1], result))
+            return;
+    }
+    else if (m_manager.is_distinct(decl)) {
+        sort * s = m_manager.get_sort(args[0]);
+        plugin * p = get_plugin(s->get_family_id());
+        if (p != 0 && p->reduce_distinct(num_args, args, result))
+            return;
+    }
+    family_id fid = decl->get_family_id();
+    plugin * p = get_plugin(fid);
+    if (p != 0 && p->reduce(decl, num_args, args, result)) {
+        //uncomment this line if you want to trace rewrites as lemmas:
+        //dump_rewrite_lemma(decl, num_args, args, result.get());
+        return;
+    }
+    result = m_manager.mk_app(decl, num_args, args);
+}
+
+/**
+   \brief Create a term congruence to n (f a[0] ... a[num_args-1]) using the
+   cached values for the a[i]'s. Store the result in r, and the proof for (= n r) in p.
+   If n and r are identical, then set p to 0.
+*/
+void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) {
+    bool has_new_args  = false;
+    ptr_vector<expr>   args;
+    ptr_vector<proof>  proofs;
+    unsigned num       = n->get_num_args();
+    for (unsigned j = 0; j < num; j++) {
+        expr * arg     = n->get_arg(j);
+        expr * new_arg;
+        proof * arg_proof;
+        get_cached(arg, new_arg, arg_proof);
+
+        CTRACE("simplifier_bug", (arg != new_arg) != (arg_proof != 0), 
+               tout << mk_ll_pp(arg, m_manager) << "\n---->\n" << mk_ll_pp(new_arg, m_manager) << "\n";
+               tout << "#" << arg->get_id() << " #" << new_arg->get_id() << "\n";
+               tout << arg << " " << new_arg << "\n";);
+        
+        
+        if (arg != new_arg) {
+            has_new_args = true;
+            proofs.push_back(arg_proof);
+            SASSERT(arg_proof);
+        } 
+        else {
+            SASSERT(arg_proof == 0);
+        }
+        args.push_back(new_arg);
+    }
+    if (has_new_args) {
+        r = m_manager.mk_app(n->get_decl(), args.size(), args.c_ptr());
+        if (m_use_oeq)
+            p = m_manager.mk_oeq_congruence(n, r, proofs.size(), proofs.c_ptr());
+        else
+            p = m_manager.mk_congruence(n, r, proofs.size(), proofs.c_ptr());
+    }
+    else {
+        r = n;
+        p = 0;
+    }
+}
+
+/**
+   \brief Store the new arguments of \c n in result. Store in p a proof for
+   (= n (f result[0] ... result[num_args - 1])), where f is the function symbol of n.
+   
+   If there are no new arguments or fine grain proofs are disabled, then p is set to 0.
+
+   Return true there are new arguments. 
+*/
+bool simplifier::get_args(app * n, ptr_vector<expr> & result, proof_ref & p) {
+    bool has_new_args  = false;
+    unsigned num       = n->get_num_args();
+    if (m_manager.fine_grain_proofs()) {
+        app_ref r(m_manager);
+        mk_congruent_term(n, r, p);
+        result.append(r->get_num_args(), r->get_args());
+        SASSERT(n->get_num_args() == result.size());
+        has_new_args = r != n;
+    }
+    else {
+        p = 0;
+        for (unsigned j = 0; j < num; j++) {
+            expr * arg     = n->get_arg(j);
+            expr * new_arg;
+            proof * arg_proof;
+            get_cached(arg, new_arg, arg_proof);
+            if (arg != new_arg) {
+                has_new_args = true;
+            }
+            result.push_back(new_arg);
+        }
+    }
+    return has_new_args;
+}
+
+/**
+   \brief Create a term congruence to n (where n is an expression such as: (f (f a_1 a_2) (f a_3 (f a_4 a_5))) using the
+   cached values for the a_i's. Store the result in r, and the proof for (= n r) in p.
+   If n and r are identical, then set p to 0.
+*/
+void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
+    SASSERT(m_ac_support);
+    func_decl * f = n->get_decl();
+    
+    m_ac_cache.reset();
+    m_ac_pr_cache.reset();
+    
+    ptr_buffer<app>   todo;
+    ptr_buffer<expr>  new_args;
+    ptr_buffer<proof> new_arg_prs;
+    todo.push_back(n);
+    while (!todo.empty()) {
+        app * curr    = todo.back();
+        if (m_ac_cache.contains(curr)) {
+            todo.pop_back();
+            continue;
+        }
+        bool visited     = true;
+        bool has_new_arg = false;
+        new_args.reset();
+        new_arg_prs.reset();
+        unsigned num_args = curr->get_num_args();
+        for (unsigned j = 0; j < num_args; j ++) {
+            expr * arg = curr->get_arg(j);
+            if (is_app_of(arg, f)) {
+                app * new_arg = 0;
+                if (m_ac_cache.find(to_app(arg), new_arg)) {
+                    SASSERT(new_arg != 0);
+                    new_args.push_back(new_arg);
+                    if (arg != new_arg)
+                        has_new_arg = true;
+                    if (m_manager.fine_grain_proofs()) {
+                        proof * pr = 0;
+                        m_ac_pr_cache.find(to_app(arg), pr);
+                        if (pr != 0)
+                            new_arg_prs.push_back(pr);
+                    }
+                }
+                else {
+                    visited = false;
+                    todo.push_back(to_app(arg));
+                }
+            }
+            else {
+                expr * new_arg = 0;
+                proof * pr;
+                get_cached(arg, new_arg, pr);
+                new_args.push_back(new_arg);
+                if (arg != new_arg)
+                    has_new_arg = true;
+                if (m_manager.fine_grain_proofs() && pr != 0)
+                    new_arg_prs.push_back(pr);
+            }
+        }
+        if (visited) {
+            SASSERT(new_args.size() == curr->get_num_args());
+            todo.pop_back();
+            if (!has_new_arg) {
+                m_ac_cache.insert(curr, curr);
+                if (m_manager.fine_grain_proofs()) 
+                    m_ac_pr_cache.insert(curr, 0);
+            }
+            else {
+                app * new_curr = m_manager.mk_app(f, new_args.size(), new_args.c_ptr());
+                m_ac_cache.insert(curr, new_curr);
+                if (m_manager.fine_grain_proofs()) {
+                    proof * p = m_manager.mk_congruence(curr, new_curr, new_arg_prs.size(), new_arg_prs.c_ptr());
+                    m_ac_pr_cache.insert(curr, p);
+                }
+            }
+        }
+    }
+    
+    SASSERT(m_ac_cache.contains(n));
+    app *   new_n = 0;
+    m_ac_cache.find(n, new_n);
+    r = new_n;
+    if (m_manager.fine_grain_proofs()) {
+        proof * new_pr = 0;
+        m_ac_pr_cache.find(n, new_pr);
+        p = new_pr;
+    }
+}
+
+#define White 0 
+#define Grey  1
+#define Black 2
+
+static int get_color(obj_map<expr, int> & colors, expr * n) {
+    obj_map<expr, int>::obj_map_entry * entry = colors.insert_if_not_there2(n, White);
+    return entry->get_data().m_value;
+}
+
+static bool visit_ac_children(func_decl * f, expr * n, obj_map<expr, int> & colors, ptr_buffer<expr> & todo, ptr_buffer<expr> & result) {
+    if (is_app_of(n, f)) {
+        unsigned num_args = to_app(n)->get_num_args();
+        bool visited      = true;
+        // Put the arguments in 'result' in reverse order.
+        // Reason: preserve the original order of the arguments in the final result.
+        // Remark: get_ac_args will traverse 'result' backwards.
+        for (unsigned i = 0; i < num_args; i++) {
+            expr * arg = to_app(n)->get_arg(i);
+            obj_map<expr, int>::obj_map_entry * entry = colors.insert_if_not_there2(arg, White);
+            if (entry->get_data().m_value == White) {
+                todo.push_back(arg);
+                visited = false;
+            }
+        }
+        return visited;
+    }
+    else {
+        return true;
+    }
+}
+
+void simplifier::ac_top_sort(app * n, ptr_buffer<expr> & result) {
+    ptr_buffer<expr> todo;
+    func_decl * f = n->get_decl();
+    obj_map<expr, int> & colors = m_colors;
+    colors.reset();
+    todo.push_back(n);
+    while (!todo.empty()) {
+        expr * curr = todo.back();
+        int color;
+        obj_map<expr, int>::obj_map_entry * entry = colors.insert_if_not_there2(curr, White); 
+        SASSERT(entry);
+        color = entry->get_data().m_value;
+        switch (color) {
+        case White:
+            // Remark: entry becomes invalid if an element is inserted into the hashtable.
+            // So, I must set Grey before executing visit_ac_children.
+            entry->get_data().m_value = Grey;
+            SASSERT(get_color(colors, curr) == Grey);
+            if (visit_ac_children(f, curr, colors, todo, result)) {
+                // If visit_ac_children succeeded, then the hashtable was not modified,
+                // and entry is still valid.
+                SASSERT(todo.back() == curr);
+                entry->get_data().m_value = Black;
+                SASSERT(get_color(colors, curr) == Black);
+                result.push_back(curr);
+                todo.pop_back();
+            }
+            break;
+        case Grey:
+            SASSERT(visit_ac_children(f, curr, colors, todo, result));
+            SASSERT(entry);
+            entry->get_data().m_value = Black;
+            SASSERT(get_color(colors, curr) == Black);
+            result.push_back(curr);
+            SASSERT(todo.back() == curr);
+            todo.pop_back();
+            break;
+        case Black:
+            todo.pop_back();
+            break;
+        default:
+            UNREACHABLE();
+        }
+    }
+}
+
+void simplifier::get_ac_args(app * n, ptr_vector<expr> & args, vector<rational> & mults) {
+    SASSERT(m_ac_support);
+    ptr_buffer<expr> sorted_exprs;
+    ac_top_sort(n, sorted_exprs);
+    SASSERT(!sorted_exprs.empty());
+    SASSERT(sorted_exprs[sorted_exprs.size()-1] == n);
+    
+    TRACE("ac", tout << mk_ll_pp(n, m_manager, true, false) << "#" << n->get_id() << "\nsorted expressions...\n";
+          for (unsigned i = 0; i < sorted_exprs.size(); i++) {
+              tout << "#" << sorted_exprs[i]->get_id() << " ";
+          }
+          tout << "\n";);
+
+    m_ac_mults.reset();
+    m_ac_mults.insert(n, rational(1));
+    func_decl * decl = n->get_decl();
+    unsigned j = sorted_exprs.size();
+    while (j > 0) {
+        --j;
+        expr * curr = sorted_exprs[j];
+        rational mult;
+        m_ac_mults.find(curr, mult);
+        SASSERT(!mult.is_zero());        
+        if (is_app_of(curr, decl)) {
+            unsigned num_args = to_app(curr)->get_num_args();
+            for (unsigned i = 0; i < num_args; i++) {
+                expr * arg = to_app(curr)->get_arg(i);
+                rational zero;
+                obj_map<expr, rational>::obj_map_entry * entry = m_ac_mults.insert_if_not_there2(arg, zero);
+                entry->get_data().m_value += mult;
+            }
+        }
+        else {
+            args.push_back(curr);
+            mults.push_back(mult);
+        }
+    }
+}
+
+void simplifier::reduce1_quantifier(quantifier * q) {
+    expr *  new_body;
+    proof * new_body_pr;
+    SASSERT(is_well_sorted(m_manager, q));
+    get_cached(q->get_expr(), new_body, new_body_pr);
+
+    quantifier_ref q1(m_manager);
+    proof * p1 = 0;
+    
+    if (is_quantifier(new_body) && 
+        to_quantifier(new_body)->is_forall() == q->is_forall() &&
+        !to_quantifier(q)->has_patterns() &&
+        !to_quantifier(new_body)->has_patterns()) {
+        
+        quantifier * nested_q = to_quantifier(new_body);
+
+        ptr_buffer<sort> sorts;
+        buffer<symbol>   names;   
+        sorts.append(q->get_num_decls(), q->get_decl_sorts());
+        names.append(q->get_num_decls(), q->get_decl_names());
+        sorts.append(nested_q->get_num_decls(), nested_q->get_decl_sorts());
+        names.append(nested_q->get_num_decls(), nested_q->get_decl_names());
+
+        q1 = m_manager.mk_quantifier(q->is_forall(),
+                                     sorts.size(),
+                                     sorts.c_ptr(),
+                                     names.c_ptr(),
+                                     nested_q->get_expr(),
+                                     std::min(q->get_weight(), nested_q->get_weight()),
+                                     q->get_qid(),
+                                     q->get_skid(),
+                                     0, 0, 0, 0);
+        SASSERT(is_well_sorted(m_manager, q1));
+        
+        if (m_manager.fine_grain_proofs()) {
+            quantifier * q0 = m_manager.update_quantifier(q, new_body);
+            proof * p0 = q == q0 ? 0 : m_manager.mk_quant_intro(q, q0, new_body_pr);
+            p1 = m_manager.mk_pull_quant(q0, q1);
+            p1 = m_manager.mk_transitivity(p0, p1);
+        }
+    }
+    else {
+        ptr_buffer<expr> new_patterns;
+        ptr_buffer<expr> new_no_patterns;
+        expr  * new_pattern;
+        proof * new_pattern_pr;
+
+        // Remark: we can ignore the proofs for the patterns.
+        unsigned num = q->get_num_patterns();
+        for (unsigned i = 0; i < num; i++) {
+            get_cached(q->get_pattern(i), new_pattern, new_pattern_pr);
+            if (m_manager.is_pattern(new_pattern)) {
+                new_patterns.push_back(new_pattern);
+            }            
+        }
+        num = q->get_num_no_patterns();
+        for (unsigned i = 0; i < num; i++) {
+            get_cached(q->get_no_pattern(i), new_pattern, new_pattern_pr);
+            new_no_patterns.push_back(new_pattern);
+        } 
+
+        remove_duplicates(new_patterns);
+        remove_duplicates(new_no_patterns);
+
+        q1 = m_manager.mk_quantifier(q->is_forall(),
+                                     q->get_num_decls(),
+                                     q->get_decl_sorts(),
+                                     q->get_decl_names(),
+                                     new_body,
+                                     q->get_weight(), 
+                                     q->get_qid(),
+                                     q->get_skid(),
+                                     new_patterns.size(),
+                                     new_patterns.c_ptr(),
+                                     new_no_patterns.size(),
+                                     new_no_patterns.c_ptr());
+        SASSERT(is_well_sorted(m_manager, q1));
+
+        TRACE("simplifier", tout << mk_pp(q, m_manager) << "\n" << mk_pp(q1, m_manager) << "\n";);
+        if (m_manager.fine_grain_proofs()) {
+            if (q != q1 && !new_body_pr) {
+                new_body_pr = m_manager.mk_rewrite(q->get_expr(), new_body);
+            }
+            p1 = q == q1 ? 0 : m_manager.mk_quant_intro(q, q1, new_body_pr);
+        }
+    }
+    
+    expr_ref r(m_manager);
+    elim_unused_vars(m_manager, q1, r);
+    
+    proof * pr = 0;
+    if (m_manager.fine_grain_proofs()) {
+        proof * p2 = 0;
+        if (q1.get() != r.get())
+            p2 = m_manager.mk_elim_unused_vars(q1, r);
+        pr = m_manager.mk_transitivity(p1, p2);
+    }
+
+    cache_result(q, r, pr);
+}
+
+/**
+   \see release_plugins
+*/
+void simplifier::borrow_plugins(simplifier const & s) {
+    ptr_vector<plugin>::const_iterator it  = s.begin_plugins();
+    ptr_vector<plugin>::const_iterator end = s.end_plugins();
+    for (; it != end; ++it) 
+        register_plugin(*it);
+}
+
+/**
+   \brief Make the simplifier behave as a pre-simplifier: No AC, and plugins are marked in pre-simplification mode.
+*/
+void simplifier::enable_presimp() {
+    enable_ac_support(false);
+    ptr_vector<plugin>::const_iterator it  = begin_plugins();
+    ptr_vector<plugin>::const_iterator end = end_plugins();
+    for (; it != end; ++it) 
+        (*it)->enable_presimp(true);
+}
+
+/**
+   \brief This method should be invoked if the plugins of this simplifier were borrowed from a different simplifier.
+*/
+void simplifier::release_plugins() {
+    m_plugins.release();
+}
+
+void subst_simplifier::set_subst_map(expr_map * s) {
+    flush_cache();
+    m_subst_map = s;
+}
+
+bool subst_simplifier::get_subst(expr * n, expr_ref & r, proof_ref & p) {
+    if (m_subst_map && m_subst_map->contains(n)) {
+        expr *  _r;
+        proof * _p = 0;
+        m_subst_map->get(n, _r, _p);
+        r = _r;
+        p = _p;
+        if (m_manager.coarse_grain_proofs()) 
+            m_subst_proofs.push_back(p);
+        return true;
+    }
+    return false;
+}
+
+static void push_core(ast_manager & m, expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) {
+    SASSERT(pr == 0 || m.is_undef_proof(pr) || e == m.get_fact(pr));
+    TRACE("preprocessor",
+          tout << mk_pp(e, m) << "\n";
+          if (pr) tout << mk_ll_pp(pr, m) << "\n\n";);
+    if (m.is_true(e)) 
+        return;
+    result.push_back(e);
+    if (m.proofs_enabled())
+        result_prs.push_back(pr);
+}
+
+static void push_and(ast_manager & m, app * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) {
+    unsigned num = e->get_num_args();
+    TRACE("push_and", tout << mk_pp(e, m) << "\n";);
+    for (unsigned i = 0; i < num; i++)
+        push_assertion(m, e->get_arg(i), m.mk_and_elim(pr, i), result, result_prs);
+}
+
+static void push_not_or(ast_manager & m, app * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) {
+    unsigned num = e->get_num_args();
+    TRACE("push_not_or", tout << mk_pp(e, m) << "\n";);
+    for (unsigned i = 0; i < num; i++) {
+        expr * child = e->get_arg(i);
+        if (m.is_not(child)) {
+            expr * not_child = to_app(child)->get_arg(0);
+            push_assertion(m, not_child, m.mk_not_or_elim(pr, i), result, result_prs);
+        }
+        else {
+            expr_ref not_child(m);
+            not_child = m.mk_not(child);
+            push_assertion(m, not_child, m.mk_not_or_elim(pr, i), result, result_prs);
+        }
+    }
+}
+
+void push_assertion(ast_manager & m, expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) {
+    CTRACE("push_assertion", !(pr == 0 || m.is_undef_proof(pr) || m.get_fact(pr) == e),
+           tout << mk_pp(e, m) << "\n" << mk_pp(m.get_fact(pr), m) << "\n";);
+    SASSERT(pr == 0 || m.is_undef_proof(pr) || m.get_fact(pr) == e);
+    if (m.is_and(e)) 
+        push_and(m, to_app(e), pr, result, result_prs);
+    else if (m.is_not(e) && m.is_or(to_app(e)->get_arg(0))) 
+        push_not_or(m, to_app(to_app(e)->get_arg(0)), pr, result, result_prs);
+    else
+        push_core(m, e, pr, result, result_prs);
+}
+

src/simplifier/simplifier.h

@@ -0,0 +1,232 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    simplifier.h
+
+Abstract:
+
+    Generic expression simplifier with support for theory specific "plugins".
+
+Author:
+
+    Leonardo (leonardo) 2008-01-03
+
+Notes:
+
+--*/
+#ifndef _SIMPLIFIER_H_
+#define _SIMPLIFIER_H_
+
+#include"base_simplifier.h"
+#include"simplifier_plugin.h"
+#include"plugin_manager.h"
+#include"ast_util.h"
+#include"obj_hashtable.h"
+
+/**
+   \brief Local simplifier.
+   Proof production can be enabled/disabled.
+   
+   The simplifier can also apply substitutions during the
+   simplification. A substitution is a mapping from expression
+   to expression+proof, where for each entry e_1->(e_2,p) p is 
+   a proof for (= e_1 e_2).
+   
+   The simplifier can also generate coarse grain proofs. In a coarse
+   proof, local rewrite steps are omitted, and only the substitutions
+   used are tracked.
+
+   Example: 
+
+   Consider the expression (+ a b), and the substitution b->(0, p)
+   When fine grain proofs are enabled, the simplifier will produce the
+   following proof
+
+   Assume the id of the proof object p is $0. Note that p is a proof for (= b 0).
+
+   $1: [reflexivity] |- (= a a)
+   $2: [congruence] $1 $0 |- (= (+ a b) (+ a 0))
+   $3: [plus-0] |- (= (+ a 0) a)
+   $4: [transitivity] $2 $3 |- (= (+ a b) a)
+
+   When coarse grain proofs are enabled, the simplifier produces the following
+   proof:
+
+   $1: [simplifier] $0 |- (= (+ a b) a)
+*/
+class simplifier : public base_simplifier {
+protected:
+    typedef simplifier_plugin plugin;
+    plugin_manager<plugin>         m_plugins;
+    ptr_vector<expr>               m_args;
+    vector<rational>               m_mults;
+    ptr_vector<expr>               m_args2;
+
+    proof_ref_vector               m_proofs; // auxiliary vector for implementing exhaustive simplification.
+    proof_ref_vector               m_subst_proofs; // in coarse grain proof generation mode, this vector tracks the justification for substitutions (see method get_subst).
+
+    bool                           m_need_reset;
+    bool                           m_use_oeq;
+
+    bool                           m_visited_quantifier; //!< true, if the simplifier found a quantifier
+
+    bool                           m_ac_support;
+
+    expr_mark                      m_ac_mark;
+    ptr_vector<expr>               m_ac_marked;
+    obj_map<app, app *>            m_ac_cache;    // temporary cache for ac
+    obj_map<app, proof *>          m_ac_pr_cache; // temporary cache for ac
+    obj_map<expr, int>             m_colors;      // temporary cache for topological sort.
+    obj_map<expr, rational>        m_ac_mults;
+
+    /*
+      Simplifier uses an idiom for rewriting ASTs without using recursive calls.
+
+      - It uses a cache (field m_cache in base_simplifier) and a todo-stack (field m_todo in base_simplifier).
+      
+      - The cache is a mapping from AST to (AST + Proof). An entry [n -> (n',pr)] is used to store the fact
+      that n and n' are equivalent and pr is a proof for that. If proofs are disabled, then pr is 0.
+      We say n' is the result of the simplification of n.
+      Note: Some simplifications do not preserve equivalence, but equisatisfiability.
+      For saving space, we use pr = 0 also to represent the reflexivity proof [n -> (n, 0)].
+
+     
+      - The simplifier can be extended using plugin (subclasses of the class simplifier_plugin).
+      Each theory has a family ID. All operators (func_decls) and sorts from a given theory have
+      the same family_id. Given an application (object of the class app), we use the method
+      get_family_id() to obtain the family id of the operator in this application. 
+      The simplifier uses plugin to apply theory specific simplifications. The basic idea is:
+      whenever an AST with family_id X is found, invoke the plugin for this family_id.
+      A simplifier_plugin implements the following API:
+         1) bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result)
+         This method is invoked when the simplifier is trying to reduce/simplify an application
+         of the form (f args[0] ... args[num_args - 1]), and f has a family_id associated with
+         the plugin. The plugin may return false to indicate it could not simplify this application.
+         If it returns true (success), the result should be stored in the argument result.
+
+         2) bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result);
+         This method is a similar to the previous one, and it is used to handle associative operators.
+         A plugin does not need to implement this method, the default implementation will use the previous one.
+         The arguments mults indicates the multiplicity of every argument in args. 
+         For example, suppose this reduce is invoked with the arguments (f, 2, [3, 2], [a, b], result).
+         This represents the application (f a a a b b). 
+         Some theory simplifiers may have efficient ways to encode this multiplicity. For example,
+         the arithmetic solver, if f is "+", the multiplicity can be encoded using "*". 
+         This optimization is used because some benchmarks can create term that are very huge when
+         flattened. One "real" example (that motivated this optimization) is:
+             let a1 = x1 + x1
+             let a2 = a1 + a1
+             ...
+             let an = a{n-1} + a{n-1}
+             an
+         In this example, n was 32, so after AC flattening, we had an application
+         (+ x1 ... x1) with 2^32 arguments. Using the simple reduce would produce a stack overflow.
+
+         This class uses a topological sort for computing the multiplicities efficiently.
+         So, the field m_colors is used to implement the topological sort.
+
+
+         3) bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result)
+         This method is invoked when the sort of lhs and rhs has a family_id associated with the plugin.
+         This method allows theory specific simplifications such as:
+         (= (+ a b) b)  --> (= a 0)
+         Assuming n1 is a reference to (+ a b) and n2 to b, the simplifier would invoke
+         reduce_eq(n1, n2, result)
+         Like reduce, false can be returned if a simplification could not be applied.
+         And if true is returned, then the result is stored in the argument result.
+
+         4) bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result)
+         It is similar to reduce_eq, but it used for theory specific simplifications for
+         (distinct args[0] ... args[num_args-1])
+         Example:
+         (distinct 0 1 ... n) --> true
+
+      - The idiom used in this class is implemented in the methdo reduce_core.
+      See reduce_core for more details. The basic idea is:
+
+         1) Get the next ast to be simplified from the todo-stack.
+         2) If it is already cached, then do nothing. That is, this expression was already simplified.
+         3) Otherwise, check whether all arguments already have been simplified (method visit_children).
+             3a) The arguments that have not been simplified are added to the todo-stack by visit_children.
+             In this case visit_children will return false.
+             3b) If all arguments have already been simplified, then invoke reduce1 to perform a reduction/simplification
+             step. The cache is updated with the result.
+
+      - After invoking reduce_core(n), the cache contains an entry [n -> (n', pr)].
+
+     */
+
+    void flush_cache();
+
+    /**
+       \brief This method can be redefined in subclasses of simplifier to implement substitutions.
+       It returns true if n should be substituted by r, where the substitution is justified by the
+       proof p. The field m_subst_proofs is used to store these justifications when coarse proofs are used (PGM_COARSE).
+       This method is redefined in the class subst_simplifier. It is used in asserted_formulas
+       for implementing constant elimination. For example, if asserted_formulas contains the atoms
+       (= a (+ b 1)) (p a c), then the constant "a" can be eliminated. This is achieved by set (+ b 1) as
+       a substitution for "a".
+    */
+    virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p);
+
+    void reduce_core(expr * n);
+    bool visit_children(expr * n);
+    bool visit_ac(app * n);
+    virtual bool visit_quantifier(quantifier * q);
+    void reduce1(expr * n);
+    void reduce1_app(app * n);
+    void reduce1_app_core(app * n);
+    void reduce1_ac_app_core(app * n);
+    void mk_congruent_term(app * n, app_ref & r, proof_ref & p);
+    void mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p);
+    bool get_args(app * n, ptr_vector<expr> & result, proof_ref & p);
+    void get_ac_args(app * n, ptr_vector<expr> & args, vector<rational> & mults);
+    virtual void reduce1_quantifier(quantifier * q);
+    void dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr * const * args, expr* result);
+    void ac_top_sort(app * n, ptr_buffer<expr> & result);
+    
+public:
+    simplifier(ast_manager & manager);
+    virtual ~simplifier();
+
+    void enable_ac_support(bool flag);
+
+    /**
+       \brief Simplify the expression \c s. Store the result in \c r, and a proof that <tt>(= s r)</tt> in \c p.
+    */
+    void operator()(expr * s, expr_ref & r, proof_ref & p);
+    void reset() { if (m_need_reset) { flush_cache(); m_need_reset = false; } }
+
+    bool visited_quantifier() const { return m_visited_quantifier; }
+
+    void mk_app(func_decl * decl, unsigned num_args, expr * const * args, expr_ref & r);
+    void cache_result(expr * n, expr * r, proof * p) { m_need_reset = true;  base_simplifier::cache_result(n, r, p); }
+
+    void register_plugin(plugin * p);
+    ptr_vector<plugin>::const_iterator begin_plugins() const { return m_plugins.begin(); }
+    ptr_vector<plugin>::const_iterator end_plugins() const { return m_plugins.end(); }
+
+    plugin * get_plugin(family_id fid) const { return m_plugins.get_plugin(fid); }
+
+    ast_manager & get_manager() { return m_manager; }
+
+    void borrow_plugins(simplifier const & s);
+    void release_plugins();
+
+    void enable_presimp();
+};
+
+class subst_simplifier : public simplifier {
+protected:
+    expr_map *                     m_subst_map;
+    virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p);
+public:
+    subst_simplifier(ast_manager & manager):simplifier(manager), m_subst_map(0) {}
+    void set_subst_map(expr_map * s);
+};
+
+void push_assertion(ast_manager & m, expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs);
+
+#endif 

src/simplifier/simplifier_plugin.cpp

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    simplifier_plugin.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-12-29.
+
+Revision History:
+
+--*/
+#include"simplifier_plugin.h"
+
+/**
+   \brief Copy every args[i] mult[i] times to new_args.
+*/
+void expand_args(unsigned num_args, rational const * mults, expr * const * args, ptr_buffer<expr> & new_args) {
+    for (unsigned i = 0; i < num_args; i++) {
+        rational const & c = mults[i];
+        SASSERT(c.is_int());
+        rational j(0);
+        while (j < c) {
+            new_args.push_back(args[i]);
+            j++;
+        }
+    }
+}
+
+bool simplifier_plugin::reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result) {
+    set_reduce_invoked();
+    if (f->is_idempotent()) {
+        return reduce(f, num_args, args, result);
+    }
+    else {
+        ptr_buffer<expr> new_args;
+        expand_args(num_args, mults, args, new_args);
+        return reduce(f, new_args.size(), new_args.c_ptr(), result);
+    }
+}

src/simplifier/simplifier_plugin.h

@@ -0,0 +1,94 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    simplifier_plugin.h
+
+Abstract:
+
+    Expression simplifier plugin interface.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-03
+
+--*/
+
+#ifndef __SIMPLIFIER_PLUGIN_H__
+#define __SIMPLIFIER_PLUGIN_H__
+
+#include"ast.h"
+
+class simplifier;
+
+void expand_args(unsigned num_args, rational const * mults, expr * const * args, ptr_buffer<expr> & new_args);
+
+/**
+   \brief Abstract simplifier for the operators in a given family.
+*/
+class simplifier_plugin {
+protected:
+    ast_manager &   m_manager;
+    family_id       m_fid;
+    bool            m_presimp; // true if simplifier is performing pre-simplification...
+    bool            m_reduce_invoked; // true if one of the reduce methods were invoked.
+
+    void set_reduce_invoked() { m_reduce_invoked = true; }
+
+public:
+    simplifier_plugin(symbol const & fname, ast_manager & m):m_manager(m), m_fid(m.get_family_id(fname)), m_presimp(false), m_reduce_invoked(false) {}
+    
+    bool reduce_invoked() const { return m_reduce_invoked; }
+
+    virtual ~simplifier_plugin() {}
+    
+    virtual simplifier_plugin * mk_fresh() {
+        UNREACHABLE();
+        return 0;
+    }
+    
+    /**
+       \brief Return in \c result an expression \c e equivalent to <tt>(f args[0] ... args[num_args - 1])</tt>.
+
+       Return true if succeeded.
+    */
+    virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { set_reduce_invoked(); return false; }
+
+    /**
+       \brief Return in \c result an expression \c e equivalent to <tt>(f args[0] ... args[0] ... args[num_args - 1])</tt>.
+       Where each args[i] occurs mults[i] times.
+
+       Return true if succeeded.
+    */
+    virtual bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result);
+
+    /**
+       \brief Return in \c result an expression \c e equivalent to <tt>(= lhs rhs)</tt>.
+
+       Return true if succeeded.
+    */
+    virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { set_reduce_invoked(); return false; }
+    
+    /**
+       \brief Return in \c result an expression \c e equivalent to <tt>(distinct args[0] ... args[num_args-1])</tt>.
+
+       Return true if succeeded.
+    */
+    virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) { set_reduce_invoked(); return false; }
+    
+    family_id get_family_id() const { return m_fid; }
+   
+    /**
+       \brief Simplifiers may maintain local caches. These caches must be flushed when this method is invoked.
+    */
+    virtual void flush_caches() { /* do nothing */ }
+
+    ast_manager & get_manager() { return m_manager; }
+
+    void enable_presimp(bool flag) { m_presimp = flag; }
+
+    virtual void enable_ac_support(bool flag) {}
+};
+
+#endif

src/util/plugin_manager.h

@@ -0,0 +1,66 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    plugin_manager.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2007-09-18.
+
+Revision History:
+
+--*/
+#ifndef _PLUGIN_MANAGER_H_
+#define _PLUGIN_MANAGER_H_
+
+#include"util.h"
+
+template<typename Plugin>
+class plugin_manager {
+    ptr_vector<Plugin>   m_fid2plugins;
+    ptr_vector<Plugin>   m_plugins;
+public:
+    ~plugin_manager() {
+        std::for_each(m_plugins.begin(), m_plugins.end(), delete_proc<Plugin>());
+    }
+
+    /**
+       \brief Release ownership of the plugins.
+    */
+    void release() {
+        m_fid2plugins.reset();
+        m_plugins.reset();
+    }
+    
+    void register_plugin(Plugin * p) {
+        SASSERT(p);
+        family_id fid = p->get_family_id();
+        SASSERT(m_fid2plugins.get(fid, 0) == 0);
+        m_fid2plugins.setx(fid, p, 0);
+        m_plugins.push_back(p);
+    }
+    
+    Plugin * get_plugin(family_id fid) const {
+        if (fid == null_family_id) {
+            return 0;
+        }
+        return m_fid2plugins.get(fid, 0);
+    }
+
+    typename ptr_vector<Plugin>::const_iterator begin() const { 
+        return m_plugins.begin(); 
+    }
+
+    typename ptr_vector<Plugin>::const_iterator end() const { 
+        return m_plugins.end(); 
+    }
+};
+
+#endif /* _PLUGIN_MANAGER_H_ */
+

src/util/smt2_util.cpp

@@ -0,0 +1,62 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    smt2_util.cpp
+
+Abstract:
+
+    Goodies for SMT2 standard
+
+Author:
+
+    Leonardo (leonardo) 2012-10-20
+
+Notes:
+
+--*/
+#include"smt2_util.h"
+
+bool is_smt2_simple_symbol_char(char s) {
+    return 
+        ('0' <= s && s <= '9') ||
+        ('a' <= s && s <= 'z') ||
+        ('A' <= s && s <= 'Z') ||
+        s == '~' || s == '!' || s == '@' || s == '$' || s == '%' || s == '^' || s == '&' ||
+        s == '*' || s == '_' || s == '-' || s == '+' || s == '=' || s == '<' || s == '>' ||
+        s == '.' || s == '?' || s == '/';
+}
+
+bool is_smt2_quoted_symbol(char const * s) {
+    if (s == 0)
+        return false;
+    if ('0' <= s[0] && s[0] <= '9')
+        return true;
+    unsigned len = static_cast<unsigned>(strlen(s));
+    for (unsigned i = 0; i < len; i++)
+        if (!is_smt2_simple_symbol_char(s[i]))
+            return true;
+    return false;
+}
+
+bool is_smt2_quoted_symbol(symbol const & s) {
+    if (s.is_numerical())
+        return false;
+    return is_smt2_quoted_symbol(s.bare_str());
+}
+
+std::string mk_smt2_quoted_symbol(symbol const & s) {
+    SASSERT(is_smt2_quoted_symbol(s));
+    string_buffer<> buffer;
+    buffer.append('|');
+    char const * str = s.bare_str();
+    while (*str) {
+        if (*str == '|' || *str == '\\')
+            buffer.append('\\');
+        buffer.append(*str);
+        str++;
+    }
+    buffer.append('|');
+    return std::string(buffer.c_str());
+}

src/util/smt2_util.h

@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    smt2_util.h
+
+Abstract:
+
+    Goodies for SMT2 standard
+
+Author:
+
+    Leonardo (leonardo) 2012-10-20
+
+Notes:
+
+--*/
+#ifndef _SMT2_UTIL_H_
+#define _SMT2_UTIL_H_
+
+#include"symbol.h"
+
+bool is_smt2_simple_symbol_char(char c);
+bool is_smt2_quoted_symbol(char const * s);
+bool is_smt2_quoted_symbol(symbol const & s);
+std::string mk_smt2_quoted_symbol(symbol const & s);
+
+#endif